63 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
63 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
64 val concl = Ind_Syntax.mk_Trueprop (pred $ t) |
64 val concl = Ind_Syntax.mk_Trueprop (pred $ t) |
65 in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end |
65 in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end |
66 handle Bind => error"Recursion term not found in conclusion"; |
66 handle Bind => error"Recursion term not found in conclusion"; |
67 |
67 |
68 (*Avoids backtracking by delivering the correct premise to each goal*) |
68 (*Minimizes backtracking by delivering the correct premise to each goal*) |
69 fun ind_tac [] 0 = all_tac |
69 fun ind_tac [] 0 = all_tac |
70 | ind_tac(prem::prems) i = |
70 | ind_tac(prem::prems) i = |
71 DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN |
71 DEPTH_SOLVE_1 (ares_tac [Part_eqI, prem, refl] i) THEN |
72 ind_tac prems (i-1); |
72 ind_tac prems (i-1); |
73 |
73 |
74 val pred = Free(pred_name, elem_type --> Ind_Syntax.boolT); |
74 val pred = Free(pred_name, elem_type --> Ind_Syntax.boolT); |
75 |
75 |
76 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) |
76 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) |
77 Inductive.intr_tms; |
77 Inductive.intr_tms; |
78 |
78 |
79 (*Debugging code... |
79 val _ = if !Ind_Syntax.trace then |
80 val _ = writeln "ind_prems = "; |
80 (writeln "ind_prems = "; |
81 val _ = seq (writeln o Sign.string_of_term sign) ind_prems; |
81 seq (writeln o Sign.string_of_term sign) ind_prems; |
82 *) |
82 writeln "raw_induct = "; print_thm Intr_elim.raw_induct) |
|
83 else (); |
|
84 |
83 |
85 |
84 (*We use a MINIMAL simpset because others (such as HOL_ss) contain too many |
86 (*We use a MINIMAL simpset because others (such as HOL_ss) contain too many |
85 simplifications. If the premises get simplified, then the proofs will |
87 simplifications. If the premises get simplified, then the proofs could |
86 fail. This arose with a premise of the form {(F n,G n)|n . True}, which |
88 fail. This arose with a premise of the form {(F n,G n)|n . True}, which |
87 expanded to something containing ...&True. *) |
89 expanded to something containing ...&True. *) |
88 val min_ss = HOL_basic_ss; |
90 val min_ss = HOL_basic_ss; |
89 |
91 |
90 val quant_induct = |
92 val quant_induct = |
95 (big_rec_tm,pred))))) |
97 (big_rec_tm,pred))))) |
96 (fn prems => |
98 (fn prems => |
97 [rtac (impI RS allI) 1, |
99 [rtac (impI RS allI) 1, |
98 DETERM (etac Intr_elim.raw_induct 1), |
100 DETERM (etac Intr_elim.raw_induct 1), |
99 full_simp_tac (min_ss addsimps [Part_Collect]) 1, |
101 full_simp_tac (min_ss addsimps [Part_Collect]) 1, |
100 REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE] |
102 (*This CollectE and disjE separates out the introduction rules*) |
|
103 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), |
|
104 (*Now break down the individual cases. No disjE here in case |
|
105 some premise involves disjunction.*) |
|
106 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, IntE, exE, conjE] |
101 ORELSE' hyp_subst_tac)), |
107 ORELSE' hyp_subst_tac)), |
102 ind_tac (rev prems) (length prems)]) |
108 ind_tac (rev prems) (length prems)]) |
103 handle e => print_sign_exn sign e; |
109 handle e => print_sign_exn sign e; |
104 |
110 |
105 (*** Prove the simultaneous induction rule ***) |
111 (*** Prove the simultaneous induction rule ***) |
159 (fn prems => |
165 (fn prems => |
160 [cut_facts_tac prems 1, |
166 [cut_facts_tac prems 1, |
161 REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN |
167 REPEAT (rewrite_goals_tac [split RS eq_reflection] THEN |
162 lemma_tac 1)]) |
168 lemma_tac 1)]) |
163 handle e => print_sign_exn sign e) |
169 handle e => print_sign_exn sign e) |
164 else TrueI; |
170 else (writeln " [ No mutual induction rule needed ]"; |
|
171 TrueI); |
165 |
172 |
166 (*Mutual induction follows by freeness of Inl/Inr.*) |
173 (*Mutual induction follows by freeness of Inl/Inr.*) |
167 |
174 |
168 (*Simplification largely reduces the mutual induction rule to the |
175 (*Simplification largely reduces the mutual induction rule to the |
169 standard rule*) |
176 standard rule*) |