equal
deleted
inserted
replaced
24 |
24 |
25 section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *} |
25 section {* Strong Exhausts Lemma and Strong Induction Lemma via Induct_schema *} |
26 |
26 |
27 lemma strong_exhaust: |
27 lemma strong_exhaust: |
28 fixes c::"'a::fs" |
28 fixes c::"'a::fs" |
29 assumes "\<And>name ca. \<lbrakk>c = ca; y = Var name\<rbrakk> \<Longrightarrow> P" |
29 assumes "\<And>name. \<lbrakk>y = Var name\<rbrakk> \<Longrightarrow> P" |
30 and "\<And>lam1 lam2 ca. \<lbrakk>c = ca; y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" |
30 and "\<And>lam1 lam2. \<lbrakk>y = App lam1 lam2\<rbrakk> \<Longrightarrow> P" |
31 and "\<And>name lam ca. \<lbrakk>c = ca; atom name \<sharp> ca; y = Lam name lam\<rbrakk> \<Longrightarrow> P" |
31 and "\<And>name lam. \<lbrakk>atom name \<sharp> c; y = Lam name lam\<rbrakk> \<Longrightarrow> P" |
32 shows "P" |
32 shows "P" |
33 apply(rule_tac y="y" in lam.exhaust) |
33 apply(rule_tac y="y" in lam.exhaust) |
34 apply(rule assms(1)) |
34 apply(rule assms(1)) |
35 apply(auto)[2] |
35 apply(assumption) |
36 apply(rule assms(2)) |
36 apply(rule assms(2)) |
37 apply(auto)[2] |
37 apply(assumption) |
38 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q") |
38 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom name)) \<sharp> c \<and> supp (Lam name lam) \<sharp>* q") |
39 apply(erule exE) |
39 apply(erule exE) |
40 apply(erule conjE) |
40 apply(erule conjE) |
41 apply(rule assms(3)) |
41 apply(rule assms(3)) |
42 apply(rule refl) |
|
43 apply(simp add: atom_eqvt) |
42 apply(simp add: atom_eqvt) |
44 apply(clarify) |
43 apply(clarify) |
45 apply(drule supp_perm_eq[symmetric]) |
44 apply(drule supp_perm_eq[symmetric]) |
46 apply(simp) |
45 apply(simp) |
47 apply(rule at_set_avoiding2_atom) |
46 apply(rule at_set_avoiding2_atom) |
62 apply(rule_tac y="lam" in strong_exhaust) |
61 apply(rule_tac y="lam" in strong_exhaust) |
63 apply(blast) |
62 apply(blast) |
64 apply(blast) |
63 apply(blast) |
65 apply(blast) |
64 apply(blast) |
66 apply(relation "measure (\<lambda>(x,y). size y)") |
65 apply(relation "measure (\<lambda>(x,y). size y)") |
67 apply(auto)[1] |
66 apply(simp_all add: lam.size) |
68 apply(simp add: lam.size) |
|
69 apply(simp add: lam.size) |
|
70 apply(simp add: lam.size) |
|
71 done |
67 done |
72 |
68 |
73 section {* Strong Induction Principles*} |
69 section {* Strong Induction Principles*} |
74 |
70 |
75 (* |
71 (* |