equal
deleted
inserted
replaced
179 apply (erule ssubst) |
179 apply (erule ssubst) |
180 apply (rule applyB) |
180 apply (rule applyB) |
181 done |
181 done |
182 |
182 |
183 lemma term_ind: |
183 lemma term_ind: |
184 assumes "P(bot)" "P(true)" "P(false)" |
184 assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)" |
185 "!!x y.[| P(x); P(y) |] ==> P(<x,y>)" |
185 and 4: "!!x y.[| P(x); P(y) |] ==> P(<x,y>)" |
186 "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" "INCL(P)" |
186 and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" |
|
187 and 6: "INCL(P)" |
187 shows "P(t)" |
188 shows "P(t)" |
188 apply (rule reachability [THEN id_apply, THEN subst]) |
189 apply (rule reachability [THEN id_apply, THEN subst]) |
189 apply (rule_tac x = t in spec) |
190 apply (rule_tac x = t in spec) |
190 apply (rule fix_ind) |
191 apply (rule fix_ind) |
191 apply (unfold idgen_def) |
192 apply (unfold idgen_def) |
192 apply (rule allI) |
193 apply (rule allI) |
193 apply (subst applyBbot) |
194 apply (subst applyBbot) |
194 apply assumption |
195 apply (rule 1) |
195 apply (rule allI) |
196 apply (rule allI) |
196 apply (rule applyB [THEN ssubst]) |
197 apply (rule applyB [THEN ssubst]) |
197 apply (rule_tac t = "xa" in term_case) |
198 apply (rule_tac t = "xa" in term_case) |
198 apply simp_all |
199 apply simp_all |
199 apply (fast intro: prems INCL_subst all_INCL)+ |
200 apply (fast intro: assms INCL_subst all_INCL)+ |
200 done |
201 done |
201 |
202 |
202 end |
203 end |