--- a/src/HOL/BNF/BNF_FP.thy Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/BNF_FP.thy Wed Sep 26 10:00:59 2012 +0200
@@ -17,7 +17,7 @@
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
by auto
-lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x"
+lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
by blast
lemma unit_case_Unity: "(case u of () => f) = f"
--- a/src/HOL/BNF/Examples/Misc_Codata.thy Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Examples/Misc_Codata.thy Wed Sep 26 10:00:59 2012 +0200
@@ -1,4 +1,4 @@
-(* Title: HOL/BNF/Examples/Misc_Data.thy
+(* Title: HOL/BNF/Examples/Misc_Codata.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Copyright 2012
--- a/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Sep 26 10:00:59 2012 +0200
@@ -60,6 +60,7 @@
val map_wpull_of_bnf: BNF -> thm
val rel_as_srel_of_bnf: BNF -> thm
val rel_def_of_bnf: BNF -> thm
+ val rel_eq_of_bnf: BNF -> thm
val rel_flip_of_bnf: BNF -> thm
val set_bd_of_bnf: BNF -> thm list
val set_defs_of_bnf: BNF -> thm list
@@ -186,6 +187,7 @@
map_id': thm lazy,
map_wppull: thm lazy,
rel_as_srel: thm lazy,
+ rel_eq: thm lazy,
rel_flip: thm lazy,
set_natural': thm lazy list,
srel_cong: thm lazy,
@@ -197,8 +199,8 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong in_mono in_srel
- map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong srel_mono srel_Id
- srel_Gr srel_converse srel_O = {
+ map_comp' map_id' map_wppull rel_as_srel rel_eq rel_flip set_natural' srel_cong srel_mono
+ srel_Id srel_Gr srel_converse srel_O = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -210,6 +212,7 @@
map_id' = map_id',
map_wppull = map_wppull,
rel_as_srel = rel_as_srel,
+ rel_eq = rel_eq,
rel_flip = rel_flip,
set_natural' = set_natural',
srel_cong = srel_cong,
@@ -231,6 +234,7 @@
map_id',
map_wppull,
rel_as_srel,
+ rel_eq,
rel_flip,
set_natural',
srel_cong,
@@ -250,6 +254,7 @@
map_id' = Lazy.map f map_id',
map_wppull = Lazy.map f map_wppull,
rel_as_srel = Lazy.map f rel_as_srel,
+ rel_eq = Lazy.map f rel_eq,
rel_flip = Lazy.map f rel_flip,
set_natural' = map (Lazy.map f) set_natural',
srel_cong = Lazy.map f srel_cong,
@@ -371,6 +376,7 @@
val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
val rel_as_srel_of_bnf = Lazy.force o #rel_as_srel o #facts o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
+val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
val set_bd_of_bnf = #set_bd o #axioms o rep_bnf;
val set_defs_of_bnf = #set_defs o #defs o rep_bnf;
@@ -504,6 +510,7 @@
val map_congN = "map_cong";
val map_wpullN = "map_wpull";
val rel_as_srelN = "rel_as_srel";
+val rel_eqN = "rel_eq";
val rel_flipN = "rel_flip";
val set_naturalN = "set_natural";
val set_natural'N = "set_natural'";
@@ -1105,7 +1112,8 @@
val in_srel = Lazy.lazy mk_in_srel;
val eqset_imp_iff_pair = @{thm eqset_imp_iff_pair};
- val mem_Collect_etc = @{thms mem_Collect_eq fst_conv snd_conv prod.cases};
+ val mem_Collect_etc = @{thms fst_conv mem_Collect_eq prod.cases snd_conv};
+ val mem_Collect_etc' = @{thms fst_conv mem_Collect_eq pair_in_Id_conv snd_conv};
fun mk_rel_as_srel () =
unfold_thms lthy mem_Collect_etc
@@ -1115,6 +1123,12 @@
val rel_as_srel = Lazy.lazy mk_rel_as_srel;
+ fun mk_rel_eq () =
+ unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
+ (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]});
+
+ val rel_eq = Lazy.lazy mk_rel_eq;
+
fun mk_rel_flip () =
let
val srel_converse_thm = Lazy.force srel_converse;
@@ -1132,8 +1146,8 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def bnf_srel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_natural in_cong
- in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_flip set_natural' srel_cong
- srel_mono srel_Id srel_Gr srel_converse srel_O;
+ in_mono in_srel map_comp' map_id' map_wppull rel_as_srel rel_eq rel_flip set_natural'
+ srel_cong srel_mono srel_Id srel_Gr srel_converse srel_O;
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1180,6 +1194,7 @@
(map_congN, [#map_cong axioms]),
(map_id'N, [Lazy.force (#map_id' facts)]),
(rel_as_srelN, [Lazy.force (#rel_as_srel facts)]),
+ (rel_eqN, [Lazy.force (#rel_eq facts)]),
(rel_flipN, [Lazy.force (#rel_flip facts)]),
(set_natural'N, map Lazy.force (#set_natural' facts)),
(srel_O_GrN, srel_O_Grs),
--- a/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -7,6 +7,10 @@
signature BNF_FP =
sig
+ type fp_result =
+ BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list
+
val time: Timer.real_timer -> string -> Timer.real_timer
val IITN: string
@@ -91,7 +95,7 @@
val simpsN: string
val strTN: string
val str_initN: string
- val strongN: string
+ val strong_coinductN: string
val sum_bdN: string
val sum_bdTN: string
val unfoldN: string
@@ -160,6 +164,10 @@
open BNF_Def
open BNF_Util
+type fp_result =
+ BNF_Def.BNF list * term list * term list * term list * term list * thm * thm * thm list *
+ thm list * thm list * thm list * thm list list * thm list * thm list * thm list;
+
val timing = true;
fun time timer msg = (if timing
then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))
@@ -242,10 +250,10 @@
val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
val dtor_coinductN = dtorN ^ "_" ^ coinductN
val dtor_srel_coinductN = dtor_srelN ^ "_" ^ coinductN
-val strongN = "strong_"
-val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strongN ^ coinductN
-val dtor_strong_coinductN = dtorN ^ "_" ^ strongN ^ coinductN
-val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strongN ^ coinductN
+val strong_coinductN = "strong_" ^ coinductN
+val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
+val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
+val dtor_srel_strong_coinductN = dtor_srelN ^ "_" ^ strong_coinductN
val hsetN = "Hset"
val hset_recN = hsetN ^ "_rec"
val set_inclN = "set_incl"
@@ -408,7 +416,7 @@
val Ds = fold (fold Term.add_tfreesT) deadss [];
val _ = (case Library.inter (op =) Ds lhss of [] => ()
- | A :: _ => error ("Nonadmissible type recursion (cannot take fixed point of dead type \
+ | A :: _ => error ("Inadmissible type recursion (cannot take fixed point of dead type \
\variable " ^ quote (Syntax.string_of_typ lthy (TFree A)) ^ ")"));
val timer = time (timer "Construction of BNFs");
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
@@ -9,19 +9,13 @@
sig
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
- BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory) ->
+ BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
(binding * typ) list) * (binding * term) list) * mixfix) list) list ->
local_theory -> local_theory
val parse_datatype_cmd: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
- BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory) ->
+ BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
(local_theory -> local_theory) parser
end;
@@ -34,6 +28,8 @@
open BNF_FP
open BNF_FP_Sugar_Tactics
+val mp_conj = @{thm mp_conj};
+
val simp_attrs = @{attributes [simp]};
val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
@@ -96,6 +92,11 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
+fun mk_rel live Ts Us t =
+ let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
+ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+ end;
+
fun liveness_of_fp_bnf n bnf =
(case T_of_bnf bnf of
Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
@@ -119,6 +120,10 @@
op aconv (Logic.dest_implies (Thm.prop_of thm))
handle TERM _ => false;
+fun reassoc_conjs thm =
+ reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
+ handle THM _ => thm;
+
fun type_args_constrained_of (((cAs, _), _), _) = cAs;
fun type_binding_of (((_, b), _), _) = b;
fun mixfix_of ((_, mx), _) = mx;
@@ -205,13 +210,15 @@
| A' :: _ => error ("Extra type variable on right-hand side: " ^
quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
- fun eq_fpT (T as Type (s, Us)) (Type (s', Us')) =
+ fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
quote (Syntax.string_of_typ fake_lthy T)))
- | eq_fpT _ _ = false;
+ | eq_fpT_check _ _ = false;
fun freeze_fp (T as Type (s, Us)) =
- (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Xs j)
+ (case find_index (eq_fpT_check T) fake_Ts of
+ ~1 => Type (s, map freeze_fp Us)
+ | kk => nth Xs kk)
| freeze_fp T = T;
val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
@@ -222,8 +229,8 @@
(* TODO: clean up list *)
val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
- dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss, fp_rel_thms,
- fp_fold_thms, fp_rec_thms), lthy)) =
+ fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
+ fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
val timer = time (Timer.startRealTimer ());
@@ -247,8 +254,8 @@
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+ val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
- val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
@@ -279,7 +286,7 @@
val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
(zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
- names_lthy) =
+ names_lthy0) =
if lfp then
let
val y_Tsss =
@@ -520,14 +527,13 @@
fun mk_rel_thm postproc ctr_defs' xs cxIn ys cyIn =
fold_thms lthy ctr_defs'
- (unfold_thms lthy (pre_rel_def ::
- (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+ (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
+ sum_prod_thms_rel)
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc |> thaw (xs @ ys);
fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
- mk_rel_thm (perhaps (try (fn th => th RS @{thm eq_sym_Unity_imp}))) [ctr_def']
- xs cxIn ys cyIn;
+ mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] xs cxIn ys cyIn;
val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
@@ -647,19 +653,18 @@
val bnf = the (bnf_of lthy s);
val live = live_of_bnf bnf;
val mapx = mk_map live Ts Us (map_of_bnf bnf);
- val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
- val args = map build_arg TUs;
- in Term.list_comb (mapx, args) end;
+ val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
+ in Term.list_comb (mapx, map build_arg TUs') end;
(* TODO: Add map, sets, rel simps *)
val mk_simp_thmss =
- map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
+ map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
injects @ distincts @ cases @ rec_likes @ fold_likes);
fun derive_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, wrap_ress), (folds, recs,
fold_defs, rec_defs)), lthy) =
let
- val (((phis, phis'), us'), names_lthy) =
+ val (((ps, ps'), us'), names_lthy) =
lthy
|> mk_Frees' "P" (map mk_pred1T fpTs)
||>> Variable.variant_fixes fp_b_names;
@@ -704,17 +709,17 @@
in
flat (map2 (map o apfst o cons) xysets ppremss)
end)
- | i => [([], (i + 1, x))])
+ | kk => [([], (kk + 1, x))])
| mk_raw_prem_prems _ _ = [];
fun close_prem_prem xs t =
fold_rev Logic.all (map Free (drop (nn + length xs)
- (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
+ (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t;
fun mk_prem_prem xs (xysets, (j, x)) =
close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
- HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
+ HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
fun mk_raw_prem phi ctr ctr_Ts =
let
@@ -725,23 +730,24 @@
fun mk_prem (xs, raw_pprems, concl) =
fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
- val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
+ val raw_premss = map3 (map2 o mk_raw_prem) ps ctrss ctr_Tsss;
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis us)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
- val induct_thm =
+ val thm =
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
nested_set_natural's pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
in
- `(conj_dests nn) induct_thm
+ `(conj_dests nn) thm
end;
(* TODO: Generate nicer names in case of clashes *)
@@ -757,27 +763,28 @@
fold_rev (fold_rev Logic.all) (xs :: fss)
(mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
- fun build_call frec_likes maybe_tick (T, U) =
+ fun build_rec_like frec_likes maybe_tick (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) T) fpTs of
- ~1 => build_map (build_call frec_likes maybe_tick) T U
- | j => maybe_tick (nth us j) (nth frec_likes j));
+ ~1 => build_map (build_rec_like frec_likes maybe_tick) T U
+ | kk => maybe_tick (nth us kk) (nth frec_likes kk));
fun mk_U maybe_mk_prodT =
typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
- fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
+ fun intr_rec_likes frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
if member (op =) fpTs T then
- maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
+ maybe_cons x [build_rec_like frec_likes (K I) (T, mk_U (K I) T) $ x]
else if exists_fp_subtype T then
- [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
+ [build_rec_like frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
else
[x];
- val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
- val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
+ val gxsss = map (map (maps (intr_rec_likes gfolds (K I) (K I) (K I)))) xsss;
+ val hxsss =
+ map (map (maps (intr_rec_likes hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
@@ -789,7 +796,9 @@
map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
ctr_defss;
- fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context)
+ |> Thm.close_derivation;
in
(map2 (map2 prove) fold_goalss fold_tacss,
map2 (map2 prove) rec_goalss rec_tacss)
@@ -822,28 +831,99 @@
fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
corecs, unfold_defs, corec_defs)), lthy) =
let
+ val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
+
val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
- val selsss = map #2 wrap_ress;
- val disc_thmsss = map #6 wrap_ress;
- val discIss = map #7 wrap_ress;
- val sel_thmsss = map #8 wrap_ress;
+ val selsss = map (map (map (mk_disc_or_sel As)) o #2) wrap_ress;
+ val exhaust_thms = map #3 wrap_ress;
+ val disc_thmsss = map #7 wrap_ress;
+ val discIss = map #8 wrap_ress;
+ val sel_thmsss = map #9 wrap_ress;
- val (us', _) =
+ val (((rs, us'), vs'), names_lthy) =
lthy
- |> Variable.variant_fixes fp_b_names;
+ |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
+ ||>> Variable.variant_fixes fp_b_names
+ ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
val us = map2 (curry Free) us' fpTs;
+ val udiscss = map2 (map o rapp) us discss;
+ val uselsss = map2 (map o map o rapp) us selsss;
- val (coinduct_thms, coinduct_thm) =
+ val vs = map2 (curry Free) vs' fpTs;
+ val vdiscss = map2 (map o rapp) vs discss;
+ val vselsss = map2 (map o map o rapp) vs selsss;
+
+ val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
let
+ val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
+ val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
+ val strong_rs =
+ map4 (fn u => fn v => fn uvr => fn uv_eq =>
+ fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
+
+ fun build_rel_step build_arg (Type (s, Ts)) =
+ let
+ val bnf = the (bnf_of lthy s);
+ val live = live_of_bnf bnf;
+ val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
+ val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
+ in Term.list_comb (rel, map build_arg Ts') end;
+
+ fun build_rel rs' T =
+ (case find_index (curry (op =) T) fpTs of
+ ~1 =>
+ if exists_fp_subtype T then build_rel_step (build_rel rs') T
+ else HOLogic.eq_const T
+ | kk => nth rs' kk);
+
+ fun build_rel_app rs' usel vsel =
+ fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
+
+ fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
+ (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
+ (if null usels then
+ []
+ else
+ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
+ Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
+
+ fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
+ Library.foldr1 HOLogic.mk_conj
+ (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
+ handle List.Empty => @{term True};
+
+ fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
+ fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
+ HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
+
+ val concl =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
+ uvrs us vs));
+
+ fun mk_goal rs' =
+ Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
+ concl);
+
+ val goal = mk_goal rs;
+ val strong_goal = mk_goal strong_rs;
+
+ fun prove dtor_coinduct' goal =
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
+ exhaust_thms ctr_defss disc_thmsss sel_thmsss)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
+
fun postproc nn thm =
Thm.permute_prems 0 nn
- (if nn = 1 then thm RS mp else funpow nn (fn thm => thm RS @{thm mp_conj}) thm)
- |> Drule.zero_var_indexes;
-
- val coinduct_thm = fp_induct;
+ (if nn = 1 then thm RS mp
+ else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
+ |> Drule.zero_var_indexes
+ |> `(conj_dests nn);
in
- `(conj_dests nn) coinduct_thm
+ (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
end;
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
@@ -859,27 +939,28 @@
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
- fun build_call frec_likes maybe_tack (T, U) =
+ fun build_corec_like fcorec_likes maybe_tack (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) U) fpTs of
- ~1 => build_map (build_call frec_likes maybe_tack) T U
- | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
+ ~1 => build_map (build_corec_like fcorec_likes maybe_tack) T U
+ | kk => maybe_tack (nth cs kk, nth us kk) (nth fcorec_likes kk));
fun mk_U maybe_mk_sumT =
typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
- fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
+ fun intr_corec_likes fcorec_likes maybe_mk_sumT maybe_tack cqf =
let val T = fastype_of cqf in
if exists_subtype (member (op =) Cs) T then
- build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+ build_corec_like fcorec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
else
cqf
end;
- val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
- val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
+ val crgsss' = map (map (map (intr_corec_likes gunfolds (K I) (K I)))) crgsss;
+ val cshsss' =
+ map (map (map (intr_corec_likes hcorecs (curry mk_sumT) (tack z)))) cshsss;
val unfold_goalss =
map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
@@ -936,8 +1017,8 @@
fun prove goal tac =
Skip_Proof.prove lthy [] [] goal (tac o #context)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy no_defs_lthy);
+ |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
+ |> Thm.close_derivation;
fun proves [_] [_] = []
| proves goals tacs = map2 prove goals tacs;
@@ -983,7 +1064,12 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val common_notes =
- (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
+ (if nn > 1 then
+ (* FIXME: attribs *)
+ [(coinductN, [coinduct_thm], []),
+ (strong_coinductN, [strong_coinduct_thm], [])]
+ else
+ [])
|> map (fn (thmN, thms, attrs) =>
((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
@@ -997,6 +1083,7 @@
(sel_unfoldsN, sel_unfold_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
(simpsN, simp_thmss, []),
+ (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
(unfoldsN, unfold_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>
--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -12,8 +12,8 @@
val sum_prod_thms_rel: thm list
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
- val mk_coinduct_tac: Proof.context -> int -> int list -> thm -> thm list -> thm list ->
- thm list -> thm list list -> thm list list list -> thm list list -> tactic
+ val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
+ thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic
val mk_corec_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
@@ -42,7 +42,9 @@
Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
-val sum_prod_thms_rel = @{thms prod.cases prod_rel_def sum.cases sum_rel_def};
+val sum_prod_thms_rel =
+ @{thms prod.cases prod_rel_def sum.cases sum_rel_def
+ sum.inject sum.distinct[THEN eq_False[THEN iffD2]]};
val ss_if_True_False = ss_only @{thms if_True if_False};
@@ -141,38 +143,37 @@
pre_set_defss mss (unflat mss (1 upto n)) kkss)
end;
-fun mk_coinduct_choose_prem_tac nn kk =
- EVERY' [rtac allI, rtac allI, rtac impI,
- select_prem_tac nn (dtac meta_spec) kk,
- dtac meta_spec, dtac meta_mp, atac];
+fun mk_coinduct_same_ctr ctxt rel_eqs pre_rel_def dtor_ctor ctr_def discs sels =
+ hyp_subst_tac THEN'
+ subst_tac ctxt (SOME [1, 2]) [ctr_def] THEN'
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN'
+ (atac ORELSE' REPEAT o etac conjE THEN'
+ full_simp_tac
+ (ss_only (@{thm prod.inject} :: no_refl discs @ rel_eqs @ more_simp_thms)) THEN_MAYBE'
+ REPEAT o hyp_subst_tac THEN' REPEAT o rtac conjI THEN' REPEAT o rtac refl);
-fun mk_coinduct_same_ctr ctxt pre_rel_def dtor_ctor ctr_def sels disc =
- hyp_subst_tac THEN' subst_tac ctxt (SOME [1, 2]) [ctr_def] THEN'
- SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels @ sum_prod_thms_rel)) THEN'
- (rtac refl ORELSE' atac ORELSE'
- full_simp_tac (ss_only (disc :: more_simp_thms)));
+fun mk_coinduct_distinct_ctrs discs discs' =
+ hyp_subst_tac THEN' REPEAT o etac conjE THEN'
+ full_simp_tac (ss_only (refl :: no_refl (discs @ discs') @ basic_simp_thms));
-fun mk_coinduct_distinct_ctrs discs =
- hyp_subst_tac THEN' full_simp_tac (ss_only (refl :: discs @ basic_simp_thms));
-
-fun mk_coinduct_exhaust_tac ctxt exhaust k i =
- rtac exhaust i THEN inst_as_projs_tac ctxt k;
-
-fun mk_coinduct_discharge_prem_tac ctxt nn kk n pre_rel_def dtor_ctor exhaust ctr_defs selss discs =
+fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def dtor_ctor exhaust ctr_defs
+ discss selss =
let val ks = 1 upto n in
- EVERY' ([mk_coinduct_choose_prem_tac nn kk, mk_coinduct_exhaust_tac ctxt exhaust 1,
- hyp_subst_tac] @
- map4 (fn k => fn ctr_def => fn sels => fn disc =>
- EVERY' (mk_coinduct_exhaust_tac ctxt exhaust 2 ::
- map2 (fn k' => fn disc' =>
- if k' = k then mk_coinduct_same_ctr ctxt pre_rel_def dtor_ctor ctr_def sels disc
- else mk_coinduct_distinct_ctrs [disc, disc']) ks discs)) ks ctr_defs selss discs)
+ EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk, dtac
+ meta_spec, dtac meta_mp, atac, rtac exhaust, K (inst_as_projs_tac ctxt 1), hyp_subst_tac] @
+ map4 (fn k => fn ctr_def => fn discs => fn sels =>
+ EVERY' ([rtac exhaust, K (inst_as_projs_tac ctxt 2)] @
+ map2 (fn k' => fn discs' =>
+ if k' = k then
+ mk_coinduct_same_ctr ctxt rel_eqs' pre_rel_def dtor_ctor ctr_def discs sels
+ else
+ mk_coinduct_distinct_ctrs discs discs') ks discss)) ks ctr_defs discss selss)
end;
-fun mk_coinduct_tac ctxt nn ns dtor_coinduct pre_rel_defs dtor_ctors exhausts ctr_defss selsss
- discss =
- (rtac dtor_coinduct THEN'
- EVERY' (map8 (mk_coinduct_discharge_prem_tac ctxt nn)
- (1 upto nn) ns pre_rel_defs dtor_ctors exhausts ctr_defss selsss discss)) 1
+fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs dtor_ctors exhausts ctr_defss
+ discsss selsss =
+ (rtac dtor_coinduct' THEN'
+ EVERY' (map8 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
+ (1 upto nn) ns pre_rel_defs dtor_ctors exhausts ctr_defss discsss selsss)) 1;
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -10,10 +10,7 @@
signature BNF_GFP =
sig
val construct_gfp: mixfix list -> (string * sort) list option -> binding list ->
- typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory
+ typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
end;
structure BNF_GFP : BNF_GFP =
@@ -1873,11 +1870,11 @@
||>> mk_Frees "z2" Ts
||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
||>> mk_Frees "x" prodFTs
- ||>> mk_Frees "R" (map (mk_relT o `I) Ts)
+ ||>> mk_Frees "r" (map (mk_relT o `I) Ts)
||>> mk_Frees "f" unfold_fTs
||>> mk_Frees "g" unfold_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
+ ||>> mk_Frees "R" (map2 mk_pred2T Ts Ts);
fun dtor_bind i = Binding.suffix_name ("_" ^ dtorN) (nth bs (i - 1));
val dtor_name = Binding.name_of o dtor_bind;
@@ -2182,6 +2179,7 @@
val timer = time (timer "corec definitions & thms");
+ (* TODO: Get rid of strong versions (since these can easily be derived from the weak ones). *)
val (dtor_map_coinduct_thm, coinduct_params, dtor_srel_coinduct_thm, dtor_coinduct_thm,
dtor_map_strong_coinduct_thm, dtor_srel_strong_coinduct_thm, dtor_strong_coinduct_thm) =
let
@@ -2190,14 +2188,14 @@
fun mk_Ids Id = if Id then map Id_const passiveAs else map mk_diag passive_UNIVs;
- fun mk_phi upto_eq phi z1 z2 = if upto_eq
+ fun mk_phi strong_eq phi z1 z2 = if strong_eq
then Term.absfree (dest_Free z1) (Term.absfree (dest_Free z2)
(HOLogic.mk_disj (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2))))
else phi;
- fun phi_srels upto_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
+ fun phi_srels strong_eq = map4 (fn phi => fn T => fn z1 => fn z2 =>
HOLogic.Collect_const (HOLogic.mk_prodT (T, T)) $
- HOLogic.mk_split (mk_phi upto_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
+ HOLogic.mk_split (mk_phi strong_eq phi z1 z2)) phis Ts Jzs1 Jzs2;
val srels = map (Term.subst_atomic_types ((activeAs ~~ Ts) @ (activeBs ~~ Ts))) relsAsBs;
@@ -2205,17 +2203,17 @@
val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map3 mk_concl phis Jzs1 Jzs2));
- fun mk_srel_prem upto_eq phi dtor srel Jz Jz_copy =
+ fun mk_srel_prem strong_eq phi dtor srel Jz Jz_copy =
let
val concl = HOLogic.mk_mem (HOLogic.mk_tuple [dtor $ Jz, dtor $ Jz_copy],
- Term.list_comb (srel, mk_Ids upto_eq @ phi_srels upto_eq));
+ Term.list_comb (srel, mk_Ids strong_eq @ phi_srels strong_eq));
in
HOLogic.mk_Trueprop
(list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
end;
val srel_prems = map5 (mk_srel_prem false) phis dtors srels Jzs Jzs_copy;
- val srel_upto_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
+ val srel_strong_prems = map5 (mk_srel_prem true) phis dtors srels Jzs Jzs_copy;
val dtor_srel_coinduct_goal =
fold_rev Logic.all frees (Logic.list_implies (srel_prems, concl));
@@ -2226,7 +2224,7 @@
(K (mk_dtor_srel_coinduct_tac ks raw_coind_thm bis_srel_thm))
|> Thm.close_derivation);
- fun mk_dtor_prem upto_eq phi dtor map_nth sets Jz Jz_copy FJz =
+ fun mk_prem strong_eq phi dtor map_nth sets Jz Jz_copy FJz =
let
val xs = [Jz, Jz_copy];
@@ -2236,7 +2234,7 @@
fun mk_set_conjunct set phi z1 z2 =
list_all_free [z1, z2]
(HOLogic.mk_imp (HOLogic.mk_mem (HOLogic.mk_prod (z1, z2), set $ FJz),
- mk_phi upto_eq phi z1 z2 $ z1 $ z2));
+ mk_phi strong_eq phi z1 z2 $ z1 $ z2));
val concl = list_exists_free [FJz] (HOLogic.mk_conj
(Library.foldr1 HOLogic.mk_conj (map2 mk_map_conjunct [fstsTs, sndsTs] xs),
@@ -2247,13 +2245,13 @@
(HOLogic.mk_Trueprop (Term.list_comb (phi, xs)), HOLogic.mk_Trueprop concl))
end;
- fun mk_dtor_prems upto_eq =
- map7 (mk_dtor_prem upto_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
-
- val dtor_prems = mk_dtor_prems false;
- val dtor_upto_prems = mk_dtor_prems true;
-
- val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (dtor_prems, concl));
+ fun mk_prems strong_eq =
+ map7 (mk_prem strong_eq) phis dtors map_FT_nths prodFT_setss Jzs Jzs_copy FJzs;
+
+ val prems = mk_prems false;
+ val strong_prems = mk_prems true;
+
+ val dtor_map_coinduct_goal = fold_rev Logic.all frees (Logic.list_implies (prems, concl));
val dtor_map_coinduct = Skip_Proof.prove lthy [] [] dtor_map_coinduct_goal
(K (mk_dtor_map_coinduct_tac m ks raw_coind_thm bis_def))
|> Thm.close_derivation;
@@ -2263,13 +2261,13 @@
val dtor_srel_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
- (fold_rev Logic.all zs (Logic.list_implies (srel_upto_prems, concl)))
+ (fold_rev Logic.all zs (Logic.list_implies (srel_strong_prems, concl)))
(K (mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids)))
|> Thm.close_derivation;
val dtor_map_strong_coinduct = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] []
- (fold_rev Logic.all zs (Logic.list_implies (dtor_upto_prems, concl)))
+ (fold_rev Logic.all zs (Logic.list_implies (strong_prems, concl)))
(K (mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def
(tcoalg_thm RS bis_diag_thm))))
|> Thm.close_derivation;
@@ -2320,8 +2318,8 @@
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
- ||>> mk_Frees "R" JRTs
+ ||>> mk_Freess "R" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
+ ||>> mk_Frees "r" JRTs
||>> mk_Frees "P" JphiTs
||>> mk_Frees "B1" B1Ts
||>> mk_Frees "B2" B2Ts
@@ -2998,9 +2996,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((Jbnfs, dtors, ctors, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
- ctor_inject_thms, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms,
- ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
+ ((Jbnfs, dtors, ctors, unfolds, corecs, dtor_coinduct_thm, dtor_strong_coinduct_thm,
+ dtor_ctor_thms, ctor_dtor_thms, ctor_inject_thms, folded_dtor_map_thms,
+ folded_dtor_set_thmss', dtor_Jrel_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -9,10 +9,7 @@
signature BNF_LFP =
sig
val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
- typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory
+ typ list * typ list list -> BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory
end;
structure BNF_LFP : BNF_LFP =
@@ -1831,9 +1828,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms,
- ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
- ctor_fold_thms, ctor_rec_thms),
+ ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, ctor_induct_thm, dtor_ctor_thms,
+ ctor_dtor_thms, ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss',
+ ctor_Irel_thms, ctor_fold_thms, ctor_rec_thms),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML Wed Sep 26 10:00:59 2012 +0200
@@ -18,7 +18,7 @@
val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
((bool * term list) * term) *
(binding list * (binding list list * (binding * term) list list)) -> local_theory ->
- (term list * term list list * thm list * thm list * thm list * thm list list * thm list *
+ (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
thm list list) * local_theory
val parse_wrap_options: bool parser
val parse_bound_term: (binding * string) parser
@@ -65,7 +65,7 @@
fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
fun mk_half_pairss' _ ([], []) = []
- | mk_half_pairss' indent (x :: xs, y :: ys) =
+ | mk_half_pairss' indent (x :: xs, _ :: ys) =
indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
fun mk_half_pairss p = mk_half_pairss' [[]] p;
@@ -201,9 +201,9 @@
val vfcase = fcase $ v;
val vgcase = gcase $ v;
- fun mk_u_eq_u () = HOLogic.mk_eq (u, u);
+ fun mk_uu_eq () = HOLogic.mk_eq (u, u);
- val u_eq_v = mk_Trueprop_eq (u, v);
+ val uv_eq = mk_Trueprop_eq (u, v);
val exist_xs_u_eq_ctrs =
map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
@@ -285,7 +285,7 @@
no_defs_lthy
|> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_u_eq_ctr =>
fn NONE =>
- if n = 1 then pair (Term.lambda u (mk_u_eq_u ()), unique_disc_no_def)
+ if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
else if m = 0 then pair (Term.lambda u exist_xs_u_eq_ctr, refl)
else pair (alternate_disc k, alternate_disc_no_def)
| SOME b => Specification.definition (SOME (b, NONE, NoSyn),
@@ -409,7 +409,7 @@
fun mk_unique_disc_def () =
let
val m = the_single ms;
- val goal = mk_Trueprop_eq (mk_u_eq_u (), the_single exist_xs_u_eq_ctrs);
+ val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
in
Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
|> singleton (Proof_Context.export names_lthy lthy)
@@ -525,12 +525,12 @@
HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
(map2 (curry HOLogic.mk_eq) usels vsels)))]);
+ val goal =
+ Library.foldr Logic.list_implies
+ (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
+
val uncollapse_thms =
map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
-
- val goal =
- Library.foldr Logic.list_implies
- (map5 mk_prems ks udiscs uselss vdiscs vselss, u_eq_v);
in
[Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_expand_tac ctxt n ms (inst_thm u disc_exhaust_thm)
@@ -560,9 +560,9 @@
mk_Trueprop_eq (f, g)));
val goal =
- Logic.list_implies (u_eq_v :: map4 mk_prem xctrs xss fs gs,
+ Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss fs gs,
mk_Trueprop_eq (ufcase, vgcase));
- val weak_goal = Logic.mk_implies (u_eq_v, mk_Trueprop_eq (ufcase, vfcase));
+ val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
in
(Skip_Proof.prove lthy [] [] goal (fn _ => mk_case_cong_tac uexhaust_thm case_thms),
Skip_Proof.prove lthy [] [] weak_goal (K (etac arg_cong 1)))
@@ -625,8 +625,8 @@
[(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
in
- ((discs, selss, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, sel_thmss),
- lthy |> Local_Theory.notes (notes' @ notes) |> snd)
+ ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
+ sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
end;
in
(goalss, after_qed, lthy')