82 lemma (in M_axioms) is_recfun_equal [rule_format]: |
82 lemma (in M_axioms) is_recfun_equal [rule_format]: |
83 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
83 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
84 wellfounded(M,r); trans(r); |
84 wellfounded(M,r); trans(r); |
85 M(f); M(g); M(r); M(x); M(a); M(b) |] |
85 M(f); M(g); M(r); M(x); M(a); M(b) |] |
86 ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x" |
86 ==> <x,a> \<in> r --> <x,b> \<in> r --> f`x=g`x" |
87 apply (frule_tac f="f" in is_recfun_type) |
87 apply (frule_tac f=f in is_recfun_type) |
88 apply (frule_tac f="g" in is_recfun_type) |
88 apply (frule_tac f=g in is_recfun_type) |
89 apply (simp add: is_recfun_def) |
89 apply (simp add: is_recfun_def) |
90 apply (erule_tac a=x in wellfounded_induct, assumption+) |
90 apply (erule_tac a=x in wellfounded_induct, assumption+) |
91 txt{*Separation to justify the induction*} |
91 txt{*Separation to justify the induction*} |
92 apply (blast intro: is_recfun_separation') |
92 apply (blast intro: is_recfun_separation') |
93 txt{*Now the inductive argument itself*} |
93 txt{*Now the inductive argument itself*} |
105 lemma (in M_axioms) is_recfun_cut: |
105 lemma (in M_axioms) is_recfun_cut: |
106 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
106 "[|is_recfun(r,a,H,f); is_recfun(r,b,H,g); |
107 wellfounded(M,r); trans(r); |
107 wellfounded(M,r); trans(r); |
108 M(f); M(g); M(r); <b,a> \<in> r |] |
108 M(f); M(g); M(r); <b,a> \<in> r |] |
109 ==> restrict(f, r-``{b}) = g" |
109 ==> restrict(f, r-``{b}) = g" |
110 apply (frule_tac f="f" in is_recfun_type) |
110 apply (frule_tac f=f in is_recfun_type) |
111 apply (rule fun_extension) |
111 apply (rule fun_extension) |
112 apply (blast intro: transD restrict_type2) |
112 apply (blast intro: transD restrict_type2) |
113 apply (erule is_recfun_type, simp) |
113 apply (erule is_recfun_type, simp) |
114 apply (blast intro: is_recfun_equal transD dest: transM) |
114 apply (blast intro: is_recfun_equal transD dest: transM) |
115 done |
115 done |