author | wenzelm |
Sat, 08 Jul 2006 12:54:33 +0200 | |
changeset 20046 | 9c8909fc5865 |
parent 18728 | 6790126ab5f6 |
child 20071 | 8f3e1ddb50e6 |
permissions | -rw-r--r-- |
12191 | 1 |
(* Title: ZF/Tools/inductive_package.ML |
6051 | 2 |
ID: $Id$ |
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1994 University of Cambridge |
|
5 |
||
6 |
Fixedpoint definition module -- for Inductive/Coinductive Definitions |
|
7 |
||
8 |
The functor will be instantiated for normal sums/products (inductive defs) |
|
9 |
and non-standard sums/products (coinductive defs) |
|
10 |
||
11 |
Sums are used only for mutual recursion; |
|
12 |
Products are used only to derive "streamlined" induction rules for relations |
|
13 |
*) |
|
14 |
||
15 |
type inductive_result = |
|
16 |
{defs : thm list, (*definitions made in thy*) |
|
17 |
bnd_mono : thm, (*monotonicity for the lfp definition*) |
|
18 |
dom_subset : thm, (*inclusion of recursive set in dom*) |
|
19 |
intrs : thm list, (*introduction rules*) |
|
20 |
elim : thm, (*case analysis theorem*) |
|
6141 | 21 |
mk_cases : string -> thm, (*generates case theorems*) |
6051 | 22 |
induct : thm, (*main induction rule*) |
23 |
mutual_induct : thm}; (*mutual induction rule*) |
|
24 |
||
25 |
||
26 |
(*Functor's result signature*) |
|
27 |
signature INDUCTIVE_PACKAGE = |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
28 |
sig |
6051 | 29 |
(*Insert definitions for the recursive sets, which |
30 |
must *already* be declared as constants in parent theory!*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
31 |
val add_inductive_i: bool -> term list * term -> |
18728 | 32 |
((bstring * term) * attribute list) list -> |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
33 |
thm list * thm list * thm list * thm list -> theory -> theory * inductive_result |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
34 |
val add_inductive: string list * string -> |
15703 | 35 |
((bstring * string) * Attrib.src list) list -> |
36 |
(thmref * Attrib.src list) list * (thmref * Attrib.src list) list * |
|
37 |
(thmref * Attrib.src list) list * (thmref * Attrib.src list) list -> |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
38 |
theory -> theory * inductive_result |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
39 |
end; |
6051 | 40 |
|
41 |
||
42 |
(*Declares functions to add fixedpoint/constructor defs to a theory. |
|
43 |
Recursive sets must *already* be declared as constants.*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
44 |
functor Add_inductive_def_Fun |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
45 |
(structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU val coind: bool) |
6051 | 46 |
: INDUCTIVE_PACKAGE = |
47 |
struct |
|
12183 | 48 |
|
16855 | 49 |
open Ind_Syntax; |
6051 | 50 |
|
12227 | 51 |
val co_prefix = if coind then "co" else ""; |
52 |
||
7695 | 53 |
|
54 |
(* utils *) |
|
55 |
||
56 |
(*make distinct individual variables a1, a2, a3, ..., an. *) |
|
57 |
fun mk_frees a [] = [] |
|
12902 | 58 |
| mk_frees a (T::Ts) = Free(a,T) :: mk_frees (Symbol.bump_string a) Ts; |
7695 | 59 |
|
60 |
||
61 |
(* add_inductive(_i) *) |
|
62 |
||
6051 | 63 |
(*internal version, accepting terms*) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
64 |
fun add_inductive_i verbose (rec_tms, dom_sum) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
65 |
intr_specs (monos, con_defs, type_intrs, type_elims) thy = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
66 |
let |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
67 |
val _ = Theory.requires thy "Inductive" "(co)inductive definitions"; |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
68 |
val sign = sign_of thy; |
6051 | 69 |
|
12191 | 70 |
val (intr_names, intr_tms) = split_list (map fst intr_specs); |
71 |
val case_names = RuleCases.case_names intr_names; |
|
6051 | 72 |
|
73 |
(*recT and rec_params should agree for all mutually recursive components*) |
|
74 |
val rec_hds = map head_of rec_tms; |
|
75 |
||
76 |
val dummy = assert_all is_Const rec_hds |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
77 |
(fn t => "Recursive set not previously declared as constant: " ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
78 |
Sign.string_of_term sign t); |
6051 | 79 |
|
80 |
(*Now we know they are all Consts, so get their names, type and params*) |
|
81 |
val rec_names = map (#1 o dest_Const) rec_hds |
|
82 |
and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); |
|
83 |
||
84 |
val rec_base_names = map Sign.base_name rec_names; |
|
85 |
val dummy = assert_all Syntax.is_identifier rec_base_names |
|
86 |
(fn a => "Base name of recursive set not an identifier: " ^ a); |
|
87 |
||
88 |
local (*Checking the introduction rules*) |
|
89 |
val intr_sets = map (#2 o rule_concl_msg sign) intr_tms; |
|
90 |
fun intr_ok set = |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
91 |
case head_of set of Const(a,recT) => a mem rec_names | _ => false; |
6051 | 92 |
in |
93 |
val dummy = assert_all intr_ok intr_sets |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
94 |
(fn t => "Conclusion of rule does not name a recursive set: " ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
95 |
Sign.string_of_term sign t); |
6051 | 96 |
end; |
97 |
||
98 |
val dummy = assert_all is_Free rec_params |
|
99 |
(fn t => "Param in recursion term not a free variable: " ^ |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
100 |
Sign.string_of_term sign t); |
6051 | 101 |
|
102 |
(*** Construct the fixedpoint definition ***) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
103 |
val mk_variant = variant (foldr add_term_names [] intr_tms); |
6051 | 104 |
|
105 |
val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; |
|
106 |
||
107 |
fun dest_tprop (Const("Trueprop",_) $ P) = P |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
108 |
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
109 |
Sign.string_of_term sign Q); |
6051 | 110 |
|
111 |
(*Makes a disjunct from an introduction rule*) |
|
112 |
fun fp_part intr = (*quantify over rule's free vars except parameters*) |
|
16855 | 113 |
let val prems = map dest_tprop (Logic.strip_imp_prems intr) |
15570 | 114 |
val dummy = List.app (fn rec_hd => List.app (chk_prem rec_hd) prems) rec_hds |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
115 |
val exfrees = term_frees intr \\ rec_params |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
116 |
val zeq = FOLogic.mk_eq (Free(z',iT), #1 (rule_concl intr)) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
117 |
in foldr FOLogic.mk_exists |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
118 |
(fold_bal FOLogic.mk_conj (zeq::prems)) exfrees |
6051 | 119 |
end; |
120 |
||
121 |
(*The Part(A,h) terms -- compose injections to make h*) |
|
122 |
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*) |
|
123 |
| mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h); |
|
124 |
||
125 |
(*Access to balanced disjoint sums via injections*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
126 |
val parts = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
127 |
map mk_Part (accesses_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, Bound 0) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
128 |
(length rec_tms)); |
6051 | 129 |
|
130 |
(*replace each set by the corresponding Part(A,h)*) |
|
131 |
val part_intrs = map (subst_free (rec_tms ~~ parts) o fp_part) intr_tms; |
|
132 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
133 |
val fp_abs = absfree(X', iT, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
134 |
mk_Collect(z', dom_sum, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
135 |
fold_bal FOLogic.mk_disj part_intrs)); |
6051 | 136 |
|
137 |
val fp_rhs = Fp.oper $ dom_sum $ fp_abs |
|
138 |
||
16855 | 139 |
val dummy = List.app (fn rec_hd => deny (Logic.occs (rec_hd, fp_rhs)) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
140 |
"Illegal occurrence of recursion operator") |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
141 |
rec_hds; |
6051 | 142 |
|
143 |
(*** Make the new theory ***) |
|
144 |
||
145 |
(*A key definition: |
|
146 |
If no mutual recursion then it equals the one recursive set. |
|
147 |
If mutual recursion then it differs from all the recursive sets. *) |
|
148 |
val big_rec_base_name = space_implode "_" rec_base_names; |
|
149 |
val big_rec_name = Sign.intern_const sign big_rec_base_name; |
|
150 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
151 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
152 |
val dummy = conditional verbose (fn () => |
12243 | 153 |
writeln ((if coind then "Coind" else "Ind") ^ "uctive definition " ^ quote big_rec_name)); |
6051 | 154 |
|
155 |
(*Forbid the inductive definition structure from clashing with a theory |
|
156 |
name. This restriction may become obsolete as ML is de-emphasized.*) |
|
16457 | 157 |
val dummy = deny (big_rec_base_name mem (Context.names_of sign)) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
158 |
("Definition " ^ big_rec_base_name ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
159 |
" would clash with the theory of the same name!"); |
6051 | 160 |
|
161 |
(*Big_rec... is the union of the mutually recursive sets*) |
|
162 |
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params); |
|
163 |
||
164 |
(*The individual sets must already be declared*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
165 |
val axpairs = map Logic.mk_defpair |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
166 |
((big_rec_tm, fp_rhs) :: |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
167 |
(case parts of |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
168 |
[_] => [] (*no mutual recursion*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
169 |
| _ => rec_tms ~~ (*define the sets as Parts*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
170 |
map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts)); |
6051 | 171 |
|
172 |
(*tracing: print the fixedpoint definition*) |
|
173 |
val dummy = if !Ind_Syntax.trace then |
|
15570 | 174 |
List.app (writeln o Sign.string_of_term sign o #2) axpairs |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
175 |
else () |
6051 | 176 |
|
177 |
(*add definitions of the inductive sets*) |
|
18377 | 178 |
val (_, thy1) = |
179 |
thy |
|
180 |
|> Theory.add_path big_rec_base_name |
|
181 |
|> PureThy.add_defs_i false (map Thm.no_attributes axpairs) |
|
6051 | 182 |
|
183 |
||
184 |
(*fetch fp definitions from the theory*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
185 |
val big_rec_def::part_rec_defs = |
6051 | 186 |
map (get_def thy1) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
187 |
(case rec_names of [_] => rec_names |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
188 |
| _ => big_rec_base_name::rec_names); |
6051 | 189 |
|
190 |
||
191 |
val sign1 = sign_of thy1; |
|
192 |
||
193 |
(********) |
|
194 |
val dummy = writeln " Proving monotonicity..."; |
|
195 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
196 |
val bnd_mono = |
20046 | 197 |
Goal.prove_global sign1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs)) |
17985 | 198 |
(fn _ => EVERY |
199 |
[rtac (Collect_subset RS bnd_monoI) 1, |
|
20046 | 200 |
REPEAT (ares_tac (basic_monos @ monos) 1)]); |
6051 | 201 |
|
202 |
val dom_subset = standard (big_rec_def RS Fp.subs); |
|
203 |
||
204 |
val unfold = standard ([big_rec_def, bnd_mono] MRS Fp.Tarski); |
|
205 |
||
206 |
(********) |
|
207 |
val dummy = writeln " Proving the introduction rules..."; |
|
208 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
209 |
(*Mutual recursion? Helps to derive subset rules for the |
6051 | 210 |
individual sets.*) |
211 |
val Part_trans = |
|
212 |
case rec_names of |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
213 |
[_] => asm_rl |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
214 |
| _ => standard (Part_subset RS subset_trans); |
6051 | 215 |
|
216 |
(*To type-check recursive occurrences of the inductive sets, possibly |
|
217 |
enclosed in some monotonic operator M.*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
218 |
val rec_typechecks = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
219 |
[dom_subset] RL (asm_rl :: ([Part_trans] RL monos)) |
6051 | 220 |
RL [subsetD]; |
221 |
||
222 |
(*Type-checking is hardest aspect of proof; |
|
223 |
disjIn selects the correct disjunct after unfolding*) |
|
17985 | 224 |
fun intro_tacsf disjIn = |
225 |
[DETERM (stac unfold 1), |
|
6051 | 226 |
REPEAT (resolve_tac [Part_eqI,CollectI] 1), |
227 |
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*) |
|
228 |
rtac disjIn 2, |
|
229 |
(*Not ares_tac, since refl must be tried before equality assumptions; |
|
230 |
backtracking may occur if the premises have extra variables!*) |
|
231 |
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2), |
|
232 |
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*) |
|
233 |
rewrite_goals_tac con_defs, |
|
234 |
REPEAT (rtac refl 2), |
|
235 |
(*Typechecking; this can fail*) |
|
6172 | 236 |
if !Ind_Syntax.trace then print_tac "The type-checking subgoal:" |
6051 | 237 |
else all_tac, |
238 |
REPEAT (FIRSTGOAL ( dresolve_tac rec_typechecks |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
239 |
ORELSE' eresolve_tac (asm_rl::PartE::SigmaE2:: |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
240 |
type_elims) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
241 |
ORELSE' hyp_subst_tac)), |
6051 | 242 |
if !Ind_Syntax.trace then print_tac "The subgoal after monos, type_elims:" |
243 |
else all_tac, |
|
244 |
DEPTH_SOLVE (swap_res_tac (SigmaI::subsetI::type_intrs) 1)]; |
|
245 |
||
246 |
(*combines disjI1 and disjI2 to get the corresponding nested disjunct...*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
247 |
val mk_disj_rls = |
6051 | 248 |
let fun f rl = rl RS disjI1 |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
249 |
and g rl = rl RS disjI2 |
6051 | 250 |
in accesses_bal(f, g, asm_rl) end; |
251 |
||
17985 | 252 |
val intrs = |
253 |
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms))) |
|
254 |
|> ListPair.map (fn (t, tacs) => |
|
20046 | 255 |
Goal.prove_global sign1 [] [] t |
256 |
(fn _ => EVERY (rewrite_goals_tac part_rec_defs :: tacs))) |
|
17985 | 257 |
handle MetaSimplifier.SIMPLIFIER (msg, thm) => (print_thm thm; error msg); |
6051 | 258 |
|
259 |
(********) |
|
260 |
val dummy = writeln " Proving the elimination rule..."; |
|
261 |
||
262 |
(*Breaks down logical connectives in the monotonic function*) |
|
263 |
val basic_elim_tac = |
|
264 |
REPEAT (SOMEGOAL (eresolve_tac (Ind_Syntax.elim_rls @ Su.free_SEs) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
265 |
ORELSE' bound_hyp_subst_tac)) |
6051 | 266 |
THEN prune_params_tac |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
267 |
(*Mutual recursion: collapse references to Part(D,h)*) |
6051 | 268 |
THEN fold_tac part_rec_defs; |
269 |
||
270 |
(*Elimination*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
271 |
val elim = rule_by_tactic basic_elim_tac |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
272 |
(unfold RS Ind_Syntax.equals_CollectD) |
6051 | 273 |
|
274 |
(*Applies freeness of the given constructors, which *must* be unfolded by |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
275 |
the given defs. Cannot simply use the local con_defs because |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
276 |
con_defs=[] for inference systems. |
12175 | 277 |
Proposition A should have the form t:Si where Si is an inductive set*) |
278 |
fun make_cases ss A = |
|
279 |
rule_by_tactic |
|
280 |
(basic_elim_tac THEN ALLGOALS (asm_full_simp_tac ss) THEN basic_elim_tac) |
|
281 |
(Thm.assume A RS elim) |
|
282 |
|> Drule.standard'; |
|
283 |
fun mk_cases a = make_cases (*delayed evaluation of body!*) |
|
284 |
(simpset ()) (read_cterm (Thm.sign_of_thm elim) (a, propT)); |
|
6051 | 285 |
|
286 |
fun induction_rules raw_induct thy = |
|
287 |
let |
|
288 |
val dummy = writeln " Proving the induction rule..."; |
|
289 |
||
290 |
(*** Prove the main induction rule ***) |
|
291 |
||
292 |
val pred_name = "P"; (*name for predicate variables*) |
|
293 |
||
294 |
(*Used to make induction rules; |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
295 |
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
296 |
prem is a premise of an intr rule*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
297 |
fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
298 |
(Const("op :",_)$t$X), iprems) = |
17314 | 299 |
(case AList.lookup (op aconv) ind_alist X of |
15531 | 300 |
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems |
301 |
| NONE => (*possibly membership in M(rec_tm), for M monotone*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
302 |
let fun mk_sb (rec_tm,pred) = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
303 |
(rec_tm, Ind_Syntax.Collect_const$rec_tm$pred) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
304 |
in subst_free (map mk_sb ind_alist) prem :: iprems end) |
6051 | 305 |
| add_induct_prem ind_alist (prem,iprems) = prem :: iprems; |
306 |
||
307 |
(*Make a premise of the induction rule.*) |
|
308 |
fun induct_prem ind_alist intr = |
|
309 |
let val quantfrees = map dest_Free (term_frees intr \\ rec_params) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
310 |
val iprems = foldr (add_induct_prem ind_alist) [] |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
311 |
(Logic.strip_imp_prems intr) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
312 |
val (t,X) = Ind_Syntax.rule_concl intr |
17314 | 313 |
val (SOME pred) = AList.lookup (op aconv) ind_alist X |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
314 |
val concl = FOLogic.mk_Trueprop (pred $ t) |
6051 | 315 |
in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end |
316 |
handle Bind => error"Recursion term not found in conclusion"; |
|
317 |
||
318 |
(*Minimizes backtracking by delivering the correct premise to each goal. |
|
319 |
Intro rules with extra Vars in premises still cause some backtracking *) |
|
320 |
fun ind_tac [] 0 = all_tac |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
321 |
| ind_tac(prem::prems) i = |
13747
bf308fcfd08e
Better treatment of equality in premises of inductive definitions. Less
paulson
parents:
13627
diff
changeset
|
322 |
DEPTH_SOLVE_1 (ares_tac [prem, refl] i) THEN ind_tac prems (i-1); |
6051 | 323 |
|
324 |
val pred = Free(pred_name, Ind_Syntax.iT --> FOLogic.oT); |
|
325 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
326 |
val ind_prems = map (induct_prem (map (rpair pred) rec_tms)) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
327 |
intr_tms; |
6051 | 328 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
329 |
val dummy = if !Ind_Syntax.trace then |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
330 |
(writeln "ind_prems = "; |
15570 | 331 |
List.app (writeln o Sign.string_of_term sign1) ind_prems; |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
332 |
writeln "raw_induct = "; print_thm raw_induct) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
333 |
else (); |
6051 | 334 |
|
335 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
336 |
(*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. |
6051 | 337 |
If the premises get simplified, then the proofs could fail.*) |
17892 | 338 |
val min_ss = Simplifier.theory_context thy empty_ss |
12725 | 339 |
setmksimps (map mk_eq o ZF_atomize o gen_all) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
340 |
setSolver (mk_solver "minimal" |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
341 |
(fn prems => resolve_tac (triv_rls@prems) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
342 |
ORELSE' assume_tac |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
343 |
ORELSE' etac FalseE)); |
6051 | 344 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
345 |
val quant_induct = |
20046 | 346 |
Goal.prove_global sign1 [] ind_prems |
17985 | 347 |
(FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred))) |
348 |
(fn prems => EVERY |
|
349 |
[rewrite_goals_tac part_rec_defs, |
|
350 |
rtac (impI RS allI) 1, |
|
351 |
DETERM (etac raw_induct 1), |
|
352 |
(*Push Part inside Collect*) |
|
353 |
full_simp_tac (min_ss addsimps [Part_Collect]) 1, |
|
354 |
(*This CollectE and disjE separates out the introduction rules*) |
|
355 |
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, disjE])), |
|
356 |
(*Now break down the individual cases. No disjE here in case |
|
357 |
some premise involves disjunction.*) |
|
358 |
REPEAT (FIRSTGOAL (eresolve_tac [CollectE, exE, conjE] |
|
359 |
ORELSE' bound_hyp_subst_tac)), |
|
20046 | 360 |
ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]); |
6051 | 361 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
362 |
val dummy = if !Ind_Syntax.trace then |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
363 |
(writeln "quant_induct = "; print_thm quant_induct) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
364 |
else (); |
6051 | 365 |
|
366 |
||
367 |
(*** Prove the simultaneous induction rule ***) |
|
368 |
||
369 |
(*Make distinct predicates for each inductive set*) |
|
370 |
||
371 |
(*The components of the element type, several if it is a product*) |
|
372 |
val elem_type = CP.pseudo_type dom_sum; |
|
373 |
val elem_factors = CP.factors elem_type; |
|
374 |
val elem_frees = mk_frees "za" elem_factors; |
|
375 |
val elem_tuple = CP.mk_tuple Pr.pair elem_type elem_frees; |
|
376 |
||
377 |
(*Given a recursive set and its domain, return the "fsplit" predicate |
|
378 |
and a conclusion for the simultaneous induction rule. |
|
379 |
NOTE. This will not work for mutually recursive predicates. Previously |
|
380 |
a summand 'domt' was also an argument, but this required the domain of |
|
381 |
mutual recursion to invariably be a disjoint sum.*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
382 |
fun mk_predpair rec_tm = |
6051 | 383 |
let val rec_name = (#1 o dest_Const o head_of) rec_tm |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
384 |
val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
385 |
elem_factors ---> FOLogic.oT) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
386 |
val qconcl = |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
387 |
foldr FOLogic.mk_all |
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
388 |
(FOLogic.imp $ |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
389 |
(Ind_Syntax.mem_const $ elem_tuple $ rec_tm) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
390 |
$ (list_comb (pfree, elem_frees))) elem_frees |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
391 |
in (CP.ap_split elem_type FOLogic.oT pfree, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
392 |
qconcl) |
6051 | 393 |
end; |
394 |
||
395 |
val (preds,qconcls) = split_list (map mk_predpair rec_tms); |
|
396 |
||
397 |
(*Used to form simultaneous induction lemma*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
398 |
fun mk_rec_imp (rec_tm,pred) = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
399 |
FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
400 |
(pred $ Bound 0); |
6051 | 401 |
|
402 |
(*To instantiate the main induction rule*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
403 |
val induct_concl = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
404 |
FOLogic.mk_Trueprop |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
405 |
(Ind_Syntax.mk_all_imp |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
406 |
(big_rec_tm, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
407 |
Abs("z", Ind_Syntax.iT, |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
408 |
fold_bal FOLogic.mk_conj |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
409 |
(ListPair.map mk_rec_imp (rec_tms, preds))))) |
6051 | 410 |
and mutual_induct_concl = |
7695 | 411 |
FOLogic.mk_Trueprop(fold_bal FOLogic.mk_conj qconcls); |
6051 | 412 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
413 |
val dummy = if !Ind_Syntax.trace then |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
414 |
(writeln ("induct_concl = " ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
415 |
Sign.string_of_term sign1 induct_concl); |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
416 |
writeln ("mutual_induct_concl = " ^ |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
417 |
Sign.string_of_term sign1 mutual_induct_concl)) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
418 |
else (); |
6051 | 419 |
|
420 |
||
421 |
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp], |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
422 |
resolve_tac [allI, impI, conjI, Part_eqI], |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
423 |
dresolve_tac [spec, mp, Pr.fsplitD]]; |
6051 | 424 |
|
425 |
val need_mutual = length rec_names > 1; |
|
426 |
||
427 |
val lemma = (*makes the link between the two induction rules*) |
|
428 |
if need_mutual then |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
429 |
(writeln " Proving the mutual induction rule..."; |
20046 | 430 |
Goal.prove_global sign1 [] [] |
17985 | 431 |
(Logic.mk_implies (induct_concl, mutual_induct_concl)) |
432 |
(fn _ => EVERY |
|
433 |
[rewrite_goals_tac part_rec_defs, |
|
20046 | 434 |
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)])) |
17985 | 435 |
else (writeln " [ No mutual induction rule needed ]"; TrueI); |
6051 | 436 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
437 |
val dummy = if !Ind_Syntax.trace then |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
438 |
(writeln "lemma = "; print_thm lemma) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
439 |
else (); |
6051 | 440 |
|
441 |
||
442 |
(*Mutual induction follows by freeness of Inl/Inr.*) |
|
443 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
444 |
(*Simplification largely reduces the mutual induction rule to the |
6051 | 445 |
standard rule*) |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
446 |
val mut_ss = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
447 |
min_ss addsimps [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff]; |
6051 | 448 |
|
449 |
val all_defs = con_defs @ part_rec_defs; |
|
450 |
||
451 |
(*Removes Collects caused by M-operators in the intro rules. It is very |
|
452 |
hard to simplify |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
453 |
list({v: tf. (v : t --> P_t(v)) & (v : f --> P_f(v))}) |
6051 | 454 |
where t==Part(tf,Inl) and f==Part(tf,Inr) to list({v: tf. P_t(v)}). |
455 |
Instead the following rules extract the relevant conjunct. |
|
456 |
*) |
|
457 |
val cmonos = [subset_refl RS Collect_mono] RL monos |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
458 |
RLN (2,[rev_subsetD]); |
6051 | 459 |
|
460 |
(*Minimizes backtracking by delivering the correct premise to each goal*) |
|
461 |
fun mutual_ind_tac [] 0 = all_tac |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
462 |
| mutual_ind_tac(prem::prems) i = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
463 |
DETERM |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
464 |
(SELECT_GOAL |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
465 |
( |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
466 |
(*Simplify the assumptions and goal by unfolding Part and |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
467 |
using freeness of the Sum constructors; proves all but one |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
468 |
conjunct by contradiction*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
469 |
rewrite_goals_tac all_defs THEN |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
470 |
simp_tac (mut_ss addsimps [Part_iff]) 1 THEN |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
471 |
IF_UNSOLVED (*simp_tac may have finished it off!*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
472 |
((*simplify assumptions*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
473 |
(*some risk of excessive simplification here -- might have |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
474 |
to identify the bare minimum set of rewrites*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
475 |
full_simp_tac |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
476 |
(mut_ss addsimps conj_simps @ imp_simps @ quant_simps) 1 |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
477 |
THEN |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
478 |
(*unpackage and use "prem" in the corresponding place*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
479 |
REPEAT (rtac impI 1) THEN |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
480 |
rtac (rewrite_rule all_defs prem) 1 THEN |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
481 |
(*prem must not be REPEATed below: could loop!*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
482 |
DEPTH_SOLVE (FIRSTGOAL (ares_tac [impI] ORELSE' |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
483 |
eresolve_tac (conjE::mp::cmonos)))) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
484 |
) i) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
485 |
THEN mutual_ind_tac prems (i-1); |
6051 | 486 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
487 |
val mutual_induct_fsplit = |
6051 | 488 |
if need_mutual then |
20046 | 489 |
Goal.prove_global sign1 [] (map (induct_prem (rec_tms~~preds)) intr_tms) |
17985 | 490 |
mutual_induct_concl |
491 |
(fn prems => EVERY |
|
492 |
[rtac (quant_induct RS lemma) 1, |
|
20046 | 493 |
mutual_ind_tac (rev prems) (length prems)]) |
6051 | 494 |
else TrueI; |
495 |
||
496 |
(** Uncurrying the predicate in the ordinary induction rule **) |
|
497 |
||
498 |
(*instantiate the variable to a tuple, if it is non-trivial, in order to |
|
499 |
allow the predicate to be "opened up". |
|
500 |
The name "x.1" comes from the "RS spec" !*) |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
501 |
val inst = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
502 |
case elem_frees of [_] => I |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
503 |
| _ => instantiate ([], [(cterm_of sign1 (Var(("x",1), Ind_Syntax.iT)), |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
504 |
cterm_of sign1 elem_tuple)]); |
6051 | 505 |
|
506 |
(*strip quantifier and the implication*) |
|
507 |
val induct0 = inst (quant_induct RS spec RSN (2,rev_mp)); |
|
508 |
||
509 |
val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0 |
|
510 |
||
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
511 |
val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
512 |
|> standard |
6051 | 513 |
and mutual_induct = CP.remove_split mutual_induct_fsplit |
8438 | 514 |
|
18377 | 515 |
val ([induct', mutual_induct'], thy') = |
516 |
thy |
|
18643 | 517 |
|> PureThy.add_thms [((co_prefix ^ "induct", induct), |
18728 | 518 |
[case_names, InductAttrib.induct_set big_rec_name]), |
18643 | 519 |
(("mutual_induct", mutual_induct), [case_names])]; |
12227 | 520 |
in ((thy', induct'), mutual_induct') |
6051 | 521 |
end; (*of induction_rules*) |
522 |
||
523 |
val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct) |
|
524 |
||
12227 | 525 |
val ((thy2, induct), mutual_induct) = |
526 |
if not coind then induction_rules raw_induct thy1 |
|
18377 | 527 |
else |
528 |
(thy1 |
|
529 |
|> PureThy.add_thms [((co_prefix ^ "induct", raw_induct), [])] |
|
530 |
|> apfst hd |> Library.swap, TrueI) |
|
6051 | 531 |
and defs = big_rec_def :: part_rec_defs |
532 |
||
533 |
||
18377 | 534 |
val (([bnd_mono', dom_subset', elim'], [defs', intrs']), thy3) = |
8438 | 535 |
thy2 |
12183 | 536 |
|> IndCases.declare big_rec_name make_cases |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
537 |
|> PureThy.add_thms |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
538 |
[(("bnd_mono", bnd_mono), []), |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
539 |
(("dom_subset", dom_subset), []), |
18728 | 540 |
(("cases", elim), [case_names, InductAttrib.cases_set big_rec_name])] |
18377 | 541 |
||>> (PureThy.add_thmss o map Thm.no_attributes) |
8438 | 542 |
[("defs", defs), |
12175 | 543 |
("intros", intrs)]; |
18377 | 544 |
val (intrs'', thy4) = |
545 |
thy3 |
|
546 |
|> PureThy.add_thms ((intr_names ~~ intrs') ~~ map #2 intr_specs) |
|
547 |
||> Theory.parent_path; |
|
8438 | 548 |
in |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
549 |
(thy4, |
8438 | 550 |
{defs = defs', |
551 |
bnd_mono = bnd_mono', |
|
552 |
dom_subset = dom_subset', |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
553 |
intrs = intrs'', |
8438 | 554 |
elim = elim', |
555 |
mk_cases = mk_cases, |
|
556 |
induct = induct, |
|
557 |
mutual_induct = mutual_induct}) |
|
558 |
end; |
|
6051 | 559 |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
560 |
(*source version*) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
561 |
fun add_inductive (srec_tms, sdom_sum) intr_srcs |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
562 |
(raw_monos, raw_con_defs, raw_type_intrs, raw_type_elims) thy = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
563 |
let |
18728 | 564 |
val intr_atts = map (map (Attrib.attribute thy) o snd) intr_srcs; |
17937 | 565 |
val sintrs = map fst intr_srcs ~~ intr_atts; |
566 |
val read = Sign.simple_read_term thy; |
|
567 |
val rec_tms = map (read Ind_Syntax.iT) srec_tms; |
|
568 |
val dom_sum = read Ind_Syntax.iT sdom_sum; |
|
569 |
val intr_tms = map (read propT o snd o fst) sintrs; |
|
570 |
val intr_specs = (map (fst o fst) sintrs ~~ intr_tms) ~~ map snd sintrs; |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
571 |
in |
18418
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
572 |
thy |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
573 |
|> IsarThy.apply_theorems raw_monos |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
574 |
||>> IsarThy.apply_theorems raw_con_defs |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
575 |
||>> IsarThy.apply_theorems raw_type_intrs |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
576 |
||>> IsarThy.apply_theorems raw_type_elims |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
577 |
|-> (fn (((monos, con_defs), type_intrs), type_elims) => |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
578 |
add_inductive_i true (rec_tms, dom_sum) intr_specs |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
579 |
(monos, con_defs, type_intrs, type_elims)) |
bf448d999b7e
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
haftmann
parents:
18377
diff
changeset
|
580 |
end; |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
581 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
582 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
583 |
(* outer syntax *) |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
584 |
|
17057 | 585 |
local structure P = OuterParse and K = OuterKeyword in |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
586 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
587 |
fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
588 |
#1 o add_inductive doms (map P.triple_swap intrs) (monos, con_defs, type_intrs, type_elims); |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
589 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
590 |
val ind_decl = |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
591 |
(P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term -- |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
592 |
((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.term))) -- |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
593 |
(P.$$$ "intros" |-- |
12876
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
594 |
P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) -- |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
595 |
Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
596 |
Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] -- |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
597 |
Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] -- |
a70df1e5bf10
got rid of explicit marginal comments (now stripped earlier from input);
wenzelm
parents:
12725
diff
changeset
|
598 |
Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) [] |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
599 |
>> (Toplevel.theory o mk_ind); |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
600 |
|
12227 | 601 |
val inductiveP = OuterSyntax.command (co_prefix ^ "inductive") |
602 |
("define " ^ co_prefix ^ "inductive sets") K.thy_decl ind_decl; |
|
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
603 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
604 |
val _ = OuterSyntax.add_keywords |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
605 |
["domains", "intros", "monos", "con_defs", "type_intros", "type_elims"]; |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
606 |
val _ = OuterSyntax.add_parsers [inductiveP]; |
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
607 |
|
6051 | 608 |
end; |
12132
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
609 |
|
1ef58b332ca9
support co/inductive definitions in new-style theories;
wenzelm
parents:
11680
diff
changeset
|
610 |
end; |
15705 | 611 |