--- 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
@@ -14,6 +14,9 @@
"defaults"
begin
+lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x"
+by blast
+
lemma unit_case_Unity: "(case u of () => f) = f"
by (cases u) (hypsubst, rule unit.cases)
@@ -97,6 +100,11 @@
lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
by blast
+lemma UN_compreh_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
lemma prod_set_simps:
"fsts (x, y) = {x}"
"snds (x, y) = {y}"
--- a/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Sep 26 10:00:59 2012 +0200
@@ -8,6 +8,9 @@
signature BNF_COMP =
sig
+ val ID_bnf: BNF_Def.BNF
+ val DEADID_bnf: BNF_Def.BNF
+
type unfold_set
val empty_unfolds: unfold_set
val map_unfolds_of: unfold_set -> thm list
@@ -34,6 +37,10 @@
open BNF_Tactics
open BNF_Comp_Tactics
+val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
+val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
+
+(* TODO: Replace by "BNF_Defs.defs list" *)
type unfold_set = {
map_unfolds: thm list,
set_unfoldss: thm list list,
@@ -677,9 +684,6 @@
((bnf', deads), lthy')
end;
-val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
-val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
-
fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
| bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
| bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold_set, lthy) =
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -101,7 +101,7 @@
else rtac map_cong 1 THEN
EVERY' (map_index (fn (i, map_cong) =>
rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
- EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac @{thm meta_mp},
+ EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2},
--- 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
@@ -29,6 +29,8 @@
val srelN: string
val map_of_bnf: BNF -> term
+ val sets_of_bnf: BNF -> term list
+ val rel_of_bnf: BNF -> term
val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
@@ -63,7 +65,6 @@
val set_defs_of_bnf: BNF -> thm list
val set_natural'_of_bnf: BNF -> thm list
val set_natural_of_bnf: BNF -> thm list
- val sets_of_bnf: BNF -> term list
val srel_def_of_bnf: BNF -> thm
val srel_Gr_of_bnf: BNF -> thm
val srel_Id_of_bnf: BNF -> thm
@@ -704,9 +705,9 @@
||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
||>> mk_Frees "b" As'
- ||>> mk_Frees' "S" setRTs
- ||>> mk_Frees "S" setRTs
- ||>> mk_Frees "T" setRTsBsCs
+ ||>> mk_Frees' "r" setRTs
+ ||>> mk_Frees "r" setRTs
+ ||>> mk_Frees "s" setRTsBsCs
||>> mk_Frees' "R" QTs;
(*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
@@ -1117,13 +1118,13 @@
fun mk_rel_flip () =
let
val srel_converse_thm = Lazy.force srel_converse;
- val Rs' = Term.add_vars (prop_of srel_converse_thm) [];
- val cts = map (pairself (certify lthy)) (map Var Rs' ~~ sQs);
- val srel_converse_thm' = Drule.cterm_instantiate cts srel_converse_thm;
+ val cts = map (SOME o certify lthy) sQs;
+ val srel_converse_thm' = cterm_instantiate_pos cts srel_converse_thm;
in
unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
(srel_converse_thm' RS eqset_imp_iff_pair)
- |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1
+ |> Drule.zero_var_indexes
+ |> Thm.generalize (map (fst o dest_TFree) (As' @ Bs'), map fst Qs') 1
end;
val rel_flip = Lazy.lazy mk_rel_flip;
--- 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
@@ -39,9 +39,9 @@
val ctor_set_inclN: string
val ctor_set_set_inclN: string
val ctor_srelN: string
- val disc_unfold_iffN: string
+ val disc_unfold_iffsN: string
val disc_unfoldsN: string
- val disc_corec_iffN: string
+ val disc_corec_iffsN: string
val disc_corecsN: string
val dtorN: string
val dtor_coinductN: string
@@ -74,6 +74,7 @@
val isNodeN: string
val lsbisN: string
val map_uniqueN: string
+ val mapsN: string
val min_algN: string
val morN: string
val nchotomyN: string
@@ -86,6 +87,7 @@
val sel_unfoldsN: string
val set_inclN: string
val set_set_inclN: string
+ val setsN: string
val simpsN: string
val strTN: string
val str_initN: string
@@ -96,13 +98,10 @@
val unfoldsN: string
val uniqueN: string
+ (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
val mk_ctor_setN: int -> string
val mk_dtor_setN: int -> string
val mk_dtor_set_inductN: int -> string
- val mk_exhaustN: string -> string
- val mk_injectN: string -> string
- val mk_nchotomyN: string -> string
- val mk_setsN: int -> string
val mk_set_inductN: int -> string
val mk_common_name: string list -> string
@@ -189,6 +188,7 @@
val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
+val mapsN = mapN ^ "s"
val ctor_mapN = ctorN ^ "_" ^ mapN
val dtor_mapN = dtorN ^ "_" ^ mapN
val map_uniqueN = mapN ^ uniqueN
@@ -206,7 +206,7 @@
val LevN = "Lev"
val rvN = "recover"
val behN = "beh"
-fun mk_setsN i = mk_setN i ^ "s"
+val setsN = "sets"
val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
fun mk_set_inductN i = mk_setN i ^ "_induct"
@@ -226,15 +226,12 @@
val ctor_dtorN = ctorN ^ "_" ^ dtorN
val dtor_ctorN = dtorN ^ "_" ^ ctorN
val nchotomyN = "nchotomy"
-fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
val injectN = "inject"
-fun mk_injectN s = s ^ "_" ^ injectN
val exhaustN = "exhaust"
-fun mk_exhaustN s = s ^ "_" ^ exhaustN
-val ctor_injectN = mk_injectN ctorN
-val ctor_exhaustN = mk_exhaustN ctorN
-val dtor_injectN = mk_injectN dtorN
-val dtor_exhaustN = mk_exhaustN dtorN
+val ctor_injectN = ctorN ^ "_" ^ injectN
+val ctor_exhaustN = ctorN ^ "_" ^ exhaustN
+val dtor_injectN = dtorN ^ "_" ^ injectN
+val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
val ctor_relN = ctorN ^ "_" ^ relN
val dtor_relN = dtorN ^ "_" ^ relN
val ctor_srelN = ctorN ^ "_" ^ srelN
@@ -263,9 +260,9 @@
val discN = "disc"
val disc_unfoldsN = discN ^ "_" ^ unfoldsN
val disc_corecsN = discN ^ "_" ^ corecsN
-val iffN = "_iff"
-val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
-val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
+val iffsN = "_iffs"
+val disc_unfold_iffsN = discN ^ "_" ^ unfoldN ^ iffsN
+val disc_corec_iffsN = discN ^ "_" ^ corecN ^ iffsN
val relsN = relN ^ "s"
val selN = "sel"
val sel_relsN = selN ^ "_" ^ relsN
@@ -401,7 +398,7 @@
| fp_sort lhss (SOME resBs) Ass =
(subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
-fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold_set lthy =
+fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy =
let
val name = mk_common_name (map Binding.name_of bs);
fun qualify i =
@@ -429,14 +426,14 @@
val timer = time (timer "Normalization & sealing of BNFs");
- val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
+ val res = construct_fp resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
val timer = time (timer "FP construction in total");
in
timer; (bnfs'', res)
end;
-fun fp_bnf construct bs mixfixes resBs eqs lthy =
+fun fp_bnf construct_fp bs mixfixes resBs eqs lthy =
let
val timer = time (Timer.startRealTimer ());
val (lhss, rhss) = split_list eqs;
@@ -446,10 +443,10 @@
(fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
(empty_unfolds, lthy));
in
- mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
+ mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
end;
-fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
+fun fp_bnf_cmd construct_fp (bs, (raw_lhss, raw_bnfs)) lthy =
let
val timer = time (Timer.startRealTimer ());
val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
@@ -461,7 +458,7 @@
bs raw_bnfs (empty_unfolds, lthy));
in
snd (mk_fp_bnf timer
- (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
+ (construct_fp (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
end;
end;
--- 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
@@ -10,16 +10,18 @@
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
BNF_Def.BNF list -> local_theory ->
- (term list * term list * term list *term list * term list * thm * thm list * thm list *
- thm list * thm list * thm 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) ->
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 ->
- (term list * term list * term list * term list * term list * thm * thm list * thm list *
- thm list * thm list * thm 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) ->
(local_theory -> local_theory) parser
end;
@@ -33,10 +35,9 @@
open BNF_FP_Sugar_Tactics
val simp_attrs = @{attributes [simp]};
+val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
-fun split_list9 xs =
- (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
- map #9 xs);
+fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
fun resort_tfree S (TFree (s, _)) = TFree (s, S);
@@ -60,6 +61,18 @@
fun mk_uncurried2_fun f xss =
mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
+fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
+ Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
+
+fun flip_rels lthy n thm =
+ let
+ val Rs = Term.add_vars (prop_of thm) [];
+ val Rs' = rev (drop (length Rs - n) Rs);
+ val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
+ in
+ Drule.cterm_instantiate cRs thm
+ end;
+
fun mk_ctor_or_dtor get_T Ts t =
let val Type (_, Ts0) = get_T (fastype_of t) in
Term.subst_atomic_types (Ts0 ~~ Ts) t
@@ -83,13 +96,10 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
-fun mk_rel Ts Us t =
- let
- val ((Type (_, Ts0), Type (_, Us0)), body) =
- strip_type (fastype_of t) |>> split_last |>> apfst List.last;
- 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
+ | _ => replicate n false);
fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
@@ -120,7 +130,7 @@
fun defaults_of ((_, ds), _) = ds;
fun ctr_mixfix_of (_, mx) = mx;
-fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
+fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp (no_dests, specs)
no_defs_lthy0 =
let
(* TODO: sanity checks on arguments *)
@@ -143,11 +153,13 @@
val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
- val ((Xs, Cs), no_defs_lthy) =
+ val (((Bs0, Cs), Xs), no_defs_lthy) =
no_defs_lthy0
|> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
- |> variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS) |>> map TFree
- ||>> mk_TFrees nn;
+ |> mk_TFrees (length unsorted_As)
+ ||>> mk_TFrees nn
+ ||>> apfst (map TFree) o
+ variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS);
(* TODO: cleaner handling of fake contexts, without "background_theory" *)
(*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
@@ -208,9 +220,13 @@
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
- val (pre_bnfs, ((dtors0, ctors0, rels0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
- ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
- fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+ (* 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_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+
+ val timer = time (Timer.startRealTimer ());
fun add_nesty_bnf_names Us =
let
@@ -227,11 +243,23 @@
val nesting_bnfs = nesty_bnfs As;
val nested_bnfs = nesty_bnfs Xs;
- val timer = time (Timer.startRealTimer ());
+ val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ 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_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;
+
+ val Bs =
+ map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
+ (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
+
+ val B_ify = Term.typ_subst_atomic (As ~~ Bs);
val ctors = map (mk_ctor As) ctors0;
val dtors = map (mk_dtor As) dtors0;
- val rels = map (mk_rel As As) rels0; (*FIXME*)
val fpTs = map (domain_type o fastype_of) dtors;
@@ -243,11 +271,11 @@
val mss = map (map length) ctr_Tsss;
val Css = map2 replicate ns Cs;
- val fp_folds as fp_fold1 :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
- val fp_recs as fp_rec1 :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
+ val fp_folds as any_fp_fold :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
+ val fp_recs as any_fp_rec :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
- val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
- val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
+ val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_fold)));
+ val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
(zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
@@ -351,9 +379,10 @@
(mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
end;
- fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
- ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
- disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
+ fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
+ fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+ pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
+ ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
let
val fp_b_name = Binding.name_of fp_b;
@@ -367,14 +396,17 @@
|> yield_singleton (mk_Frees "w") dtorT
||>> mk_Frees "f" case_Ts
||>> mk_Freess "x" ctr_Tss
- ||>> mk_Freess "y" ctr_Tss
+ ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
||>> yield_singleton Variable.variant_fixes fp_b_name;
val u = Free (u', fpT);
+ val tuple_xs = map HOLogic.mk_tuple xss;
+ val tuple_ys = map HOLogic.mk_tuple yss;
+
val ctr_rhss =
- map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $
- mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
+ map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
+ mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
@@ -391,6 +423,8 @@
val phi = Proof_Context.export_morphism lthy lthy';
val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+ val ctr_defs' =
+ map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
val case_def = Morphism.thm phi raw_case_def;
val ctrs0 = map (Morphism.term phi) raw_ctrs;
@@ -398,45 +432,130 @@
val ctrs = map (mk_ctr As) ctrs0;
- fun exhaust_tac {context = ctxt, ...} =
+ fun wrap lthy =
let
- val ctor_iff_dtor_thm =
+ fun exhaust_tac {context = ctxt, ...} =
let
- val goal =
- fold_rev Logic.all [w, u]
- (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ val ctor_iff_dtor_thm =
+ let
+ val goal =
+ fold_rev Logic.all [w, u]
+ (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
+ (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
+ |> Thm.close_derivation
+ |> Morphism.thm phi
+ end;
+
+ val sumEN_thm' =
+ unfold_thms lthy @{thms all_unit_eq}
+ (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
+ (mk_sumEN_balanced n))
+ |> Morphism.thm phi;
in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
- (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
- |> Thm.close_derivation
- |> Morphism.thm phi
+ mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
end;
- val sumEN_thm' =
- unfold_thms lthy @{thms all_unit_eq}
- (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
- (mk_sumEN_balanced n))
- |> Morphism.thm phi;
+ val inject_tacss =
+ map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
+ mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+
+ val half_distinct_tacss =
+ map (map (fn (def, def') => fn {context = ctxt, ...} =>
+ mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs));
+
+ val case_tacs =
+ map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
+ mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+
+ val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+
+ val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
in
- mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
+ wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
+ sel_defaultss))) lthy
end;
- val inject_tacss =
- map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
- mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+ fun derive_maps_sets_rels (wrap_res, lthy) =
+ let
+ val rel_flip = rel_flip_of_bnf fp_bnf;
+ val nones = replicate live NONE;
+
+ val ctor_cong =
+ if lfp then Drule.dummy_thm
+ else cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor)] arg_cong;
+
+ fun mk_cIn ify =
+ certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
+ mk_InN_balanced (ify ctr_sum_prod_T) n;
+
+ val cxIns = map2 (mk_cIn I) tuple_xs ks;
+ val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
+
+ fun thaw xs = Thm.generalize ([], map (fst o dest_Free) xs) 1 o Drule.zero_var_indexes;
- val half_distinct_tacss =
- map (map (fn (def, def') => fn {context = ctxt, ...} =>
- mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss ctr_defs);
+ fun mk_map_thm ctr_def' xs cxIn =
+ fold_thms lthy [ctr_def']
+ (unfold_thms lthy (pre_map_def ::
+ (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
+ (cterm_instantiate_pos (nones @ [SOME cxIn])
+ (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
+ |> thaw xs;
+
+ fun mk_set_thm fp_set_thm ctr_def' xs cxIn =
+ fold_thms lthy [ctr_def']
+ (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
+ (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
+ (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
+ |> thaw xs;
+
+ fun mk_set_thms fp_set_thm = map3 (mk_set_thm fp_set_thm) ctr_defs' xss cxIns;
+
+ val map_thms = map3 mk_map_thm ctr_defs' xss cxIns;
+ val set_thmss = map mk_set_thms fp_set_thms;
- val case_tacs =
- map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
- mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+ val rel_infos = (ctr_defs' ~~ xss ~~ cxIns, ctr_defs' ~~ yss ~~ cyIns);
+
+ fun mk_rel_thm finish_off 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)
+ (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
+ |> finish_off |> 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;
+
+ val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
+
+ fun mk_half_neg_rel_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
+ mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
+ xs cxIn ys cyIn;
- val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+ fun mk_other_half_neg_rel_thm thm =
+ flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
+
+ val half_neg_rel_thmss = map (map mk_half_neg_rel_thm) (mk_half_pairss rel_infos);
+ val other_half_neg_rel_thmss = map (map mk_other_half_neg_rel_thm) half_neg_rel_thmss;
+ val (neg_rel_thms, _) = join_halves n half_neg_rel_thmss other_half_neg_rel_thmss;
+
+ val rel_thms = pos_rel_thms @ neg_rel_thms;
- fun define_fold_rec (wrap_res, no_defs_lthy) =
+ val notes =
+ [(mapsN, map_thms, code_simp_attrs),
+ (relsN, rel_thms, code_simp_attrs),
+ (setsN, flat set_thmss, code_simp_attrs)]
+ |> filter_out (null o #2)
+ |> map (fn (thmN, thms, attrs) =>
+ ((Binding.qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
+ in
+ (wrap_res, lthy |> Local_Theory.notes notes |> snd)
+ end;
+
+ fun define_fold_rec no_defs_lthy =
let
val fpT_to_C = fpT --> C;
@@ -468,10 +587,10 @@
val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, foldx, recx, xss, yss, ctr_defs, fold_def, rec_def), lthy)
+ ((foldx, recx, fold_def, rec_def), lthy)
end;
- fun define_unfold_corec (wrap_res, no_defs_lthy) =
+ fun define_unfold_corec no_defs_lthy =
let
val B_to_fpT = C --> fpT;
@@ -508,27 +627,20 @@
val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
in
- ((wrap_res, ctrs, unfold, corec, xss, yss, ctr_defs, unfold_def, corec_def), lthy)
- end;
-
- fun wrap lthy =
- let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
- wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
- sel_defaultss))) lthy
+ ((unfold, corec, unfold_def, corec_def), lthy)
end;
val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
+
+ fun massage_res ((wrap_res, rec_like_res), lthy) =
+ (((ctrs, xss, ctr_defs, wrap_res), rec_like_res), lthy);
in
- ((wrap, define_rec_likes), lthy')
+ (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
end;
- fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
- fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list9
-
- val pre_map_defs = map map_def_of_bnf pre_bnfs;
- val pre_set_defss = map set_defs_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;
+ fun wrap_types_and_more (wrap_types_and_mores, lthy) =
+ fold_map I wrap_types_and_mores lthy
+ |>> apsnd split_list4 o apfst split_list4 o split_list;
fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
let
@@ -539,12 +651,13 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
+ (* TODO: Add map, sets, rel simps *)
val mk_simp_thmss =
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 ((wrap_ress, ctrss, folds, recs, xsss, _, ctr_defss,
- fold_defs, rec_defs), lthy) =
+ 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) =
lthy
@@ -687,8 +800,6 @@
val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
- (* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
- old package)? And for codatatypes as well? *)
val common_notes =
(if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
|> map (fn (thmN, thms, attrs) =>
@@ -697,9 +808,9 @@
val notes =
[(inductN, map single induct_thms,
fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
- (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
- (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
- (simpsN, simp_thmss, K [])] (* TODO: Add relator simps *)
+ (foldsN, fold_thmss, K (code_simp_attrs)),
+ (recsN, rec_thmss, K (code_simp_attrs)),
+ (simpsN, simp_thmss, K [])]
|> maps (fn (thmN, thmss, attrs) =>
map3 (fn b => fn Type (T_name, _) => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
@@ -708,8 +819,8 @@
lthy |> Local_Theory.notes (common_notes @ notes) |> snd
end;
- fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, _,
- ctr_defss, unfold_defs, corec_defs), lthy) =
+ fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
+ corecs, unfold_defs, corec_defs)), lthy) =
let
val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
val selsss = map #2 wrap_ress;
@@ -725,6 +836,9 @@
val (coinduct_thms, coinduct_thm) =
let
+(* val goal =
+ *)
+
val coinduct_thm = fp_induct;
in
`(conj_dests nn) coinduct_thm
@@ -874,13 +988,13 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
(corecsN, corec_thmss, []),
- (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+ (disc_corec_iffsN, disc_corec_iff_thmss, simp_attrs),
+ (disc_corecsN, disc_corec_thmss, simp_attrs),
+ (disc_unfold_iffsN, disc_unfold_iff_thmss, simp_attrs),
(disc_unfoldsN, disc_unfold_thmss, simp_attrs),
- (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
- (disc_corecsN, disc_corec_thmss, simp_attrs),
(sel_unfoldsN, sel_unfold_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
- (simpsN, simp_thmss, []), (* TODO: Add relator simps *)
+ (simpsN, simp_thmss, []),
(unfoldsN, unfold_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>
@@ -890,86 +1004,15 @@
lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
end;
- fun derive_rel_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, xsss, ysss, ctr_defss,
- unfold_defs, corec_defs), lthy) =
- let
- val selsss = map #2 wrap_ress;
-
- val theta_Ts = [] (*###*)
-
- val (thetas, _) =
- lthy
- |> mk_Frees "Q" (map mk_pred1T theta_Ts);
-
- val (rel_thmss, rel_thmsss) =
- let
- val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
- val yctrss = map2 (map2 (curry Term.list_comb)) ctrss ysss;
- val threls = map (fold_rev rapp thetas) rels;
-
- fun mk_goal threl (xctr, xs) (yctr, ys) =
- let
- val lhs = threl $ xctr $ yctr;
-
- (* ### fixme: lift rel *)
- fun mk_conjunct x y = HOLogic.mk_eq (x, y);
-
- fun mk_rhs () =
- Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct xs ys);
- in
- HOLogic.mk_Trueprop
- (if Term.head_of xctr = Term.head_of yctr then
- if null xs then
- lhs
- else
- HOLogic.mk_eq (lhs, mk_rhs ())
- else
- HOLogic.mk_not lhs)
- end;
-
-(*###*)
- (* TODO: Prove and exploit symmetry of relators to halve the number of goals. *)
- fun mk_goals threl xctrs xss yctrs yss =
- map_product (mk_goal threl) (xctrs ~~ xss) (yctrs ~~ yss);
-
- val goalsss = map5 mk_goals threls xctrss xsss yctrss ysss;
-
-(*###
- val goalsss = map6 (fn threl =>
- map5 (fn xctr => fn xs => fn sels =>
- map2 (mk_goal threl xctr xs sels))) threls xctrss xsss selsss yctrss ysss;
-*)
-(* val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*) *)
- in
- ([], [])
- end;
-
- val (sel_rel_thmss, sel_rel_thmsss) =
- let
- in
- ([], [])
- end;
-
- val notes =
- [(* (relsN, rel_thmss, []),
- (sel_relsN, sel_rel_thmss, []) *)]
- |> maps (fn (thmN, thmss, attrs) =>
- map2 (fn b => fn thms =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
- [(thms, [])])) fp_bs thmss);
- in
- lthy |> Local_Theory.notes notes |> snd
- end;
-
val lthy' = lthy
- |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
- fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
- ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
- |>> split_list |> wrap_types_and_define_rec_likes
- |> `(if lfp then derive_induct_fold_rec_thms_for_types
- else derive_coinduct_unfold_corec_thms_for_types)
- |> swap |>> fst
- |> (if null rels then snd else derive_rel_thms_for_types);
+ |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
+ fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
+ pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
+ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
+ raw_sel_defaultsss)
+ |> wrap_types_and_more
+ |> (if lfp then derive_induct_fold_rec_thms_for_types
+ else derive_coinduct_unfold_corec_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
(if lfp then "" else "co") ^ "datatype"));
@@ -995,6 +1038,6 @@
val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
-fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct;
+fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
end;
--- 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
@@ -7,6 +7,10 @@
signature BNF_FP_SUGAR_TACTICS =
sig
+ val sum_prod_thms_map: thm list
+ val sum_prod_thms_set: thm list
+ val sum_prod_thms_rel: thm list
+
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> 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 ->
@@ -27,8 +31,16 @@
open BNF_Util
open BNF_FP
-val meta_mp = @{thm meta_mp};
-val meta_spec = @{thm meta_spec};
+val sum_prod_thms_map = @{thms id_apply map_pair_simp sum_map.simps prod.cases};
+
+val sum_prod_thms_set0 =
+ @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
+ 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};
fun inst_spurious_fs lthy thm =
let
@@ -70,8 +82,7 @@
unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
-(* TODO: Try "map_pair_simp" instead of "map_pair_def" everywhere. *)
-
+(*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
val rec_like_unfold_thms =
@{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps
split_conv unit_case_Unity};
@@ -81,12 +92,11 @@
rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
val corec_like_ss = ss_only @{thms if_True if_False};
-val corec_like_unfold_thms = @{thms id_apply map_pair_def prod.cases sum_map.simps};
fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
- unfold_thms_tac ctxt (pre_map_def :: corec_like_unfold_thms @ map_ids) THEN
+ unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN
unfold_thms_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
@@ -102,14 +112,9 @@
hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
(rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
-val induct_prem_prem_thms =
- @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
- 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};
-
fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
- SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
+ SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ sum_prod_thms_set0)),
solve_prem_prem_tac]) (rev kks)) 1;
fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
--- 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
@@ -9,10 +9,11 @@
signature BNF_GFP =
sig
- val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
+ val construct_gfp: mixfix list -> (string * sort) list option -> binding list ->
typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
- (term list * term list * term list * term list * term list * thm * thm list * thm list *
- thm list * thm list * thm 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
end;
structure BNF_GFP : BNF_GFP =
@@ -21,6 +22,7 @@
open BNF_Def
open BNF_Util
open BNF_Tactics
+open BNF_Comp
open BNF_FP
open BNF_FP_Sugar
open BNF_GFP_Util
@@ -55,7 +57,7 @@
((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
(*all BNFs have the same lives*)
-fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -2285,8 +2287,12 @@
val timer = time (timer "coinduction");
(*register new codatatypes as BNFs*)
- val (Jrels, lthy) = if m = 0 then ([], lthy) else
- let
+ val (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms, lthy) =
+ if m = 0 then
+ let val dummy_thms = replicate n Drule.dummy_thm in
+ (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
+ end
+ else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
val gTs = map2 (curry op -->) passiveBs passiveCs;
val f1Ts = map2 (curry op -->) passiveAs passiveYs;
@@ -2425,7 +2431,7 @@
val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks;
val setss_by_range = transpose setss_by_bnf;
- val set_simp_thmss =
+ val dtor_set_thmss =
let
fun mk_simp_goal relate pas_set act_sets sets dtor z set =
relate (set $ z, mk_union (pas_set $ (dtor $ z),
@@ -2454,7 +2460,7 @@
in
map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))
+ (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets))
|> Thm.close_derivation))
simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
end;
@@ -2860,7 +2866,7 @@
coind_wit_thms (map (pair []) ctor_witss)
|> map (apsnd (map snd o minimize_wits));
- val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+ val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
val (Jbnfs, lthy) =
fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
@@ -2870,10 +2876,10 @@
tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
val fold_maps = fold_thms lthy (map (fn bnf =>
- mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
+ mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
val fold_sets = fold_thms lthy (maps (fn bnf =>
- map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
+ map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Jbnfs);
val timer = time (timer "registered new codatatypes as BNFs");
@@ -2897,8 +2903,8 @@
val Jrel_defs = map rel_def_of_bnf Jbnfs;
val folded_dtor_map_thms = map fold_maps dtor_map_thms;
- val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
- val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
+ val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
+ val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
val dtor_Jsrel_thms =
let
@@ -2914,7 +2920,7 @@
(K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
+ ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss'
dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
dtor_set_set_incl_thmsss
end;
@@ -2951,13 +2957,14 @@
[(dtor_srelN, map single dtor_Jsrel_thms)]
else
[]) @
- map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_set_simp_thmss
+ map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- timer; (Jrels, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
+ timer; (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms,
+ lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
end;
val common_notes =
@@ -2991,8 +2998,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((dtors, ctors, Jrels, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
- ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
+ ((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),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
@@ -3001,10 +3009,10 @@
"define BNF-based coinductive datatypes (low-level)"
(Parse.and_list1
((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
- (snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list));
+ (snd oo fp_bnf_cmd construct_gfp o apsnd split_list o split_list));
val _ =
Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
- (parse_datatype_cmd false bnf_gfp);
+ (parse_datatype_cmd false construct_gfp);
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -40,6 +40,7 @@
val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
thm -> thm -> tactic
+ val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
thm list -> thm list -> tactic
@@ -110,7 +111,6 @@
val mk_set_natural_tac: thm -> thm -> tactic
val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> tactic
- val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
thm list list -> thm list list -> thm -> thm list list -> tactic
@@ -157,11 +157,9 @@
fun mk_mor_incl_tac mor_def map_id's =
(stac mor_def THEN'
rtac conjI THEN'
- CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))
- map_id's THEN'
+ CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
CONJ_WRAP' (fn thm =>
- (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
- map_id's) 1;
+ (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
let
@@ -410,7 +408,7 @@
hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
rtac (mk_sum_casesN n i), rtac CollectI,
EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
- etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])
+ etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
passive_sets),
CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
@@ -564,7 +562,7 @@
then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
- rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
+ rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
@@ -1114,8 +1112,8 @@
unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
EVERY' (map (fn thm =>
- rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
- rtac sym, rtac @{thm id_apply}] 1;
+ rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
+ rtac sym, rtac id_apply] 1;
fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
@@ -1168,7 +1166,7 @@
fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
EVERY' (map (fn i =>
- EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
+ EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
@@ -1196,7 +1194,7 @@
EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
(1 upto n) set_hsets set_hset_hsetss)] 1;
-fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets =
+fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
@@ -1232,11 +1230,11 @@
set_hset_hsetss) =>
[REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
- REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
+ REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
EVERY' (maps (fn set_hset =>
- [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
+ [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
@@ -1473,10 +1471,10 @@
rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
(pick_cols ~~ hset_defs)] 1;
-fun mk_wit_tac n dtor_ctors set_simp wit coind_wits {context = ctxt, prems = _} =
+fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
REPEAT_DETERM (atac 1 ORELSE
- EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+ EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
K (unfold_thms_tac ctxt dtor_ctors),
REPEAT_DETERM_N n o etac UnE,
REPEAT_DETERM o
@@ -1484,7 +1482,7 @@
(eresolve_tac wit ORELSE'
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
- EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
@@ -1524,8 +1522,8 @@
val only_if_tac =
EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
- CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
- EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+ CONJ_WRAP' (fn (dtor_set, passive_set_natural) =>
+ EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
--- 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
@@ -8,10 +8,11 @@
signature BNF_LFP =
sig
- val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
+ val construct_lfp: mixfix list -> (string * sort) list option -> binding list ->
typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
- (term list * term list * term list * term list * term list * thm * thm list * thm list *
- thm list * thm list * thm 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
end;
structure BNF_LFP : BNF_LFP =
@@ -20,13 +21,14 @@
open BNF_Def
open BNF_Util
open BNF_Tactics
+open BNF_Comp
open BNF_FP
open BNF_FP_Sugar
open BNF_LFP_Util
open BNF_LFP_Tactics
(*all BNFs have the same lives*)
-fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
let
val timer = time (Timer.startRealTimer ());
@@ -208,8 +210,8 @@
end;
val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
- val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs
- val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs
+ val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
+ val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
val timer = time (timer "Derived simple theorems");
@@ -1346,8 +1348,12 @@
val timer = time (timer "induction");
(*register new datatypes as BNFs*)
- val (Irels, lthy) = if m = 0 then ([], lthy) else
- let
+ val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
+ if m = 0 then
+ let val dummy_thms = replicate n Drule.dummy_thm in
+ (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
+ end
+ else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
val f1Ts = map2 (curry op -->) passiveAs passiveYs;
val f2Ts = map2 (curry op -->) passiveBs passiveYs;
@@ -1457,7 +1463,7 @@
val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
val setss_by_bnf = transpose setss_by_range;
- val set_simp_thmss =
+ val ctor_set_thmss =
let
fun mk_goal sets ctor set col map =
mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
@@ -1480,19 +1486,19 @@
val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
Skip_Proof.prove lthy [] [] goal
- (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
+ (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
|> Thm.close_derivation)
set_natural'ss) ls simp_goalss setss;
in
ctor_setss
end;
- fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) ::
- map (fn i => (@{thm xt1(3)} OF [set_simp, @{thm Un_upper2}]) RS
+ fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
+ map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
(mk_Un_upper n i RS subset_trans) RSN
(2, @{thm UN_upper} RS subset_trans))
(1 upto n);
- val Fset_set_thmsss = transpose (map (map mk_set_thms) set_simp_thmss);
+ val Fset_set_thmsss = transpose (map (map mk_set_thms) ctor_set_thmss);
val timer = time (timer "set functions for the new datatypes");
@@ -1529,7 +1535,7 @@
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal (mk_tac induct csets ctor_sets i))
|> Thm.close_derivation)
- goals csetss set_simp_thmss inducts ls;
+ goals csetss ctor_set_thmss inducts ls;
in
map split_conj_thm thms
end;
@@ -1556,7 +1562,7 @@
singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal (mk_tac induct ctor_sets i))
|> Thm.close_derivation)
- goals set_simp_thmss inducts ls;
+ goals ctor_set_thmss inducts ls;
in
map split_conj_thm thms
end;
@@ -1654,7 +1660,7 @@
val thm = singleton (Proof_Context.export names_lthy lthy)
(Skip_Proof.prove lthy [] [] goal
(K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
- (transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms)))
+ (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
|> Thm.close_derivation;
in
split_conj_thm thm
@@ -1704,7 +1710,7 @@
ctors (0 upto n - 1) witss
end;
- fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+ fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
val (Ibnfs, lthy) =
fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
@@ -1714,10 +1720,10 @@
tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
val fold_maps = fold_thms lthy (map (fn bnf =>
- mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
+ mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
val fold_sets = fold_thms lthy (maps (fn bnf =>
- map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
+ map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Ibnfs);
val timer = time (timer "registered new datatypes as BNFs");
@@ -1740,8 +1746,8 @@
val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
val folded_ctor_map_thms = map fold_maps ctor_map_thms;
- val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
- val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
+ val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
+ val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
val ctor_Isrel_thms =
let
@@ -1757,7 +1763,7 @@
(K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
+ ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_ctor_set_thmss'
ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
ctor_set_set_incl_thmsss
end;
@@ -1793,13 +1799,14 @@
[(ctor_srelN, map single ctor_Isrel_thms)]
else
[]) @
- map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_set_simp_thmss
+ map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- timer; (Irels, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
+ timer; (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
+ lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
end;
val common_notes =
@@ -1824,8 +1831,9 @@
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- ((dtors, ctors, Irels, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms,
- ctor_inject_thms, ctor_fold_thms, ctor_rec_thms),
+ ((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),
lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
end;
@@ -1834,10 +1842,10 @@
"define BNF-based inductive datatypes (low-level)"
(Parse.and_list1
((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
- (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
+ (snd oo fp_bnf_cmd construct_lfp o apsnd split_list o split_list));
val _ =
Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
- (parse_datatype_cmd true bnf_lfp);
+ (parse_datatype_cmd true construct_lfp);
end;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Sep 26 10:00:59 2012 +0200
@@ -22,6 +22,7 @@
thm list -> tactic
val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
+ val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -69,7 +70,6 @@
val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
val mk_set_natural_tac: thm -> tactic
- val mk_set_simp_tac: thm -> thm -> thm list -> tactic
val mk_set_tac: thm -> tactic
val mk_wit_tac: int -> thm list -> thm list -> tactic
val mk_wpull_tac: thm -> tactic
@@ -83,8 +83,6 @@
open BNF_Util
val fst_snd_convs = @{thms fst_conv snd_conv};
-val id_apply = @{thm id_apply};
-val meta_mp = @{thm meta_mp};
val ord_eq_le_trans = @{thm ord_eq_le_trans};
val subset_trans = @{thm subset_trans};
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
@@ -594,7 +592,7 @@
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
-fun mk_set_simp_tac set set_natural' set_natural's =
+fun mk_ctor_set_tac set set_natural' set_natural's =
let
val n = length set_natural's;
fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
@@ -615,9 +613,9 @@
rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
- fun mk_set_nat cset ctor_map set_simp set_nats =
- EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl,
- rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, set_simp RS trans]),
+ fun mk_set_nat cset ctor_map ctor_set set_nats =
+ EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
+ rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
rtac sym, rtac (nth set_nats (i - 1)),
REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
@@ -633,8 +631,8 @@
fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI,
Goal.assume_rule_tac ctxt, rtac bd_Cinfinite];
- fun mk_set_nat set_simp set_bds =
- EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac set_simp,
+ fun mk_set_nat ctor_set set_bds =
+ EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac ctor_set,
rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_bds (i - 1)),
REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
EVERY' (map useIH (drop m set_bds))];
@@ -759,15 +757,15 @@
EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
rtac wpull, REPEAT_DETERM o atac] 1;
-fun mk_wit_tac n set_simp wit =
+fun mk_wit_tac n ctor_set wit =
REPEAT_DETERM (atac 1 ORELSE
- EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+ EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM o
(TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
(eresolve_tac wit ORELSE'
(dresolve_tac wit THEN'
(etac FalseE ORELSE'
- EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+ EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
REPEAT_DETERM_N n o etac UnE]))))] 1);
fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
@@ -806,8 +804,8 @@
val only_if_tac =
EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
- CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
- EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+ CONJ_WRAP' (fn (ctor_set, passive_set_natural) =>
+ EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
--- a/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 26 10:00:59 2012 +0200
@@ -121,13 +121,16 @@
val mk_ordLeq_csum: int -> int -> thm -> thm
val mk_UnIN: int -> int -> thm
+ val Pair_eqD: thm
+ val Pair_eqI: thm
val ctrans: thm
+ val id_apply: thm
+ val meta_mp: thm
+ val meta_spec: thm
val o_apply: thm
val set_mp: thm
val set_rev_mp: thm
val subset_UNIV: thm
- val Pair_eqD: thm
- val Pair_eqI: thm
val mk_sym: thm -> thm
val mk_trans: thm -> thm -> thm
val mk_unabs_def: int -> thm -> thm
@@ -136,6 +139,7 @@
val no_refl: thm list -> thm list
val no_reflexive: thm list -> thm list
+ val cterm_instantiate_pos: cterm option list -> thm -> thm
val fold_thms: Proof.context -> thm list -> thm -> thm
val unfold_thms: Proof.context -> thm list -> thm -> thm
@@ -525,13 +529,16 @@
fun mk_sym thm = sym OF [thm];
(*TODO: antiquote heavily used theorems once*)
+val Pair_eqD = @{thm iffD1[OF Pair_eq]};
+val Pair_eqI = @{thm iffD2[OF Pair_eq]};
val ctrans = @{thm ordLeq_transitive};
+val id_apply = @{thm id_apply};
+val meta_mp = @{thm meta_mp};
+val meta_spec = @{thm meta_spec};
val o_apply = @{thm o_apply};
val set_mp = @{thm set_mp};
val set_rev_mp = @{thm set_rev_mp};
val subset_UNIV = @{thm subset_UNIV};
-val Pair_eqD = @{thm iffD1[OF Pair_eq]};
-val Pair_eqI = @{thm iffD2[OF Pair_eq]};
fun mk_nthN 1 t 1 = t
| mk_nthN _ t 1 = HOLogic.mk_fst t
@@ -607,8 +614,7 @@
map (f false) negs @ [f true pos]
end;
-fun mk_unabs_def 0 thm = thm
- | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};
+fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
fun is_refl thm =
op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
@@ -617,6 +623,17 @@
val no_refl = filter_out is_refl;
val no_reflexive = filter_out Thm.is_reflexive;
+fun cterm_instantiate_pos cts thm =
+ let
+ val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+ val vars = Term.add_vars (prop_of thm) [];
+ val vars' = rev (drop (length vars - length cts) vars);
+ val ps = map_filter (fn (_, NONE) => NONE
+ | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+ in
+ Drule.cterm_instantiate ps thm
+ end;
+
fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
--- 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
@@ -7,10 +7,14 @@
signature BNF_WRAP =
sig
- val mk_half_pairss: 'a list -> ('a * 'a) list list
+ val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
+ val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
+
val mk_ctr: typ list -> term -> term
val mk_disc_or_sel: typ list -> term -> term
+
val base_name_of_ctr: term -> string
+
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 ->
@@ -60,11 +64,11 @@
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) =
- indent @ fold_rev (cons o single o pair x) xs (mk_half_pairss' ([] :: indent) xs);
+fun mk_half_pairss' _ ([], []) = []
+ | mk_half_pairss' indent (x :: xs, y :: ys) =
+ indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
-fun mk_half_pairss xs = mk_half_pairss' [[]] xs;
+fun mk_half_pairss p = mk_half_pairss' [[]] p;
fun join_halves n half_xss other_half_xss =
let
@@ -72,7 +76,7 @@
map2 (map2 append) (Library.chop_groups n half_xss)
(transpose (Library.chop_groups n other_half_xss))
val xs = interleave (flat half_xss) (flat other_half_xss);
- in (xs, xsss |> `transpose) end;
+ in (xs, xsss) end;
fun mk_undefined T = Const (@{const_name undefined}, T);
@@ -337,7 +341,7 @@
fold_rev Logic.all (xs @ xs')
(HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
in
- map (map mk_goal) (mk_half_pairss (xss ~~ xctrs))
+ map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
end;
val cases_goal =
@@ -366,7 +370,7 @@
val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
- join_halves n half_distinct_thmss other_half_distinct_thmss;
+ join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
val nchotomy_thm =
let
@@ -463,8 +467,7 @@
fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
- val infos = ms ~~ discD_thms ~~ udiscs;
- val half_pairss = mk_half_pairss infos;
+ val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
val half_goalss = map mk_goal half_pairss;
val half_thmss =
@@ -477,7 +480,7 @@
map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
other_half_goalss;
in
- join_halves n half_thmss other_half_thmss
+ join_halves n half_thmss other_half_thmss ||> `transpose
|>> has_alternate_disc_def ? K []
end;