60 Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair NONE) |
60 Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair NONE) |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
61 ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
62 "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0", |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
63 "Lim_inject", "Suml_inject", "Sumr_inject"]; |
64 |
64 |
65 val descr' = flat descr; |
65 val descr' = List.concat descr; |
66 |
66 |
67 val big_name = space_implode "_" new_type_names; |
67 val big_name = space_implode "_" new_type_names; |
68 val thy1 = add_path flat_names big_name thy; |
68 val thy1 = add_path flat_names big_name thy; |
69 val big_rec_name = big_name ^ "_rep_set"; |
69 val big_rec_name = big_name ^ "_rep_set"; |
70 val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) |
70 val rep_set_names = map (Sign.full_name (Theory.sign_of thy1)) |
76 val leafTs' = get_nonrec_types descr' sorts; |
76 val leafTs' = get_nonrec_types descr' sorts; |
77 val branchTs = get_branching_types descr' sorts; |
77 val branchTs = get_branching_types descr' sorts; |
78 val branchT = if null branchTs then HOLogic.unitT |
78 val branchT = if null branchTs then HOLogic.unitT |
79 else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs; |
79 else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs; |
80 val arities = get_arities descr' \ 0; |
80 val arities = get_arities descr' \ 0; |
81 val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []); |
81 val unneeded_vars = hd tyvars \\ Library.foldr add_typ_tfree_names (leafTs' @ branchTs, []); |
82 val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars); |
82 val leafTs = leafTs' @ (map (fn n => TFree (n, valOf (assoc (sorts, n)))) unneeded_vars); |
83 val recTs = get_rec_types descr' sorts; |
83 val recTs = get_rec_types descr' sorts; |
84 val newTs = take (length (hd descr), recTs); |
84 val newTs = Library.take (length (hd descr), recTs); |
85 val oldTs = drop (length (hd descr), recTs); |
85 val oldTs = Library.drop (length (hd descr), recTs); |
86 val sumT = if null leafTs then HOLogic.unitT |
86 val sumT = if null leafTs then HOLogic.unitT |
87 else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs; |
87 else fold_bal (fn (T, U) => Type ("+", [T, U])) leafTs; |
88 val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); |
88 val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT])); |
89 val UnivT = HOLogic.mk_setT Univ_elT; |
89 val UnivT = HOLogic.mk_setT Univ_elT; |
90 |
90 |
150 val Ts = map (typ_of_dtyp descr' sorts) dts; |
150 val Ts = map (typ_of_dtyp descr' sorts) dts; |
151 val free_t = |
151 val free_t = |
152 app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts) |
152 app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts) |
153 in (j + 1, list_all (map (pair "x") Ts, |
153 in (j + 1, list_all (map (pair "x") Ts, |
154 HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t, |
154 HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t, |
155 Const (nth_elem (k, rep_set_names), UnivT)))) :: prems, |
155 Const (List.nth (rep_set_names, k), UnivT)))) :: prems, |
156 mk_lim (Ts, free_t) :: ts) |
156 mk_lim (Ts, free_t) :: ts) |
157 end |
157 end |
158 | _ => |
158 | _ => |
159 let val T = typ_of_dtyp descr' sorts dt |
159 let val T = typ_of_dtyp descr' sorts dt |
160 in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts) |
160 in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts) |
161 end); |
161 end); |
162 |
162 |
163 val (_, prems, ts) = foldr mk_prem (cargs, (1, [], [])); |
163 val (_, prems, ts) = Library.foldr mk_prem (cargs, (1, [], [])); |
164 val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem |
164 val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem |
165 (mk_univ_inj ts n i, Const (s, UnivT))) |
165 (mk_univ_inj ts n i, Const (s, UnivT))) |
166 in Logic.list_implies (prems, concl) |
166 in Logic.list_implies (prems, concl) |
167 end; |
167 end; |
168 |
168 |
169 val consts = map (fn s => Const (s, UnivT)) rep_set_names; |
169 val consts = map (fn s => Const (s, UnivT)) rep_set_names; |
170 |
170 |
171 val intr_ts = flat (map (fn ((_, (_, _, constrs)), rep_set_name) => |
171 val intr_ts = List.concat (map (fn ((_, (_, _, constrs)), rep_set_name) => |
172 map (make_intr rep_set_name (length constrs)) |
172 map (make_intr rep_set_name (length constrs)) |
173 ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); |
173 ((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names)); |
174 |
174 |
175 val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = |
175 val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) = |
176 setmp InductivePackage.quiet_mode (!quiet_mode) |
176 setmp InductivePackage.quiet_mode (!quiet_mode) |
177 (InductivePackage.add_inductive_i false true big_rec_name false true false |
177 (InductivePackage.add_inductive_i false true big_rec_name false true false |
178 consts (map (fn x => (("", x), [])) intr_ts) []) thy1; |
178 consts (map (fn x => (("", x), [])) intr_ts) []) thy1; |
179 |
179 |
180 (********************************* typedef ********************************) |
180 (********************************* typedef ********************************) |
181 |
181 |
182 val thy3 = add_path flat_names big_name (foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
182 val thy3 = add_path flat_names big_name (Library.foldl (fn (thy, ((((name, mx), tvs), c), name')) => |
183 setmp TypedefPackage.quiet_mode true |
183 setmp TypedefPackage.quiet_mode true |
184 (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE |
184 (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE |
185 (rtac exI 1 THEN |
185 (rtac exI 1 THEN |
186 QUIET_BREADTH_FIRST (has_fewer_prems 1) |
186 QUIET_BREADTH_FIRST (has_fewer_prems 1) |
187 (resolve_tac rep_intrs 1))) thy |> #1) |
187 (resolve_tac rep_intrs 1))) thy |> #1) |
188 (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ |
188 (parent_path flat_names thy2, types_syntax ~~ tyvars ~~ |
189 (take (length newTs, consts)) ~~ new_type_names)); |
189 (Library.take (length newTs, consts)) ~~ new_type_names)); |
190 |
190 |
191 (*********************** definition of constructors ***********************) |
191 (*********************** definition of constructors ***********************) |
192 |
192 |
193 val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; |
193 val big_rep_name = (space_implode "_" new_type_names) ^ "_Rep_"; |
194 val rep_names = map (curry op ^ "Rep_") new_type_names; |
194 val rep_names = map (curry op ^ "Rep_") new_type_names; |
195 val rep_names' = map (fn i => big_rep_name ^ (string_of_int i)) |
195 val rep_names' = map (fn i => big_rep_name ^ (string_of_int i)) |
196 (1 upto (length (flat (tl descr)))); |
196 (1 upto (length (List.concat (tl descr)))); |
197 val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @ |
197 val all_rep_names = map (Sign.intern_const (Theory.sign_of thy3)) rep_names @ |
198 map (Sign.full_name (Theory.sign_of thy3)) rep_names'; |
198 map (Sign.full_name (Theory.sign_of thy3)) rep_names'; |
199 |
199 |
200 (* isomorphism declarations *) |
200 (* isomorphism declarations *) |
201 |
201 |
209 fun constr_arg (dt, (j, l_args, r_args)) = |
209 fun constr_arg (dt, (j, l_args, r_args)) = |
210 let val T = typ_of_dtyp descr' sorts dt; |
210 let val T = typ_of_dtyp descr' sorts dt; |
211 val free_t = mk_Free "x" T j |
211 val free_t = mk_Free "x" T j |
212 in (case (strip_dtyp dt, strip_type T) of |
212 in (case (strip_dtyp dt, strip_type T) of |
213 ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us, |
213 ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us, |
214 Const (nth_elem (m, all_rep_names), U --> Univ_elT) $ |
214 Const (List.nth (all_rep_names, m), U --> Univ_elT) $ |
215 app_bnds free_t (length Us)) :: r_args) |
215 app_bnds free_t (length Us)) :: r_args) |
216 | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) |
216 | _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args)) |
217 end; |
217 end; |
218 |
218 |
219 val (_, l_args, r_args) = foldr constr_arg (cargs, (1, [], [])); |
219 val (_, l_args, r_args) = Library.foldr constr_arg (cargs, (1, [], [])); |
220 val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T; |
220 val constrT = (map (typ_of_dtyp descr' sorts) cargs) ---> T; |
221 val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); |
221 val abs_name = Sign.intern_const (Theory.sign_of thy) ("Abs_" ^ tname); |
222 val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); |
222 val rep_name = Sign.intern_const (Theory.sign_of thy) ("Rep_" ^ tname); |
223 val lhs = list_comb (Const (cname, constrT), l_args); |
223 val lhs = list_comb (Const (cname, constrT), l_args); |
224 val rhs = mk_univ_inj r_args n i; |
224 val rhs = mk_univ_inj r_args n i; |
241 val sg = Theory.sign_of thy; |
241 val sg = Theory.sign_of thy; |
242 val rep_const = cterm_of sg |
242 val rep_const = cterm_of sg |
243 (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT)); |
243 (Const (Sign.intern_const sg ("Rep_" ^ tname), T --> Univ_elT)); |
244 val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong); |
244 val cong' = standard (cterm_instantiate [(cterm_of sg cong_f, rep_const)] arg_cong); |
245 val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma); |
245 val dist = standard (cterm_instantiate [(cterm_of sg distinct_f, rep_const)] distinct_lemma); |
246 val (thy', defs', eqns', _) = foldl ((make_constr_def tname T) (length constrs)) |
246 val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs)) |
247 ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) |
247 ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax) |
248 in |
248 in |
249 (parent_path flat_names thy', defs', eqns @ [eqns'], |
249 (parent_path flat_names thy', defs', eqns @ [eqns'], |
250 rep_congs @ [cong'], dist_lemmas @ [dist]) |
250 rep_congs @ [cong'], dist_lemmas @ [dist]) |
251 end; |
251 end; |
252 |
252 |
253 val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = foldl dt_constr_defs |
253 val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs |
254 ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []), |
254 ((thy3 |> Theory.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []), |
255 hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); |
255 hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax); |
256 |
256 |
257 (*********** isomorphisms for new types (introduced by typedef) ***********) |
257 (*********** isomorphisms for new types (introduced by typedef) ***********) |
258 |
258 |
316 (*---------------------------------------------------------------------*) |
316 (*---------------------------------------------------------------------*) |
317 |
317 |
318 fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) = |
318 fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) = |
319 let |
319 let |
320 val argTs = map (typ_of_dtyp descr' sorts) cargs; |
320 val argTs = map (typ_of_dtyp descr' sorts) cargs; |
321 val T = nth_elem (k, recTs); |
321 val T = List.nth (recTs, k); |
322 val rep_name = nth_elem (k, all_rep_names); |
322 val rep_name = List.nth (all_rep_names, k); |
323 val rep_const = Const (rep_name, T --> Univ_elT); |
323 val rep_const = Const (rep_name, T --> Univ_elT); |
324 val constr = Const (cname, argTs ---> T); |
324 val constr = Const (cname, argTs ---> T); |
325 |
325 |
326 fun process_arg ks' ((i2, i2', ts, Ts), dt) = |
326 fun process_arg ks' ((i2, i2', ts, Ts), dt) = |
327 let |
327 let |
332 (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds |
332 (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds |
333 (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))], |
333 (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))], |
334 Ts @ [Us ---> Univ_elT]) |
334 Ts @ [Us ---> Univ_elT]) |
335 else |
335 else |
336 (i2 + 1, i2', ts @ [mk_lim (Us, |
336 (i2 + 1, i2', ts @ [mk_lim (Us, |
337 Const (nth_elem (j, all_rep_names), U --> Univ_elT) $ |
337 Const (List.nth (all_rep_names, j), U --> Univ_elT) $ |
338 app_bnds (mk_Free "x" T' i2) (length Us))], Ts) |
338 app_bnds (mk_Free "x" T' i2) (length Us))], Ts) |
339 | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) |
339 | _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts)) |
340 end; |
340 end; |
341 |
341 |
342 val (i2, i2', ts, Ts) = foldl (process_arg ks) ((1, 1, [], []), cargs); |
342 val (i2, i2', ts, Ts) = Library.foldl (process_arg ks) ((1, 1, [], []), cargs); |
343 val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1))); |
343 val xs = map (uncurry (mk_Free "x")) (argTs ~~ (1 upto (i2 - 1))); |
344 val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1))); |
344 val ys = map (uncurry (mk_Free "y")) (Ts ~~ (1 upto (i2' - 1))); |
345 val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); |
345 val f = list_abs_free (map dest_Free (xs @ ys), mk_univ_inj ts n i); |
346 |
346 |
347 val (_, _, ts', _) = foldl (process_arg []) ((1, 1, [], []), cargs); |
347 val (_, _, ts', _) = Library.foldl (process_arg []) ((1, 1, [], []), cargs); |
348 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq |
348 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq |
349 (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) |
349 (rep_const $ list_comb (constr, xs), mk_univ_inj ts' n i)) |
350 |
350 |
351 in (fs @ [f], eqns @ [eqn], i + 1) end; |
351 in (fs @ [f], eqns @ [eqn], i + 1) end; |
352 |
352 |
354 |
354 |
355 fun make_iso_defs (ds, (thy, char_thms)) = |
355 fun make_iso_defs (ds, (thy, char_thms)) = |
356 let |
356 let |
357 val ks = map fst ds; |
357 val ks = map fst ds; |
358 val (_, (tname, _, _)) = hd ds; |
358 val (_, (tname, _, _)) = hd ds; |
359 val {rec_rewrites, rec_names, ...} = the (Symtab.lookup (dt_info, tname)); |
359 val {rec_rewrites, rec_names, ...} = valOf (Symtab.lookup (dt_info, tname)); |
360 |
360 |
361 fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = |
361 fun process_dt ((fs, eqns, isos), (k, (tname, _, constrs))) = |
362 let |
362 let |
363 val (fs', eqns', _) = foldl (make_iso_def k ks (length constrs)) |
363 val (fs', eqns', _) = Library.foldl (make_iso_def k ks (length constrs)) |
364 ((fs, eqns, 1), constrs); |
364 ((fs, eqns, 1), constrs); |
365 val iso = (nth_elem (k, recTs), nth_elem (k, all_rep_names)) |
365 val iso = (List.nth (recTs, k), List.nth (all_rep_names, k)) |
366 in (fs', eqns', isos @ [iso]) end; |
366 in (fs', eqns', isos @ [iso]) end; |
367 |
367 |
368 val (fs, eqns, isos) = foldl process_dt (([], [], []), ds); |
368 val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); |
369 val fTs = map fastype_of fs; |
369 val fTs = map fastype_of fs; |
370 val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", |
370 val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def", |
371 equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $ |
371 equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $ |
372 list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos); |
372 list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos); |
373 val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; |
373 val (thy', def_thms) = (PureThy.add_defs_i false o map Thm.no_attributes) defs thy; |
410 (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) |
410 (* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *) |
411 |
411 |
412 fun prove_iso_thms (ds, (inj_thms, elem_thms)) = |
412 fun prove_iso_thms (ds, (inj_thms, elem_thms)) = |
413 let |
413 let |
414 val (_, (tname, _, _)) = hd ds; |
414 val (_, (tname, _, _)) = hd ds; |
415 val {induction, ...} = the (Symtab.lookup (dt_info, tname)); |
415 val {induction, ...} = valOf (Symtab.lookup (dt_info, tname)); |
416 |
416 |
417 fun mk_ind_concl (i, _) = |
417 fun mk_ind_concl (i, _) = |
418 let |
418 let |
419 val T = nth_elem (i, recTs); |
419 val T = List.nth (recTs, i); |
420 val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT); |
420 val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT); |
421 val rep_set_name = nth_elem (i, rep_set_names) |
421 val rep_set_name = List.nth (rep_set_names, i) |
422 in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ |
422 in (HOLogic.all_const T $ Abs ("y", T, HOLogic.imp $ |
423 HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ |
423 HOLogic.mk_eq (Rep_t $ mk_Free "x" T i, Rep_t $ Bound 0) $ |
424 HOLogic.mk_eq (mk_Free "x" T i, Bound 0)), |
424 HOLogic.mk_eq (mk_Free "x" T i, Bound 0)), |
425 HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT))) |
425 HOLogic.mk_mem (Rep_t $ mk_Free "x" T i, Const (rep_set_name, UnivT))) |
426 end; |
426 end; |
492 |
492 |
493 val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq)) |
493 val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq)) |
494 iso_inj_thms_unfolded; |
494 iso_inj_thms_unfolded; |
495 |
495 |
496 val iso_thms = if length descr = 1 then [] else |
496 val iso_thms = if length descr = 1 then [] else |
497 drop (length newTs, split_conj_thm |
497 Library.drop (length newTs, split_conj_thm |
498 (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ => |
498 (prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ => |
499 [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, |
499 [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1, |
500 REPEAT (rtac TrueI 1), |
500 REPEAT (rtac TrueI 1), |
501 rewrite_goals_tac (mk_meta_eq choice_eq :: |
501 rewrite_goals_tac (mk_meta_eq choice_eq :: |
502 symmetric (mk_meta_eq expand_fun_eq) :: range_eqs), |
502 symmetric (mk_meta_eq expand_fun_eq) :: range_eqs), |
503 rewrite_goals_tac (map symmetric range_eqs), |
503 rewrite_goals_tac (map symmetric range_eqs), |
504 REPEAT (EVERY |
504 REPEAT (EVERY |
505 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ |
505 [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @ |
506 flat (map (mk_funs_inv o #1) newT_iso_axms)) 1), |
506 List.concat (map (mk_funs_inv o #1) newT_iso_axms)) 1), |
507 TRY (hyp_subst_tac 1), |
507 TRY (hyp_subst_tac 1), |
508 rtac (sym RS range_eqI) 1, |
508 rtac (sym RS range_eqI) 1, |
509 resolve_tac iso_char_thms 1])]))); |
509 resolve_tac iso_char_thms 1])]))); |
510 |
510 |
511 val Abs_inverse_thms' = |
511 val Abs_inverse_thms' = |
512 map #1 newT_iso_axms @ |
512 map #1 newT_iso_axms @ |
513 map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) |
513 map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp]) |
514 (iso_inj_thms_unfolded, iso_thms); |
514 (iso_inj_thms_unfolded, iso_thms); |
515 |
515 |
516 val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms'); |
516 val Abs_inverse_thms = List.concat (map mk_funs_inv Abs_inverse_thms'); |
517 |
517 |
518 (******************* freeness theorems for constructors *******************) |
518 (******************* freeness theorems for constructors *******************) |
519 |
519 |
520 val _ = message "Proving freeness of constructors ..."; |
520 val _ = message "Proving freeness of constructors ..."; |
521 |
521 |
594 (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); |
594 (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded); |
595 val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; |
595 val Rep_inverse_thms' = map (fn r => r RS myinv_f_f) iso_inj_thms_unfolded; |
596 |
596 |
597 fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = |
597 fun mk_indrule_lemma ((prems, concls), ((i, _), T)) = |
598 let |
598 let |
599 val Rep_t = Const (nth_elem (i, all_rep_names), T --> Univ_elT) $ |
599 val Rep_t = Const (List.nth (all_rep_names, i), T --> Univ_elT) $ |
600 mk_Free "x" T i; |
600 mk_Free "x" T i; |
601 |
601 |
602 val Abs_t = if i < length newTs then |
602 val Abs_t = if i < length newTs then |
603 Const (Sign.intern_const (Theory.sign_of thy6) |
603 Const (Sign.intern_const (Theory.sign_of thy6) |
604 ("Abs_" ^ (nth_elem (i, new_type_names))), Univ_elT --> T) |
604 ("Abs_" ^ (List.nth (new_type_names, i))), Univ_elT --> T) |
605 else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $ |
605 else Const ("Inductive.myinv", [T --> Univ_elT, Univ_elT] ---> T) $ |
606 Const (nth_elem (i, all_rep_names), T --> Univ_elT) |
606 Const (List.nth (all_rep_names, i), T --> Univ_elT) |
607 |
607 |
608 in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, |
608 in (prems @ [HOLogic.imp $ HOLogic.mk_mem (Rep_t, |
609 Const (nth_elem (i, rep_set_names), UnivT)) $ |
609 Const (List.nth (rep_set_names, i), UnivT)) $ |
610 (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], |
610 (mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ (Abs_t $ Rep_t))], |
611 concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) |
611 concls @ [mk_Free "P" (T --> HOLogic.boolT) (i + 1) $ mk_Free "x" T i]) |
612 end; |
612 end; |
613 |
613 |
614 val (indrule_lemma_prems, indrule_lemma_concls) = |
614 val (indrule_lemma_prems, indrule_lemma_concls) = |
615 foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); |
615 Library.foldl mk_indrule_lemma (([], []), (descr' ~~ recTs)); |
616 |
616 |
617 val cert = cterm_of (Theory.sign_of thy6); |
617 val cert = cterm_of (Theory.sign_of thy6); |
618 |
618 |
619 val indrule_lemma = prove_goalw_cterm [] (cert |
619 val indrule_lemma = prove_goalw_cterm [] (cert |
620 (Logic.mk_implies |
620 (Logic.mk_implies |