# HG changeset patch # User traytel # Date 1443090495 -7200 # Node ID 1f92b0ac9c96cb26b5627520b20db8cf4883ff5f # Parent 69a97fc33f7a3b7a6fc56372285f490bedc7edb7 congruence rules for the relator diff -r 69a97fc33f7a -r 1f92b0ac9c96 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 12:21:19 2015 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 24 12:28:15 2015 +0200 @@ -1000,6 +1000,15 @@ The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin (Section~\ref{ssec:lifting}). +\item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\ +@{thm list.rel_mono_strong[no_vars]} + +\item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\ +@{thm list.rel_cong[no_vars]} + +\item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\ +@{thm list.rel_cong_simp[no_vars]} + \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\ @{thm list.rel_refl[no_vars]} diff -r 69a97fc33f7a -r 1f92b0ac9c96 src/HOL/Tools/BNF/bnf_comp.ML --- a/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_comp.ML Thu Sep 24 12:28:15 2015 +0200 @@ -325,13 +325,12 @@ fun rel_OO_Grp_tac ctxt = let val outer_rel_Grp = rel_Grp_of_bnf outer RS sym; - val outer_rel_cong = rel_cong_of_bnf outer; 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, outer_rel_cong OF + 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 @@ -441,7 +440,7 @@ 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_cong_of_bnf bnf OF + 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 diff -r 69a97fc33f7a -r 1f92b0ac9c96 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Thu Sep 24 12:28:15 2015 +0200 @@ -76,7 +76,9 @@ val rel_Grp_of_bnf: bnf -> thm val rel_OO_of_bnf: bnf -> thm val rel_OO_Grp_of_bnf: bnf -> thm + val rel_cong0_of_bnf: bnf -> thm val rel_cong_of_bnf: bnf -> thm + val rel_cong_simp_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 @@ -248,7 +250,9 @@ rel_eq: thm lazy, rel_flip: thm lazy, set_map: thm lazy list, + rel_cong0: thm lazy, rel_cong: thm lazy, + rel_cong_simp: thm lazy, rel_map: thm list lazy, rel_mono: thm lazy, rel_mono_strong0: thm lazy, @@ -267,9 +271,9 @@ fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp 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 set_transfer - rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp - rel_transfer = { + rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0 + rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp + rel_symp rel_transp rel_transfer = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -290,7 +294,9 @@ rel_eq = rel_eq, rel_flip = rel_flip, set_map = set_map, + rel_cong0 = rel_cong0, rel_cong = rel_cong, + rel_cong_simp = rel_cong_simp, rel_map = rel_map, rel_mono = rel_mono, rel_mono_strong0 = rel_mono_strong0, @@ -327,7 +333,9 @@ rel_eq, rel_flip, set_map, + rel_cong0, rel_cong, + rel_cong_simp, rel_map, rel_mono, rel_mono_strong0, @@ -362,7 +370,9 @@ rel_eq = Lazy.map f rel_eq, rel_flip = Lazy.map f rel_flip, set_map = map (Lazy.map f) set_map, + rel_cong0 = Lazy.map f rel_cong0, rel_cong = Lazy.map f rel_cong, + rel_cong_simp = Lazy.map f rel_cong_simp, rel_map = Lazy.map (map f) rel_map, rel_mono = Lazy.map f rel_mono, rel_mono_strong0 = Lazy.map f rel_mono_strong0, @@ -503,7 +513,9 @@ val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf; val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf; val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf; +val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf; val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf; +val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp 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; @@ -695,6 +707,8 @@ val rel_monoN = "rel_mono"; val rel_mono_strong0N = "rel_mono_strong0"; val rel_mono_strongN = "rel_mono_strong"; +val rel_congN = "rel_cong"; +val rel_cong_simpN = "rel_cong_simp"; val rel_reflN = "rel_refl"; val rel_refl_strongN = "rel_refl_strong"; val rel_reflpN = "rel_reflp"; @@ -771,6 +785,8 @@ (rel_mapN, Lazy.force (#rel_map facts), []), (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs), (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []), + (rel_congN, [Lazy.force (#rel_cong facts)], fundefcong_attrs), + (rel_cong_simpN, [Lazy.force (#rel_cong_simp facts)], []), (rel_reflN, [Lazy.force (#rel_refl facts)], []), (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []), (rel_reflpN, [Lazy.force (#rel_reflp facts)], []), @@ -1066,7 +1082,7 @@ fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel; val pre_names_lthy = lthy; - val ((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As), + val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As), As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs), transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy |> mk_Frees "f" (map2 (curry op -->) As' Bs') @@ -1077,6 +1093,7 @@ ||>> yield_singleton (mk_Frees "x") CA' ||>> yield_singleton (mk_Frees "x") CA' ||>> yield_singleton (mk_Frees "y") CB' + ||>> yield_singleton (mk_Frees "y") CB' ||>> mk_Frees "z" As' ||>> mk_Frees "z" As' ||>> mk_Frees "y" Bs' @@ -1093,7 +1110,8 @@ ||>> mk_Frees "S" transfer_ranRTs; val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs; - val x_copy = retype_const_or_free CA' y; + val x_copy = retype_const_or_free CA' y'; + val y_copy = retype_const_or_free CB' x'; val rel = mk_bnf_rel pred2RTs CA' CB'; val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE'; @@ -1322,7 +1340,7 @@ val rel_Grp = Lazy.lazy mk_rel_Grp; - fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy + fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy; fun mk_rel_concl f = HOLogic.mk_Trueprop (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy))); @@ -1338,7 +1356,7 @@ |> Thm.close_derivation end; - fun mk_rel_cong () = + fun mk_rel_cong0 () = let val cong_prems = mk_rel_prems (curry HOLogic.mk_eq); val cong_concl = mk_rel_concl HOLogic.mk_eq; @@ -1350,14 +1368,14 @@ end; val rel_mono = Lazy.lazy mk_rel_mono; - val rel_cong = Lazy.lazy mk_rel_cong; + val rel_cong0 = Lazy.lazy mk_rel_cong0; fun mk_rel_eq () = Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'), HOLogic.eq_const CA')) (fn {context = ctxt, prems = _} => - mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms)) + mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms)) |> Thm.close_derivation; val rel_eq = Lazy.lazy mk_rel_eq; @@ -1433,6 +1451,30 @@ val rel_mono_strong = Lazy.lazy mk_rel_mono_strong; + fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy = + Logic.all z (Logic.all z' + (mk_implies (mk_Trueprop_mem (z, set $ x), mk_implies (mk_Trueprop_mem (z', set' $ x'), + mk_Trueprop_eq (R $ z $ z', R_copy $ z $ z'))))); + + fun mk_rel_cong mk_implies () = + let + val prem0 = mk_Trueprop_eq (x, x_copy); + val prem1 = mk_Trueprop_eq (y, y_copy); + val prems = @{map 6} (mk_rel_cong_prem mk_implies x_copy y_copy) + zs ys bnf_sets_As bnf_sets_Bs Rs Rs_copy; + val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y, + Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy); + in + Goal.prove_sorry lthy [] (prem0 :: prem1 :: prems) eq + (fn {context = ctxt, prems} => + mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong)) + |> Thm.close_derivation + |> singleton (Proof_Context.export names_lthy lthy) + end; + + val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies); + val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b)); + fun mk_rel_map () = let fun mk_goal lhs rhs = @@ -1579,9 +1621,9 @@ val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp 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 set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong - rel_reflp rel_symp rel_transp rel_transfer; + map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map + rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO + rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer; val wits = map2 mk_witness bnf_wits wit_thms; diff -r 69a97fc33f7a -r 1f92b0ac9c96 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Thu Sep 24 12:28:15 2015 +0200 @@ -28,6 +28,7 @@ val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic + val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic @@ -356,4 +357,15 @@ REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN' rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps); +fun mk_rel_cong_tac ctxt (eqs, prems) mono = + let + fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt; + fun mk_tacs iffD = etac ctxt mono :: + map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD) + |> Drule.rotate_prems ~1 |> mk_tac) prems; + in + unfold_thms_tac ctxt eqs THEN + HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2)) + end; + end; diff -r 69a97fc33f7a -r 1f92b0ac9c96 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 24 12:21:19 2015 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 24 12:28:15 2015 +0200 @@ -219,7 +219,7 @@ val map_ids = map map_id_of_bnf bnfs; val set_bdss = map set_bd_of_bnf bnfs; val set_mapss = map set_map_of_bnf bnfs; - val rel_congs = map rel_cong_of_bnf bnfs; + val rel_congs = map rel_cong0_of_bnf bnfs; val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; val le_rel_OOs = map le_rel_OO_of_bnf bnfs;