# HG changeset patch # User blanchet # Date 1398241406 -7200 # Node ID b07c8ad230100e428aaba7235e51a5cedca74952 # Parent a001337c8d24f60e8192b22921e21f3fe65b7a5e added 'inj_map' as auxiliary BNF theorem diff -r a001337c8d24 -r b07c8ad23010 src/HOL/BNF_Def.thy --- a/src/HOL/BNF_Def.thy Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/BNF_Def.thy Wed Apr 23 10:23:26 2014 +0200 @@ -14,19 +14,19 @@ "bnf" :: thy_goal begin -lemma collect_comp: "collect F o g = collect ((\f. f o g) ` F)" +lemma collect_comp: "collect F \ g = collect ((\f. f \ g) ` F)" by (rule ext) (auto simp only: comp_apply collect_def) definition convol ("<_ , _>") where " \ %a. (f a, g a)" lemma fst_convol: -"fst o = f" +"fst \ = f" apply(rule ext) unfolding convol_def by simp lemma snd_convol: -"snd o = g" +"snd \ = g" apply(rule ext) unfolding convol_def by simp @@ -97,10 +97,10 @@ "csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)" unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp -lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy" +lemma snd_fst_flip: "snd xy = (fst \ (%(x, y). (y, x))) xy" by (simp split: prod.split) -lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy" +lemma fst_snd_flip: "fst xy = (snd \ (%(x, y). (y, x))) xy" by (simp split: prod.split) lemma flip_pred: "A \ Collect (split (R ^--1)) \ (%(x, y). (y, x)) ` A \ Collect (split R)" @@ -134,16 +134,19 @@ lemma If_the_inv_into_f_f: "\i \ C; inj_on g C\ \ - ((\i. if i \ g ` C then the_inv_into C g i else x) o g) i = id i" + ((\i. if i \ g ` C then the_inv_into C g i else x) \ g) i = id i" unfolding Func_def by (auto elim: the_inv_into_f_f) +lemma the_inv_f_o_f_id: "inj f \ (the_inv f \ f) z = id z" + by (simp add: the_inv_f_f) + lemma vimage2pI: "R (f x) (g y) \ vimage2p f g R x y" unfolding vimage2p_def by - lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \ vimage2p f g S)" unfolding rel_fun_def vimage2p_def by auto -lemma convol_image_vimage2p: " ` Collect (split (vimage2p f g R)) \ Collect (split R)" +lemma convol_image_vimage2p: " fst, g \ snd> ` Collect (split (vimage2p f g R)) \ Collect (split R)" unfolding vimage2p_def convol_def by auto lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\\" diff -r a001337c8d24 -r b07c8ad23010 src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:26 2014 +0200 @@ -53,6 +53,7 @@ val in_cong_of_bnf: bnf -> thm val in_mono_of_bnf: bnf -> thm val in_rel_of_bnf: bnf -> thm + val inj_map_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 @@ -217,6 +218,7 @@ in_cong: thm lazy, in_mono: thm lazy, in_rel: thm lazy, + inj_map: thm lazy, map_comp: thm lazy, map_cong: thm lazy, map_id: thm lazy, @@ -233,7 +235,7 @@ }; fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel - map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono + inj_map map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = { bd_Card_order = bd_Card_order, bd_Cinfinite = bd_Cinfinite, @@ -243,6 +245,7 @@ in_cong = in_cong, in_mono = in_mono, in_rel = in_rel, + inj_map = inj_map, map_comp = map_comp, map_cong = map_cong, map_id = map_id, @@ -266,6 +269,7 @@ in_cong, in_mono, in_rel, + inj_map, map_comp, map_cong, map_id, @@ -287,6 +291,7 @@ in_cong = Lazy.map f in_cong, in_mono = Lazy.map f in_mono, in_rel = Lazy.map f in_rel, + inj_map = Lazy.map f inj_map, map_comp = Lazy.map f map_comp, map_cong = Lazy.map f map_cong, map_id = Lazy.map f map_id, @@ -404,6 +409,7 @@ val in_cong_of_bnf = Lazy.force o #in_cong o #facts o rep_bnf; 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 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; @@ -572,6 +578,7 @@ val in_bdN = "in_bd"; val in_monoN = "in_mono"; val in_relN = "in_rel"; +val inj_mapN = "inj_map"; val map_id0N = "map_id0"; val map_idN = "map_id"; val map_comp0N = "map_comp0"; @@ -624,6 +631,7 @@ (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_id0N, [#map_id0 axioms]), (map_transferN, [Lazy.force (#map_transfer facts)]), @@ -1103,6 +1111,19 @@ val map_cong = Lazy.lazy mk_map_cong; + fun mk_inj_map () = + let + val prems = map (HOLogic.mk_Trueprop o mk_inj) fs; + val concl = HOLogic.mk_Trueprop (mk_inj (Term.list_comb (bnf_map_AsBs, fs))); + val goal = fold_rev Logic.all fs (Logic.list_implies (prems, concl)); + in + Goal.prove_sorry lthy [] [] goal (fn _ => mk_inj_map_tac live (Lazy.force map_id) + (Lazy.force map_comp) (#map_cong0 axioms) (Lazy.force map_cong)) + |> Thm.close_derivation + end; + + val inj_map = Lazy.lazy mk_inj_map; + val set_map = map (fn thm => Lazy.lazy (fn () => mk_set_map thm)) (#set_map0 axioms); val wit_thms = @@ -1289,7 +1310,7 @@ 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 map_comp map_cong map_id map_transfer rel_eq rel_flip set_map + in_mono in_rel inj_map map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO; val wits = map2 mk_witness bnf_wits wit_thms; diff -r a001337c8d24 -r b07c8ad23010 src/HOL/Tools/BNF/bnf_def_tactics.ML --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Apr 23 10:23:26 2014 +0200 @@ -9,10 +9,11 @@ signature BNF_DEF_TACTICS = sig val mk_collect_set_map_tac: thm list -> tactic + val mk_in_mono_tac: int -> tactic + val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic val mk_map_id: thm -> thm val mk_map_comp: thm -> thm val mk_map_cong_tac: Proof.context -> thm -> tactic - val mk_in_mono_tac: int -> tactic val mk_set_map: thm -> thm val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic @@ -55,6 +56,16 @@ ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN (etac subset_trans THEN' atac) 1; +fun mk_inj_map_tac n map_id map_comp map_cong0 map_cong = + let + val map_cong' = map_cong OF (asm_rl :: replicate n refl); + val map_cong0' = map_cong0 OF (replicate n @{thm the_inv_f_o_f_id}); + in + HEADGOAL (rtac @{thm injI} THEN' etac (map_cong' RS box_equals) THEN' + REPEAT_DETERM_N 2 o (rtac (box_equals OF [map_cong0', map_comp RS sym, map_id]) THEN' + REPEAT_DETERM_N n o atac)) + 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 => diff -r a001337c8d24 -r b07c8ad23010 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200 @@ -101,6 +101,7 @@ val mk_rel_fun: term -> term -> term val mk_image: term -> term val mk_in: term list -> term list -> typ -> term + val mk_inj: term -> term val mk_leq: term -> term -> term val mk_ordLeq: term -> term -> term val mk_rel_comp: term * term -> term @@ -470,6 +471,12 @@ else HOLogic.mk_UNIV T end; +fun mk_inj t = + let val T as Type (@{type_name fun}, [domT, ranT]) = fastype_of t in + Const (@{const_name inj_on}, T --> HOLogic.mk_setT domT --> HOLogic.boolT) $ t + $ HOLogic.mk_UNIV domT + end; + fun mk_leq t1 t2 = Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;