# HG changeset patch # User blanchet # Date 1410624518 -7200 # Node ID be0f5d8d511bd043e9a5544bdbe3892e699e91a7 # Parent 054e9a9fccadc977556a394949bbbfb06f569287 imported patch phantoms diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Datatype_Examples/Misc_Codatatype.thy --- 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 \ 'b" codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ '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" diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Datatype_Examples/Misc_Datatype.thy --- 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 \ 'c + 'a" datatype (discs_sels) 'a deadfoo = DeadFoo "'a \ '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 \ 't) + 't" | Bar (bar: 'id) diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_comp.ML --- 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; diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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) = diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_fp_util.ML --- 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 diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_lfp.ML --- 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)); diff -r 054e9a9fccad -r be0f5d8d511b src/HOL/Tools/BNF/bnf_tactics.ML --- 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