31 qed "wf_induct"; |
31 qed "wf_induct"; |
32 |
32 |
33 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
33 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
34 fun wf_ind_tac a prems i = |
34 fun wf_ind_tac a prems i = |
35 EVERY [res_inst_tac [("a",a)] wf_induct i, |
35 EVERY [res_inst_tac [("a",a)] wf_induct i, |
36 rename_last_tac a ["1"] (i+1), |
36 rename_last_tac a ["1"] (i+1), |
37 ares_tac prems i]; |
37 ares_tac prems i]; |
38 |
38 |
39 val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; |
39 val prems = goal WF.thy "[| wf(r); (a,x):r; (x,a):r |] ==> P"; |
40 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); |
40 by (subgoal_tac "! x. (a,x):r --> (x,a):r --> P" 1); |
41 by (fast_tac (HOL_cs addIs prems) 1); |
41 by (fast_tac (HOL_cs addIs prems) 1); |
42 by (wf_ind_tac "a" prems 1); |
42 by (wf_ind_tac "a" prems 1); |
90 mp amd allE instantiate induction hypotheses*) |
90 mp amd allE instantiate induction hypotheses*) |
91 fun indhyp_tac hyps = |
91 fun indhyp_tac hyps = |
92 ares_tac (TrueI::hyps) ORELSE' |
92 ares_tac (TrueI::hyps) ORELSE' |
93 (cut_facts_tac hyps THEN' |
93 (cut_facts_tac hyps THEN' |
94 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
94 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
95 eresolve_tac [transD, mp, allE])); |
95 eresolve_tac [transD, mp, allE])); |
96 |
96 |
97 (*** NOTE! some simplifications need a different finish_tac!! ***) |
97 (*** NOTE! some simplifications need a different finish_tac!! ***) |
98 fun indhyp_tac hyps = |
98 fun indhyp_tac hyps = |
99 resolve_tac (TrueI::refl::hyps) ORELSE' |
99 resolve_tac (TrueI::refl::hyps) ORELSE' |
100 (cut_facts_tac hyps THEN' |
100 (cut_facts_tac hyps THEN' |
101 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
101 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
102 eresolve_tac [transD, mp, allE])); |
102 eresolve_tac [transD, mp, allE])); |
103 val wf_super_ss = !simpset setsolver indhyp_tac; |
103 val wf_super_ss = !simpset setsolver indhyp_tac; |
104 |
104 |
105 val prems = goalw WF.thy [is_recfun_def,cut_def] |
105 val prems = goalw WF.thy [is_recfun_def,cut_def] |
106 "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \ |
106 "[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \ |
107 \ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
107 \ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
165 |
165 |
166 goalw WF.thy [wftrec_def] |
166 goalw WF.thy [wftrec_def] |
167 "!!r. [| wf(r); trans(r) |] ==> \ |
167 "!!r. [| wf(r); trans(r) |] ==> \ |
168 \ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; |
168 \ wftrec r a H = H a (cut (%x.wftrec r x H) r a)"; |
169 by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), |
169 by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun), |
170 REPEAT o atac, rtac H_cong1]); |
170 REPEAT o atac, rtac H_cong1]); |
171 by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1); |
171 by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1); |
172 qed "wftrec"; |
172 qed "wftrec"; |
173 |
173 |
174 (*Unused but perhaps interesting*) |
174 (*Unused but perhaps interesting*) |
175 val prems = goal WF.thy |
175 val prems = goal WF.thy |
176 "[| wf(r); trans(r); !!f x. H x (cut f r x) = H x f |] ==> \ |
176 "[| wf(r); trans(r); !!f x. H x (cut f r x) = H x f |] ==> \ |
177 \ wftrec r a H = H a (%x.wftrec r x H)"; |
177 \ wftrec r a H = H a (%x.wftrec r x H)"; |
178 by (rtac (wftrec RS trans) 1); |
178 by (rtac (wftrec RS trans) 1); |
179 by (REPEAT (resolve_tac prems 1)); |
179 by (REPEAT (resolve_tac prems 1)); |
180 qed "wftrec2"; |
180 qed "wftrec2"; |
181 |
181 |
182 (** Removal of the premise trans(r) **) |
182 (** Removal of the premise trans(r) **) |