--- a/src/HOL/Datatype_Examples/Misc_Codatatype.thy Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Codatatype.thy Sat Sep 13 18:08:38 2014 +0200
@@ -105,8 +105,11 @@
codatatype ('b, 'a) bar = BAR "'a \<Rightarrow> 'b"
codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
-codatatype 'a dead_foo = A
-codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+codatatype (dead 'a) dead_foo = A
+codatatype ('a, 'b) use_dead_foo = Y 'a "'b dead_foo"
+
+codatatype 'a phantom = A
+codatatype 'a use_phantom = Y 'a "'a use_phantom phantom"
(* SLOW, MEMORY-HUNGRY
codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Sat Sep 13 18:08:38 2014 +0200
@@ -150,8 +150,11 @@
datatype (discs_sels) ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
datatype (discs_sels) 'a deadfoo = DeadFoo "'a \<Rightarrow> 'a + 'a"
-datatype (discs_sels) 'a dead_foo = A
-datatype (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
+datatype (discs_sels) (dead 'a) dead_foo = A
+datatype (discs_sels) ('a, 'b) use_dead_foo = Y 'a "'b dead_foo"
+
+datatype (discs_sels) 'a phantom = A
+datatype (discs_sels) 'a use_phantom = Y 'a "'a use_phantom phantom"
datatype ('t, 'id) dead_sum_fun = Dead_sum_fun "('t list \<Rightarrow> 't) + 't" | Bar (bar: 'id)
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Sep 13 18:08:38 2014 +0200
@@ -42,7 +42,7 @@
val mk_repT: typ -> typ -> typ -> typ
val mk_abs: typ -> term -> term
val mk_rep: typ -> term -> term
- val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf ->
+ val seal_bnf: (binding -> binding) -> unfold_set -> binding -> bool -> typ list -> BNF_Def.bnf ->
local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory
end;
@@ -629,7 +629,7 @@
lift_bnf qualify n bnf
#> uncurry (permute_bnf qualify src dest);
-fun normalize_bnfs qualify Ass Ds sort bnfs accum =
+fun normalize_bnfs qualify Ass Ds flatten_tyargs bnfs accum =
let
val before_kill_src = map (fn As => 0 upto (length As - 1)) Ass;
val kill_poss = map (find_indices op = Ds) Ass;
@@ -642,7 +642,7 @@
kill_ns before_kill_src before_kill_dest bnfs accum;
val Ass' = map2 (map o nth) Ass live_poss;
- val As = sort Ass';
+ val As = flatten_tyargs Ass';
val after_lift_dest = replicate (length Ass') (0 upto (length As - 1));
val old_poss = map (map (fn x => find_index (fn y => x = y) As)) Ass';
val new_poss = map2 (subtract op =) old_poss after_lift_dest;
@@ -657,7 +657,7 @@
fun default_comp_sort Ass =
Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
-fun raw_compose_bnf const_policy qualify sort outer inners oDs Dss tfreess accum =
+fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum =
let
val b = name_of_bnf outer;
@@ -665,7 +665,7 @@
val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
- normalize_bnfs qualify Ass Ds sort inners accum;
+ normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
val As = map TFree As;
@@ -675,12 +675,14 @@
(clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy')))
end;
-fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (accum as ((cache, _), _)) =
+fun compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess
+ (accum as ((cache, _), _)) =
let val key = key_of_compose oDs Dss tfreess outer inners in
(case Typtab.lookup cache key of
SOME bnf_Ds_As => (bnf_Ds_As, accum)
| NONE =>
- cache_comp key (raw_compose_bnf const_policy qualify sort outer inners oDs Dss tfreess accum))
+ cache_comp key
+ (raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum))
end;
(* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
@@ -730,35 +732,34 @@
val smart_max_inline_type_size = 5; (*FUDGE*)
-fun maybe_typedef (b, As, mx) set opt_morphs tac =
+fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac =
let
val repT = HOLogic.dest_setT (fastype_of set);
- val inline = Term.size_of_typ repT <= smart_max_inline_type_size;
+ val out_of_line = force_out_of_line orelse Term.size_of_typ repT > smart_max_inline_type_size;
in
- if inline then
+ if out_of_line then
+ typedef (b, As, mx) set opt_morphs tac
+ #>> (fn (T_name, ({Rep_name, Abs_name, ...},
+ {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) =>
+ (Type (T_name, map TFree As),
+ (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases)))
+ else
pair (repT,
(@{const_name id_bnf}, @{const_name id_bnf},
@{thm type_definition_id_bnf_UNIV},
@{thm type_definition.Abs_inverse[OF type_definition_id_bnf_UNIV]},
@{thm type_definition.Abs_inject[OF type_definition_id_bnf_UNIV]},
@{thm type_definition.Abs_cases[OF type_definition_id_bnf_UNIV]}))
- else
- typedef (b, As, mx) set opt_morphs tac
- #>> (fn (T_name, ({Rep_name, Abs_name, ...},
- {type_definition, Abs_inverse, Abs_inject, Abs_cases, ...}) : Typedef.info) =>
- (Type (T_name, map TFree As),
- (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, Abs_cases)))
end;
-fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
+fun seal_bnf qualify (unfold_set : unfold_set) b has_live_phantoms Ds bnf lthy =
let
val live = live_of_bnf bnf;
val nwits = nwits_of_bnf bnf;
- val (As, lthy1) = apfst (map TFree)
+ val ((As, As'), lthy1) = apfst (`(map TFree))
(Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
- val (Bs, _) = apfst (map TFree)
- (Variable.invent_types (replicate live @{sort type}) lthy1);
+ val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live @{sort type}) lthy1);
val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
|> mk_Frees' "f" (map2 (curry op -->) As Bs)
@@ -766,10 +767,10 @@
val repTA = mk_T_of_bnf Ds As bnf;
val T_bind = qualify b;
- val TA_params = Term.add_tfreesT repTA [];
+ val TA_params = Term.add_tfreesT repTA (if has_live_phantoms then As' else []);
val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) =
- maybe_typedef (T_bind, TA_params, NoSyn)
- (HOLogic.mk_UNIV repTA) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
+ maybe_typedef has_live_phantoms (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE
+ (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val repTB = mk_T_of_bnf Ds Bs bnf;
val TB = Term.typ_subst_atomic (As ~~ Bs) TA;
@@ -798,7 +799,7 @@
val all_deads = map TFree (fold Term.add_tfreesT Ds []);
val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) =
- maybe_typedef (bdT_bind, params, NoSyn)
+ maybe_typedef false (bdT_bind, params, NoSyn)
(HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) =
@@ -836,9 +837,11 @@
rtac (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1;
fun rel_OO_Grp_tac ctxt =
(rtac (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN'
- SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
- type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
- type_definition RS @{thm vimage2p_relcompp_converse}]) THEN' rtac refl) 1;
+ subst_tac ctxt NONE [type_definition RS @{thm vimage2p_relcompp_converse}] THEN'
+ SELECT_GOAL (unfold_thms_tac ctxt [o_apply,
+ type_definition RS @{thm type_copy_vimage2p_Grp_Rep},
+ type_definition RS @{thm vimage2p_relcompp_converse}]) THEN'
+ rtac refl) 1;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac
(map set_map0_tac (set_map0_of_bnf bnf)) (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1))
@@ -888,7 +891,8 @@
fun bnf_of_typ _ _ _ _ Ds0 (T as TFree T') accum =
(if member (op =) Ds0 T' then (DEADID_bnf, ([T], [])) else (ID_bnf, ([], [T])), accum)
| bnf_of_typ _ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
- | bnf_of_typ const_policy qualify' sort Xs Ds0 (T as Type (C, Ts)) (accum as (_, lthy)) =
+ | bnf_of_typ const_policy qualify' flatten_tyargs Xs Ds0 (T as Type (C, Ts))
+ (accum as (_, lthy)) =
let
fun check_bad_dead ((_, (deads, _)), _) =
let val Ds = fold Term.add_tfreesT deads [] in
@@ -926,10 +930,10 @@
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
val ((inners, (Dss, Ass)), (accum', lthy')) =
apfst (apsnd split_list o split_list)
- (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort Xs Ds0)
+ (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
(if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
in
- compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (accum', lthy')
+ compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
end)
|> tap check_bad_dead
end;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Sep 13 18:08:38 2014 +0200
@@ -1273,11 +1273,6 @@
val fp_eqs =
map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_repTs;
- val rhsXs_As' = fold (fold (fold Term.add_tfreesT)) ctrXs_Tsss [];
- val _ = (case subtract (op =) rhsXs_As' As' of [] => ()
- | extras => List.app (fn extra => warning ("Unused type variable on right-hand side of " ^
- co_prefix fp ^ "datatype definition: " ^ qsoty (TFree extra))) extras);
-
val killed_As =
map_filter (fn (A, set_bos) => if exists is_none set_bos then SOME A else NONE)
(unsorted_As ~~ transpose set_boss);
@@ -1710,32 +1705,35 @@
val selBss = map (map (mk_disc_or_sel Bs)) selss;
val n = length discAs;
- fun mk_rhs n k discA selAs discB selBs =
+ fun mk_conjunct n k discA selAs discB selBs =
(if k = n then [] else [HOLogic.mk_eq (discA $ ta, discB $ tb)]) @
- (case (selAs, selBs) of
- ([], []) => []
- | (_ :: _, _ :: _) => [Library.foldr HOLogic.mk_imp
- (if n = 1 then [] else [discA $ ta, discB $ tb],
- Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs [])
- (map (rapp ta) selAs) (map (rapp tb) selBs)))]);
+ (if null selAs then
+ []
+ else
+ [Library.foldr HOLogic.mk_imp
+ (if n = 1 then [] else [discA $ ta, discB $ tb],
+ Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app names_lthy Rs [])
+ (map (rapp ta) selAs) (map (rapp tb) selBs)))]);
- val goals = if n = 0 then []
- else [mk_Trueprop_eq
- (build_rel_app names_lthy Rs [] ta tb,
- Library.foldr1 HOLogic.mk_conj
- (flat (map5 (mk_rhs n) (1 upto n) discAs selAss discBs selBss)))];
- in
- if null goals then
- []
- else
- Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+ val goals =
+ if n = 0 then
+ []
+ else
+ [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
+ (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
+ [] => @{term True}
+ | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))];
+
+ fun prove goal =
+ Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
(flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
rel_distinct_thms live_nesting_rel_eqs)
- |> Conjunction.elim_balanced (length goals)
- |> Proof_Context.export names_lthy lthy
- |> map Thm.close_derivation
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
+ in
+ map prove goals
end;
val (rel_cases_thm, rel_cases_attrs) =
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Sat Sep 13 18:08:38 2014 +0200
@@ -572,11 +572,11 @@
let
val time = time lthy;
val timer = time (Timer.startRealTimer ());
+
+ val nn = length fp_eqs;
val (Xs, rhsXs) = split_list fp_eqs;
- (* FIXME: because of "@ Xs", the output could contain type variables that are not in the
- input; also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
- fun fp_sort Ass =
+ fun flatten_tyargs Ass =
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
fun raw_qualify base_b =
@@ -589,20 +589,23 @@
val ((bnfs, (deadss, livess)), accum) =
apfst (apsnd split_list o split_list)
- (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs Ds0) bs rhsXs
+ (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
((empty_comp_cache, empty_unfolds), lthy));
fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
#> Binding.conceal;
val Ass = map (map dest_TFree) livess;
- val resDs = fold (subtract (op =)) Ass resBs;
- val Ds = fold (fold Term.add_tfreesT) deadss Ds0;
+ val Ds' = fold (fold Term.add_tfreesT) deadss [];
+ val Ds = union (op =) Ds' Ds0;
+ val missing = resBs |> fold (subtract (op =)) (Ds' :: Ass);
+ val (dead_phantoms, live_phantoms) = List.partition (member (op =) Ds0) missing;
+ val resBs' = resBs |> fold (subtract (op =)) [dead_phantoms, Ds];
val timer = time (timer "Construction of BNFs");
val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
- normalize_bnfs norm_qualify Ass Ds fp_sort bnfs accum;
+ normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
val Dss = map3 (append oo map o nth) livess kill_poss deadss;
@@ -610,14 +613,14 @@
#> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
- fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
- bs Dss bnfs' lthy'
+ fold_map4 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
+ bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy'
|>> split_list
|>> apsnd split_list;
val timer = time (timer "Normalization & sealing of BNFs");
- val res = construct_fp bs resBs (map TFree resDs, deadss) pre_bnfs absT_infos lthy'';
+ val res = construct_fp bs resBs (map TFree dead_phantoms, deadss) pre_bnfs absT_infos lthy'';
val timer = time (timer "FP construction in total");
in
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Sat Sep 13 18:08:38 2014 +0200
@@ -250,9 +250,9 @@
end;
val ((alg_free, (_, alg_def_free)), (lthy, lthy_old)) =
- lthy
- |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
- ||> `Local_Theory.restore;
+ lthy
+ |> Local_Theory.define ((alg_bind, NoSyn), (alg_def_bind, alg_spec))
+ ||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
val alg = fst (Term.dest_Const (Morphism.term phi alg_free));
--- a/src/HOL/Tools/BNF/bnf_tactics.ML Fri Sep 12 17:51:31 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_tactics.ML Sat Sep 13 18:08:38 2014 +0200
@@ -11,6 +11,7 @@
include CTR_SUGAR_GENERAL_TACTICS
val fo_rtac: thm -> Proof.context -> int -> tactic
+ val subst_tac: Proof.context -> int list option -> thm list -> int -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
int -> tactic
@@ -41,6 +42,9 @@
end
handle Pattern.MATCH => no_tac);
+(*unlike "unfold_thms_tac", it succeed when the RHS contains schematic variables not in the LHS*)
+fun subst_tac ctxt = EqSubst.eqsubst_tac ctxt o the_default [0];
+
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
fun mk_pointfree ctxt thm = thm
|> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq