author blanchet Wed, 23 Apr 2014 10:23:26 +0200 changeset 56635 b07c8ad23010 parent 56634 a001337c8d24 child 56636 bb8b37480d3f
added 'inj_map' as auxiliary BNF theorem
 src/HOL/BNF_Def.thy file | annotate | diff | comparison | revisions src/HOL/Tools/BNF/bnf_def.ML file | annotate | diff | comparison | revisions src/HOL/Tools/BNF/bnf_def_tactics.ML file | annotate | diff | comparison | revisions src/HOL/Tools/BNF/bnf_util.ML file | annotate | diff | comparison | revisions
```--- 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 ((\<lambda>f. f o g) ` F)"
+lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
by (rule ext) (auto simp only: comp_apply collect_def)

definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"

lemma fst_convol:
-"fst o <f , g> = f"
+"fst \<circ> <f , g> = f"
apply(rule ext)
unfolding convol_def by simp

lemma snd_convol:
-"snd o <f , g> = g"
+"snd \<circ> <f , g> = 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 \<circ> (%(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 \<circ> (%(x, y). (y, x))) xy"
by (simp split: prod.split)

lemma flip_pred: "A \<subseteq> Collect (split (R ^--1)) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> Collect (split R)"
@@ -134,16 +134,19 @@

lemma If_the_inv_into_f_f:
"\<lbrakk>i \<in> C; inj_on g C\<rbrakk> \<Longrightarrow>
-  ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
+  ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) \<circ> g) i = id i"
unfolding Func_def by (auto elim: the_inv_into_f_f)

+lemma the_inv_f_o_f_id: "inj f \<Longrightarrow> (the_inv f \<circ> f) z = id z"
+
lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
unfolding vimage2p_def by -

lemma rel_fun_iff_leq_vimage2p: "(rel_fun R S) f g = (R \<le> vimage2p f g S)"
unfolding rel_fun_def vimage2p_def by auto

-lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+lemma convol_image_vimage2p: "<f \<circ> fst, g \<circ> snd> ` Collect (split (vimage2p f g R)) \<subseteq> 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)\<inverse>\<inverse>"```
```--- 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;```
```--- 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 =>```
```--- 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;
```