30 |
30 |
31 val _ = writeln " Proving the induction rule..."; |
31 val _ = writeln " Proving the induction rule..."; |
32 |
32 |
33 (*** Prove the main induction rule ***) |
33 (*** Prove the main induction rule ***) |
34 |
34 |
35 val pred_name = "P"; (*name for predicate variables*) |
35 val pred_name = "P"; (*name for predicate variables*) |
36 |
36 |
37 val big_rec_def::part_rec_defs = Intr_elim.defs; |
37 val big_rec_def::part_rec_defs = Intr_elim.defs; |
38 |
38 |
39 (*Used to make induction rules; |
39 (*Used to make induction rules; |
40 ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops |
40 ind_alist = [(rec_tm1,pred1),...] -- associates predicates with rec ops |
41 prem is a premise of an intr rule*) |
41 prem is a premise of an intr rule*) |
42 fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ |
42 fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ |
43 (Const("op :",_)$t$X), iprems) = |
43 (Const("op :",_)$t$X), iprems) = |
44 (case gen_assoc (op aconv) (ind_alist, X) of |
44 (case gen_assoc (op aconv) (ind_alist, X) of |
45 Some pred => prem :: Ind_Syntax.mk_tprop (pred $ t) :: iprems |
45 Some pred => prem :: Ind_Syntax.mk_tprop (pred $ t) :: iprems |
46 | None => (*possibly membership in M(rec_tm), for M monotone*) |
46 | None => (*possibly membership in M(rec_tm), for M monotone*) |
47 let fun mk_sb (rec_tm,pred) = |
47 let fun mk_sb (rec_tm,pred) = |
48 (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred) |
48 (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred) |
49 in subst_free (map mk_sb ind_alist) prem :: iprems end) |
49 in subst_free (map mk_sb ind_alist) prem :: iprems end) |
50 | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; |
50 | add_induct_prem ind_alist (prem,iprems) = prem :: iprems; |
51 |
51 |
52 (*Make a premise of the induction rule.*) |
52 (*Make a premise of the induction rule.*) |
53 fun induct_prem ind_alist intr = |
53 fun induct_prem ind_alist intr = |
54 let val quantfrees = map dest_Free (term_frees intr \\ rec_params) |
54 let val quantfrees = map dest_Free (term_frees intr \\ rec_params) |
55 val iprems = foldr (add_induct_prem ind_alist) |
55 val iprems = foldr (add_induct_prem ind_alist) |
56 (Logic.strip_imp_prems intr,[]) |
56 (Logic.strip_imp_prems intr,[]) |
57 val (t,X) = Ind_Syntax.rule_concl intr |
57 val (t,X) = Ind_Syntax.rule_concl intr |
58 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
58 val (Some pred) = gen_assoc (op aconv) (ind_alist, X) |
59 val concl = Ind_Syntax.mk_tprop (pred $ t) |
59 val concl = Ind_Syntax.mk_tprop (pred $ t) |
60 in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end |
60 in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end |
61 handle Bind => error"Recursion term not found in conclusion"; |
61 handle Bind => error"Recursion term not found in conclusion"; |
62 |
62 |
63 (*Reduces backtracking by delivering the correct premise to each goal. |
63 (*Reduces backtracking by delivering the correct premise to each goal. |
64 Intro rules with extra Vars in premises still cause some backtracking *) |
64 Intro rules with extra Vars in premises still cause some backtracking *) |
65 fun ind_tac [] 0 = all_tac |
65 fun ind_tac [] 0 = all_tac |
66 | ind_tac(prem::prems) i = |
66 | ind_tac(prem::prems) i = |
67 DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN |
67 DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN |
68 ind_tac prems (i-1); |
68 ind_tac prems (i-1); |
69 |
69 |
70 val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT); |
70 val pred = Free(pred_name, Ind_Syntax.iT --> Ind_Syntax.oT); |
71 |
71 |
72 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) |
72 val ind_prems = map (induct_prem (map (rpair pred) Inductive.rec_tms)) |
73 Inductive.intr_tms; |
73 Inductive.intr_tms; |
74 |
74 |
75 val quant_induct = |
75 val quant_induct = |
76 prove_goalw_cterm part_rec_defs |
76 prove_goalw_cterm part_rec_defs |
77 (cterm_of sign |
77 (cterm_of sign |
78 (Logic.list_implies (ind_prems, |
78 (Logic.list_implies (ind_prems, |
79 Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred))))) |
79 Ind_Syntax.mk_tprop (Ind_Syntax.mk_all_imp(big_rec_tm,pred))))) |
80 (fn prems => |
80 (fn prems => |
81 [rtac (impI RS allI) 1, |
81 [rtac (impI RS allI) 1, |
82 DETERM (etac Intr_elim.raw_induct 1), |
82 DETERM (etac Intr_elim.raw_induct 1), |
83 (*Push Part inside Collect*) |
83 (*Push Part inside Collect*) |
84 asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1, |
84 asm_full_simp_tac (FOL_ss addsimps [Part_Collect]) 1, |
85 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE' |
85 REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE, disjE] ORELSE' |
86 hyp_subst_tac)), |
86 hyp_subst_tac)), |
87 ind_tac (rev prems) (length prems) ]); |
87 ind_tac (rev prems) (length prems) ]); |
88 |
88 |
89 (*** Prove the simultaneous induction rule ***) |
89 (*** Prove the simultaneous induction rule ***) |
90 |
90 |
91 (*Make distinct predicates for each inductive set*) |
91 (*Make distinct predicates for each inductive set*) |
92 |
92 |
128 (pred $ Bound 0); |
128 (pred $ Bound 0); |
129 |
129 |
130 (*To instantiate the main induction rule*) |
130 (*To instantiate the main induction rule*) |
131 val induct_concl = |
131 val induct_concl = |
132 Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm, |
132 Ind_Syntax.mk_tprop(Ind_Syntax.mk_all_imp(big_rec_tm, |
133 Abs("z", Ind_Syntax.iT, |
133 Abs("z", Ind_Syntax.iT, |
134 fold_bal (app Ind_Syntax.conj) |
134 fold_bal (app Ind_Syntax.conj) |
135 (map mk_rec_imp (Inductive.rec_tms~~preds))))) |
135 (map mk_rec_imp (Inductive.rec_tms~~preds))))) |
136 and mutual_induct_concl = |
136 and mutual_induct_concl = |
137 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
137 Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls); |
138 |
138 |
139 val lemma = (*makes the link between the two induction rules*) |
139 val lemma = (*makes the link between the two induction rules*) |
140 prove_goalw_cterm part_rec_defs |
140 prove_goalw_cterm part_rec_defs |
141 (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl))) |
141 (cterm_of sign (Logic.mk_implies (induct_concl,mutual_induct_concl))) |
142 (fn prems => |
142 (fn prems => |
143 [cut_facts_tac prems 1, |
143 [cut_facts_tac prems 1, |
144 REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 |
144 REPEAT (eresolve_tac [asm_rl, conjE, PartE, mp] 1 |
145 ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 |
145 ORELSE resolve_tac [allI, impI, conjI, Part_eqI] 1 |
146 ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); |
146 ORELSE dresolve_tac [spec, mp, Pr.fsplitD] 1)]); |
147 |
147 |
148 (*Mutual induction follows by freeness of Inl/Inr.*) |
148 (*Mutual induction follows by freeness of Inl/Inr.*) |
149 |
149 |
150 (*Simplification largely reduces the mutual induction rule to the |
150 (*Simplification largely reduces the mutual induction rule to the |
151 standard rule*) |
151 standard rule*) |
165 (*Avoids backtracking by delivering the correct premise to each goal*) |
165 (*Avoids backtracking by delivering the correct premise to each goal*) |
166 fun mutual_ind_tac [] 0 = all_tac |
166 fun mutual_ind_tac [] 0 = all_tac |
167 | mutual_ind_tac(prem::prems) i = |
167 | mutual_ind_tac(prem::prems) i = |
168 DETERM |
168 DETERM |
169 (SELECT_GOAL |
169 (SELECT_GOAL |
170 ( |
170 ( |
171 (*Simplify the assumptions and goal by unfolding Part and |
171 (*Simplify the assumptions and goal by unfolding Part and |
172 using freeness of the Sum constructors; proves all but one |
172 using freeness of the Sum constructors; proves all but one |
173 conjunct by contradiction*) |
173 conjunct by contradiction*) |
174 rewrite_goals_tac all_defs THEN |
174 rewrite_goals_tac all_defs THEN |
175 simp_tac (mut_ss addsimps [Part_iff]) 1 THEN |
175 simp_tac (mut_ss addsimps [Part_iff]) 1 THEN |
176 IF_UNSOLVED (*simp_tac may have finished it off!*) |
176 IF_UNSOLVED (*simp_tac may have finished it off!*) |
177 ((*simplify assumptions, but don't accept new rewrite rules!*) |
177 ((*simplify assumptions, but don't accept new rewrite rules!*) |
178 asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1 THEN |
178 asm_full_simp_tac (mut_ss setmksimps (fn _=>[])) 1 THEN |
179 (*unpackage and use "prem" in the corresponding place*) |
179 (*unpackage and use "prem" in the corresponding place*) |
180 REPEAT (rtac impI 1) THEN |
180 REPEAT (rtac impI 1) THEN |
181 rtac (rewrite_rule all_defs prem) 1 THEN |
181 rtac (rewrite_rule all_defs prem) 1 THEN |
182 (*prem must not be REPEATed below: could loop!*) |
182 (*prem must not be REPEATed below: could loop!*) |
183 DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' |
183 DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' |
184 eresolve_tac (conjE::mp::cmonos)))) |
184 eresolve_tac (conjE::mp::cmonos)))) |
185 ) i) |
185 ) i) |
186 THEN mutual_ind_tac prems (i-1); |
186 THEN mutual_ind_tac prems (i-1); |
187 |
187 |
188 val _ = writeln " Proving the mutual induction rule..."; |
188 val _ = writeln " Proving the mutual induction rule..."; |
189 |
189 |
190 val mutual_induct_fsplit = |
190 val mutual_induct_fsplit = |
191 prove_goalw_cterm [] |
191 prove_goalw_cterm [] |
192 (cterm_of sign |
192 (cterm_of sign |
193 (Logic.list_implies |
193 (Logic.list_implies |
194 (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms, |
194 (map (induct_prem (Inductive.rec_tms~~preds)) Inductive.intr_tms, |
195 mutual_induct_concl))) |
195 mutual_induct_concl))) |
196 (fn prems => |
196 (fn prems => |
197 [rtac (quant_induct RS lemma) 1, |
197 [rtac (quant_induct RS lemma) 1, |
198 mutual_ind_tac (rev prems) (length prems)]); |
198 mutual_ind_tac (rev prems) (length prems)]); |
199 |
199 |
200 (*Attempts to remove all occurrences of fsplit*) |
200 (*Attempts to remove all occurrences of fsplit*) |
201 val fsplit_tac = |
201 val fsplit_tac = |
202 REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, |
202 REPEAT (SOMEGOAL (FIRST' [rtac Pr.fsplitI, |
203 dtac Pr.fsplitD, |
203 dtac Pr.fsplitD, |
204 etac Pr.fsplitE, (*apparently never used!*) |
204 etac Pr.fsplitE, (*apparently never used!*) |
205 bound_hyp_subst_tac])) |
205 bound_hyp_subst_tac])) |
206 THEN prune_params_tac |
206 THEN prune_params_tac |
207 |
207 |
208 in |
208 in |
209 struct |
209 struct |
210 (*strip quantifier*) |
210 (*strip quantifier*) |