Theory Types
theory Types imports Language begin
consts
Ty :: i
TyConst :: i
datatype
"Ty" = t_const ("tc ∈ TyConst")
| t_fun ("t1 ∈ Ty","t2 ∈ Ty")
consts
TyEnv :: i
datatype
"TyEnv" = te_emp
| te_owr ("te ∈ TyEnv","x ∈ ExVar","t ∈ Ty")
consts
te_dom :: "i ⇒ i"
te_app :: "[i,i] ⇒ i"
primrec
"te_dom (te_emp) = 0"
"te_dom (te_owr(te,x,v)) = te_dom(te) ∪ {x}"
primrec
"te_app (te_emp,x) = 0"
"te_app (te_owr(te,y,t),x) = (if x=y then t else te_app(te,x))"
inductive_cases te_owrE [elim!]: "te_owr(te,f,t) ∈ TyEnv"
lemma te_app_owr1: "te_app(te_owr(te,x,t),x) = t"
by simp
lemma te_app_owr2: "x ≠ y ⟹ te_app(te_owr(te,x,t),y) = te_app(te,y)"
by auto
lemma te_app_owr [simp]:
"te_app(te_owr(te,x,t),y) = (if x=y then t else te_app(te,y))"
by auto
lemma te_appI:
"⟦te ∈ TyEnv; x ∈ ExVar; x ∈ te_dom(te)⟧ ⟹ te_app(te,x) ∈ Ty"
apply (erule_tac P = "x ∈ te_dom (te) " in rev_mp)
apply (erule TyEnv.induct, auto)
done
end