author traytel Wed, 08 May 2013 09:45:30 +0200 changeset 51916 eac9e9a45bf5 parent 51915 87767611de37 child 51917 f964a9887713
stronger monotonicity property for relators
 src/HOL/BNF/BNF_Def.thy file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_def.ML file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_def_tactics.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:39:30 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:45:30 2013 +0200
@@ -177,19 +177,14 @@
lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
by auto

+lemma Collect_split_mono_strong:
+  "\<lbrakk>\<forall>a\<in>fst ` A. \<forall>b \<in> snd ` A. P a b \<longrightarrow> Q a b; A \<subseteq> Collect (split P)\<rbrakk> \<Longrightarrow>
+  A \<subseteq> Collect (split Q)"
+  by fastforce
+
lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
by metis

-lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
-by (rule fun_cong)
-
-lemma flip_as_converse: "{(a, b). R b a} = converse {(a, b). R a b}"
-unfolding converse_def mem_Collect_eq prod.cases
-apply (rule arg_cong[of _ _ "\<lambda>x. Collect (prod_case x)"])
-apply (rule ext)+
-apply (unfold conversep_iff)
-by (rule refl)
-
ML_file "Tools/bnf_def_tactics.ML"
ML_file "Tools/bnf_def.ML"
```
```--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 09:39:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed May 08 09:45:30 2013 +0200
@@ -66,6 +66,7 @@
val rel_cong_of_bnf: bnf -> thm
val rel_conversep_of_bnf: bnf -> thm
val rel_mono_of_bnf: bnf -> thm
+  val rel_mono_strong_of_bnf: bnf -> thm
val rel_eq_of_bnf: bnf -> thm
val rel_flip_of_bnf: bnf -> thm
val set_bd_of_bnf: bnf -> thm list
@@ -192,13 +193,14 @@
set_map': thm lazy list,
rel_cong: thm lazy,
rel_mono: thm lazy,
+  rel_mono_strong: thm lazy,
rel_Grp: thm lazy,
rel_conversep: thm lazy,
rel_OO: thm lazy
};

fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_cong in_mono in_rel
-    map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map' rel_cong rel_mono
+    map_comp' map_cong map_id' map_wppull 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,
@@ -216,6 +218,7 @@
set_map' = set_map',
rel_cong = rel_cong,
rel_mono = rel_mono,
+  rel_mono_strong = rel_mono_strong,
rel_Grp = rel_Grp,
rel_conversep = rel_conversep,
rel_OO = rel_OO};
@@ -237,6 +240,7 @@
set_map',
rel_cong,
rel_mono,
+  rel_mono_strong,
rel_Grp,
rel_conversep,
rel_OO} =
@@ -256,6 +260,7 @@
set_map' = map (Lazy.map f) set_map',
rel_cong = Lazy.map f rel_cong,
rel_mono = Lazy.map f rel_mono,
+    rel_mono_strong = Lazy.map f rel_mono_strong,
rel_Grp = Lazy.map f rel_Grp,
rel_conversep = Lazy.map f rel_conversep,
rel_OO = Lazy.map f rel_OO};
@@ -372,6 +377,7 @@
val set_map'_of_bnf = map Lazy.force o #set_map' o #facts o rep_bnf;
val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
+val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong 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;
@@ -494,6 +500,7 @@
val rel_GrpN = "rel_Grp";
val rel_conversepN = "rel_conversep";
val rel_monoN = "rel_mono"
+val rel_mono_strongN = "rel_mono_strong"
val rel_OON = "rel_compp";
val rel_OO_GrpN = "rel_compp_Grp";

@@ -673,7 +680,7 @@
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;

val pre_names_lthy = lthy;
-    val ((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), As),
+    val (((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
@@ -683,6 +690,7 @@
||>> yield_singleton (mk_Frees "y") CB'
||>> yield_singleton (apfst (op ~~) oo mk_Frees' "z") CRs'
||>> mk_Frees "z" As'
+      ||>> mk_Frees "y" Bs'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "A" (map HOLogic.mk_setT domTs)
@@ -1093,11 +1101,30 @@

val rel_flip = Lazy.lazy mk_rel_flip;

+        fun mk_rel_mono_strong () =
+          let
+            fun mk_prem setA setB R S a b =
+              HOLogic.mk_Trueprop
+                (mk_Ball (setA \$ x) (Term.absfree (dest_Free a)
+                  (mk_Ball (setB \$ y) (Term.absfree (dest_Free b)
+                    (HOLogic.mk_imp (R \$ a \$ b, S \$ a \$ b))))));
+            val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) \$ x \$ y) ::
+              map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
+            val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) \$ x \$ y);
+          in
+            Goal.prove_sorry lthy [] []
+              (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
+              (mk_rel_mono_strong_tac (Lazy.force in_rel) (map Lazy.force set_map'))
+            |> Thm.close_derivation
+          end;
+
+        val rel_mono_strong = Lazy.lazy mk_rel_mono_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_cong in_mono
in_rel map_comp' map_cong map_id' map_wppull rel_eq rel_flip set_map'
-          rel_cong rel_mono rel_Grp rel_conversep rel_OO;
+          rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;

val wits = map2 mk_witness bnf_wits wit_thms;

@@ -1124,6 +1151,7 @@
(map_compN, [#map_comp axioms]),
(map_idN, [#map_id axioms]),
(map_wpullN, [#map_wpull axioms]),
+                    (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
(set_mapN, #set_map axioms),
(set_bdN, #set_bd axioms)] @
(witNs ~~ wit_thms)```
```--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed May 08 09:39:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed May 08 09:45:30 2013 +0200
@@ -26,6 +26,7 @@
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_mono_strong_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
end;

structure BNF_Def_Tactics : BNF_DEF_TACTICS =
@@ -192,4 +193,15 @@
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;

+fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
+  if null set_maps then atac 1
+  else
+    unfold_tac [in_rel] ctxt THEN
+    REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
+    hyp_subst_tac ctxt 1 THEN
+    unfold_tac set_maps ctxt THEN
+    EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
+      CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
+
+
end;```