# HG changeset patch # User traytel # Date 1395074139 -3600 # Node ID 6b5c46582260bdf867bcdc94c412c584e27c63d3 # Parent 2a6f5893857316fdd806c974014d4eeba1f0b891 tuned internal construction diff -r 2a6f58938573 -r 6b5c46582260 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 17 15:48:30 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 17 17:35:39 2014 +0100 @@ -1707,9 +1707,9 @@ fun col_spec j Zero hrec hrec' = let - fun mk_Suc dtor setss z z' = + fun mk_Suc dtor sets z z' = let - val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setss); + val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m sets); fun mk_UN set k = mk_UNION (set $ (dtor $ z)) (mk_nthN n hrec k); in Term.absfree z' @@ -1748,295 +1748,32 @@ val col_0ss' = transpose col_0ss; val col_Sucss' = transpose col_Sucss; - fun mk_hset Ts i j T = + fun mk_set Ts i j T = Abs (Name.uu, nth Ts (i - 1), mk_UNION (HOLogic.mk_UNIV HOLogic.natT) (Term.absfree nat' (mk_col Ts nat i j T $ Bound 1))); - val setss_by_bnf = map (fn i => map2 (mk_hset Ts i) ls passiveAs) ks; - val setss_by_range = transpose setss_by_bnf; - - val hset_minimal_thms = - let - fun mk_passive_prem set dtor x K = - Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x))); - - fun mk_active_prem dtor x1 K1 set x2 K2 = - fold_rev Logic.all [x1, x2] - (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))), - HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1)))); - - val premss = map2 (fn j => fn Ks => - map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @ - flat (map4 (fn sets => fn s => fn x1 => fn K1 => - map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks)) - ls Kss; - - val col_minimal_thms = - let - fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x); - fun mk_concl j T Ks = list_all_free Jzs - (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs)); - val concls = map3 mk_concl ls passiveAs Kss; - - val goals = map2 (fn prems => fn concl => - Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls - - val ctss = - map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; - in - map4 (fn goal => fn cts => fn col_0s => fn col_Sucs => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s - col_Sucs)) - |> Thm.close_derivation) - goals ctss col_0ss' col_Sucss' - end; - - fun mk_conjunct j T i K x = mk_leq (mk_hset Ts i j T $ x) (K $ x); - fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs); - val concls = map3 mk_concl ls passiveAs Kss; - - val goals = map3 (fn Ks => fn prems => fn concl => - fold_rev Logic.all (Ks @ Jzs) - (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls; - in - map2 (fn goal => fn col_minimal => - Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n col_minimal) - |> Thm.close_derivation) - goals col_minimal_thms - end; - - val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) = - let - fun mk_set_incl_hset dtor x set hset = fold_rev Logic.all (x :: ss) - (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (hset $ x))); - - fun mk_set_hset_incl_hset dtor x y set hset1 hset2 = - fold_rev Logic.all [x, y] - (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))), - HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y)))); - - val set_incl_hset_goalss = - map4 (fn dtor => fn x => fn sets => fn hsets => - map2 (mk_set_incl_hset dtor x) (take m sets) hsets) - dtors Jzs FTs_setss setss_by_bnf; - - (*xk : F(i)set(m+k) (si yi) ==> F(k)_hset(j) s1 ... sn xk <= F(i)_hset(j) s1 ... sn yi*) - val set_hset_incl_hset_goalsss = - map4 (fn dtori => fn yi => fn sets => fn hsetsi => - map3 (fn xk => fn set => fn hsetsk => - map2 (mk_set_hset_incl_hset dtori xk yi set) hsetsk hsetsi) - Jzs_copy (drop m sets) setss_by_bnf) - dtors Jzs FTs_setss setss_by_bnf; - in - (map2 (fn goals => fn rec_Sucs => - map2 (fn goal => fn rec_Suc => - Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac rec_Suc)) - |> Thm.close_derivation) - goals rec_Sucs) - set_incl_hset_goalss col_Sucss, - map2 (fn goalss => fn rec_Sucs => - map2 (fn k => fn goals => - map2 (fn goal => fn rec_Suc => - Goal.prove_sorry lthy [] [] goal - (K (mk_set_hset_incl_hset_tac n rec_Suc k)) - |> Thm.close_derivation) - goals rec_Sucs) - ks goalss) - set_hset_incl_hset_goalsss col_Sucss) - end; - - val set_incl_hset_thmss' = transpose set_incl_hset_thmss; - val set_hset_incl_hset_thmsss' = transpose (map transpose set_hset_incl_hset_thmsss); - val set_hset_thmss = map (map (fn thm => thm RS @{thm set_mp})) set_incl_hset_thmss; - val set_hset_hset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp}))) - set_hset_incl_hset_thmsss; - val set_hset_thmss' = transpose set_hset_thmss; - val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss); - - - val timer = time (timer "Hereditary sets"); - - val dtor_hset_induct_thms = - let - val incls = - maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_hset_thmss @ - @{thms subset_Collect_iff[OF subset_refl]}; - - val cTs = map (SOME o certifyT lthy) params'; - fun mk_induct_tinst phis jsets y y' = - map4 (fn phi => fn jset => fn Jz => fn Jz' => - SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', - HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) - phis jsets Jzs Jzs'; - in - map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => - ((set_minimal - |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y') - |> unfold_thms lthy incls) OF - (replicate n ballI @ - maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) - |> singleton (Proof_Context.export names_lthy lthy) - |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) - hset_minimal_thms set_hset_incl_hset_thmsss' setss_by_range ys ys' dtor_set_induct_phiss - end; - - fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); - - val all_unitTs = replicate live HOLogic.unitT; - val unitTs = replicate n HOLogic.unitT; - val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit); - fun mk_map_args I = - map (fn i => - if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i) - else mk_undefined (HOLogic.unitT --> nth passiveAs i)) - (0 upto (m - 1)); - - fun mk_nat_wit Ds bnf (I, wit) () = - let - val passiveI = filter (fn i => i < m) I; - val map_args = mk_map_args passiveI; - in - Term.absdummy HOLogic.unitT (Term.list_comb - (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit) - end; - - fun mk_dummy_wit Ds bnf I = - let - val map_args = mk_map_args I; - in - Term.absdummy HOLogic.unitT (Term.list_comb - (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ - mk_undefined (mk_T_of_bnf Ds all_unitTs bnf)) - end; - - val nat_witss = - map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) - (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf - |> map (fn (I, wit) => - (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I)))))) - Dss bnfs; - - val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs) - - val Iss = map (map fst) nat_witss; - - fun filter_wits (I, wit) = - let val J = filter (fn i => i < m) I; - in (J, (length J < length I, wit)) end; - - val wit_treess = map_index (fn (i, Is) => - map_index (finish Iss m [i+m] (i+m)) Is) Iss - |> map (minimize_wits o map filter_wits o minimize_wits o flat); - - val coind_wit_argsss = - map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess; - - val nonredundant_coind_wit_argsss = - fold (fn i => fn argsss => - nth_map (i - 1) (filter_out (fn xs => - exists (fn ys => - let - val xs' = (map (fst o fst) xs, snd (fst (hd xs))); - val ys' = (map (fst o fst) ys, snd (fst (hd ys))); - in - eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys') - end) - (flat argsss))) - argsss) - ks coind_wit_argsss; - - fun prepare_args args = - let - val I = snd (fst (hd args)); - val (dummys, args') = - map_split (fn i => - (case find_first (fn arg => fst (fst arg) = i - 1) args of - SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms)) - | NONE => - (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, [])))) - ks; - in - ((I, dummys), apsnd flat (split_list args')) - end; - - fun mk_coind_wits ((I, dummys), (args, thms)) = - ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms)); - - val coind_witss = - maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss; - - val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf - (replicate (nwits_of_bnf bnf) Ds) - (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; - - val ctor_witss = - map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o - filter_out (fst o snd)) wit_treess; - - fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) = - let - fun mk_goal sets y y_copy y'_copy j = - let - fun mk_conjunct set z dummy wit = - mk_Ball (set $ z) (Term.absfree y'_copy - (if dummy = NONE orelse member (op =) I (j - 1) then - HOLogic.mk_imp (HOLogic.mk_eq (z, wit), - if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y) - else @{term False}) - else @{term True})); - in - fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop - (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))) - end; - val goals = map5 mk_goal setss_by_range ys ys_copy ys'_copy ls; - in - map2 (fn goal => fn induct => - Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms - (flat set_mapss) wit_thms) - |> Thm.close_derivation) - goals dtor_hset_induct_thms - |> map split_conj_thm - |> transpose - |> map (map_filter (try (fn thm => thm RS bspec RS mp))) - |> curry op ~~ (map_index Library.I (map (close_wit I) wits)) - |> filter (fn (_, thms) => length thms = m) - end; - - val coind_wit_thms = maps mk_coind_wit_thms coind_witss; - - val (wit_thmss, all_witss) = - fold (fn ((i, wit), thms) => fn witss => - nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) - coind_wit_thms (map (pair []) ctor_witss) - |> map (apsnd (map snd o minimize_wits)) - |> split_list; + val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks; val (Jbnf_consts, lthy) = - fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits => - fn T => fn lthy => - define_bnf_consts Dont_Inline (user_policy Note_Some lthy) false (SOME deads) + fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T => + fn lthy => + define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads) map_b rel_b set_bs - ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy) - bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy; + ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), + [Const (@{const_name undefined}, T)]), NONE) lthy) + bs map_bs rel_bs set_bss fs_maps setss Ts lthy; val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts; - val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts; - val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs; + val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts; + val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs; val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts; val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs; val Jset_defs = flat Jset_defss; - val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs; fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds; fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss; val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds; - val Jwitss = - map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds; fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds; val Jmaps = mk_Jmaps passiveAs passiveBs; @@ -2098,6 +1835,135 @@ val timer = time (timer "map functions for the new codatatypes"); + val Jset_minimal_thms = + let + fun mk_passive_prem set dtor x K = + Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (K $ x))); + + fun mk_active_prem dtor x1 K1 set x2 K2 = + fold_rev Logic.all [x1, x2] + (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (dtor $ x1))), + HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1)))); + + val premss = map2 (fn j => fn Ks => + map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @ + flat (map4 (fn sets => fn s => fn x1 => fn K1 => + map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks)) + ls Kss; + + val col_minimal_thms = + let + fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x); + fun mk_concl j T Ks = list_all_free Jzs + (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs)); + val concls = map3 mk_concl ls passiveAs Kss; + + val goals = map2 (fn prems => fn concl => + Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls + + val ctss = + map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls; + in + map4 (fn goal => fn cts => fn col_0s => fn col_Sucs => + singleton (Proof_Context.export names_lthy lthy) + (Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s + col_Sucs)) + |> Thm.close_derivation) + goals ctss col_0ss' col_Sucss' + end; + + fun mk_conjunct set K x = mk_leq (set $ x) (K $ x); + fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs); + val concls = map2 mk_concl Jsetss_by_range Kss; + + val goals = map3 (fn Ks => fn prems => fn concl => + fold_rev Logic.all (Ks @ Jzs) + (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls; + in + map2 (fn goal => fn col_minimal => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_Jset_minimal_tac ctxt n col_minimal) + |> Thm.close_derivation) + goals col_minimal_thms + end; + + val (dtor_Jset_incl_thmss, dtor_set_Jset_incl_thmsss) = + let + fun mk_set_incl_Jset dtor x set Jset = fold_rev Logic.all (x :: ss) + (HOLogic.mk_Trueprop (mk_leq (set $ (dtor $ x)) (Jset $ x))); + + fun mk_set_Jset_incl_Jset dtor x y set Jset1 Jset2 = + fold_rev Logic.all [x, y] + (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (dtor $ y))), + HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)))); + + val set_incl_Jset_goalss = + map4 (fn dtor => fn x => fn sets => fn Jsets => + map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets) + dtors Jzs FTs_setss Jsetss_by_bnf; + + (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*) + val set_Jset_incl_Jset_goalsss = + map4 (fn dtori => fn yi => fn sets => fn Jsetsi => + map3 (fn xk => fn set => fn Jsetsk => + map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi) + Jzs_copy (drop m sets) Jsetss_by_bnf) + dtors Jzs FTs_setss Jsetss_by_bnf; + in + (map2 (fn goals => fn rec_Sucs => + map2 (fn goal => fn rec_Suc => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_set_incl_Jset_tac rec_Suc) + |> Thm.close_derivation) + goals rec_Sucs) + set_incl_Jset_goalss col_Sucss, + map2 (fn goalss => fn rec_Sucs => + map2 (fn k => fn goals => + map2 (fn goal => fn rec_Suc => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN + mk_set_Jset_incl_Jset_tac n rec_Suc k) + |> Thm.close_derivation) + goals rec_Sucs) + ks goalss) + set_Jset_incl_Jset_goalsss col_Sucss) + end; + + val set_incl_Jset_thmss' = transpose dtor_Jset_incl_thmss; + val set_Jset_incl_Jset_thmsss' = transpose (map transpose dtor_set_Jset_incl_thmsss); + val set_Jset_thmss = map (map (fn thm => thm RS @{thm set_mp})) dtor_Jset_incl_thmss; + val set_Jset_Jset_thmsss = map (map (map (fn thm => thm RS @{thm set_mp}))) + dtor_set_Jset_incl_thmsss; + val set_Jset_thmss' = transpose set_Jset_thmss; + val set_Jset_Jset_thmsss' = transpose (map transpose set_Jset_Jset_thmsss); + + val dtor_Jset_induct_thms = + let + val incls = + maps (map (fn thm => thm RS @{thm subset_Collect_iff})) dtor_Jset_incl_thmss @ + @{thms subset_Collect_iff[OF subset_refl]}; + + val cTs = map (SOME o certifyT lthy) params'; + fun mk_induct_tinst phis jsets y y' = + map4 (fn phi => fn jset => fn Jz => fn Jz' => + SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y', + HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz)))))) + phis jsets Jzs Jzs'; + in + map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => + ((set_minimal + |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y') + |> unfold_thms lthy incls) OF + (replicate n ballI @ + maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss)) + |> singleton (Proof_Context.export names_lthy lthy) + |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl))) + Jset_minimal_thms set_Jset_incl_Jset_thmsss' Jsetss_by_range ys ys' dtor_set_induct_phiss + end; + val (dtor_Jset_thmss', dtor_Jset_thmss) = let fun mk_simp_goal relate pas_set act_sets sets dtor z set = @@ -2115,23 +1981,21 @@ (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj) (mk_goals (uncurry mk_leq)); val set_le_thmss = map split_conj_thm - (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss => + (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss => Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN - mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss) + (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss)) |> Thm.close_derivation) - le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss'); + le_goals Jset_minimal_thms set_Jset_thmss' set_Jset_Jset_thmsss'); val ge_goalss = map (map2 (fn z => fn goal => Logic.all z (HOLogic.mk_Trueprop goal)) Jzs) (mk_goals (uncurry mk_leq o swap)); val set_ge_thmss = - map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets => + map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets => Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN - mk_set_ge_tac n set_incl_hset set_hset_incl_hsets) + (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets)) |> Thm.close_derivation)) - ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss' + ge_goalss set_incl_Jset_thmss' set_Jset_incl_Jset_thmsss' in map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss |> `transpose @@ -2222,8 +2086,7 @@ val cphis = map9 mk_cphi Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy; - val coinduct = unfold_thms lthy Jset_defs - (Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm); + val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj @@ -2231,9 +2094,8 @@ val thm = singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN - mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s - set_mapss set_hset_thmss set_hset_hset_thmsss in_rels)) + (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s + set_mapss set_Jset_thmss set_Jset_Jset_thmsss in_rels))) |> Thm.close_derivation in split_conj_thm thm @@ -2242,12 +2104,6 @@ val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD}) Jrel_unabs_defs; - val fold_Jsets = fold_thms lthy Jset_unabs_defs; - val dtor_Jset_incl_thmss = map (map fold_Jsets) set_incl_hset_thmss; - val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) set_hset_incl_hset_thmsss; - val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms; - val Jwit_thmss = map (map fold_Jsets) wit_thmss; - val Jrels = mk_Jrels passiveAs passiveBs; val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels; val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels; @@ -2413,6 +2269,140 @@ val timer = time (timer "helpers for BNF properties"); + fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit); + + val all_unitTs = replicate live HOLogic.unitT; + val unitTs = replicate n HOLogic.unitT; + val unit_funs = replicate n (Term.absdummy HOLogic.unitT HOLogic.unit); + fun mk_map_args I = + map (fn i => + if member (op =) I i then Term.absdummy HOLogic.unitT (nth ys i) + else mk_undefined (HOLogic.unitT --> nth passiveAs i)) + (0 upto (m - 1)); + + fun mk_nat_wit Ds bnf (I, wit) () = + let + val passiveI = filter (fn i => i < m) I; + val map_args = mk_map_args passiveI; + in + Term.absdummy HOLogic.unitT (Term.list_comb + (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ wit) + end; + + fun mk_dummy_wit Ds bnf I = + let + val map_args = mk_map_args I; + in + Term.absdummy HOLogic.unitT (Term.list_comb + (mk_map_of_bnf Ds all_unitTs (passiveAs @ unitTs) bnf, map_args @ unit_funs) $ + mk_undefined (mk_T_of_bnf Ds all_unitTs bnf)) + end; + + val nat_witss = + map2 (fn Ds => fn bnf => mk_wits_of_bnf (replicate (nwits_of_bnf bnf) Ds) + (replicate (nwits_of_bnf bnf) (replicate live HOLogic.unitT)) bnf + |> map (fn (I, wit) => + (I, Lazy.lazy (mk_nat_wit Ds bnf (I, Term.list_comb (wit, map (K HOLogic.unit) I)))))) + Dss bnfs; + + val nat_wit_thmss = map2 (curry op ~~) nat_witss (map wit_thmss_of_bnf bnfs) + + val Iss = map (map fst) nat_witss; + + fun filter_wits (I, wit) = + let val J = filter (fn i => i < m) I; + in (J, (length J < length I, wit)) end; + + val wit_treess = map_index (fn (i, Is) => + map_index (finish Iss m [i+m] (i+m)) Is) Iss + |> map (minimize_wits o map filter_wits o minimize_wits o flat); + + val coind_wit_argsss = + map (map (tree_to_coind_wits nat_wit_thmss o snd o snd) o filter (fst o snd)) wit_treess; + + val nonredundant_coind_wit_argsss = + fold (fn i => fn argsss => + nth_map (i - 1) (filter_out (fn xs => + exists (fn ys => + let + val xs' = (map (fst o fst) xs, snd (fst (hd xs))); + val ys' = (map (fst o fst) ys, snd (fst (hd ys))); + in + eq_pair (subset (op =)) (eq_set (op =)) (xs', ys') andalso not (fst xs' = fst ys') + end) + (flat argsss))) + argsss) + ks coind_wit_argsss; + + fun prepare_args args = + let + val I = snd (fst (hd args)); + val (dummys, args') = + map_split (fn i => + (case find_first (fn arg => fst (fst arg) = i - 1) args of + SOME (_, ((_, wit), thms)) => (NONE, (Lazy.force wit, thms)) + | NONE => + (SOME (i - 1), (mk_dummy_wit (nth Dss (i - 1)) (nth bnfs (i - 1)) I, [])))) + ks; + in + ((I, dummys), apsnd flat (split_list args')) + end; + + fun mk_coind_wits ((I, dummys), (args, thms)) = + ((I, dummys), (map (fn i => mk_unfold Ts args i $ HOLogic.unit) ks, thms)); + + val coind_witss = + maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss; + + val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf + (replicate (nwits_of_bnf bnf) Ds) + (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs; + + val ctor_witss = + map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o + filter_out (fst o snd)) wit_treess; + + fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) = + let + fun mk_goal sets y y_copy y'_copy j = + let + fun mk_conjunct set z dummy wit = + mk_Ball (set $ z) (Term.absfree y'_copy + (if dummy = NONE orelse member (op =) I (j - 1) then + HOLogic.mk_imp (HOLogic.mk_eq (z, wit), + if member (op =) I (j - 1) then HOLogic.mk_eq (y_copy, y) + else @{term False}) + else @{term True})); + in + fold_rev Logic.all (map (nth ys) I @ Jzs) (HOLogic.mk_Trueprop + (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))) + end; + val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls; + in + map2 (fn goal => fn induct => + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => mk_coind_wit_tac ctxt induct dtor_unfold_thms + (flat set_mapss) wit_thms) + |> Thm.close_derivation) + goals dtor_Jset_induct_thms + |> map split_conj_thm + |> transpose + |> map (map_filter (try (fn thm => thm RS bspec RS mp))) + |> curry op ~~ (map_index Library.I (map (close_wit I) wits)) + |> filter (fn (_, thms) => length thms = m) + end; + + val coind_wit_thms = maps mk_coind_wit_thms coind_witss; + + val (wit_thmss, all_witss) = + fold (fn ((i, wit), thms) => fn witss => + nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss) + coind_wit_thms (map (pair []) ctor_witss) + |> map (apsnd (map snd o minimize_wits)) + |> split_list; + + val timer = time (timer "witnesses"); + val map_id0_tacs = map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms; val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms; @@ -2439,17 +2429,17 @@ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs; - fun wit_tac thms ctxt = unfold_thms_tac ctxt (flat Jwit_defss) THEN + fun wit_tac thms ctxt = mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; val (Jbnfs, lthy) = - fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => + fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => fn consts => fn lthy => - bnf_def Do_Inline (user_policy Note_Some) false I tacs (wit_tac Jwit_thms) (SOME deads) - map_b rel_b set_bs consts lthy + bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) + (SOME deads) map_b rel_b set_bs consts lthy |> register_bnf (Local_Theory.full_name lthy b)) - bs tacss map_bs rel_bs set_bss Jwit_thmss - ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels) + bs tacss map_bs rel_bs set_bss wit_thmss + ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels) lthy; val timer = time (timer "registered new codatatypes as BNFs"); diff -r 2a6f58938573 -r 6b5c46582260 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 17 15:48:30 2014 +0000 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 17 17:35:39 2014 +0100 @@ -32,7 +32,7 @@ thm -> thm -> thm list -> thm list -> thm list list -> tactic val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic - val mk_hset_minimal_tac: Proof.context -> int -> thm -> tactic + val mk_Jset_minimal_tac: Proof.context -> int -> thm -> tactic val mk_col_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> tactic val mk_incl_lsbis_tac: int -> int -> thm -> tactic @@ -75,10 +75,10 @@ val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> tactic val mk_set_bd_tac: thm -> thm -> tactic - val mk_set_hset_incl_hset_tac: int -> thm -> int -> tactic + val mk_set_Jset_incl_Jset_tac: int -> thm -> int -> tactic val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic - val mk_set_incl_hset_tac: thm -> tactic + val mk_set_incl_Jset_tac: thm -> tactic val mk_set_ge_tac: int -> thm -> thm list -> tactic val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic val mk_set_map0_tac: thm -> tactic @@ -162,11 +162,11 @@ fun mk_mor_case_sum_tac ks mor_UNIV = (rtac (mor_UNIV RS iffD2) THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1; -fun mk_set_incl_hset_tac rec_Suc = +fun mk_set_incl_Jset_tac rec_Suc = EVERY' (map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, sym, rec_Suc]) 1; -fun mk_set_hset_incl_hset_tac n rec_Suc i = +fun mk_set_Jset_incl_Jset_tac n rec_Suc i = EVERY' (map rtac [@{thm UN_least}, subsetI, @{thm UN_I}, UNIV_I, set_mp, equalityD2, rec_Suc, UnI2, mk_UnIN n i] @ [etac @{thm UN_I}, atac]) 1; @@ -185,7 +185,7 @@ rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s]) rec_Sucs] 1; -fun mk_hset_minimal_tac ctxt n col_minimal = +fun mk_Jset_minimal_tac ctxt n col_minimal = (CONJ_WRAP' (K (EVERY' [rtac @{thm UN_least}, rtac rev_mp, rtac col_minimal, EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI, REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1 @@ -777,20 +777,20 @@ REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), rtac map_arg_cong, rtac (o_apply RS sym)] 1; -fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss = - EVERY' [rtac hset_minimal, +fun mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss = + EVERY' [rtac Jset_minimal, REPEAT_DETERM_N n o rtac @{thm Un_upper1}, REPEAT_DETERM_N n o - EVERY' (map3 (fn i => fn set_hset => fn set_hset_hsets => + EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets => EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I}, - etac UnE, etac set_hset, REPEAT_DETERM_N (n - 1) o etac UnE, - EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)]) - (1 upto n) set_hsets set_hset_hsetss)] 1; + etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE, + EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)]) + (1 upto n) set_Jsets set_Jset_Jsetss)] 1; -fun mk_set_ge_tac n set_incl_hset set_hset_incl_hsets = - EVERY' [rtac @{thm Un_least}, rtac set_incl_hset, +fun mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets = + EVERY' [rtac @{thm Un_least}, rtac set_incl_Jset, REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least}, - EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1; + EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_Jset_incl_Jsets)] 1; fun mk_map_id0_tac maps unfold_unique unfold_dtor = EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps), @@ -807,15 +807,15 @@ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]])) maps map_comp0s)] 1; -fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss - set_hset_hsetsss in_rels = +fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_Jsetss + set_Jset_Jsetsss in_rels = let val n = length map_comps; val ks = 1 upto n; in EVERY' ([rtac rev_mp, coinduct_tac] @ - maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_hsets), - set_hset_hsetss), in_rel) => + maps (fn ((((((map_comp_trans, dtor_maps_trans), map_cong0), set_map0s), set_Jsets), + set_Jset_Jsetss), in_rel) => [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2], REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac (Drule.rotate_prems 1 conjI), @@ -823,25 +823,25 @@ REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm fst_conv}), REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym, rtac map_comp_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0, - EVERY' (maps (fn set_hset => + EVERY' (maps (fn set_Jset => [rtac o_apply_trans_sym, rtac (@{thm snd_conv} RS trans), etac CollectE, - REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets), + REPEAT_DETERM o etac conjE, etac bspec, etac set_Jset]) set_Jsets), REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym, rtac CollectI, EVERY' (map (fn set_map0 => EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac refl]) (take m set_map0s)), - CONJ_WRAP' (fn (set_map0, set_hset_hsets) => + CONJ_WRAP' (fn (set_map0, set_Jset_Jsets) => EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI, rtac @{thm case_prodI}, rtac exI, rtac conjI, rtac CollectI, etac CollectE, REPEAT_DETERM o etac conjE, - CONJ_WRAP' (fn set_hset_hset => - EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets, + CONJ_WRAP' (fn set_Jset_Jset => + EVERY' [rtac ballI, etac bspec, etac set_Jset_Jset, atac]) set_Jset_Jsets, rtac (conjI OF [refl, refl])]) - (drop m set_map0s ~~ set_hset_hsetss)]) + (drop m set_map0s ~~ set_Jset_Jsetss)]) (map (fn th => th RS trans) map_comps ~~ map (fn th => th RS trans) dtor_maps ~~ - map_cong0s ~~ set_map0ss ~~ set_hsetss ~~ set_hset_hsetsss ~~ in_rels) @ + map_cong0s ~~ set_map0ss ~~ set_Jsetss ~~ set_Jset_Jsetsss ~~ in_rels) @ [rtac impI, CONJ_WRAP' (fn k => EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,