equal
deleted
inserted
replaced
28 thm trm_assn.supp |
28 thm trm_assn.supp |
29 thm trm_assn.fresh |
29 thm trm_assn.fresh |
30 thm trm_assn.exhaust |
30 thm trm_assn.exhaust |
31 thm trm_assn.strong_exhaust |
31 thm trm_assn.strong_exhaust |
32 |
32 |
33 lemma strong_exhaust1: |
|
34 fixes c::"'a::fs" |
|
35 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
36 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
37 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
38 and "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P" |
|
39 shows "P" |
|
40 apply(rule_tac y="y" in trm_assn.strong_exhaust(1)) |
|
41 apply(rule assms(1)) |
|
42 apply(assumption) |
|
43 apply(rule assms(2)) |
|
44 apply(assumption) |
|
45 apply(rule assms(3)) |
|
46 apply(assumption) |
|
47 apply(assumption) |
|
48 apply(rule assms(4)) |
|
49 apply(assumption) |
|
50 apply(assumption) |
|
51 sorry |
|
52 |
|
53 |
|
54 lemma strong_exhaust2: |
|
55 assumes "as = ANil \<Longrightarrow> P" |
|
56 and "\<And>x t assn. \<lbrakk>as = ACons x t assn\<rbrakk> \<Longrightarrow> P" |
|
57 shows "P" |
|
58 apply(rule_tac y="as" in trm_assn.exhaust(2)) |
|
59 apply(rule assms(1)) |
|
60 apply(assumption) |
|
61 apply(rule assms(2)) |
|
62 apply(assumption)+ |
|
63 done |
|
64 |
|
65 |
|
66 lemma |
33 lemma |
67 fixes t::trm |
34 fixes t::trm |
68 and as::assn |
35 and as::assn |
69 and c::"'a::fs" |
36 and c::"'a::fs" |
70 assumes a1: "\<And>x c. P1 c (Var x)" |
37 assumes a1: "\<And>x c. P1 c (Var x)" |
74 and a5: "\<And>c. P2 c ANil" |
41 and a5: "\<And>c. P2 c ANil" |
75 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
42 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
76 shows "P1 c t" "P2 c as" |
43 shows "P1 c t" "P2 c as" |
77 using assms |
44 using assms |
78 apply(induction_schema) |
45 apply(induction_schema) |
79 apply(rule_tac y="t" in strong_exhaust1) |
46 apply(rule_tac y="t" in trm_assn.strong_exhaust(1)) |
80 apply(blast) |
47 apply(blast) |
81 apply(blast) |
48 apply(blast) |
82 apply(blast) |
49 apply(blast) |
83 apply(blast) |
50 apply(blast) |
84 apply(rule_tac as="as" in strong_exhaust2) |
51 apply(rule_tac ya="as" in trm_assn.strong_exhaust(2)) |
85 apply(blast) |
52 apply(blast) |
86 apply(blast) |
53 apply(blast) |
87 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
54 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
88 apply(simp_all add: trm_assn.size) |
55 apply(simp_all add: trm_assn.size) |
89 done |
56 done |