53 thm foo.supports |
54 thm foo.supports |
54 thm foo.fsupp |
55 thm foo.fsupp |
55 thm foo.supp |
56 thm foo.supp |
56 thm foo.fresh |
57 thm foo.fresh |
57 thm foo.bn_finite |
58 thm foo.bn_finite |
58 |
|
59 lemma strong_exhaust1: |
|
60 fixes c::"'a::fs" |
|
61 assumes "\<exists>name. y = Var name \<Longrightarrow> P" |
|
62 and "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
63 and "\<exists>name trm. {atom name} \<sharp>* c \<and> y = Lam name trm \<Longrightarrow> P" |
|
64 and "\<exists>(c::'a::fs) assn trm. set (bn1 assn) \<sharp>* c \<and> y = Let1 assn trm \<Longrightarrow> P" |
|
65 and "\<exists>(c::'a::fs) assn trm. set (bn2 assn) \<sharp>* c \<and> y = Let2 assn trm \<Longrightarrow> P" |
|
66 and "\<exists>(c::'a::fs) assn trm. set (bn3 assn) \<sharp>* c \<and> y = Let3 assn trm \<Longrightarrow> P" |
|
67 and "\<exists>(c::'a::fs) assn' trm. (bn4 assn') \<sharp>* c \<and> y = Let4 assn' trm \<Longrightarrow> P" |
|
68 shows "P" |
|
69 oops |
|
70 |
|
71 |
|
72 lemma strong_exhaust2: |
|
73 fixes c::"'a::fs" |
|
74 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
75 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
76 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
77 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
|
78 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
|
79 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
|
80 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
|
81 shows "P" |
|
82 oops |
|
83 |
|
84 lemma strong_exhaust1: |
|
85 fixes c::"'a::fs" |
|
86 assumes "\<And>name. y = Var name \<Longrightarrow> P" |
|
87 and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" |
|
88 and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" |
|
89 and "\<And>assn trm. \<lbrakk>set (bn1 assn) \<sharp>* c; y = Let1 assn trm\<rbrakk> \<Longrightarrow> P" |
|
90 and "\<And>assn trm. \<lbrakk>set (bn2 assn) \<sharp>* c; y = Let2 assn trm\<rbrakk> \<Longrightarrow> P" |
|
91 and "\<And>assn trm. \<lbrakk>set (bn3 assn) \<sharp>* c; y = Let3 assn trm\<rbrakk> \<Longrightarrow> P" |
|
92 and "\<And>assn' trm. \<lbrakk>(bn4 assn') \<sharp>* c; y = Let4 assn' trm\<rbrakk> \<Longrightarrow> P" |
|
93 shows "P" |
|
94 oops |
|
95 |
|
96 lemma strong_exhaust2: |
|
97 assumes "\<And>x y t. as = As x y t \<Longrightarrow> P" |
|
98 shows "P" |
|
99 apply(rule_tac y="as" in foo.exhaust(2)) |
|
100 apply(rule assms(1)) |
|
101 apply(assumption) |
|
102 done |
|
103 |
|
104 lemma strong_exhaust3: |
|
105 assumes "as' = BNil \<Longrightarrow> P" |
|
106 and "\<And>a as. as' = BAs a as \<Longrightarrow> P" |
|
107 shows "P" |
|
108 apply(rule_tac y="as'" in foo.exhaust(3)) |
|
109 apply(rule assms(1)) |
|
110 apply(assumption) |
|
111 apply(rule assms(2)) |
|
112 apply(assumption) |
|
113 done |
|
114 |
59 |
115 lemma |
60 lemma |
116 fixes t::trm |
61 fixes t::trm |
117 and as::assg |
62 and as::assg |
118 and as'::assg' |
63 and as'::assg' |
126 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
71 and a7: "\<And>as' t c. \<lbrakk>(bn4 as') \<sharp>* c; \<And>d. P3 d as'; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let4 as' t)" |
127 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
72 and a8: "\<And>x y t c. \<And>d. P1 d t \<Longrightarrow> P2 c (As x y t)" |
128 and a9: "\<And>c. P3 c (BNil)" |
73 and a9: "\<And>c. P3 c (BNil)" |
129 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
74 and a10: "\<And>c a as. \<And>d. P3 d as \<Longrightarrow> P3 c (BAs a as)" |
130 shows "P1 c t" "P2 c as" "P3 c as'" |
75 shows "P1 c t" "P2 c as" "P3 c as'" |
131 oops |
|
132 (* |
|
133 using assms |
76 using assms |
134 apply(induction_schema) |
77 apply(induction_schema) |
135 apply(rule_tac y="t" and c="c" in strong_exhaust1) |
78 apply(rule_tac y="t" and c="c" in foo.strong_exhaust(1)) |
136 apply(simp_all)[7] |
79 apply(simp_all)[7] |
137 apply(rule_tac as="as" in strong_exhaust2) |
80 apply(rule_tac ya="as"in foo.strong_exhaust(2)) |
138 apply(simp) |
81 apply(simp_all)[1] |
139 apply(rule_tac as'="as'" in strong_exhaust3) |
82 apply(rule_tac yb="as'" in foo.strong_exhaust(3)) |
140 apply(simp_all)[2] |
83 apply(simp_all)[2] |
141 apply(relation "measure (sum_case (size o snd) (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z))))") |
84 apply(relation "measure (sum_case (size o snd) (sum_case (size o snd) (size o snd)))") |
142 apply(simp_all add: foo.size) |
85 apply(simp_all add: foo.size) |
143 done |
86 done |
144 *) |
|
145 |
87 |
146 end |
88 end |
147 |
89 |
148 |
90 |
149 |
91 |