diff --git a/src/HOL/Tools/BNF/bnf_comp.ML b/src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML +++ b/src/HOL/Tools/BNF/bnf_comp.ML @@ -1,1043 +1,1038 @@ (* Title: HOL/Tools/BNF/bnf_comp.ML Author: Dmitriy Traytel, TU Muenchen Author: Jasmin Blanchette, TU Muenchen Copyright 2012 Composition of bounded natural functors. *) signature BNF_COMP = sig val typedef_threshold: int Config.T val with_typedef_threshold: int -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context val with_typedef_threshold_yield: int -> (Proof.context -> 'a * Proof.context) -> Proof.context -> 'a * Proof.context val ID_bnf: BNF_Def.bnf val DEADID_bnf: BNF_Def.bnf type comp_cache type unfold_set = {map_unfolds: thm list, set_unfoldss: thm list list, rel_unfolds: thm list, pred_unfolds: thm list} val empty_comp_cache: comp_cache val empty_unfolds: unfold_set exception BAD_DEAD of typ * typ val bnf_of_typ: bool -> BNF_Def.inline_policy -> (binding -> binding) -> ((string * sort) list list -> (string * sort) list) -> (string * sort) list -> (string * sort) list -> typ -> (comp_cache * unfold_set) * local_theory -> (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory) val default_comp_sort: (string * sort) list list -> (string * sort) list val clean_compose_bnf: BNF_Def.inline_policy -> (binding -> binding) -> binding -> BNF_Def.bnf -> BNF_Def.bnf list -> unfold_set * local_theory -> BNF_Def.bnf * (unfold_set * local_theory) val kill_bnf: (binding -> binding) -> int -> BNF_Def.bnf -> (comp_cache * unfold_set) * local_theory -> BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) val lift_bnf: (binding -> binding) -> int -> BNF_Def.bnf -> (comp_cache * unfold_set) * local_theory -> BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) val permute_bnf: (binding -> binding) -> int list -> int list -> BNF_Def.bnf -> (comp_cache * unfold_set) * local_theory -> BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) val permute_and_kill_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf -> (comp_cache * unfold_set) * local_theory -> BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) val lift_and_permute_bnf: (binding -> binding) -> int -> int list -> int list -> BNF_Def.bnf -> (comp_cache * unfold_set) * local_theory -> BNF_Def.bnf * ((comp_cache * unfold_set) * local_theory) val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list -> (''a list list -> ''a list) -> BNF_Def.bnf list -> (comp_cache * unfold_set) * local_theory -> (int list list * ''a list) * (BNF_Def.bnf list * ((comp_cache * unfold_set) * local_theory)) val compose_bnf: BNF_Def.inline_policy -> (int -> binding -> binding) -> ((string * sort) list list -> (string * sort) list) -> BNF_Def.bnf -> BNF_Def.bnf list -> typ list -> typ list list -> typ list list -> (comp_cache * unfold_set) * local_theory -> (BNF_Def.bnf * (typ list * typ list)) * ((comp_cache * unfold_set) * local_theory) type absT_info = {absT: typ, repT: typ, abs: term, rep: term, abs_inject: thm, abs_inverse: thm, type_definition: thm} val morph_absT_info: morphism -> absT_info -> absT_info val mk_absT: theory -> typ -> typ -> typ -> typ 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 -> bool -> typ list -> typ list -> BNF_Def.bnf -> local_theory -> (BNF_Def.bnf * (typ list * absT_info)) * local_theory end; structure BNF_Comp : BNF_COMP = struct open BNF_Def open BNF_Util open BNF_Tactics open BNF_Comp_Tactics val typedef_threshold = Attrib.setup_config_int \<^binding>\bnf_typedef_threshold\ (K 6); fun with_typedef_threshold threshold f lthy = lthy |> Config.put typedef_threshold threshold |> f |> Config.put typedef_threshold (Config.get lthy typedef_threshold); fun with_typedef_threshold_yield threshold f lthy = lthy |> Config.put typedef_threshold threshold |> f ||> Config.put typedef_threshold (Config.get lthy typedef_threshold); val ID_bnf = the (bnf_of \<^context> "BNF_Composition.ID"); val DEADID_bnf = the (bnf_of \<^context> "BNF_Composition.DEADID"); type comp_cache = (bnf * (typ list * typ list)) Typtab.table; fun key_of_types s Ts = Type (s, Ts); fun key_of_typess s = key_of_types s o map (key_of_types ""); fun typ_of_int n = Type (string_of_int n, []); fun typ_of_bnf bnf = key_of_typess "" [[T_of_bnf bnf], lives_of_bnf bnf, sort Term_Ord.typ_ord (deads_of_bnf bnf)]; fun key_of_kill n bnf = key_of_types "k" [typ_of_int n, typ_of_bnf bnf]; fun key_of_lift n bnf = key_of_types "l" [typ_of_int n, typ_of_bnf bnf]; fun key_of_permute src dest bnf = key_of_types "p" (map typ_of_int src @ map typ_of_int dest @ [typ_of_bnf bnf]); fun key_of_compose oDs Dss Ass outer inners = key_of_types "c" (map (key_of_typess "") [[oDs], Dss, Ass, [map typ_of_bnf (outer :: inners)]]); fun cache_comp_simple key cache (bnf, (unfold_set, lthy)) = (bnf, ((Typtab.update (key, (bnf, ([], []))) cache, unfold_set), lthy)); fun cache_comp key (bnf_Ds_As, ((cache, unfold_set), lthy)) = (bnf_Ds_As, ((Typtab.update (key, bnf_Ds_As) cache, unfold_set), lthy)); type unfold_set = { map_unfolds: thm list, set_unfoldss: thm list list, rel_unfolds: thm list, pred_unfolds: thm list }; val empty_comp_cache = Typtab.empty; val empty_unfolds = {map_unfolds = [], set_unfoldss = [], rel_unfolds = [], pred_unfolds = []}; fun add_to_thms thms new = thms |> not (Thm.is_reflexive new) ? insert Thm.eq_thm new; fun adds_to_thms thms news = insert (eq_set Thm.eq_thm) (no_reflexive news) thms; fun add_to_unfolds map sets rel pred {map_unfolds, set_unfoldss, rel_unfolds, pred_unfolds} = {map_unfolds = add_to_thms map_unfolds map, set_unfoldss = adds_to_thms set_unfoldss sets, rel_unfolds = add_to_thms rel_unfolds rel, pred_unfolds = add_to_thms pred_unfolds pred}; fun add_bnf_to_unfolds bnf = add_to_unfolds (map_def_of_bnf bnf) (set_defs_of_bnf bnf) (rel_def_of_bnf bnf) (pred_def_of_bnf bnf); val bdTN = "bdT"; fun mk_killN n = "_kill" ^ string_of_int n; fun mk_liftN n = "_lift" ^ string_of_int n; fun mk_permuteN src dest = "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest); -(*copied from Envir.expand_term_free*) -fun expand_term_const defs = - let - val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs; - val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE; - in Envir.expand_term get end; - val id_bnf_def = @{thm id_bnf_def}; -val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals]; +val expand_id_bnf_def = + Envir.expand_term_defs dest_Const + [Thm.prop_of id_bnf_def |> Logic.dest_equals |> apfst dest_Const]; fun is_sum_prod_natLeq (Const (\<^const_name>\csum\, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] | is_sum_prod_natLeq (Const (\<^const_name>\cprod\, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] | is_sum_prod_natLeq t = t aconv \<^term>\natLeq\; fun clean_compose_bnf const_policy qualify b outer inners (unfold_set, lthy) = let val olive = live_of_bnf outer; val onwits = nwits_of_bnf outer; val odeads = deads_of_bnf outer; val inner = hd inners; val ilive = live_of_bnf inner; val ideadss = map deads_of_bnf inners; val inwitss = map nwits_of_bnf inners; (* TODO: check olive = length inners > 0, forall inner from inners. ilive = live, forall inner from inners. idead = dead *) val (oDs, lthy1) = apfst (map TFree) (Variable.invent_types (map Type.sort_of_atyp odeads) lthy); val (Dss, lthy2) = apfst (map (map TFree)) (fold_map Variable.invent_types (map (map Type.sort_of_atyp) ideadss) lthy1); val (Ass, lthy3) = apfst (replicate ilive o map TFree) (Variable.invent_types (replicate ilive \<^sort>\type\) lthy2); val As = if ilive > 0 then hd Ass else []; val Ass_repl = replicate olive As; val (Bs, names_lthy) = apfst (map TFree) (Variable.invent_types (replicate ilive \<^sort>\type\) lthy3); val Bss_repl = replicate olive Bs; val (((((fs', Qs'), Ps'), Asets), xs), _) = names_lthy |> apfst snd o mk_Frees' "f" (map2 (curry op -->) As Bs) ||>> apfst snd o mk_Frees' "Q" (map2 mk_pred2T As Bs) ||>> apfst snd o mk_Frees' "P" (map mk_pred1T As) ||>> mk_Frees "A" (map HOLogic.mk_setT As) ||>> mk_Frees "x" As; val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners; val CCA = mk_T_of_bnf oDs CAs outer; val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners; val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer; val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners; val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners; val outer_bd = mk_bd_of_bnf oDs CAs outer; (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*) val mapx = fold_rev Term.abs fs' (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer, map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o mk_map_of_bnf Ds As Bs) Dss inners)); (*%Q1 ... Qn. outer.rel (inner_1.rel Q1 ... Qn) ... (inner_m.rel Q1 ... Qn)*) val rel = fold_rev Term.abs Qs' (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer, map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o mk_rel_of_bnf Ds As Bs) Dss inners)); (*%P1 ... Pn. outer.pred (inner_1.pred P1 ... Pn) ... (inner_m.pred P1 ... Pn)*) val pred = fold_rev Term.abs Ps' (Term.list_comb (mk_pred_of_bnf oDs CAs outer, map2 (fn Ds => (fn f => Term.list_comb (f, map Bound (ilive - 1 downto 0))) o mk_pred_of_bnf Ds As) Dss inners)); (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*) (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*) fun mk_set i = let val (setTs, T) = `(replicate olive o HOLogic.mk_setT) (nth As i); val outer_set = mk_collect (mk_sets_of_bnf (replicate olive oDs) (replicate olive setTs) outer) (mk_T_of_bnf oDs setTs outer --> HOLogic.mk_setT T); val inner_sets = map (fn sets => nth sets i) inner_setss; val outer_map = mk_map_of_bnf oDs CAs setTs outer; val map_inner_sets = Term.list_comb (outer_map, inner_sets); val collect_image = mk_collect (map2 (fn f => fn set => HOLogic.mk_comp (mk_image f, set)) inner_sets outer_sets) (CCA --> HOLogic.mk_setT T); in (Library.foldl1 HOLogic.mk_comp [mk_Union T, outer_set, map_inner_sets], HOLogic.mk_comp (mk_Union T, collect_image)) end; val (sets, sets_alt) = map_split mk_set (0 upto ilive - 1); fun mk_simplified_set set = let val setT = fastype_of set; val var_set' = Const (\<^const_name>\id_bnf\, setT --> setT) $ Var ((Name.uu, 0), setT); val goal = mk_Trueprop_eq (var_set', set); fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer); val set'_eq_set = Goal.prove (*no sorry*) names_lthy [] [] goal tac |> Thm.close_derivation \<^here>; val set' = fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of set'_eq_set))); in (set', set'_eq_set) end; val (sets', set'_eq_sets) = map_split mk_simplified_set sets ||> Proof_Context.export names_lthy lthy; (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*) val bd = mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd; val (bd', bd_ordIso_natLeq_thm_opt) = if is_sum_prod_natLeq bd then let val bd' = \<^term>\natLeq\; val bd_bd' = HOLogic.mk_prod (bd, bd'); val ordIso = Const (\<^const_name>\ordIso\, HOLogic.mk_setT (fastype_of bd_bd')); val goal = mk_Trueprop_mem (bd_bd', ordIso); in (bd', SOME (Goal.prove_sorry lthy [] [] goal (bd_ordIso_natLeq_tac o #context) |> Thm.close_derivation \<^here>)) end else (bd, NONE); fun map_id0_tac ctxt = mk_comp_map_id0_tac ctxt (map_id0_of_bnf outer) (map_cong0_of_bnf outer) (map map_id0_of_bnf inners); fun map_comp0_tac ctxt = mk_comp_map_comp0_tac ctxt (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) (map map_comp0_of_bnf inners); fun mk_single_set_map0_tac i ctxt = mk_comp_set_map0_tac ctxt (nth set'_eq_sets i) (map_comp0_of_bnf outer) (map_cong0_of_bnf outer) (collect_set_map_of_bnf outer) (map ((fn thms => nth thms i) o set_map0_of_bnf) inners); val set_map0_tacs = map mk_single_set_map0_tac (0 upto ilive - 1); fun bd_card_order_tac ctxt = mk_comp_bd_card_order_tac ctxt (map bd_card_order_of_bnf inners) (bd_card_order_of_bnf outer); fun bd_cinfinite_tac ctxt = mk_comp_bd_cinfinite_tac ctxt (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer); val set_alt_thms = if Config.get lthy quick_and_dirty then [] else map (fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_comp_set_alt_tac ctxt (collect_set_map_of_bnf outer)) |> Thm.close_derivation \<^here>) (map2 (curry mk_Trueprop_eq) sets sets_alt); fun map_cong0_tac ctxt = mk_comp_map_cong0_tac ctxt set'_eq_sets set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners); val set_bd_tacs = if Config.get lthy quick_and_dirty then replicate ilive (K all_tac) else let val outer_set_bds = set_bd_of_bnf outer; val inner_set_bdss = map set_bd_of_bnf inners; val inner_bd_Card_orders = map bd_Card_order_of_bnf inners; fun single_set_bd_thm i j = @{thm comp_single_set_bd} OF [nth inner_bd_Card_orders j, nth (nth inner_set_bdss j) i, nth outer_set_bds j] val single_set_bd_thmss = map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1); in @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt => mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds) set'_eq_sets set_alt_thms single_set_bd_thmss end; val in_alt_thm = let val inx = mk_in Asets sets CCA; val in_alt = mk_in (map2 (mk_in Asets) inner_setss CAs) outer_sets CCA; val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_comp_in_alt_tac ctxt set_alt_thms) |> Thm.close_derivation \<^here> end; fun le_rel_OO_tac ctxt = mk_le_rel_OO_tac ctxt (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer) (map le_rel_OO_of_bnf inners); fun rel_OO_Grp_tac ctxt = let val outer_rel_Grp = rel_Grp_of_bnf outer RS sym; val thm = trans OF [in_alt_thm RS @{thm OO_Grp_cong}, trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]}, rel_conversep_of_bnf outer RS sym], outer_rel_Grp], trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym; in unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1 end; fun pred_set_tac ctxt = let val pred_alt = unfold_thms ctxt @{thms Ball_Collect} (trans OF [pred_cong0_of_bnf outer OF map pred_set_of_bnf inners, pred_set_of_bnf outer]); val in_alt = in_alt_thm RS @{thm Collect_inj} RS sym; in unfold_thms_tac ctxt (@{thm Ball_Collect} :: set'_eq_sets) THEN HEADGOAL (rtac ctxt (trans OF [pred_alt, in_alt])) end val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer; val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I))) (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As)) Dss inwitss inners); val inner_witsss = map (map (nth inner_witss) o fst) outer_wits; val wits = (inner_witsss, (map (single o snd) outer_wits)) |-> map2 (fold (map_product (fn iwit => fn owit => owit $ iwit))) |> flat |> map (`(fn t => Term.add_frees t [])) |> minimize_wits |> map (fn (frees, t) => fold absfree frees t); fun wit_tac ctxt = mk_comp_wit_tac ctxt set'_eq_sets (wit_thms_of_bnf outer) (collect_set_map_of_bnf outer) (maps wit_thms_of_bnf inners); val (bnf', lthy') = bnf_def const_policy (K Dont_Note) true qualify tacs wit_tac (SOME (oDs @ flat Dss)) Binding.empty Binding.empty Binding.empty [] (((((((b, CCA), mapx), sets'), bd'), wits), SOME rel), SOME pred) lthy; val phi = Morphism.thm_morphism "BNF" (unfold_thms lthy' [id_bnf_def]) $> Morphism.term_morphism "BNF" expand_id_bnf_def; val bnf'' = morph_bnf phi bnf'; in (bnf'', (add_bnf_to_unfolds bnf'' unfold_set, lthy')) end; (* Killing live variables *) fun raw_kill_bnf qualify n bnf (accum as (unfold_set, lthy)) = if n = 0 then (bnf, accum) else let val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf); val live = live_of_bnf bnf; val deads = deads_of_bnf bnf; val nwits = nwits_of_bnf bnf; (* TODO: check 0 < n <= live *) val (Ds, lthy1) = apfst (map TFree) (Variable.invent_types (map Type.sort_of_atyp deads) lthy); val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree) (Variable.invent_types (replicate live \<^sort>\type\) lthy1); val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree) (Variable.invent_types (replicate (live - n) \<^sort>\type\) lthy2); val ((Asets, lives), _(*names_lthy*)) = lthy |> mk_Frees "A" (map HOLogic.mk_setT (drop n As)) ||>> mk_Frees "x" (drop n As); val xs = map (fn T => Const (\<^const_name>\undefined\, T)) killedAs @ lives; val T = mk_T_of_bnf Ds As bnf; (*bnf.map id ... id*) val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs); (*bnf.rel (op =) ... (op =)*) val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map HOLogic.eq_const killedAs); (*bnf.pred (%_. True) ... (%_ True)*) val pred = Term.list_comb (mk_pred_of_bnf Ds As bnf, map (fn T => Term.absdummy T \<^term>\True\) killedAs); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = drop n bnf_sets; val bd = mk_bd_of_bnf Ds As bnf; fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; fun map_comp0_tac ctxt = unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1; fun map_cong0_tac ctxt = mk_kill_map_cong0_tac ctxt n (live - n) (map_cong0_of_bnf bnf); val set_map0_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_map0_of_bnf bnf)); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt thm 1) (drop n (set_bd_of_bnf bnf)); val in_alt_thm = let val inx = mk_in Asets sets T; val in_alt = mk_in (map HOLogic.mk_UNIV killedAs @ Asets) bnf_sets T; val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => kill_in_alt_tac ctxt) |> Thm.close_derivation \<^here> end; fun le_rel_OO_tac ctxt = EVERY' [rtac ctxt @{thm ord_le_eq_trans}, rtac ctxt (le_rel_OO_of_bnf bnf)] 1 THEN unfold_thms_tac ctxt @{thms eq_OO} THEN rtac ctxt refl 1; fun rel_OO_Grp_tac ctxt = let val rel_Grp = rel_Grp_of_bnf bnf RS sym val thm = (trans OF [in_alt_thm RS @{thm OO_Grp_cong}, trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]}, rel_conversep_of_bnf bnf RS sym], rel_Grp], trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym); in rtac ctxt thm 1 end; fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf; val wits = map (fn t => fold absfree (Term.add_frees t []) t) (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)) bnf_wits); fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME (Ds @ killedAs)) Binding.empty Binding.empty Binding.empty [] (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; fun kill_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) = let val key = key_of_kill n bnf in (case Typtab.lookup cache key of SOME (bnf, _) => (bnf, accum) | NONE => cache_comp_simple key cache (raw_kill_bnf qualify n bnf (unfold_set, lthy))) end; (* Adding dummy live variables *) fun raw_lift_bnf qualify n bnf (accum as (unfold_set, lthy)) = if n = 0 then (bnf, accum) else let val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf); val live = live_of_bnf bnf; val deads = deads_of_bnf bnf; val nwits = nwits_of_bnf bnf; (* TODO: check 0 < n *) val (Ds, lthy1) = apfst (map TFree) (Variable.invent_types (map Type.sort_of_atyp deads) lthy); val ((newAs, As), lthy2) = apfst (chop n o map TFree) (Variable.invent_types (replicate (n + live) \<^sort>\type\) lthy1); val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree) (Variable.invent_types (replicate (n + live) \<^sort>\type\) lthy2); val (Asets, _(*names_lthy*)) = lthy |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As)); val T = mk_T_of_bnf Ds As bnf; (*%f1 ... fn. bnf.map*) val mapx = fold_rev Term.absdummy (map2 (curry op -->) newAs newBs) (mk_map_of_bnf Ds As Bs bnf); (*%Q1 ... Qn. bnf.rel*) val rel = fold_rev Term.absdummy (map2 mk_pred2T newAs newBs) (mk_rel_of_bnf Ds As Bs bnf); (*%P1 ... Pn. bnf.pred*) val pred = fold_rev Term.absdummy (map mk_pred1T newAs) (mk_pred_of_bnf Ds As bnf); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets; val bd = mk_bd_of_bnf Ds As bnf; fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; fun map_comp0_tac ctxt = unfold_thms_tac ctxt ((map_comp0_of_bnf bnf RS sym) :: @{thms comp_assoc id_comp comp_id}) THEN rtac ctxt refl 1; fun map_cong0_tac ctxt = rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); val set_map0_tacs = if Config.get lthy quick_and_dirty then replicate (n + live) (K all_tac) else replicate n empty_natural_tac @ map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = if Config.get lthy quick_and_dirty then replicate (n + live) (K all_tac) else replicate n (fn ctxt => mk_lift_set_bd_tac ctxt (bd_Card_order_of_bnf bnf)) @ (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); val in_alt_thm = let val inx = mk_in Asets sets T; val in_alt = mk_in (drop n Asets) bnf_sets T; val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => lift_in_alt_tac ctxt) |> Thm.close_derivation \<^here> end; fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty Binding.empty [] (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; fun lift_bnf qualify n bnf (accum as ((cache, unfold_set), lthy)) = let val key = key_of_lift n bnf in (case Typtab.lookup cache key of SOME (bnf, _) => (bnf, accum) | NONE => cache_comp_simple key cache (raw_lift_bnf qualify n bnf (unfold_set, lthy))) end; (* Changing the order of live variables *) fun raw_permute_bnf qualify src dest bnf (accum as (unfold_set, lthy)) = if src = dest then (bnf, accum) else let val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf) |> Binding.reset_pos; val live = live_of_bnf bnf; val deads = deads_of_bnf bnf; val nwits = nwits_of_bnf bnf; fun permute xs = permute_like_unique (op =) src dest xs; fun unpermute xs = permute_like_unique (op =) dest src xs; val (Ds, lthy1) = apfst (map TFree) (Variable.invent_types (map Type.sort_of_atyp deads) lthy); val (As, lthy2) = apfst (map TFree) (Variable.invent_types (replicate live \<^sort>\type\) lthy1); val (Bs, _(*lthy3*)) = apfst (map TFree) (Variable.invent_types (replicate live \<^sort>\type\) lthy2); val (Asets, _(*names_lthy*)) = lthy |> mk_Frees "A" (map HOLogic.mk_setT (permute As)); val T = mk_T_of_bnf Ds As bnf; (*%f(1) ... f(n). bnf.map f\(1) ... f\(n)*) val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs)) (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); (*%Q(1) ... Q(n). bnf.rel Q\(1) ... Q\(n)*) val rel = fold_rev Term.absdummy (permute (map2 mk_pred2T As Bs)) (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, unpermute (map Bound (live - 1 downto 0)))); (*%P(1) ... P(n). bnf.pred P\(1) ... P\(n)*) val pred = fold_rev Term.absdummy (permute (map mk_pred1T As)) (Term.list_comb (mk_pred_of_bnf Ds As bnf, unpermute (map Bound (live - 1 downto 0)))); val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf; val sets = permute bnf_sets; val bd = mk_bd_of_bnf Ds As bnf; fun map_id0_tac ctxt = rtac ctxt (map_id0_of_bnf bnf) 1; fun map_comp0_tac ctxt = rtac ctxt (map_comp0_of_bnf bnf) 1; fun map_cong0_tac ctxt = rtac ctxt (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1); val set_map0_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_map0_of_bnf bnf)); fun bd_card_order_tac ctxt = rtac ctxt (bd_card_order_of_bnf bnf) 1; fun bd_cinfinite_tac ctxt = rtac ctxt (bd_cinfinite_of_bnf bnf) 1; val set_bd_tacs = permute (map (fn thm => fn ctxt => rtac ctxt thm 1) (set_bd_of_bnf bnf)); val in_alt_thm = let val inx = mk_in Asets sets T; val in_alt = mk_in (unpermute Asets) bnf_sets T; val goal = fold_rev Logic.all Asets (mk_Trueprop_eq (inx, in_alt)); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_permute_in_alt_tac ctxt src dest) |> Thm.close_derivation \<^here> end; fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf) 1; fun rel_OO_Grp_tac ctxt = mk_simple_rel_OO_Grp_tac ctxt (rel_OO_Grp_of_bnf bnf) in_alt_thm; fun pred_set_tac ctxt = mk_simple_pred_set_tac ctxt (pred_set_of_bnf bnf) in_alt_thm; val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); fun wit_tac ctxt = mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); val (bnf', lthy') = bnf_def Smart_Inline (K Dont_Note) true qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty Binding.empty [] (((((((b, T), mapx), sets), bd), wits), SOME rel), SOME pred) lthy; in (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy')) end; fun permute_bnf qualify src dest bnf (accum as ((cache, unfold_set), lthy)) = let val key = key_of_permute src dest bnf in (case Typtab.lookup cache key of SOME (bnf, _) => (bnf, accum) | NONE => cache_comp_simple key cache (raw_permute_bnf qualify src dest bnf (unfold_set, lthy))) end; (* Composition pipeline *) fun permute_and_kill_bnf qualify n src dest bnf = permute_bnf qualify src dest bnf #> uncurry (kill_bnf qualify n); fun lift_and_permute_bnf qualify n src dest bnf = lift_bnf qualify n bnf #> uncurry (permute_bnf qualify src dest); 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; val live_poss = map2 (subtract op =) kill_poss before_kill_src; val before_kill_dest = map2 append kill_poss live_poss; val kill_ns = map length kill_poss; val (inners', accum') = @{fold_map 5} (permute_and_kill_bnf o qualify) (if length bnfs = 1 then [0] else 1 upto length bnfs) kill_ns before_kill_src before_kill_dest bnfs accum; val Ass' = map2 (map o nth) Ass live_poss; 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; val after_lift_src = map2 append new_poss old_poss; val lift_ns = map (fn xs => length As - length xs) Ass'; in ((kill_poss, As), @{fold_map 5} (lift_and_permute_bnf o qualify) (if length bnfs = 1 then [0] else 1 upto length bnfs) lift_ns after_lift_src after_lift_dest inners' accum') end; fun default_comp_sort Ass = Library.sort (Term_Ord.typ_ord o apply2 TFree) (fold (fold (insert (op =))) Ass []); fun raw_compose_bnf const_policy qualify flatten_tyargs outer inners oDs Dss tfreess accum = let val b = name_of_bnf outer; val Ass = map (map Term.dest_TFree) tfreess; val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) []; val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) = normalize_bnfs qualify Ass Ds flatten_tyargs inners accum; val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss); val As = map TFree As; in apfst (rpair (Ds, As)) (apsnd (apfst (pair cache')) (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold_set', lthy'))) end; 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 flatten_tyargs outer inners oDs Dss tfreess accum)) end; (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *) type absT_info = {absT: typ, repT: typ, abs: term, rep: term, abs_inject: thm, abs_inverse: thm, type_definition: thm}; fun morph_absT_info phi {absT, repT, abs, rep, abs_inject, abs_inverse, type_definition} = {absT = Morphism.typ phi absT, repT = Morphism.typ phi repT, abs = Morphism.term phi abs, rep = Morphism.term phi rep, abs_inject = Morphism.thm phi abs_inject, abs_inverse = Morphism.thm phi abs_inverse, type_definition = Morphism.thm phi type_definition}; fun mk_absT thy repT absT repU = let val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (repT, repU) Vartab.empty) []; in Term.typ_subst_TVars rho absT end handle Type.TYPE_MATCH => raise Term.TYPE ("mk_absT", [repT, absT, repU], []); fun mk_repT absT repT absU = if absT = repT then absU else (case (absT, absU) of (Type (C, Ts), Type (C', Us)) => if C = C' then Term.typ_subst_atomic (Ts ~~ Us) repT else raise Term.TYPE ("mk_repT", [absT, repT, absU], []) | _ => raise Term.TYPE ("mk_repT", [absT, repT, absU], [])); fun mk_abs_or_rep _ absU (Const (\<^const_name>\id_bnf\, _)) = Const (\<^const_name>\id_bnf\, absU --> absU) | mk_abs_or_rep getT (Type (_, Us)) abs = let val Ts = snd (dest_Type (getT (fastype_of abs))) in Term.subst_atomic_types (Ts ~~ Us) abs end; val mk_abs = mk_abs_or_rep range_type; val mk_rep = mk_abs_or_rep domain_type; fun maybe_typedef force_out_of_line (b, As, mx) set opt_morphs tac lthy = let val threshold = Config.get lthy typedef_threshold; val repT = HOLogic.dest_setT (fastype_of set); val out_of_line = force_out_of_line orelse (threshold >= 0 andalso Term.size_of_typ repT >= threshold); in if out_of_line then typedef (b, As, mx) set opt_morphs tac lthy |>> (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 ((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]})), lthy) end; fun seal_bnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds bnf lthy = let val live = live_of_bnf bnf; val nwits = nwits_of_bnf bnf; val ((As, As'), lthy1) = apfst (`(map TFree)) (Variable.invent_types (replicate live \<^sort>\type\) (fold Variable.declare_typ all_Ds lthy)); val (Bs, _) = apfst (map TFree) (Variable.invent_types (replicate live \<^sort>\type\) lthy1); val ((((fs, fs'), (Rs, Rs')), (Ps, Ps')), _(*names_lthy*)) = lthy |> mk_Frees' "f" (map2 (curry op -->) As Bs) ||>> mk_Frees' "R" (map2 mk_pred2T As Bs) ||>> mk_Frees' "P" (map mk_pred1T As); val repTA = mk_T_of_bnf Ds As bnf; val T_bind = qualify b; val repTA_tfrees = Term.add_tfreesT repTA []; val all_TA_params_in_order = fold_rev Term.add_tfreesT all_Ds As'; val TA_params = (if force_out_of_line then all_TA_params_in_order else inter (op =) repTA_tfrees all_TA_params_in_order); val ((TA, (Rep_name, Abs_name, type_definition, Abs_inverse, Abs_inject, _)), lthy) = maybe_typedef force_out_of_line (T_bind, TA_params, NoSyn) (HOLogic.mk_UNIV repTA) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val repTB = mk_T_of_bnf Ds Bs bnf; val TB = Term.typ_subst_atomic (As ~~ Bs) TA; val RepA = Const (Rep_name, TA --> repTA); val RepB = Const (Rep_name, TB --> repTB); val AbsA = Const (Abs_name, repTA --> TA); val AbsB = Const (Abs_name, repTB --> TB); val Abs_inject' = Abs_inject OF @{thms UNIV_I UNIV_I}; val Abs_inverse' = Abs_inverse OF @{thms UNIV_I}; val absT_info = {absT = TA, repT = repTA, abs = AbsA, rep = RepA, abs_inject = Abs_inject', abs_inverse = Abs_inverse', type_definition = type_definition}; val bnf_map = fold_rev Term.absfree fs' (HOLogic.mk_comp (HOLogic.mk_comp (AbsB, Term.list_comb (mk_map_of_bnf Ds As Bs bnf, fs)), RepA)); val bnf_sets = map ((fn t => HOLogic.mk_comp (t, RepA))) (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf); val bnf_bd = mk_bd_of_bnf Ds As bnf; val bnf_rel = fold_rev Term.absfree Rs' (mk_vimage2p RepA RepB $ (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, Rs))); val bnf_pred = fold_rev Term.absfree Ps' (HOLogic.mk_comp (Term.list_comb (mk_pred_of_bnf Ds As bnf, Ps), RepA)); (*bd may depend only on dead type variables*) val bd_repT = fst (dest_relT (fastype_of bnf_bd)); val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b); val params = Term.add_tfreesT bd_repT []; val all_deads = map TFree (fold_rev Term.add_tfreesT all_Ds []); val ((bdT, (_, Abs_bd_name, _, _, Abs_bdT_inject, Abs_bdT_cases)), lthy) = maybe_typedef false (bdT_bind, params, NoSyn) (HOLogic.mk_UNIV bd_repT) NONE (fn ctxt => EVERY' [rtac ctxt exI, rtac ctxt UNIV_I] 1) lthy; val (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) = if bdT = bd_repT then (bnf_bd, bd_Card_order_of_bnf bnf RS @{thm ordIso_refl}, bd_card_order_of_bnf bnf, bd_cinfinite_of_bnf bnf) else let val bnf_bd' = mk_dir_image bnf_bd (Const (Abs_bd_name, bd_repT --> bdT)); val Abs_bdT_inj = mk_Abs_inj_thm Abs_bdT_inject; val Abs_bdT_bij = mk_Abs_bij_thm lthy Abs_bdT_inj Abs_bdT_cases; val bd_ordIso = @{thm dir_image} OF [Abs_bdT_inj, bd_Card_order_of_bnf bnf]; val bd_card_order = @{thm card_order_dir_image} OF [Abs_bdT_bij, bd_card_order_of_bnf bnf]; val bd_cinfinite = (@{thm Cinfinite_cong} OF [bd_ordIso, bd_Cinfinite_of_bnf bnf]) RS conjunct1; in (bnf_bd', bd_ordIso, bd_card_order, bd_cinfinite) end; fun map_id0_tac ctxt = rtac ctxt (@{thm type_copy_map_id0} OF [type_definition, map_id0_of_bnf bnf]) 1; fun map_comp0_tac ctxt = rtac ctxt (@{thm type_copy_map_comp0} OF [type_definition, map_comp0_of_bnf bnf]) 1; fun map_cong0_tac ctxt = EVERY' (rtac ctxt @{thm type_copy_map_cong0} :: rtac ctxt (map_cong0_of_bnf bnf) :: map (fn i => EVERY' [select_prem_tac ctxt live (dtac ctxt meta_spec) i, etac ctxt meta_mp, etac ctxt (o_apply RS equalityD2 RS set_mp)]) (1 upto live)) 1; fun set_map0_tac thm ctxt = rtac ctxt (@{thm type_copy_set_map0} OF [type_definition, thm]) 1; val set_bd_tacs = map (fn thm => fn ctxt => rtac ctxt (@{thm ordLeq_ordIso_trans} OF [thm, bd_ordIso] RS @{thm type_copy_set_bd}) 1) (set_bd_of_bnf bnf); fun le_rel_OO_tac ctxt = rtac ctxt (le_rel_OO_of_bnf bnf RS @{thm vimage2p_relcompp_mono}) 1; fun rel_OO_Grp_tac ctxt = (rtac ctxt (rel_OO_Grp_of_bnf bnf RS @{thm vimage2p_cong} RS trans) THEN' (if force_out_of_line then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt) [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 ctxt refl) 1; fun pred_set_tac ctxt = HEADGOAL (EVERY' [rtac ctxt (pred_set_of_bnf bnf RS @{thm arg_cong[of _ _ "\f. f \ _"]} RS trans), SELECT_GOAL (unfold_thms_tac ctxt (@{thms Ball_comp_iff conj_comp_iff})), rtac ctxt refl]); val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac (map set_map0_tac (set_map0_of_bnf bnf)) (fn ctxt => rtac ctxt bd_card_order 1) (fn ctxt => rtac ctxt bd_cinfinite 1) set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac pred_set_tac; val bnf_wits = map (fn (I, t) => fold Term.absdummy (map (nth As) I) (AbsA $ Term.list_comb (t, map Bound (0 upto length I - 1)))) (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf); fun wit_tac ctxt = ALLGOALS (dtac ctxt (type_definition RS @{thm type_copy_wit})) THEN mk_simple_wit_tac ctxt (wit_thms_of_bnf bnf); val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) true qualify tacs wit_tac (SOME all_deads) Binding.empty Binding.empty Binding.empty [] (((((((b, TA), bnf_map), bnf_sets), bnf_bd'), bnf_wits), SOME bnf_rel), SOME bnf_pred) lthy; val unfolds = @{thm id_bnf_apply} :: (#map_unfolds unfold_set @ flat (#set_unfoldss unfold_set) @ #rel_unfolds unfold_set @ #pred_unfolds unfold_set); val bnf'' = bnf' |> morph_bnf_defs (Morphism.thm_morphism "BNF" (unfold_thms lthy' unfolds)); val map_def = map_def_of_bnf bnf''; val set_defs = set_defs_of_bnf bnf''; val rel_def = rel_def_of_bnf bnf''; val bnf_b = qualify b; val def_qualify = Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b); fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b; val map_b = def_qualify (mk_prefix_binding mapN); val rel_b = def_qualify (mk_prefix_binding relN); val set_bs = if live = 1 then [def_qualify (mk_prefix_binding setN)] else map (def_qualify o mk_prefix_binding o mk_setN) (1 upto live); val notes = (map_b, map_def) :: (rel_b, rel_def) :: (set_bs ~~ set_defs) |> map (fn (b, def) => ((b, []), [([def], [])])) val (noted, lthy'') = lthy' |> Local_Theory.notes notes ||> (if repTA = TA then I else register_bnf_raw (fst (dest_Type TA)) bnf'') in ((morph_bnf (substitute_noted_thm noted) bnf'', (all_deads, absT_info)), lthy'') end; exception BAD_DEAD of typ * typ; 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 optim 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 (case Library.inter (op =) Ds Xs of [] => () | X :: _ => raise BAD_DEAD (TFree X, T)) end; val tfrees = subtract (op =) Ds0 (Term.add_tfreesT T []); val bnf_opt = if null tfrees then NONE else bnf_of lthy C; in (case bnf_opt of NONE => ((DEADID_bnf, ([T], [])), accum) | SOME bnf => if optim andalso forall (can Term.dest_TFree) Ts andalso length Ts = length tfrees then let val T' = T_of_bnf bnf; val deads = deads_of_bnf bnf; val lives = lives_of_bnf bnf; val tvars' = Term.add_tvarsT T' []; val Ds_As = apply2 (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees))) (deads, lives); in ((bnf, Ds_As), accum) end else let val name = Long_Name.base_name C; fun qualify i = let val namei = name ^ nonzero_string_of_int i; in qualify' o Binding.qualify true namei end; val odead = dead_of_bnf bnf; val olive = live_of_bnf bnf; val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead); val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf)); val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds |> filter (fn x => x >= 0); val oDs = map (nth Ts) oDs_pos; 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_map 2} (fn i => bnf_of_typ optim 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 flatten_tyargs bnf inners oDs Dss Ass (accum', lthy') end) |> tap check_bad_dead end; end; diff --git a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML @@ -1,292 +1,292 @@ (* Title: HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Author: Lukas Bulwahn, TU Muenchen Preprocessing definitions of predicates to introduction rules. *) signature PREDICATE_COMPILE_PRED = sig (* preprocesses an equation to a set of intro rules; defines new constants *) val preprocess : Predicate_Compile_Aux.options -> (string * thm list) -> theory -> ((string * thm list) list * theory) val flat_higher_order_arguments : ((string * thm list) list * theory) -> ((string * thm list) list * ((string * thm list) list * theory)) end; structure Predicate_Compile_Pred : PREDICATE_COMPILE_PRED = struct open Predicate_Compile_Aux fun is_compound ((Const (\<^const_name>\Not\, _)) $ _) = error "is_compound: Negation should not occur; preprocessing is defect" | is_compound ((Const (\<^const_name>\Ex\, _)) $ _) = true | is_compound ((Const (\<^const_name>\HOL.disj\, _)) $ _ $ _) = true | is_compound ((Const (\<^const_name>\HOL.conj\, _)) $ _ $ _) = error "is_compound: Conjunction should not occur; preprocessing is defect" | is_compound _ = false fun try_destruct_case thy names atom = (case find_split_thm thy (fst (strip_comb atom)) of NONE => NONE | SOME raw_split_thm => let val split_thm = prepare_split_thm (Proof_Context.init_global thy) raw_split_thm (* TODO: contextify things - this line is to unvarify the split_thm *) (*val ((_, [isplit_thm]), _) = Variable.import true [split_thm] (Proof_Context.init_global thy)*) val (assms, concl) = Logic.strip_horn (Thm.prop_of split_thm) val (_, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl) val atom' = case_betapply thy atom val subst = Pattern.match thy (split_t, atom') (Vartab.empty, Vartab.empty) val names' = Term.add_free_names atom' names fun mk_subst_rhs assm = let val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm)) val var_names = Name.variant_list names' (map fst vTs) val vars = map Free (var_names ~~ (map snd vTs)) val (prems', pre_res) = Logic.strip_horn (subst_bounds (rev vars, assm')) fun partition_prem_subst prem = (case HOLogic.dest_eq (HOLogic.dest_Trueprop prem) of (Free (x, T), r) => (NONE, SOME ((x, T), r)) | _ => (SOME prem, NONE)) fun partition f xs = let fun partition' acc1 acc2 [] = (rev acc1, rev acc2) | partition' acc1 acc2 (x :: xs) = let val (y, z) = f x val acc1' = (case y of NONE => acc1 | SOME y' => y' :: acc1) val acc2' = (case z of NONE => acc2 | SOME z' => z' :: acc2) in partition' acc1' acc2' xs end in partition' [] [] xs end val (prems'', subst) = partition partition_prem_subst prems' val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res) val pre_rhs = fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t - val rhs = Envir.expand_term_frees subst pre_rhs + val rhs = Envir.expand_term_defs dest_Free subst pre_rhs in (case try_destruct_case thy (var_names @ names') rhs of NONE => [(subst, rhs)] | SOME (_, srs) => map (fn (subst', rhs') => (subst @ subst', rhs')) srs) end in SOME (atom', maps mk_subst_rhs assms) end) fun flatten constname atom (defs, thy) = if is_compound atom then let val atom = Envir.beta_norm (Envir.eta_long [] atom) val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) ((Long_Name.base_name constname) ^ "_aux") val full_constname = Sign.full_bname thy constname val (params, args) = List.partition (is_predT o fastype_of) (map Free (Term.add_frees atom [])) val constT = map fastype_of (params @ args) ---> HOLogic.boolT val lhs = list_comb (Const (full_constname, constT), params @ args) val def = Logic.mk_equals (lhs, atom) val ([definition], thy') = thy |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] in (lhs, ((full_constname, [definition]) :: defs, thy')) end else (case (fst (strip_comb atom)) of (Const (\<^const_name>\If\, _)) => let val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} val atom' = Raw_Simplifier.rewrite_term thy (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom val _ = \<^assert> (not (atom = atom')) in flatten constname atom' (defs, thy) end | _ => (case try_destruct_case thy [] atom of NONE => (atom, (defs, thy)) | SOME (atom', srs) => let val frees = map Free (Term.add_frees atom' []) val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs)) ((Long_Name.base_name constname) ^ "_aux") val full_constname = Sign.full_bname thy constname val constT = map fastype_of frees ---> HOLogic.boolT val lhs = list_comb (Const (full_constname, constT), frees) fun mk_def (subst, rhs) = - Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs) + Logic.mk_equals (fold (Envir.expand_term_defs dest_Free) (map single subst) lhs, rhs) val new_defs = map mk_def srs val (definition, thy') = thy |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> fold_map Specification.axiom (* FIXME !?!?!?! *) (map_index (fn (i, t) => ((Binding.name (constname ^ "_def" ^ string_of_int i), []), t)) new_defs) in (lhs, ((full_constname, map Drule.export_without_context definition) :: defs, thy')) end)) fun flatten_intros constname intros thy = let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val ((_, intros), ctxt') = Variable.import true intros ctxt val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms) (flatten constname) (map Thm.prop_of intros) ([], thy) val ctxt'' = Proof_Context.transfer thy' ctxt' val intros'' = map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS (Skip_Proof.cheat_tac ctxt''))) intros' |> Variable.export ctxt'' ctxt in (intros'', (local_defs, thy')) end fun introrulify ctxt ths = let val ((_, ths'), ctxt') = Variable.import true ths ctxt fun introrulify' th = let val (lhs, rhs) = Logic.dest_equals (Thm.prop_of th) val frees = Term.add_free_names rhs [] val disjuncts = HOLogic.dest_disj rhs val nctxt = Name.make_context frees fun mk_introrule t = let val ((ps, t'), _) = focus_ex t nctxt val prems = map HOLogic.mk_Trueprop (HOLogic.dest_conj t') in (ps, Logic.list_implies (prems, HOLogic.mk_Trueprop lhs)) end val Var (x, _) = (the_single o snd o strip_comb o HOLogic.dest_Trueprop o fst o Logic.dest_implies o Thm.prop_of) @{thm exI} fun prove_introrule (index, (ps, introrule)) = let val tac = Simplifier.simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [th]) 1 THEN Inductive.select_disj_tac ctxt' (length disjuncts) (index + 1) 1 THEN (EVERY (map (fn y => resolve_tac ctxt' [infer_instantiate ctxt' [(x, Thm.cterm_of ctxt' (Free y))] @{thm exI}] 1) ps)) THEN REPEAT_DETERM (resolve_tac ctxt' @{thms conjI} 1 THEN assume_tac ctxt' 1) THEN TRY (assume_tac ctxt' 1) in Goal.prove ctxt' (map fst ps) [] introrule (fn _ => tac) end in map_index prove_introrule (map mk_introrule disjuncts) end in maps introrulify' ths' |> Variable.export ctxt' ctxt end fun rewrite ctxt = Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm Ball_def}, @{thm Bex_def}]) #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) #> Conv.fconv_rule (nnf_conv ctxt) #> Simplifier.simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm ex_disj_distrib}]) fun rewrite_intros ctxt = Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps [@{thm all_not_ex}]) #> Simplifier.full_simplify (put_simpset HOL_basic_ss ctxt addsimps (tl @{thms bool_simps}) addsimps @{thms nnf_simps}) #> split_conjuncts_in_assms ctxt fun print_specs options thy msg ths = if show_intermediate_results options then (tracing (msg); tracing (commas (map (Thm.string_of_thm_global thy) ths))) else () fun preprocess options (constname, specs) thy = (* case Predicate_Compile_Data.processed_specs thy constname of SOME specss => (specss, thy) | NONE =>*) let val ctxt = Proof_Context.init_global thy (* FIXME proper context!? *) val intros = if forall is_pred_equation specs then map (split_conjuncts_in_assms ctxt) (introrulify ctxt (map (rewrite ctxt) specs)) else if forall (is_intro constname) specs then map (rewrite_intros ctxt) specs else error ("unexpected specification for constant " ^ quote constname ^ ":\n" ^ commas (map (quote o Thm.string_of_thm_global thy) specs)) val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp} val intros = map (rewrite_rule ctxt [if_beta RS @{thm eq_reflection}]) intros val _ = print_specs options thy "normalized intros" intros (*val intros = maps (split_cases thy) intros*) val (intros', (local_defs, thy')) = flatten_intros constname intros thy val (intross, thy'') = fold_map (preprocess options) local_defs thy' val full_spec = (constname, intros') :: flat intross (*val thy''' = Predicate_Compile_Data.store_processed_specs (constname, full_spec) thy''*) in (full_spec, thy'') end; fun flat_higher_order_arguments (intross, thy) = let fun process constname atom (new_defs, thy) = let val (pred, args) = strip_comb atom fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = let val vars = map Var (Term.add_vars abs_arg []) val abs_arg' = Logic.unvarify_global abs_arg val frees = map Free (Term.add_frees abs_arg' []) val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) new_defs)) ((Long_Name.base_name constname) ^ "_hoaux") val full_constname = Sign.full_bname thy constname val constT = map fastype_of frees ---> (fastype_of abs_arg') val const = Const (full_constname, constT) val lhs = list_comb (const, frees) val def = Logic.mk_equals (lhs, abs_arg') val ([definition], thy') = thy |> Sign.add_consts [(Binding.name constname, constT, NoSyn)] |> Global_Theory.add_defs false [((Binding.name (Thm.def_name constname), def), [])] in (list_comb (Logic.varify_global const, vars), ((full_constname, [definition])::new_defs, thy')) end | replace_abs_arg arg (new_defs, thy) = if is_some (try HOLogic.dest_prodT (fastype_of arg)) then (case try HOLogic.dest_prod arg of SOME (t1, t2) => (new_defs, thy) |> process constname t1 ||>> process constname t2 |>> HOLogic.mk_prod | NONE => (warning ("Replacing higher order arguments " ^ "is not applied in an undestructable product type"); (arg, (new_defs, thy)))) else if (is_predT (fastype_of arg)) then process constname arg (new_defs, thy) else (arg, (new_defs, thy)) val (args', (new_defs', thy')) = fold_map replace_abs_arg (map Envir.beta_eta_contract args) (new_defs, thy) in (list_comb (pred, args'), (new_defs', thy')) end fun flat_intro intro (new_defs, thy) = let val constname = fst (dest_Const (fst (strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (Thm.prop_of intro)))))) val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (Thm.prop_of intro) (new_defs, thy) val th = Skip_Proof.make_thm thy intro_ts in (th, (new_defs, thy)) end fun fold_map_spec f [] s = ([], s) | fold_map_spec f ((c, ths) :: specs) s = let val (ths', s') = f ths s val (specs', s'') = fold_map_spec f specs s' in ((c, ths') :: specs', s'') end val (intross', (new_defs, thy')) = fold_map_spec (fold_map flat_intro) intross ([], thy) in (intross', (new_defs, thy')) end end diff --git a/src/Pure/Isar/local_defs.ML b/src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML +++ b/src/Pure/Isar/local_defs.ML @@ -1,270 +1,270 @@ (* Title: Pure/Isar/local_defs.ML Author: Makarius Local definitions. *) signature LOCAL_DEFS = sig val cert_def: Proof.context -> (string -> Position.T list) -> term -> (string * typ) * term val abs_def: term -> (string * typ) * term val expand: cterm list -> thm -> thm val def_export: Assumption.export val define: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context -> (term * (string * thm)) list * Proof.context val fixed_abbrev: (binding * mixfix) * term -> Proof.context -> (term * term) * Proof.context val export: Proof.context -> Proof.context -> thm -> (thm list * thm list) * thm val export_cterm: Proof.context -> Proof.context -> cterm -> (thm list * thm list) * cterm val contract: Proof.context -> thm list -> cterm -> thm -> thm val print_rules: Proof.context -> unit val defn_add: attribute val defn_del: attribute val meta_rewrite_conv: Proof.context -> conv val meta_rewrite_rule: Proof.context -> thm -> thm val abs_def_rule: Proof.context -> thm -> thm val unfold_abs_def: bool Config.T val unfold: Proof.context -> thm list -> thm -> thm val unfold_goals: Proof.context -> thm list -> thm -> thm val unfold_tac: Proof.context -> thm list -> tactic val unfold0: Proof.context -> thm list -> thm -> thm val unfold0_goals: Proof.context -> thm list -> thm -> thm val unfold0_tac: Proof.context -> thm list -> tactic val fold: Proof.context -> thm list -> thm -> thm val fold_tac: Proof.context -> thm list -> tactic val derived_def: Proof.context -> (string -> Position.T list) -> {conditional: bool} -> term -> ((string * typ) * term) * (Proof.context -> thm -> thm) end; structure Local_Defs: LOCAL_DEFS = struct (** primitive definitions **) (* prepare defs *) fun cert_def ctxt get_pos eq = let fun err msg = cat_error msg ("The error(s) above occurred in definition:\n" ^ quote (Syntax.string_of_term ctxt eq)); val ((lhs, _), args, eq') = eq |> Sign.no_vars ctxt |> Primitive_Defs.dest_def ctxt {check_head = Term.is_Free, check_free_lhs = not o Variable.is_fixed ctxt, check_free_rhs = if Variable.is_body ctxt then K true else Variable.is_fixed ctxt, check_tfree = K true} handle TERM (msg, _) => err msg | ERROR msg => err msg; val _ = Context_Position.reports ctxt (maps (fn Free (x, _) => Syntax_Phases.reports_of_scope (get_pos x) | _ => []) args); in (Term.dest_Free (Term.head_of lhs), eq') end; val abs_def = Primitive_Defs.abs_def #>> Term.dest_Free; fun mk_def ctxt args = let val (bs, rhss) = split_list args; val Ts = map Term.fastype_of rhss; val (xs, _) = ctxt |> Context_Position.set_visible false |> Proof_Context.add_fixes (map2 (fn b => fn T => (b, SOME T, NoSyn)) bs Ts); val lhss = ListPair.map Free (xs, Ts); in map Logic.mk_equals (lhss ~~ rhss) end; (* export defs *) val head_of_def = Term.dest_Free o Term.head_of o #1 o Logic.dest_equals o Term.strip_all_body; (* [x, x \ a] : B x ----------- B a *) fun expand defs = Drule.implies_intr_list defs #> Drule.generalize (Names.empty, Names.build (fold (Names.add_set o #1 o head_of_def o Thm.term_of) defs)) #> funpow (length defs) (fn th => Drule.reflexive_thm RS th); -val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of); +val expand_term = Envir.expand_term_defs dest_Free o map (abs_def o Thm.term_of); fun def_export _ defs = (expand defs, expand_term defs); (* define *) fun define defs ctxt = let val ((xs, mxs), specs) = defs |> split_list |>> split_list; val (bs, rhss) = specs |> split_list; val eqs = mk_def ctxt (xs ~~ rhss); val lhss = map (fst o Logic.dest_equals) eqs; in ctxt |> Proof_Context.add_fixes (map2 (fn x => fn mx => (x, NONE, mx)) xs mxs) |> #2 |> fold Variable.declare_term eqs |> Proof_Context.add_assms def_export (map2 (fn b => fn eq => (b, [(eq, [])])) bs eqs) |>> map2 (fn lhs => fn (name, [th]) => (lhs, (name, th))) lhss end; (* fixed_abbrev *) fun fixed_abbrev ((x, mx), rhs) ctxt = let val T = Term.fastype_of rhs; val ([x'], ctxt') = ctxt |> Variable.declare_term rhs |> Proof_Context.add_fixes [(x, SOME T, mx)]; val lhs = Free (x', T); val _ = cert_def ctxt' (K []) (Logic.mk_equals (lhs, rhs)); - fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]); + fun abbrev_export _ _ = (I, Envir.expand_term_defs dest_Free [((x', T), rhs)]); val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt'; in ((lhs, rhs), ctxt'') end; (* specific export -- result based on educated guessing *) (* [xs, xs \ as] : B xs -------------- B as *) fun export inner outer th = let val defs_asms = Assumption.local_assms_of inner outer |> filter_out (Drule.is_sort_constraint o Thm.term_of) |> map (Thm.assume #> (fn asm => (case try (head_of_def o Thm.prop_of) asm of NONE => (asm, false) | SOME x => let val t = Free x in (case try (Assumption.export_term inner outer) t of NONE => (asm, false) | SOME u => if t aconv u then (asm, false) else (Drule.abs_def (Variable.gen_all outer asm), true)) end))); in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end; (* [xs, xs \ as] : TERM b xs -------------- and -------------- TERM b as b xs \ b as *) fun export_cterm inner outer ct = export inner outer (Drule.mk_term ct) ||> Drule.dest_term; fun contract ctxt defs ct th = th COMP (Raw_Simplifier.rewrite ctxt true defs ct COMP_INCR Drule.equal_elim_rule2); (** defived definitions **) (* transformation via rewrite rules *) structure Rules = Generic_Data ( type T = thm list; val empty = []; val merge = Thm.merge_thms; ); fun print_rules ctxt = Pretty.writeln (Pretty.big_list "definitional rewrite rules:" (map (Thm.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt)))); val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm o Thm.trim_context); val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm); (* meta rewrite rules *) fun meta_rewrite_conv ctxt = Raw_Simplifier.rewrite_cterm (false, false, false) (K (K NONE)) (ctxt |> Raw_Simplifier.init_simpset (Rules.get (Context.Proof ctxt)) |> Raw_Simplifier.add_eqcong Drule.equals_cong); (*protect meta-level equality*) val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv; fun abs_def_rule ctxt = meta_rewrite_rule ctxt #> Drule.abs_def; (* unfold object-level rules *) val unfold_abs_def = Config.declare_bool ("unfold_abs_def", \<^here>) (K true); local fun gen_unfold rewrite ctxt rews = let val meta_rews = map (meta_rewrite_rule ctxt) rews in if Config.get ctxt unfold_abs_def then rewrite ctxt meta_rews #> rewrite ctxt (map (perhaps (try Drule.abs_def)) meta_rews) else rewrite ctxt meta_rews end; val no_unfold_abs_def = Config.put unfold_abs_def false; in val unfold = gen_unfold Raw_Simplifier.rewrite_rule; val unfold_goals = gen_unfold Raw_Simplifier.rewrite_goals_rule; val unfold_tac = PRIMITIVE oo unfold_goals; val unfold0 = unfold o no_unfold_abs_def; val unfold0_goals = unfold_goals o no_unfold_abs_def; val unfold0_tac = unfold_tac o no_unfold_abs_def; end (* fold object-level rules *) fun fold ctxt rews = Raw_Simplifier.fold_rule ctxt (map (meta_rewrite_rule ctxt) rews); fun fold_tac ctxt rews = Raw_Simplifier.fold_goals_tac ctxt (map (meta_rewrite_rule ctxt) rews); (* derived defs -- potentially within the object-logic *) fun derived_def ctxt get_pos {conditional} prop = let val ((c, T), rhs) = prop |> Thm.cterm_of ctxt |> meta_rewrite_conv ctxt |> (snd o Logic.dest_equals o Thm.prop_of) |> conditional ? Logic.strip_imp_concl |> (abs_def o #2 o cert_def ctxt get_pos); fun prove def_ctxt0 def = let val def_ctxt = Proof_Context.augment prop def_ctxt0; val def_thm = Goal.prove def_ctxt [] [] prop (fn {context = goal_ctxt, ...} => ALLGOALS (CONVERSION (meta_rewrite_conv goal_ctxt) THEN' rewrite_goal_tac goal_ctxt [def] THEN' resolve_tac goal_ctxt [Drule.reflexive_thm])) handle ERROR msg => cat_error msg "Failed to prove definitional specification"; in def_thm |> singleton (Proof_Context.export def_ctxt def_ctxt0) |> Drule.zero_var_indexes end; in (((c, T), rhs), prove) end; end; diff --git a/src/Pure/envir.ML b/src/Pure/envir.ML --- a/src/Pure/envir.ML +++ b/src/Pure/envir.ML @@ -1,424 +1,424 @@ (* Title: Pure/envir.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory Free-form environments. The type of a term variable / sort of a type variable is part of its name. The lookup function must apply type substitutions, since they may change the identity of a variable. *) signature ENVIR = sig type tenv = (typ * term) Vartab.table datatype env = Envir of {maxidx: int, tenv: tenv, tyenv: Type.tyenv} val maxidx_of: env -> int val term_env: env -> tenv val type_env: env -> Type.tyenv val is_empty: env -> bool val empty: int -> env val init: env val merge: env * env -> env val insert_sorts: env -> sort list -> sort list val genvars: string -> env * typ list -> env * term list val genvar: string -> env * typ -> env * term val lookup1: tenv -> indexname * typ -> term option val lookup: env -> indexname * typ -> term option val update: (indexname * typ) * term -> env -> env val above: env -> int -> bool val vupdate: (indexname * typ) * term -> env -> env val norm_type_same: Type.tyenv -> typ Same.operation val norm_types_same: Type.tyenv -> typ list Same.operation val norm_type: Type.tyenv -> typ -> typ val norm_term_same: env -> term Same.operation val norm_term: env -> term -> term val beta_norm: term -> term val head_norm: env -> term -> term val eta_long: typ list -> term -> term val eta_contract: term -> term val beta_eta_contract: term -> term val aeconv: term * term -> bool val body_type: env -> typ -> typ val binder_types: env -> typ -> typ list val strip_type: env -> typ -> typ list * typ val fastype: env -> typ list -> term -> typ val subst_type_same: Type.tyenv -> typ Same.operation val subst_term_types_same: Type.tyenv -> term Same.operation val subst_term_same: Type.tyenv * tenv -> term Same.operation val subst_type: Type.tyenv -> typ -> typ val subst_term_types: Type.tyenv -> term -> term val subst_term: Type.tyenv * tenv -> term -> term val expand_atom: typ -> typ * term -> term val expand_term: (term -> (typ * term) option) -> term -> term - val expand_term_frees: ((string * typ) * term) list -> term -> term + val expand_term_defs: (term -> string * typ) -> ((string * typ) * term) list -> term -> term end; structure Envir: ENVIR = struct (** datatype env **) (*Updating can destroy environment in 2 ways! (1) variables out of range (2) circular assignments *) type tenv = (typ * term) Vartab.table; datatype env = Envir of {maxidx: int, (*upper bound of maximum index of vars*) tenv: tenv, (*assignments to Vars*) tyenv: Type.tyenv}; (*assignments to TVars*) fun make_env (maxidx, tenv, tyenv) = Envir {maxidx = maxidx, tenv = tenv, tyenv = tyenv}; fun maxidx_of (Envir {maxidx, ...}) = maxidx; fun term_env (Envir {tenv, ...}) = tenv; fun type_env (Envir {tyenv, ...}) = tyenv; fun is_empty env = Vartab.is_empty (term_env env) andalso Vartab.is_empty (type_env env); (* build env *) fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty); val init = empty ~1; fun merge (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1}, Envir {maxidx = maxidx2, tenv = tenv2, tyenv = tyenv2}) = make_env (Int.max (maxidx1, maxidx2), Vartab.merge (op =) (tenv1, tenv2), Vartab.merge (op =) (tyenv1, tyenv2)); (*NB: type unification may invent new sorts*) (* FIXME tenv!? *) val insert_sorts = Vartab.fold (fn (_, (_, T)) => Sorts.insert_typ T) o type_env; (*Generate a list of distinct variables. Increments index to make them distinct from ALL present variables. *) fun genvars name (Envir {maxidx, tenv, tyenv}, Ts) : env * term list = let fun genvs (_, [] : typ list) : term list = [] | genvs (_, [T]) = [Var ((name, maxidx + 1), T)] | genvs (n, T :: Ts) = Var ((name ^ radixstring (26, "a" , n), maxidx + 1), T) :: genvs (n + 1, Ts); in (Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv}, genvs (0, Ts)) end; (*Generate a variable.*) fun genvar name (env, T) : env * term = let val (env', [v]) = genvars name (env, [T]) in (env', v) end; fun var_clash xi T T' = raise TYPE ("Variable has two distinct types", [], [Var (xi, T'), Var (xi, T)]); fun lookup_check check tenv (xi, T) = (case Vartab.lookup tenv xi of NONE => NONE | SOME (U, t) => if check (T, U) then SOME t else var_clash xi T U); (*When dealing with environments produced by matching instead of unification, there is no need to chase assigned TVars. In this case, we can simply ignore the type substitution and use = instead of eq_type.*) fun lookup1 tenv = lookup_check (op =) tenv; fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv; fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) = Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv}; (*Determine if the least index updated exceeds lim*) fun above (Envir {tenv, tyenv, ...}) lim = (case Vartab.min tenv of SOME ((_, i), _) => i > lim | NONE => true) andalso (case Vartab.min tyenv of SOME ((_, i), _) => i > lim | NONE => true); (*Update, checking Var-Var assignments: try to suppress higher indexes*) fun vupdate ((a, U), t) env = (case t of Var (nT as (name', T)) => if a = name' then env (*cycle!*) else if Term_Ord.indexname_ord (a, name') = LESS then (case lookup env nT of (*if already assigned, chase*) NONE => update (nT, Var (a, T)) env | SOME u => vupdate ((a, U), u) env) else update ((a, U), t) env | _ => update ((a, U), t) env); (** beta normalization wrt. environment **) (*Chases variables in env. Does not exploit sharing of variable bindings Does not check types, so could loop.*) local fun norm_type0 tyenv : typ Same.operation = let fun norm (Type (a, Ts)) = Type (a, Same.map norm Ts) | norm (TFree _) = raise Same.SAME | norm (TVar v) = (case Type.lookup tyenv v of SOME U => Same.commit norm U | NONE => raise Same.SAME); in norm end; fun norm_term1 tenv : term Same.operation = let fun norm (Var v) = (case lookup1 tenv v of SOME u => Same.commit norm u | NONE => raise Same.SAME) | norm (Abs (a, T, body)) = Abs (a, T, norm body) | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) | norm (f $ t) = ((case norm f of Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) | nf => nf $ Same.commit norm t) handle Same.SAME => f $ norm t) | norm _ = raise Same.SAME; in norm end; fun norm_term2 (envir as Envir {tyenv, ...}) : term Same.operation = let val normT = norm_type0 tyenv; fun norm (Const (a, T)) = Const (a, normT T) | norm (Free (a, T)) = Free (a, normT T) | norm (Var (xi, T)) = (case lookup envir (xi, T) of SOME u => Same.commit norm u | NONE => Var (xi, normT T)) | norm (Abs (a, T, body)) = (Abs (a, normT T, Same.commit norm body) handle Same.SAME => Abs (a, T, norm body)) | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) | norm (f $ t) = ((case norm f of Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) | nf => nf $ Same.commit norm t) handle Same.SAME => f $ norm t) | norm _ = raise Same.SAME; in norm end; in fun norm_type_same tyenv T = if Vartab.is_empty tyenv then raise Same.SAME else norm_type0 tyenv T; fun norm_types_same tyenv Ts = if Vartab.is_empty tyenv then raise Same.SAME else Same.map (norm_type0 tyenv) Ts; fun norm_type tyenv T = norm_type_same tyenv T handle Same.SAME => T; fun norm_term_same (envir as Envir {tenv, tyenv, ...}) = if Vartab.is_empty tyenv then norm_term1 tenv else norm_term2 envir; fun norm_term envir t = norm_term_same envir t handle Same.SAME => t; fun beta_norm t = if Term.could_beta_contract t then norm_term init t else t; end; (* head normal form for unification *) fun head_norm env = let fun norm (Var v) = (case lookup env v of SOME u => head_norm env u | NONE => raise Same.SAME) | norm (Abs (a, T, body)) = Abs (a, T, norm body) | norm (Abs (_, _, body) $ t) = Same.commit norm (subst_bound (t, body)) | norm (f $ t) = (case norm f of Abs (_, _, body) => Same.commit norm (subst_bound (t, body)) | nf => nf $ t) | norm _ = raise Same.SAME; in Same.commit norm end; (* eta-long beta-normal form *) fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t) | eta_long Ts t = (case strip_comb t of (Abs _, _) => eta_long Ts (beta_norm t) | (u, ts) => let val Us = binder_types (fastype_of1 (Ts, t)); val i = length Us; val long = eta_long (rev Us @ Ts); in fold_rev (Term.abs o pair "x") Us (list_comb (incr_boundvars i u, map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0))) end); (* full eta contraction *) local fun decr lev (Bound i) = if i >= lev then Bound (i - 1) else raise Same.SAME | decr lev (Abs (a, T, body)) = Abs (a, T, decr (lev + 1) body) | decr lev (t $ u) = (decr lev t $ decrh lev u handle Same.SAME => t $ decr lev u) | decr _ _ = raise Same.SAME and decrh lev t = (decr lev t handle Same.SAME => t); fun eta (Abs (a, T, body)) = ((case eta body of body' as (f $ Bound 0) => if Term.is_dependent f then Abs (a, T, body') else decrh 0 f | body' => Abs (a, T, body')) handle Same.SAME => (case body of f $ Bound 0 => if Term.is_dependent f then raise Same.SAME else decrh 0 f | _ => raise Same.SAME)) | eta (t $ u) = (eta t $ Same.commit eta u handle Same.SAME => t $ eta u) | eta _ = raise Same.SAME; in fun eta_contract t = if Term.could_eta_contract t then Same.commit eta t else t; end; val beta_eta_contract = eta_contract o beta_norm; fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u; fun body_type env (Type ("fun", [_, T])) = body_type env T | body_type env (T as TVar v) = (case Type.lookup (type_env env) v of NONE => T | SOME T' => body_type env T') | body_type _ T = T; fun binder_types env (Type ("fun", [T, U])) = T :: binder_types env U | binder_types env (TVar v) = (case Type.lookup (type_env env) v of NONE => [] | SOME T' => binder_types env T') | binder_types _ _ = []; fun strip_type env T = (binder_types env T, body_type env T); (*finds type of term without checking that combinations are consistent Ts holds types of bound variables*) fun fastype (Envir {tyenv, ...}) = let val funerr = "fastype: expected function type"; fun fast Ts (f $ u) = (case Type.devar tyenv (fast Ts f) of Type ("fun", [_, T]) => T | TVar _ => raise TERM (funerr, [f $ u]) | _ => raise TERM (funerr, [f $ u])) | fast _ (Const (_, T)) = T | fast _ (Free (_, T)) = T | fast Ts (Bound i) = (nth Ts i handle General.Subscript => raise TERM ("fastype: Bound", [Bound i])) | fast _ (Var (_, T)) = T | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u; in fast end; (** plain substitution -- without variable chasing **) local fun subst_type0 tyenv = Term_Subst.map_atypsT_same (fn TVar v => (case Type.lookup tyenv v of SOME U => U | NONE => raise Same.SAME) | _ => raise Same.SAME); fun subst_term1 tenv = Term_Subst.map_aterms_same (fn Var v => (case lookup1 tenv v of SOME u => u | NONE => raise Same.SAME) | _ => raise Same.SAME); fun subst_term2 tenv tyenv : term Same.operation = let val substT = subst_type0 tyenv; fun subst (Const (a, T)) = Const (a, substT T) | subst (Free (a, T)) = Free (a, substT T) | subst (Var (xi, T)) = (case lookup1 tenv (xi, T) of SOME u => u | NONE => Var (xi, substT T)) | subst (Bound _) = raise Same.SAME | subst (Abs (a, T, t)) = (Abs (a, substT T, Same.commit subst t) handle Same.SAME => Abs (a, T, subst t)) | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u); in subst end; in fun subst_type_same tyenv T = if Vartab.is_empty tyenv then raise Same.SAME else subst_type0 tyenv T; fun subst_term_types_same tyenv t = if Vartab.is_empty tyenv then raise Same.SAME else Term_Subst.map_types_same (subst_type0 tyenv) t; fun subst_term_same (tyenv, tenv) = if Vartab.is_empty tenv then subst_term_types_same tyenv else if Vartab.is_empty tyenv then subst_term1 tenv else subst_term2 tenv tyenv; fun subst_type tyenv T = subst_type_same tyenv T handle Same.SAME => T; fun subst_term_types tyenv t = subst_term_types_same tyenv t handle Same.SAME => t; fun subst_term envs t = subst_term_same envs t handle Same.SAME => t; end; (** expand defined atoms -- with local beta reduction **) fun expand_atom T (U, u) = subst_term_types (Vartab.build (Type.raw_match (U, T))) u handle Type.TYPE_MATCH => raise TYPE ("expand_atom: ill-typed replacement", [T, U], [u]); fun expand_term get = let fun expand tm = let val (head, args) = Term.strip_comb tm; val args' = map expand args; fun comb head' = Term.list_comb (head', args'); in (case head of Abs (x, T, t) => comb (Abs (x, T, expand t)) | _ => (case get head of SOME def => Term.betapplys (expand_atom (Term.fastype_of head) def, args') | NONE => comb head)) end; in expand end; -fun expand_term_frees defs = +fun expand_term_defs dest defs = let - val eqs = map (fn ((x, U), u) => (x, (U, u))) defs; - val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE; + val eqs = map (fn ((x, U), u) => (x: string, (U, u))) defs; + fun get t = (case try dest t of SOME (x, _: typ) => AList.lookup (op =) eqs x | _ => NONE); in expand_term get end; end;