src/CCL/Fix.thy
changeset 23467 d1b97708d5eb
parent 20140 98acc6d0fab6
child 24825 c4f13ab78f9d
equal deleted inserted replaced
23466:886655a150f6 23467:d1b97708d5eb
   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