equal
deleted
inserted
replaced
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
14 subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt" ("_ [_ ::= _]" [90, 90, 90] 90) |
15 where |
15 where |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
19 unfolding eqvt_def subst_graph_def |
19 unfolding eqvt_def subst_graph_aux_def |
20 apply (simp) |
20 apply (simp) |
21 apply(rule TrueI) |
21 apply(rule TrueI) |
22 using [[simproc del: alpha_lst]] |
22 using [[simproc del: alpha_lst]] |
23 apply(auto simp add: lt.distinct lt.eq_iff) |
23 apply(auto simp add: lt.distinct lt.eq_iff) |
24 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
24 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
49 isValue:: "lt => bool" |
49 isValue:: "lt => bool" |
50 where |
50 where |
51 "isValue (Var x) = True" |
51 "isValue (Var x) = True" |
52 | "isValue (Lam y N) = True" |
52 | "isValue (Lam y N) = True" |
53 | "isValue (A $$ B) = False" |
53 | "isValue (A $$ B) = False" |
54 unfolding eqvt_def isValue_graph_def |
54 unfolding eqvt_def isValue_graph_aux_def |
55 by (perm_simp, auto) |
55 by (auto) |
56 (erule lt.exhaust, auto) |
56 (erule lt.exhaust, auto) |
57 |
57 |
58 termination (eqvt) |
58 termination (eqvt) |
59 by (relation "measure size") (simp_all) |
59 by (relation "measure size") (simp_all) |
60 |
60 |