Theory Term

Up to index of Isabelle/HOL/Marvin99-1

Term = Marvin_lemmas + String + Bag +

datatype
  Val = natV nat
    | listV (nat list)
    | bagV (nat bag)
    | setV (nat set)
    | pairV Val Val
    | undefV
types
  Var = "string"
  Fun = "string"
  Bnds = "Var => Val"

  
(* arities *)
(*  Var :: term *)
(*   Fun :: term *)
  
datatype rterm = varT Var  | funT Fun (rterm list) 

consts
  freeVarslist :: "rterm list => Var set" 
  freeVars :: "rterm => Var set"
  arity    :: "Fun => nat"
  evallist :: "[rterm list , Bnds] => Val list"
  eval :: "[rterm ,Bnds] => Val"
  apply :: "Fun => (Val list => Val)"
  pair  :: "Fun"
  vless :: "[Val,Val] => bool" (infixr 76)
  substt :: "[rterm, Var, rterm] => rterm"
  substl :: "[rterm list, Var, rterm] => rterm list"
  domF :: "Fun => (Val list) set"
  listof :: "Val => nat list"
  natof :: "Val => nat"
  setof :: "Val => nat set"
  bagof :: "Val => nat bag"
  
  rules
  listof_def "listof(listV l) = l"
  natof_def "natof(natV n) = n"
  setof_def "setof(setV s) = s"
  bagof_def "bagof(bagV b) = b"

primrec
  "(natV n) vless v =  
          (case v of natV  m => n < m
                  | listV s => False
                  | bagV b => False
                  | setV s1 => False
                  | pairV u v => False
                  | undefV => False)"
  "(listV s) vless v = (case v of natV  m => False
                  | listV t => length s < length t 
                  | bagV b => False
                  | setV s1 => False
                  | pairV x y => False | undefV => False)"
  "(bagV b1) vless v = (case v of natV  m => False
                  | listV t => False
                  | bagV b2 => b1 < b2 
                  | setV s1 => False
                  | pairV c d => False
                  | undefV => False)"
  "(setV s) vless v = (case v of natV  m => False
                  | listV t => False
                  | bagV b => False
                  | setV s1 => s < s1
                  | pairV x y => False | undefV => False)"
  "(pairV a b) vless v = (case v of natV  m => False
                  | listV t => False
                  | bagV b => False
                  | setV s1 => False
                  | pairV c d => a vless c | (a  = c & b vless d)
                  | undefV => False)"
  
primrec
  "substt (varT v) u t = (if v = u then t else varT v)"
  "substt (funT f xs) u t = funT f (substl xs u t)"

  "substl [] u t = []"
  "substl (x#xs) u t = (substt x u t) # (substl xs u t)"
primrec
  "freeVarslist([]) = {}"
  "freeVarslist(x # xs) = freeVars(x) Un freeVarslist(xs)"

  "freeVars(varT v) = {v}"
  "freeVars(funT f xs) = freeVarslist(xs)"

primrec
  "evallist([]) b = []"
  "evallist(x # xs) b = (eval x b) # (evallist xs b)"
  
  "eval(varT v) b = b(v)"
  "eval(funT f xs) b =  ((apply f) (evallist xs b))"
                        

syntax(symbols)
  "funT" :: "[Fun,rterm list] => rterm" ("_ %^ _")

rules
  apply_pair "apply ''pair'' [a,b] = pairV a b"
  dom_pair "domF ''pair'' = {x . ? f s. x = [f,s]}"
end