# HG changeset patch # User wenzelm # Date 1408364363 -7200 # Node ID 381b3c4fc75ad85ee66df8ef732fd230eb862e65 # Parent 07e81758788d6edb4ead1cbbcf7a069169b6b795# Parent fc136831d6cad9c5df83d043c3591ec930e77801 merged diff -r fc136831d6ca -r 381b3c4fc75a src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 13:19:04 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Aug 18 14:19:23 2014 +0200 @@ -913,6 +913,12 @@ \begin{indentblock} \begin{description} +\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\ +@{thm list.inj_map[no_vars]} + +\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\ +@{thm list.inj_map_strong[no_vars]} + \item[@{text "t."}\hthm{set_map}\rm:] ~ \\ @{thm list.set_map[no_vars]} diff -r fc136831d6ca -r 381b3c4fc75a src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 13:19:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 14:19:23 2014 +0200 @@ -55,6 +55,7 @@ val in_mono_of_bnf: bnf -> thm val in_rel_of_bnf: bnf -> thm val inj_map_of_bnf: bnf -> thm + val inj_map_strong_of_bnf: bnf -> thm val map_comp0_of_bnf: bnf -> thm val map_comp_of_bnf: bnf -> thm val map_cong0_of_bnf: bnf -> thm @@ -73,6 +74,7 @@ val rel_cong_of_bnf: bnf -> thm val rel_conversep_of_bnf: bnf -> thm val rel_mono_of_bnf: bnf -> thm + val rel_mono_strong0_of_bnf: bnf -> thm val rel_mono_strong_of_bnf: bnf -> thm val rel_eq_of_bnf: bnf -> thm val rel_flip_of_bnf: bnf -> thm @@ -222,6 +224,7 @@ in_mono: thm lazy, in_rel: thm lazy, inj_map: thm lazy, + inj_map_strong: thm lazy, map_comp: thm lazy, map_cong: thm lazy, map_id: thm lazy, @@ -234,6 +237,7 @@ rel_cong: thm lazy, rel_map: thm list lazy, rel_mono: thm lazy, + rel_mono_strong0: thm lazy, rel_mono_strong: thm lazy, rel_Grp: thm lazy, rel_conversep: thm lazy, @@ -241,8 +245,9 @@ }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map - rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { + inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq + rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong rel_Grp + rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -252,6 +257,7 @@ in_mono = in_mono, in_rel = in_rel, inj_map = inj_map, + inj_map_strong = inj_map_strong, map_comp = map_comp, map_cong = map_cong, map_id = map_id, @@ -264,6 +270,7 @@ rel_cong = rel_cong, rel_map = rel_map, rel_mono = rel_mono, + rel_mono_strong0 = rel_mono_strong0, rel_mono_strong = rel_mono_strong, rel_Grp = rel_Grp, rel_conversep = rel_conversep, @@ -279,6 +286,7 @@ in_mono, in_rel, inj_map, + inj_map_strong, map_comp, map_cong, map_id, @@ -291,6 +299,7 @@ rel_cong, rel_map, rel_mono, + rel_mono_strong0, rel_mono_strong, rel_Grp, rel_conversep, @@ -304,6 +313,7 @@ in_mono = Lazy.map f in_mono, in_rel = Lazy.map f in_rel, inj_map = Lazy.map f inj_map, + inj_map_strong = Lazy.map f inj_map_strong, map_comp = Lazy.map f map_comp, map_cong = Lazy.map f map_cong, map_id = Lazy.map f map_id, @@ -316,6 +326,7 @@ rel_cong = Lazy.map f rel_cong, rel_map = Lazy.map (map f) rel_map, rel_mono = Lazy.map f rel_mono, + rel_mono_strong0 = Lazy.map f rel_mono_strong0, rel_mono_strong = Lazy.map f rel_mono_strong, rel_Grp = Lazy.map f rel_Grp, rel_conversep = Lazy.map f rel_conversep, @@ -425,6 +436,7 @@ val in_mono_of_bnf = Lazy.force o #in_mono o #facts o rep_bnf; val in_rel_of_bnf = Lazy.force o #in_rel o #facts o rep_bnf; val inj_map_of_bnf = Lazy.force o #inj_map o #facts o rep_bnf; +val inj_map_strong_of_bnf = Lazy.force o #inj_map_strong o #facts o rep_bnf; val map_def_of_bnf = #map_def o #defs o rep_bnf; val map_id0_of_bnf = #map_id0 o #axioms o rep_bnf; val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf; @@ -445,6 +457,7 @@ val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf; val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf; +val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf; val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf; val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf; val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf; @@ -598,6 +611,7 @@ val in_monoN = "in_mono"; val in_relN = "in_rel"; val inj_mapN = "inj_map"; +val inj_map_strongN = "inj_map_strong"; val map_id0N = "map_id0"; val map_idN = "map_id"; val map_identN = "map_ident"; @@ -615,6 +629,7 @@ val rel_conversepN = "rel_conversep"; val rel_mapN = "rel_map" val rel_monoN = "rel_mono" +val rel_mono_strong0N = "rel_mono_strong0" val rel_mono_strongN = "rel_mono_strong" val rel_comppN = "rel_compp"; val rel_compp_GrpN = "rel_compp_Grp"; @@ -652,9 +667,9 @@ (in_bdN, [Lazy.force (#in_bd facts)]), (in_monoN, [Lazy.force (#in_mono facts)]), (in_relN, [Lazy.force (#in_rel facts)]), - (inj_mapN, [Lazy.force (#inj_map facts)]), (map_comp0N, [#map_comp0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), + (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]), (set_map0N, #set_map0 axioms), (set_bdN, #set_bd axioms)] @ @@ -669,7 +684,9 @@ fun note_unless_dont_note (noted0, lthy0) = let val notes = - [(map_compN, [Lazy.force (#map_comp facts)], []), + [(inj_mapN, [Lazy.force (#inj_map facts)], []), + (inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []), + (map_compN, [Lazy.force (#map_comp facts)], []), (map_cong0N, [#map_cong0 axioms], []), (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs), (map_idN, [Lazy.force (#map_id facts)], []), @@ -948,16 +965,19 @@ fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel; val pre_names_lthy = lthy; - val ((((((((((((((((((fs, gs), hs), is), x), y), zs), ys), As), + val (((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As), As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy |> mk_Frees "f" (map2 (curry op -->) As' Bs') + ||>> mk_Frees "f" (map2 (curry op -->) As' Bs') ||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs) ||>> mk_Frees "h" (map2 (curry op -->) As' Ts) ||>> mk_Frees "i" (map2 (curry op -->) As' Cs) ||>> yield_singleton (mk_Frees "x") CA' + ||>> yield_singleton (mk_Frees "x") CA' ||>> yield_singleton (mk_Frees "y") CB' ||>> mk_Frees "z" As' + ||>> mk_Frees "z" As' ||>> mk_Frees "y" Bs' ||>> mk_Frees "A" (map HOLogic.mk_setT As') ||>> mk_Frees "A" (map HOLogic.mk_setT As') @@ -1299,7 +1319,7 @@ val rel_flip = Lazy.lazy mk_rel_flip; - fun mk_rel_mono_strong () = + fun mk_rel_mono_strong0 () = let fun mk_prem setA setB R S a b = HOLogic.mk_Trueprop @@ -1312,11 +1332,15 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl))) - (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel) + (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel) (map Lazy.force set_map)) |> Thm.close_derivation end; + val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0; + + fun mk_rel_mono_strong () = Object_Logic.rulify lthy (Lazy.force rel_mono_strong0) + val rel_mono_strong = Lazy.lazy mk_rel_mono_strong; fun mk_rel_map () = @@ -1334,12 +1358,13 @@ mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y]; val goals = map2 mk_goal lhss rhss; in - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + goals + |> map (fn goal => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_rel_map0_tac ctxt live (Lazy.force rel_OO) (Lazy.force rel_conversep) - (Lazy.force rel_Grp) (Lazy.force map_id)) - |> Conjunction.elim_balanced (length goals) - |> map (unfold_thms lthy @{thms vimage2p_def id_apply}) + (Lazy.force rel_Grp) (Lazy.force map_id))) + |> map (unfold_thms lthy @{thms vimage2p_def[of id, unfolded id_apply] + vimage2p_def[of _ id, unfolded id_apply]}) |> map Thm.close_derivation end; @@ -1364,11 +1389,36 @@ val map_transfer = Lazy.lazy mk_map_transfer; + fun mk_inj_map_strong () = + let + val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' => + fold_rev Logic.all [z, z'] + (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x), + Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'), + Logic.mk_implies (mk_Trueprop_eq (f $ z, f' $ z'), + mk_Trueprop_eq (z, z')))))) bnf_sets_As zs fs zs' fs'; + val concl = Logic.mk_implies + (mk_Trueprop_eq + (Term.list_comb (bnf_map_AsBs, fs) $ x, + Term.list_comb (bnf_map_AsBs, fs') $ x'), + mk_Trueprop_eq (x, x')); + val goal = fold_rev Logic.all (x :: x' :: fs @ fs') + (fold_rev (curry Logic.mk_implies) assms concl); + in + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => + mk_inj_map_strong_tac ctxt (Lazy.force rel_eq) (Lazy.force rel_map) + (Lazy.force rel_mono_strong)) + |> Thm.close_derivation + end; + + val inj_map_strong = Lazy.lazy mk_inj_map_strong; + val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def; val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong - in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq - rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; + in_mono in_rel inj_map inj_map_strong map_comp map_cong map_id map_ident0 map_ident + map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 + rel_mono_strong rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; diff -r fc136831d6ca -r 381b3c4fc75a src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 13:19:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 14:19:23 2014 +0200 @@ -11,6 +11,7 @@ sig val mk_collect_set_map_tac: thm list -> tactic val mk_in_mono_tac: int -> tactic + val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic val mk_map_id: thm -> thm val mk_map_ident: Proof.context -> thm -> thm @@ -25,7 +26,7 @@ val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic val mk_rel_mono_tac: thm list -> thm -> tactic - val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic + val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic @@ -70,6 +71,17 @@ REPEAT_DETERM_N n o atac)) end; +fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong = + let + val rel_eq' = rel_eq RS @{thm predicate2_eqD}; + val rel_maps' = map (fn thm => thm RS iffD1) rel_maps; + in + HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN + EVERY (map (HEADGOAL o dtac) rel_maps') THEN + HEADGOAL (etac rel_mono_strong) THEN + TRYALL (Goal.assume_rule_tac ctxt) + end; + fun mk_collect_set_map_tac set_map0s = (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN' EVERY' (map (fn set_map0 => @@ -197,7 +209,7 @@ REPEAT_DETERM_N n o rtac @{thm fst_fstOp}, in_tac @{thm fstOp_in}, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0, - REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, + REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst, rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE, etac set_mp, atac], @@ -211,7 +223,7 @@ in_tac @{thm sndOp_in}] 1 end; -fun mk_rel_mono_strong_tac ctxt in_rel set_maps = +fun mk_rel_mono_strong0_tac ctxt in_rel set_maps = if null set_maps then atac 1 else unfold_tac ctxt [in_rel] THEN @@ -252,10 +264,10 @@ let val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1}; val inserts = - map (fn set_bd => + map (fn set_bd => iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]]) - set_bds; + set_bds; in EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound}, rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order}, diff -r fc136831d6ca -r 381b3c4fc75a src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Aug 18 13:19:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Mon Aug 18 14:19:23 2014 +0200 @@ -167,7 +167,7 @@ val map_id0s = map map_id0_of_bnf bnfs; val map_ids = map map_id_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; - val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs; + val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs; val le_rel_OOs = map le_rel_OO_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -1691,7 +1691,7 @@ in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms - ctor_Irel_thms rel_mono_strongs le_rel_OOs) + ctor_Irel_thms rel_mono_strong0s le_rel_OOs) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -1762,7 +1762,7 @@ val Irel_induct_thm = mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks - ctor_Irel_thms rel_mono_strongs) lthy; + ctor_Irel_thms rel_mono_strong0s) lthy; val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; val ctor_fold_transfer_thms = diff -r fc136831d6ca -r 381b3c4fc75a src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Aug 18 13:19:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Aug 18 14:19:23 2014 +0200 @@ -582,7 +582,7 @@ (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1 end; -fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs = +fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs = EVERY' (rtac induct :: map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO => EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}), @@ -592,7 +592,7 @@ REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac], REPEAT_DETERM_N (length le_rel_OOs) o EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]]) - ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1; + ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1; (* BNF tactics *) @@ -701,19 +701,19 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; -fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs = +fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s = let val n = length ks; in unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2, - EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong => + EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 => EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp), - etac rel_mono_strong, + etac rel_mono_strong0, REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]}, EVERY' (map (fn j => EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]}, Goal.assume_rule_tac ctxt]) ks)]) - IHs ctor_rels rel_mono_strongs)] 1 + IHs ctor_rels rel_mono_strong0s)] 1 end; fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =