equal
deleted
inserted
replaced
15 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
15 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
16 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
16 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
17 unfolding eqvt_def subst_graph_def |
17 unfolding eqvt_def subst_graph_def |
18 apply (rule, perm_simp, rule) |
18 apply (rule, perm_simp, rule) |
19 apply(rule TrueI) |
19 apply(rule TrueI) |
20 apply(auto simp add: lam.distinct lam.eq_iff) |
20 apply(auto) |
21 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
21 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
22 apply(blast)+ |
22 apply(blast)+ |
23 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
23 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
24 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
24 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
25 apply(simp_all add: Abs_fresh_iff) |
25 apply(simp_all add: Abs_fresh_iff) |
209 (auto dest!: One_Lam simp add: fresh_Pair lam.fresh Abs1_eq_iff) |
209 (auto dest!: One_Lam simp add: fresh_Pair lam.fresh Abs1_eq_iff) |
210 |
210 |
211 inductive |
211 inductive |
212 One_star :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>1* _" [80,80] 80) |
212 One_star :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>1* _" [80,80] 80) |
213 where |
213 where |
214 os1[intro]: "t \<longrightarrow>1* t" |
214 os1[intro, simp]: "t \<longrightarrow>1* t" |
215 | os2[intro]: "t \<longrightarrow>1 s \<Longrightarrow> t \<longrightarrow>1* s" |
215 | os2[intro]: "t \<longrightarrow>1* r \<Longrightarrow> r \<longrightarrow>1 s \<Longrightarrow> t \<longrightarrow>1* s" |
216 | os3[intro, trans]: "t1 \<longrightarrow>1* t2 \<Longrightarrow> t2 \<longrightarrow>1* t3 \<Longrightarrow> t1 \<longrightarrow>1* t3" |
216 |
|
217 lemma os3[intro, trans]: |
|
218 assumes a1: "M1 \<longrightarrow>1* M2" |
|
219 and a2: "M2 \<longrightarrow>1* M3" |
|
220 shows "M1 \<longrightarrow>1* M3" |
|
221 using a2 a1 |
|
222 by induct auto |
217 |
223 |
218 section {* Complete Development Reduction *} |
224 section {* Complete Development Reduction *} |
219 |
225 |
220 inductive |
226 inductive |
221 Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>d _" [80,80] 80) |
227 Dev :: "lam \<Rightarrow> lam \<Rightarrow> bool" (" _ \<longrightarrow>d _" [80,80] 80) |