# HG changeset patch # User desharna # Date 1408363749 -7200 # Node ID eaa986cd285a8189c48def9722ad59853bbaa3c8 # Parent 1e7b9579b14fc50d2cb832f35943177defea97dc generate 'inj_map_strong' for BNFs diff -r 1e7b9579b14f -r eaa986cd285a src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 13:49:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Aug 18 14:09:09 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 @@ -223,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, @@ -243,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_strong0 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, @@ -254,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, @@ -282,6 +286,7 @@ in_mono, in_rel, inj_map, + inj_map_strong, map_comp, map_cong, map_id, @@ -308,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, @@ -430,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; @@ -604,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"; @@ -677,6 +685,7 @@ let val notes = [(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), @@ -956,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') @@ -1346,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; @@ -1376,12 +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_strong0 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 1e7b9579b14f -r eaa986cd285a src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 13:49:47 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Aug 18 14:09:09 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 @@ -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], @@ -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},