# HG changeset patch # User traytel # Date 1394705704 -3600 # Node ID e3b8f8319d7349d2b227cec93ad86e2c4e65bf1f # Parent d397030fb27e69c3ee927835f74a07cf82334e11 simplified internal codatatype construction diff -r d397030fb27e -r e3b8f8319d73 src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Mar 13 11:15:04 2014 +0100 @@ -85,8 +85,7 @@ val dtor_unfold_transferN: string val dtor_unfold_uniqueN: string val exhaustN: string - val hsetN: string - val hset_recN: string + val colN: string val inductN: string val injectN: string val isNodeN: string @@ -307,8 +306,7 @@ val strong_coinductN = "strong_" ^ coinductN val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN -val hsetN = "Hset" -val hset_recN = hsetN ^ "_rec" +val colN = "col" val set_inclN = "set_incl" val ctor_set_inclN = ctorN ^ "_" ^ set_inclN val dtor_set_inclN = dtorN ^ "_" ^ set_inclN diff -r d397030fb27e -r e3b8f8319d73 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Mar 13 11:15:04 2014 +0100 @@ -158,15 +158,10 @@ val sum_bd = Library.foldr1 (uncurry mk_csum) bds; val sum_bdT = fst (dest_relT (fastype_of sum_bd)); - val emptys = map (fn T => HOLogic.mk_set T []) passiveAs; - val Zeros = map (fn empty => - HOLogic.mk_tuple (map (fn U => absdummy U empty) activeAs)) emptys; - val hrecTs = map fastype_of Zeros; - - val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), + val ((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy), - self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')), - (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy + self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), + (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), names_lthy) = lthy |> mk_Frees' "b" activeAs ||>> mk_Frees "b" activeAs ||>> mk_Frees "b" activeAs @@ -190,7 +185,6 @@ ||>> mk_Frees "y" FTsBs ||>> mk_Frees "x" FRTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT - ||>> mk_Frees' "rec" hrecTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "n") HOLogic.natT ||>> mk_Frees "R" setRTs ||>> mk_Frees "R" setRTs @@ -198,8 +192,7 @@ ||>> mk_Frees "R" setsRTs ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "i") idxT ||>> yield_singleton (mk_Frees "I") (HOLogic.mk_setT idxT) - ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs) - ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) activeAs) ATs); + ||>> mk_Frees "Ri" (map (fn T => idxT --> T) setRTs); val passive_UNIVs = map HOLogic.mk_UNIV passiveAs; val passive_eqs = map HOLogic.eq_const passiveAs; @@ -506,203 +499,6 @@ val timer = time (timer "Morphism definition & thms"); - fun hset_rec_bind j = mk_internal_b (hset_recN ^ (if m = 1 then "" else string_of_int j)); - val hset_rec_def_bind = rpair [] o Thm.def_binding o hset_rec_bind; - - fun hset_rec_spec j Zero hrec hrec' = - let - fun mk_Suc s setsAs z z' = - let - val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setsAs); - fun mk_UN set k = mk_UNION (set $ (s $ z)) (mk_nthN n hrec k); - in - Term.absfree z' - (mk_union (set $ (s $ z), Library.foldl1 mk_union (map2 mk_UN sets ks))) - end; - - val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec' - (HOLogic.mk_tuple (map4 mk_Suc ss setssAs zs zs'))); - - val rhs = mk_rec_nat Zero Suc; - in - fold_rev (Term.absfree o Term.dest_Free) ss rhs - end; - - val ((hset_rec_frees, (_, hset_rec_def_frees)), (lthy, lthy_old)) = - lthy - |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define - ((hset_rec_bind j, NoSyn), (hset_rec_def_bind j, hset_rec_spec j Zero hrec hrec'))) - ls Zeros hrecs hrecs' - |>> apsnd split_list o split_list - ||> `Local_Theory.restore; - - val phi = Proof_Context.export_morphism lthy_old lthy; - - val hset_rec_defs = map (fn def => - mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) hset_rec_def_frees; - val hset_recs = map (fst o Term.dest_Const o Morphism.term phi) hset_rec_frees; - - fun mk_hset_rec ss nat i j T = - let - val args = ss @ [nat]; - val Ts = map fastype_of ss; - val bTs = map domain_type Ts; - val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) bTs) - val hset_recT = Library.foldr (op -->) (Ts, HOLogic.natT --> hrecT); - in - mk_nthN n (Term.list_comb (Const (nth hset_recs (j - 1), hset_recT), args)) i - end; - - val hset_rec_0ss = mk_rec_simps n @{thm rec_nat_0_imp} hset_rec_defs; - val hset_rec_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} hset_rec_defs; - val hset_rec_0ss' = transpose hset_rec_0ss; - val hset_rec_Sucss' = transpose hset_rec_Sucss; - - fun hset_binds j = mk_internal_bs (hsetN ^ (if m = 1 then "" else string_of_int j)) - fun hset_bind i j = nth (hset_binds j) (i - 1); - val hset_def_bind = rpair [] o Thm.def_binding oo hset_bind; - - fun hset_spec i j = - let - val z = nth zs (i - 1); - val T = nth passiveAs (j - 1); - - val rhs = mk_UNION (HOLogic.mk_UNIV HOLogic.natT) - (Term.absfree nat' (mk_hset_rec ss nat i j T $ z)); - in - fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) rhs - end; - - val ((hset_frees, (_, hset_def_frees)), (lthy, lthy_old)) = - lthy - |> fold_map (fn i => fold_map (fn j => Local_Theory.define - ((hset_bind i j, NoSyn), (hset_def_bind i j, hset_spec i j))) ls) ks - |>> map (apsnd split_list o split_list) - |>> apsnd split_list o split_list - ||> `Local_Theory.restore; - - val phi = Proof_Context.export_morphism lthy_old lthy; - - val hset_defss = map (map (fn def => - mk_unabs_def (n + 1) (Morphism.thm phi def RS meta_eq_to_obj_eq))) hset_def_frees; - val hset_defss' = transpose hset_defss; - val hset_namess = map (map (fst o Term.dest_Const o Morphism.term phi)) hset_frees; - - fun mk_hset ss i j T = - let - val Ts = map fastype_of ss; - val bTs = map domain_type Ts; - val hsetT = Library.foldr (op -->) (Ts, nth bTs (i - 1) --> HOLogic.mk_setT T); - in - Term.list_comb (Const (nth (nth hset_namess (i - 1)) (j - 1), hsetT), ss) - end; - - val hsetssAs = map (fn i => map2 (mk_hset ss i) ls passiveAs) ks; - - val (set_incl_hset_thmss, set_hset_incl_hset_thmsss) = - let - fun mk_set_incl_hset s x set hset = fold_rev Logic.all (x :: ss) - (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (hset $ x))); - - fun mk_set_hset_incl_hset s x y set hset1 hset2 = - fold_rev Logic.all (x :: y :: ss) - (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x, set $ (s $ y))), - HOLogic.mk_Trueprop (mk_leq (hset1 $ x) (hset2 $ y)))); - - val set_incl_hset_goalss = - map4 (fn s => fn x => fn sets => fn hsets => - map2 (mk_set_incl_hset s x) (take m sets) hsets) - ss zs setssAs hsetssAs; - - (*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 si => fn yi => fn sets => fn hsetsi => - map3 (fn xk => fn set => fn hsetsk => - map2 (mk_set_hset_incl_hset si xk yi set) hsetsk hsetsi) - zs_copy (drop m sets) hsetssAs) - ss zs setssAs hsetssAs; - in - (map3 (fn goals => fn defs => fn rec_Sucs => - map3 (fn goal => fn def => fn rec_Suc => - Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hset_tac def rec_Suc)) - |> Thm.close_derivation) - goals defs rec_Sucs) - set_incl_hset_goalss hset_defss hset_rec_Sucss, - map3 (fn goalss => fn defsi => fn rec_Sucs => - map3 (fn k => fn goals => fn defsk => - map4 (fn goal => fn defk => fn defi => fn rec_Suc => - Goal.prove_sorry lthy [] [] goal - (K (mk_set_hset_incl_hset_tac n [defk, defi] rec_Suc k)) - |> Thm.close_derivation) - goals defsk defsi rec_Sucs) - ks goalss hset_defss) - set_hset_incl_hset_goalsss hset_defss hset_rec_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 hset_minimal_thms = - let - fun mk_passive_prem set s x K = - Logic.all x (HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (K $ x))); - - fun mk_active_prem s x1 K1 set x2 K2 = - fold_rev Logic.all [x1, x2] - (Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_mem (x2, set $ (s $ 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)) setssAs) ss zs Ks @ - flat (map4 (fn sets => fn s => fn x1 => fn K1 => - map3 (mk_active_prem s x1 K1) (drop m sets) zs_copy Ks) setssAs ss zs Ks)) - ls Kss; - - val hset_rec_minimal_thms = - let - fun mk_conjunct j T i K x = mk_leq (mk_hset_rec ss nat i j T $ x) (K $ x); - fun mk_concl j T Ks = list_all_free zs - (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs)); - 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 hset_rec_0s => fn hset_rec_Sucs => - singleton (Proof_Context.export names_lthy lthy) - (Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => mk_hset_rec_minimal_tac ctxt m cts hset_rec_0s - hset_rec_Sucs)) - |> Thm.close_derivation) - goals ctss hset_rec_0ss' hset_rec_Sucss' - end; - - fun mk_conjunct j T i K x = mk_leq (mk_hset ss i j T $ x) (K $ x); - fun mk_concl j T Ks = Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks zs); - val concls = map3 mk_concl ls passiveAs Kss; - - val goals = map3 (fn Ks => fn prems => fn concl => - fold_rev Logic.all (Ks @ ss @ zs) - (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))) Kss premss concls; - in - map3 (fn goal => fn hset_defs => fn hset_rec_minimal => - Goal.prove_sorry lthy [] [] goal - (fn {context = ctxt, prems = _} => mk_hset_minimal_tac ctxt n hset_defs - hset_rec_minimal) - |> Thm.close_derivation) - goals hset_defss' hset_rec_minimal_thms - end; - - val timer = time (timer "Hereditary sets"); - (* bisimulation *) val bis_bind = mk_internal_b bisN; @@ -1500,8 +1296,13 @@ val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls; val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs; - val ((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2), - TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), + val emptys = map (fn T => HOLogic.mk_set T []) passiveAs; + val Zeros = map (fn empty => + HOLogic.mk_tuple (map (fn U => absdummy U empty) Ts)) emptys; + val hrecTs = map fastype_of Zeros; + + val (((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2), + TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss), (hrecs, hrecs')), names_lthy) = names_lthy |> mk_Frees' "z" Ts ||>> mk_Frees "y" Ts' @@ -1513,7 +1314,8 @@ ||>> mk_Frees "f" unfold_fTs ||>> mk_Frees "s" corec_sTs ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts) - ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs); + ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs) + ||>> mk_Frees' "rec" hrecTs; fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_"); val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind; @@ -1831,59 +1633,6 @@ val timer = time (timer "coinduction"); - val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks; - val setss_by_range = transpose setss_by_bnf; - - val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) = - let - fun tinst_of dtor = - map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors); - fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts; - val Tinst = map (pairself (certifyT lthy)) - (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts)); - val set_incl_thmss = - map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (tinst_of' dtor) o - Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)) - dtors set_incl_hset_thmss; - - val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE) - val set_minimal_thms = - map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o - Drule.zero_var_indexes) - hset_minimal_thms; - - val set_set_incl_thmsss = - map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o - Drule.instantiate' [] (NONE :: tinst_of' dtor) o - Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))) - dtors set_hset_incl_hset_thmsss; - - val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss); - - val incls = - maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @ - @{thms subset_Collect_iff[OF subset_refl]}; - - 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'; - val dtor_set_induct_thms = - map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis => - ((set_minimal - |> Drule.instantiate' [] (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))) - set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss - in - (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms) - end; - fun mk_dtor_map_DEADID_thm dtor_inject map_id0 = trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym]; @@ -1925,15 +1674,16 @@ val gTs = map2 (curry op -->) passiveBs passiveCs; val uTs = map2 (curry op -->) Ts Ts'; - val ((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), - (ys_copy, ys'_copy)), names_lthy) = names_lthy + val (((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)), + (ys_copy, ys'_copy)), Kss), names_lthy) = names_lthy |> mk_Frees' "f" fTs ||>> mk_Frees "f" fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "u" uTs ||>> mk_Frees' "b" Ts' ||>> mk_Frees' "b" Ts' - ||>> mk_Frees' "y" passiveAs; + ||>> mk_Frees' "y" passiveAs + ||>> mk_Freess "K" (map (fn AT => map (fn T => T --> AT) Ts) ATs);; val map_FTFT's = map2 (fn Ds => mk_map_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; @@ -1951,6 +1701,187 @@ val set_bss = map (flat o map2 (fn B => fn b => if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0; + + fun col_bind j = mk_internal_b (colN ^ (if m = 1 then "" else string_of_int j)); + val col_def_bind = rpair [] o Thm.def_binding o col_bind; + + fun col_spec j Zero hrec hrec' = + let + fun mk_Suc dtor setss z z' = + let + val (set, sets) = apfst (fn xs => nth xs (j - 1)) (chop m setss); + fun mk_UN set k = mk_UNION (set $ (dtor $ z)) (mk_nthN n hrec k); + in + Term.absfree z' + (mk_union (set $ (dtor $ z), Library.foldl1 mk_union (map2 mk_UN sets ks))) + end; + + val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec' + (HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs'))); + in + mk_rec_nat Zero Suc + end; + + val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) = + lthy + |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define + ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec'))) + ls Zeros hrecs hrecs' + |>> apsnd split_list o split_list + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy_old lthy; + + val col_defs = map (fn def => Morphism.thm phi def RS meta_eq_to_obj_eq) col_def_frees; + val cols = map (fst o Term.dest_Const o Morphism.term phi) col_frees; + + fun mk_col Ts nat i j T = + let + val hrecT = HOLogic.mk_tupleT (map (fn U => U --> HOLogic.mk_setT T) Ts) + val colT = HOLogic.natT --> hrecT; + in + mk_nthN n (Term.list_comb (Const (nth cols (j - 1), colT), [nat])) i + end; + + val col_0ss = mk_rec_simps n @{thm rec_nat_0_imp} col_defs; + val col_Sucss = mk_rec_simps n @{thm rec_nat_Suc_imp} col_defs; + val col_0ss' = transpose col_0ss; + val col_Sucss' = transpose col_Sucss; + + fun mk_hset 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); @@ -2209,9 +2140,9 @@ val timer = time (timer "set functions for the new codatatypes"); val colss = map2 (fn j => fn T => - map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs; + map (fn i => mk_col Ts nat i j T) ks) ls passiveAs; val colss' = map2 (fn j => fn T => - map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs; + map (fn i => mk_col Ts' nat i j T) ks) ls passiveBs; val col_natural_thmss = let @@ -2233,7 +2164,7 @@ (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss)) |> Thm.close_derivation) - goals ctss hset_rec_0ss' hset_rec_Sucss'; + goals ctss col_0ss' col_Sucss'; in map (split_conj_thm o mk_specN n) thms end; @@ -2257,7 +2188,7 @@ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)) |> Thm.close_derivation) - ls goals ctss hset_rec_0ss' hset_rec_Sucss'; + ls goals ctss col_0ss' col_Sucss'; in map (split_conj_thm o mk_specN n) thms end; @@ -2312,8 +2243,8 @@ Jrel_unabs_defs; val fold_Jsets = fold_thms lthy Jset_unabs_defs; - val dtor_Jset_incl_thmss = map (map fold_Jsets) hset_dtor_incl_thmss; - val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) hset_hset_dtor_incl_thmsss; + 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; @@ -2487,9 +2418,8 @@ val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms; val map_cong0_tacs = map (fn thm => fn ctxt => mk_map_cong0_tac ctxt m thm) map_cong0_thms; val set_map0_tacss = - map2 (map2 (fn def => fn col => fn ctxt => - unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col)) - hset_defss (transpose col_natural_thmss); + map (map (fn col => fn ctxt => unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac col)) + (transpose col_natural_thmss); val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs; val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs; @@ -2498,9 +2428,9 @@ val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites; val set_bd_tacss = - map3 (fn Cinf => map2 (fn def => fn col => fn ctxt => - unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col)) - Jbd_Cinfinites hset_defss (transpose col_bd_thmss); + map2 (fn Cinf => map (fn col => fn ctxt => + unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf col)) + Jbd_Cinfinites (transpose col_bd_thmss); val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks; diff -r d397030fb27e -r e3b8f8319d73 src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 13 08:56:08 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Mar 13 11:15:04 2014 +0100 @@ -32,8 +32,8 @@ 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 list -> thm -> tactic - val mk_hset_rec_minimal_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> + val mk_hset_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 val mk_length_Lev'_tac: thm -> tactic @@ -56,7 +56,7 @@ val mk_mor_case_sum_tac: 'a list -> thm -> tactic val mk_mor_comp_tac: thm -> thm list -> thm list -> thm list -> tactic val mk_mor_elim_tac: thm -> tactic - val mk_mor_hset_rec_tac: int -> int -> cterm option list -> int -> thm list -> thm list -> + val mk_mor_col_tac: int -> int -> cterm option list -> int -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_mor_incl_tac: thm -> thm list -> tactic val mk_mor_str_tac: 'a list -> thm -> tactic @@ -74,14 +74,14 @@ val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic 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 -> thm -> tactic - val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic + val mk_set_bd_tac: thm -> thm -> tactic + val mk_set_hset_incl_hset_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 -> thm -> tactic + val mk_set_incl_hset_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 -> thm -> tactic + val mk_set_map0_tac: thm -> tactic val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic val mk_unfold_transfer_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm list -> tactic @@ -160,18 +160,15 @@ fun mk_mor_case_sum_tac ks mor_UNIV = (stac mor_UNIV THEN' CONJ_WRAP' (K (rtac @{thm case_sum_o_inj(1)[symmetric]})) ks) 1; -fun mk_set_incl_hset_tac def rec_Suc = - EVERY' (stac def :: - map rtac [@{thm SUP_upper2}, UNIV_I, @{thm ord_le_eq_trans}, @{thm Un_upper1}, - sym, rec_Suc]) 1; +fun mk_set_incl_hset_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 defs rec_Suc i = - EVERY' (map (TRY oo stac) defs @ - 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; +fun mk_set_hset_incl_hset_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; -fun mk_hset_rec_minimal_tac ctxt m cts rec_0s rec_Sucs = +fun mk_col_minimal_tac ctxt m cts rec_0s rec_Sucs = EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, CONJ_WRAP' (fn thm => EVERY' @@ -186,13 +183,12 @@ rtac subset_trans, atac, Goal.assume_rule_tac ctxt])) rec_0s]) rec_Sucs] 1; -fun mk_hset_minimal_tac ctxt n hset_defs hset_rec_minimal = - (CONJ_WRAP' (fn def => (EVERY' [rtac ord_eq_le_trans, rtac def, - rtac @{thm UN_least}, rtac rev_mp, rtac hset_rec_minimal, +fun mk_hset_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])) hset_defs) 1 + REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) (1 upto n)) 1 -fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss = +fun mk_mor_col_tac m n cts j rec_0s rec_Sucs morEs set_map0ss coalg_setss = EVERY' [rtac (Drule.instantiate' [] cts nat_induct), REPEAT_DETERM o rtac allI, CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s, @@ -873,10 +869,9 @@ (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1 end; -fun mk_set_map0_tac hset_def col_natural = - EVERY' (map rtac [@{thm ext}, o_apply RS trans, hset_def RS trans, sym, - o_apply RS trans, @{thm image_cong} OF [hset_def, refl] RS trans, - @{thm image_UN} RS trans, refl RS @{thm UN_cong}, col_natural]) 1; +fun mk_set_map0_tac col_natural = + EVERY' (map rtac [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans, + refl RS @{thm UN_cong}, col_natural]) 1; fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss = let @@ -897,9 +892,8 @@ (rec_Sucs ~~ set_sbdss)] 1 end; -fun mk_set_bd_tac sbd_Cinfinite hset_def col_bd = - EVERY' (map rtac [ordIso_ordLeq_trans, @{thm card_of_ordIso_subst}, hset_def, - @{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, +fun mk_set_bd_tac sbd_Cinfinite col_bd = + EVERY' (map rtac [@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat}, @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1; fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs =