1 (* Title: ZF/intr_elim.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1994 University of Cambridge |
|
5 |
|
6 Introduction/elimination rule module -- for Inductive/Coinductive Definitions |
|
7 *) |
|
8 |
|
9 signature INDUCTIVE_ARG = (** Description of a (co)inductive def **) |
|
10 sig |
|
11 val thy : theory (*new theory with inductive defs*) |
|
12 val monos : thm list (*monotonicity of each M operator*) |
|
13 val con_defs : thm list (*definitions of the constructors*) |
|
14 val type_intrs : thm list (*type-checking intro rules*) |
|
15 val type_elims : thm list (*type-checking elim rules*) |
|
16 end; |
|
17 |
|
18 |
|
19 signature INDUCTIVE_I = (** Terms read from the theory section **) |
|
20 sig |
|
21 val rec_tms : term list (*the recursive sets*) |
|
22 val dom_sum : term (*their common domain*) |
|
23 val intr_tms : term list (*terms for the introduction rules*) |
|
24 end; |
|
25 |
|
26 signature INTR_ELIM = |
|
27 sig |
|
28 val thy : theory (*copy of input theory*) |
|
29 val defs : thm list (*definitions made in thy*) |
|
30 val bnd_mono : thm (*monotonicity for the lfp definition*) |
|
31 val dom_subset : thm (*inclusion of recursive set in dom*) |
|
32 val intrs : thm list (*introduction rules*) |
|
33 val elim : thm (*case analysis theorem*) |
|
34 val mk_cases : thm list -> string -> thm (*generates case theorems*) |
|
35 end; |
|
36 |
|
37 signature INTR_ELIM_AUX = (** Used to make induction rules **) |
|
38 sig |
|
39 val raw_induct : thm (*raw induction rule from Fp.induct*) |
|
40 val rec_names : string list (*names of recursive sets*) |
|
41 end; |
|
42 |
|
43 (*prove intr/elim rules for a fixedpoint definition*) |
|
44 functor Intr_elim_Fun |
|
45 (structure Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end |
|
46 and Fp: FP and Pr : PR and Su : SU) |
|
47 : sig include INTR_ELIM INTR_ELIM_AUX end = |
|
48 let |
|
49 |
|
50 val rec_names = map (#1 o dest_Const o head_of) Inductive.rec_tms; |
|
51 val big_rec_base_name = space_implode "_" (map Sign.base_name rec_names); |
|
52 |
|
53 val _ = deny (big_rec_base_name mem (Sign.stamp_names_of (sign_of Inductive.thy))) |
|
54 ("Definition " ^ big_rec_base_name ^ |
|
55 " would clash with the theory of the same name!"); |
|
56 |
|
57 (*fetch fp definitions from the theory*) |
|
58 val big_rec_def::part_rec_defs = |
|
59 map (get_def Inductive.thy) |
|
60 (case rec_names of [_] => rec_names | _ => big_rec_base_name::rec_names); |
|
61 |
|
62 |
|
63 val sign = sign_of Inductive.thy; |
|
64 |
|
65 (********) |
|
66 val _ = writeln " Proving monotonicity..."; |
|
67 |
|
68 val Const("==",_) $ _ $ (_ $ dom_sum $ fp_abs) = |
|
69 big_rec_def |> rep_thm |> #prop |> Logic.unvarify; |
|
70 |
|
71 val bnd_mono = |
|
72 prove_goalw_cterm [] |
|
73 (cterm_of sign (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))) |
|
74 (fn _ => |
|
75 [rtac (Collect_subset RS bnd_monoI) 1, |
|
76 REPEAT (ares_tac (basic_monos @ Inductive.monos) 1)]); |
|
77 |
|
78 val dom_subset = standard (big_rec_def RS Fp.subs); |
|
79 |
|
80 val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski); |
|
81 |
|
82 (********) |
|
83 val _ = writeln " Proving the introduction rules..."; |
|
84 |
|
85 (*Mutual recursion? Helps to derive subset rules for the individual sets.*) |
|
86 val Part_trans = |
|
87 case rec_names of |
|
88 [_] => asm_rl |
|
89 | _ => standard (Part_subset RS subset_trans); |
|
90 |
|
91 (*To type-check recursive occurrences of the inductive sets, possibly |
|
92 enclosed in some monotonic operator M.*) |
|
93 val rec_typechecks = |
|
94 [dom_subset] RL (asm_rl :: ([Part_trans] RL Inductive.monos)) RL [subsetD]; |
|
95 |
|
96 (*Type-checking is hardest aspect of proof; |
|
97 disjIn selects the correct disjunct after unfolding*) |
|
98 fun intro_tacsf disjIn prems = |
|
99 [(*insert prems and underlying sets*) |
|
100 cut_facts_tac prems 1, |
|
101 DETERM (stac unfold 1), |
|
102 REPEAT (resolve_tac [Part_eqI,CollectI] 1), |
|
103 (*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) |
|
104 rtac disjIn 2, |
|
105 (*Not ares_tac, since refl must be tried before any equality assumptions; |
|
106 backtracking may occur if the premises have extra variables!*) |
|
107 DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2), |
|
108 (*Now solve the equations like Tcons(a,f) = Inl(?b4)*) |
|
109 rewrite_goals_tac Inductive.con_defs, |
|
110 REPEAT (rtac refl 2), |
|
111 (*Typechecking; this can fail*) |
|
112 REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks |
|
113 ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2:: |
|
114 Inductive.type_elims) |
|
115 ORELSE' hyp_subst_tac)), |
|
116 DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::Inductive.type_intrs) 1)]; |
|
117 |
|
118 (*combines disjI1 and disjI2 to access the corresponding nested disjunct...*) |
|
119 val mk_disj_rls = |
|
120 let fun f rl = rl RS disjI1 |
|
121 and g rl = rl RS disjI2 |
|
122 in accesses_bal(f, g, asm_rl) end; |
|
123 |
|
124 val intrs = ListPair.map (uncurry (prove_goalw_cterm part_rec_defs)) |
|
125 (map (cterm_of sign) Inductive.intr_tms, |
|
126 map intro_tacsf (mk_disj_rls(length Inductive.intr_tms))); |
|
127 |
|
128 (********) |
|
129 val _ = writeln " Proving the elimination rule..."; |
|
130 |
|
131 (*Breaks down logical connectives in the monotonic function*) |
|
132 val basic_elim_tac = |
|
133 REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs) |
|
134 ORELSE' bound_hyp_subst_tac)) |
|
135 THEN prune_params_tac |
|
136 (*Mutual recursion: collapse references to Part(D,h)*) |
|
137 THEN fold_tac part_rec_defs; |
|
138 |
|
139 in |
|
140 struct |
|
141 val thy = Inductive.thy |
|
142 and defs = big_rec_def :: part_rec_defs |
|
143 and bnd_mono = bnd_mono |
|
144 and dom_subset = dom_subset |
|
145 and intrs = intrs; |
|
146 |
|
147 val elim = rule_by_tactic basic_elim_tac |
|
148 (unfold RS Ind_Syntax.equals_CollectD); |
|
149 |
|
150 (*Applies freeness of the given constructors, which *must* be unfolded by |
|
151 the given defs. Cannot simply use the local con_defs because |
|
152 con_defs=[] for inference systems. |
|
153 String s should have the form t:Si where Si is an inductive set*) |
|
154 fun mk_cases defs s = |
|
155 rule_by_tactic (rewrite_goals_tac defs THEN |
|
156 basic_elim_tac THEN |
|
157 fold_tac defs) |
|
158 (assume_read Inductive.thy s RS elim) |
|
159 |> standard; |
|
160 |
|
161 val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) |
|
162 and rec_names = rec_names |
|
163 end |
|
164 end; |
|
165 |
|