theory DeepLogic = FiniteMap + SALSyntax:

section {* Syntax and Manipulation of formulae *}

datatype
  tval = ILLEGAL | NAT nat | POS pos

constdefs
  MAX :: nat
 "MAX \<equiv> 15"

datatype
vtype= Nat | Pos

types var = nat

datatype expr = V var | Lv var |
                C tval | 
                Pc | 
                Rp | 
                Tm |
                Add expr expr (infixr "\<oplus>" 65) | 
                Minus expr expr (infixr "\<ominus>" 65) |
                Mult expr expr (infixr "\<odot>" 65) | 
              (*  Ref expr | verursacht Probleme bei Substitution und ist ueberfluessig. *)
                Deref expr | 
                Ifeq expr expr expr expr ("IF _ \<doteq> _ THEN _ ELSE _" [61,61,60,60] 60) |
                Old expr 

datatype form =  T | 
                 F | 
                 And "form list" ("\<Lambda> _" 70) | 
                 Imp form form  (infix "\<supset>" 65) | 
                 Neg form |
                 Eq expr expr (infixr "\<doteq>" 65)   | 
                 Leq expr expr (infixr "\<preceq>" 65)  | 
                 Less expr expr (infixr "\<prec>" 65) | 
                 Ty expr vtype | 
                 Forall var form ("(3\<Prod>_./ _)" [0, 10] 10) |
                 Yields expr "tval list" 


datatype mode = NoPt | Mv var var

consts 
substE::"mode \<Rightarrow> (expr ~~> expr) \<Rightarrow> expr \<Rightarrow> expr"
(* substE m em e substitutes expresions in e. All instances
   of V v, Pc, Rp, Tm are replaced by their mappings in em. 
   The substitution does not step into expressions starting with
   "Old". 
   The mode m is used to protect variables (V v) or Dereference terms
   that could be invalidated by a pointer operation. In mode NoPt no 
   pointer operations occurs. In mode Mv s t the value referenced by t
   is assumed to be overwritten by the value referenced by t. Hence
   all variables are replaced by expressions saying "If I am the variable
   referenced by t then my value is the one referenced by s.". Derefence
   operations are also augmented by checks on s and t. 
*)

consts
changedvars :: "(expr ~~> expr) \<Rightarrow> (var ~~> expr)"

primrec
"changedvars [] = []"
"changedvars (m#ms) = (case (fst m) 
                     of V v \<Rightarrow> [(v,snd m)]
                     | Lv v \<Rightarrow> []
                     | C tv \<Rightarrow> []
                     | Pc \<Rightarrow> []
                     | Rp \<Rightarrow> []
                     | Tm \<Rightarrow> []
                     | Add e1 e2 \<Rightarrow> []
                     | Minus e1 e2 \<Rightarrow> []
                     | Mult e1 e2 \<Rightarrow> []
                     | Deref e \<Rightarrow> []
                     | Ifeq e1 e2 e3 e4 \<Rightarrow> []
                     | Old e \<Rightarrow> [])@(changedvars ms)"




primrec substE:
"substE m em (V v) = (case m 
                        of NoPt \<Rightarrow> em ?\<^sub>= (V v)
                        | Mv s t \<Rightarrow> (Ifeq (V t) (C (NAT v)) (Deref (V s)) (em ?\<^sub>= (V v))))"
"substE m em (Lv v) = (Lv v)"
"substE m em (C tv) = (C tv)" 
"substE m em Pc = em ?\<^sub>= Pc"
"substE m em Rp = em ?\<^sub>= Rp"
"substE m em Tm = em ?\<^sub>= Tm"
"substE m em (Add e1 e2) = Add (substE m em e1) (substE m em e2)"
"substE m em (Minus e1 e2) = Minus (substE m em e1) (substE m em e2)"
"substE m em (Mult e1 e2) = Mult (substE m em e1) (substE m em e2)"
"substE m em (Deref e1) =  (let e1'= (substE m em e1);
                                res=(foldl (\<lambda> e (a,b). (Ifeq e1' (C (NAT a)) b e)) (Deref e1') (changedvars em))                               in (case m
                                  of NoPt \<Rightarrow> res
                                  | Mv s t \<Rightarrow> Ifeq (V t) e1' (Deref (V s)) res))"
"substE m em (Ifeq e1 e2 e3 e4) = Ifeq (substE m em e1) (substE m em e2) (substE m em e3) (substE m em e4)"
"substE m em (Old e1) = Old e1"

consts
intVarsE :: "expr \<Rightarrow> var list"

primrec
"intVarsE (V n) = []"
"intVarsE (Lv v) = [v]"
"intVarsE (C tv) = []"
"intVarsE Pc = []"
"intVarsE Rp = []"
"intVarsE Tm = []"
"intVarsE (Add e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"intVarsE (Minus e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"intVarsE (Mult e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"intVarsE (Deref e1) = intVarsE e1"
"intVarsE (Ifeq e1 e2 e3 e4) = (intVarsE e1) @ (intVarsE e2) @ (intVarsE e3) @ (intVarsE e4)"
"intVarsE (Old e) = intVarsE e"

consts
freeIntVars :: "form \<Rightarrow> var list"
freeIntVarsL :: "form list \<Rightarrow> var list"


primrec
"freeIntVarsL [] = []"
"freeIntVarsL (f#fs) = (freeIntVars f)@(freeIntVarsL fs)"
"freeIntVars T = []"
"freeIntVars F = []"
"freeIntVars (And fs) = freeIntVarsL fs"
"freeIntVars (Imp f1 f2) = (freeIntVars f1) @ (freeIntVars f2)"
"freeIntVars (Neg f) = freeIntVars f"
"freeIntVars (Eq e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"freeIntVars (Leq e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"freeIntVars (Less e1 e2) = (intVarsE e1) @ (intVarsE e2)"
"freeIntVars (Ty e tv) = (intVarsE e)"
"freeIntVars (Forall n f) = filter (\<lambda> v. v\<noteq> n) (freeIntVars f)"
"freeIntVars (Yields e vs) = (intVarsE e) "

constdefs del_id_rns::"(var ~~> expr) \<Rightarrow> (var ~~> expr)"
"del_id_rns rm == filter (\<lambda> (v,e). e \<noteq> V v) rm"

consts
modevars:: "mode \<Rightarrow> var list"
primrec
"modevars NoPt = []"
"modevars (Mv s t) = [s,t]"


consts
substF::"mode \<Rightarrow> (expr ~~> expr) \<Rightarrow> form \<Rightarrow> form"
substFL::"mode \<Rightarrow> (expr ~~> expr) \<Rightarrow> form list \<Rightarrow> form list"

primrec
"substFL m em [] = []"
"substFL m em (f#fs) = (substF m em f)#(substFL m em fs)"
"substF m em T = T"
"substF m em F = F"
"substF m em (And fs) = And (substFL m em fs)"
"substF m em (Imp f1 f2) = Imp (substF m em f1) (substF m em f2)"
"substF m em (Neg f) = Neg (substF m em f)"
"substF m em (Eq e1 e2) = (Eq (substE m em e1) (substE m em e2))"
"substF m em (Leq e1 e2) = (Leq (substE m em e1) (substE m em e2))"
"substF m em (Less e1 e2) = (Less (substE m em e1) (substE m em e2))"
"substF m em (Ty ex vt) = (Ty (substE m em ex) vt)"
"substF m em (Forall v f) = (Forall v (substF m em f))"
"substF m em (Yields ex vs) = (Yields (substE m em ex) vs)"  

constdefs
nv::"tval \<Rightarrow> nat"
"nv v \<equiv> (case v of ILLEGAL \<Rightarrow> (MAX+1) | NAT n \<Rightarrow> n | POS r \<Rightarrow> (MAX+1))"

constdefs
rv::"tval \<Rightarrow> pos"
"rv v \<equiv> (case v of ILLEGAL \<Rightarrow> (0,0) | NAT n \<Rightarrow> (0,0) | POS r \<Rightarrow> r)"

end