equal
deleted
inserted
replaced
36 height :: "lam \<Rightarrow> int" |
36 height :: "lam \<Rightarrow> int" |
37 where |
37 where |
38 "height (Var x) = 1" |
38 "height (Var x) = 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
39 | "height (App t1 t2) = max (height t1) (height t2) + 1" |
40 | "height (Lam [x].t) = height t + 1" |
40 | "height (Lam [x].t) = height t + 1" |
41 apply(simp add: eqvt_def height_graph_def) |
41 apply(simp add: eqvt_def height_graph_aux_def) |
42 apply(rule TrueI) |
42 apply(rule TrueI) |
43 apply(rule_tac y="x" in lam.exhaust) |
43 apply(rule_tac y="x" in lam.exhaust) |
44 using [[simproc del: alpha_lst]] |
44 using [[simproc del: alpha_lst]] |
45 apply(auto) |
45 apply(auto) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
57 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90,90,90] 90) |
58 where |
58 where |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
59 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
60 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
61 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
62 unfolding eqvt_def subst_graph_def |
62 unfolding eqvt_def subst_graph_aux_def |
63 apply(rule, perm_simp, rule) |
63 apply(simp) |
64 apply(rule TrueI) |
64 apply(rule TrueI) |
65 using [[simproc del: alpha_lst]] |
65 using [[simproc del: alpha_lst]] |
66 apply(auto) |
66 apply(auto) |
67 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
67 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
68 apply(blast)+ |
68 apply(blast)+ |