# HG changeset patch # User desharna # Date 1409570619 -7200 # Node ID c5316f843f72aef18c0d2c773699ec68e2a983cc # Parent c23bdb4ed2f6955751c5f5bbfa074233d6c946d5 generate 'rel_transfer' for BNFs diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/BNF_Def.thy Mon Sep 01 13:23:39 2014 +0200 @@ -15,6 +15,9 @@ "bnf" :: thy_goal begin +lemma Collect_splitD: "x \ Collect (split A) \ A (fst x) (snd x)" + by auto + definition rel_fun :: "('a \ 'c \ bool) \ ('b \ 'd \ bool) \ ('a \ 'b) \ ('c \ 'd) \ bool" where @@ -30,6 +33,20 @@ shows "B (f x) (g y)" using assms by (simp add: rel_fun_def) +definition rel_set :: "('a \ 'b \ bool) \ 'a set \ 'b set \ bool" + where "rel_set R = (\A B. (\x\A. \y\B. R x y) \ (\y\B. \x\A. R x y))" + +lemma rel_setI: + assumes "\x. x \ A \ \y\B. R x y" + assumes "\y. y \ B \ \x\A. R x y" + shows "rel_set R A B" + using assms unfolding rel_set_def by simp + +lemma predicate2_transferD: + "\rel_fun R1 (rel_fun R2 (op =)) P Q; a \ A; b \ B; A \ {(x, y). R1 x y}; B \ {(x, y). R2 x y}\ \ + P (fst a) (fst b) \ Q (snd a) (snd b)" + unfolding rel_fun_def by (blast dest!: Collect_splitD) + definition collect where "collect F x = (\f \ F. f x)" diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/BNF_GFP.thy --- a/src/HOL/BNF_GFP.thy Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/BNF_GFP.thy Mon Sep 01 13:23:39 2014 +0200 @@ -226,9 +226,6 @@ lemma not_arg_cong_Inr: "x \ y \ Inr x \ Inr y" by simp -lemma Collect_splitD: "x \ Collect (split A) \ A (fst x) (snd x)" - by auto - definition image2p where "image2p f g R = (\x y. \x' y'. R x' y' \ f x' = x \ g y' = y)" diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/Lifting_Set.thy --- a/src/HOL/Lifting_Set.thy Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/Lifting_Set.thy Mon Sep 01 13:23:39 2014 +0200 @@ -10,15 +10,6 @@ subsection {* Relator and predicator properties *} -definition rel_set :: "('a \ 'b \ bool) \ 'a set \ 'b set \ bool" - where "rel_set R = (\A B. (\x\A. \y\B. R x y) \ (\y\B. \x\A. R x y))" - -lemma rel_setI: - assumes "\x. x \ A \ \y\B. R x y" - assumes "\y. y \ B \ \x\A. R x y" - shows "rel_set R A B" - using assms unfolding rel_set_def by simp - lemma rel_setD1: "\ rel_set R A B; x \ A \ \ \y \ B. R x y" and rel_setD2: "\ rel_set R A B; y \ B \ \ \x \ A. R x y" by(simp_all add: rel_set_def) diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Mon Sep 01 13:23:39 2014 +0200 @@ -89,7 +89,8 @@ val mk_map: int -> typ list -> typ list -> term -> term val mk_rel: int -> typ list -> typ list -> term -> term val build_map: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term - val build_rel: Proof.context -> typ list -> (typ * typ -> term) -> typ * typ -> term + val build_rel: (string * (int * term)) list -> Proof.context -> typ list -> (typ * typ -> term) -> + typ * typ -> term val flatten_type_args_of_bnf: bnf -> 'a -> 'a list -> 'a list val map_flattened_map_args: Proof.context -> string -> (term list -> 'a list) -> term list -> 'a list @@ -241,6 +242,7 @@ rel_mono: thm lazy, rel_mono_strong0: thm lazy, rel_mono_strong: thm lazy, + rel_transfer: thm lazy, rel_Grp: thm lazy, rel_conversep: thm lazy, rel_OO: thm lazy @@ -249,7 +251,7 @@ 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 - rel_Grp rel_conversep rel_OO = { + rel_transfer rel_Grp rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, bd_Cnotzero = bd_Cnotzero, @@ -275,6 +277,7 @@ rel_mono = rel_mono, rel_mono_strong0 = rel_mono_strong0, rel_mono_strong = rel_mono_strong, + rel_transfer = rel_transfer, rel_Grp = rel_Grp, rel_conversep = rel_conversep, rel_OO = rel_OO}; @@ -305,6 +308,7 @@ rel_mono, rel_mono_strong0, rel_mono_strong, + rel_transfer, rel_Grp, rel_conversep, rel_OO} = @@ -333,6 +337,7 @@ 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_transfer = Lazy.map f rel_transfer, rel_Grp = Lazy.map f rel_Grp, rel_conversep = Lazy.map f rel_conversep, rel_OO = Lazy.map f rel_OO}; @@ -465,6 +470,7 @@ 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_transfer_of_bnf = Lazy.force o #rel_transfer 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; val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf; @@ -563,7 +569,7 @@ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t end; -fun build_map_or_rel is_rel mk const of_bnf dest ctxt simpleTs build_simple = +fun build_map_or_rel mk const of_bnf dest pre_cst_table ctxt simpleTs build_simple = let fun build (TU as (T, U)) = if exists (curry (op =) T) simpleTs then @@ -576,18 +582,19 @@ if s = s' then let val (live, cst0) = - if is_rel andalso s = @{type_name fun} then (2, @{term rel_fun}) - else let val bnf = the (bnf_of ctxt s) in (live_of_bnf bnf, of_bnf bnf) end; + (case AList.lookup (op =) pre_cst_table s of + NONE => let val bnf = the (bnf_of ctxt s) in (live_of_bnf bnf, of_bnf bnf) end + | SOME p => p); val cst = mk live Ts Us cst0; val TUs' = map dest (fst (strip_typeN live (fastype_of cst))); in Term.list_comb (cst, map build TUs') end - else - build_simple TU + else build_simple TU | _ => build_simple TU); in build end; -val build_map = build_map_or_rel false mk_map HOLogic.id_const map_of_bnf dest_funT; -val build_rel = build_map_or_rel true mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T; +val build_map = build_map_or_rel mk_map HOLogic.id_const map_of_bnf dest_funT []; +val build_rel = build_map_or_rel mk_rel HOLogic.eq_const rel_of_bnf dest_pred2T o append + [(@{type_name set}, (1, @{term rel_set})), (@{type_name fun}, (2, @{term rel_fun}))]; fun map_flattened_map_args ctxt s map_args fs = let @@ -639,6 +646,7 @@ val rel_monoN = "rel_mono" val rel_mono_strong0N = "rel_mono_strong0" val rel_mono_strongN = "rel_mono_strong" +val rel_transferN = "rel_transfer" val rel_comppN = "rel_compp"; val rel_compp_GrpN = "rel_compp_Grp"; @@ -686,7 +694,7 @@ [(thms, [])])); in Local_Theory.notes notes lthy0 |>> append noted0 - end + end; fun note_unless_dont_note (noted0, lthy0) = let @@ -709,6 +717,7 @@ (rel_GrpN, [Lazy.force (#rel_Grp facts)], []), (rel_mapN, Lazy.force (#rel_map facts), []), (rel_monoN, [Lazy.force (#rel_mono facts)], []), + (rel_transferN, [Lazy.force (#rel_transfer facts)], []), (set_mapN, map Lazy.force (#set_map facts), [])] |> filter_out (null o #2) |> map (fn (thmN, thms, attrs) => @@ -716,7 +725,7 @@ [(thms, [])])); in Local_Theory.notes notes lthy0 |>> append noted0 - end + end; in ([], lthy) |> fact_policy = Note_All ? note_if_note_all @@ -934,13 +943,14 @@ val dead = length deads; - val ((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), (Ts, T)) = lthy + val (((((((As', Bs'), Cs), Ds), Es), B1Ts), B2Ts), (Ts, T)) = lthy |> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees live ||>> mk_TFrees dead ||>> mk_TFrees live ||>> mk_TFrees live + ||>> mk_TFrees live ||> fst o mk_TFrees 1 ||> the_single ||> `(replicate live); @@ -952,7 +962,9 @@ val pred2RTs = map2 mk_pred2T As' Bs'; val pred2RTsAsCs = map2 mk_pred2T As' Cs; val pred2RTsBsCs = map2 mk_pred2T Bs' Cs; + val pred2RTsBsEs = map2 mk_pred2T Bs' Es; val pred2RTsCsBs = map2 mk_pred2T Cs Bs'; + val pred2RTsCsEs = map2 mk_pred2T Cs Es; val pred2RT's = map2 mk_pred2T Bs' As'; val self_pred2RTs = map2 mk_pred2T As' As'; val transfer_domRTs = map2 mk_pred2T As' B1Ts; @@ -961,6 +973,7 @@ val CA' = mk_bnf_T As' Calpha; val CB' = mk_bnf_T Bs' Calpha; val CC' = mk_bnf_T Cs Calpha; + val CE' = mk_bnf_T Es Calpha; val CB1 = mk_bnf_T B1Ts Calpha; val CB2 = mk_bnf_T B2Ts Calpha; @@ -974,8 +987,8 @@ 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), - As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), + val ((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), 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') ||>> mk_Frees "f" (map2 (curry op -->) As' Bs') @@ -996,6 +1009,7 @@ ||>> mk_Frees "S" pred2RTsBsCs ||>> mk_Frees "S" pred2RTsAsCs ||>> mk_Frees "S" pred2RTsCsBs + ||>> mk_Frees "S" pred2RTsBsEs ||>> mk_Frees "R" transfer_domRTs ||>> mk_Frees "S" transfer_ranRTs; @@ -1003,6 +1017,7 @@ val x_copy = retype_const_or_free CA' y; val rel = mk_bnf_rel pred2RTs CA' CB'; + val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE'; val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; @@ -1165,9 +1180,8 @@ val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy) (Logic.list_implies (prem0 :: prems, eq)); in - Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - unfold_thms_tac lthy @{thms simp_implies_def} THEN - mk_map_cong_tac lthy (#map_cong0 axioms)) + Goal.prove_sorry lthy [] [] goal (K (unfold_thms_tac lthy @{thms simp_implies_def} THEN + mk_map_cong_tac lthy (#map_cong0 axioms))) |> Thm.close_derivation end; @@ -1401,6 +1415,27 @@ val map_transfer = Lazy.lazy mk_map_transfer; + fun mk_rel_transfer () = + let + val iff = HOLogic.eq_const HOLogic.boolT; + val prem_rels = + map2 (fn T1 => fn T2 => mk_rel_fun T1 (mk_rel_fun T2 iff)) S_AsCs S_BsEs; + val prem_elems = + mk_rel_fun (Term.list_comb (mk_bnf_rel pred2RTsAsCs CA' CC', S_AsCs)) + (mk_rel_fun (Term.list_comb (mk_bnf_rel pred2RTsBsEs CB' CE', S_BsEs)) iff); + val goal = + HOLogic.mk_Trueprop (fold_rev mk_rel_fun prem_rels prem_elems $ rel $ relCsEs); + in + Goal.prove_sorry lthy [] [] goal + (fn {context = ctxt, prems = _} => + mk_rel_transfer_tac ctxt (Lazy.force in_rel) (Lazy.force rel_map) + (Lazy.force rel_mono_strong)) + |> singleton (Proof_Context.export names_lthy lthy) + |> Thm.close_derivation + end; + + val rel_transfer = Lazy.lazy mk_rel_transfer; + fun mk_inj_map_strong () = let val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' => @@ -1430,7 +1465,7 @@ 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 rel_Grp rel_conversep rel_OO; + rel_mono_strong rel_transfer rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Mon Sep 01 13:23:39 2014 +0200 @@ -27,6 +27,7 @@ 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_strong0_tac: Proof.context -> thm -> thm list -> 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 @@ -234,6 +235,21 @@ (etac (@{thm Collect_split_mono_strong} OF [thm, thm]) THEN' atac)) set_maps] 1; +fun mk_rel_transfer_tac ctxt in_rel rel_map rel_mono_strong = + let + fun last_tac iffD = + HEADGOAL (etac rel_mono_strong) THEN + REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN' + REPEAT_DETERM o atac)); + in + REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN + (HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE + REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) :: + @{thms exE conjE CollectE}))) THEN + HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac iffI) THEN + last_tac iffD1 THEN last_tac iffD2) + end; + fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp = let val n = length set_maps; diff -r c23bdb4ed2f6 -r c5316f843f72 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 13:23:05 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Sep 01 13:23:39 2014 +0200 @@ -123,21 +123,24 @@ | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys in zmap [] end; + fun choose_binary_fun fs AB = find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs; -fun build_binary_fun_app fs a b = - Option.map (rapp b o rapp a) (choose_binary_fun fs (fastype_of a, fastype_of b)); +fun build_binary_fun_app fs t u = + Option.map (rapp u o rapp t) (choose_binary_fun fs (fastype_of t, fastype_of u)); -fun build_the_rel ctxt Rs Ts A B = build_rel ctxt Ts (the o choose_binary_fun Rs) (A, B); -fun build_rel_app ctxt Rs Ts a b = build_the_rel ctxt Rs Ts (fastype_of a) (fastype_of b) $ a $ b; +fun build_the_rel rel_table ctxt Rs Ts A B = + build_rel rel_table ctxt Ts (the o choose_binary_fun Rs) (A, B); +fun build_rel_app ctxt Rs Ts t u = + build_the_rel [] ctxt Rs Ts (fastype_of t) (fastype_of u) $ t $ u; + +fun mk_parametricity_goal ctxt Rs t u = + let val prem = build_the_rel [] ctxt Rs [] (fastype_of t) (fastype_of u) in + HOLogic.mk_Trueprop (prem $ t $ u) + end; val name_of_set = name_of_const "set"; -fun mk_parametricity_goal ctxt Rs f g = - let val prem = build_the_rel ctxt Rs [] (fastype_of f) (fastype_of g) in - HOLogic.mk_Trueprop (prem $ f $ g) - end; - fun fp_sugar_of ctxt = Symtab.lookup (Data.get (Context.Proof ctxt)) #> Option.map (transfer_fp_sugar ctxt); @@ -514,7 +517,7 @@ end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq - (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); + (map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs)); val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} => @@ -765,7 +768,7 @@ end; val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq - IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts))); + IRs (map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts))); val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} => @@ -924,7 +927,7 @@ fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs; fun build_the_rel rs' T Xs_T = - build_rel lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) + build_rel [] lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T) |> Term.subst_atomic_types (Xs ~~ fpTs); fun build_rel_app rs' usel vsel Xs_T =