author traytel Sun, 28 Jul 2013 12:59:59 +0200 changeset 52749 ed416f4ac34e parent 52748 8e398d9bedf3 child 52750 96d53ab825cf
more converse(p) theorems; tuned proofs;
 src/HOL/BNF/BNF_Def.thy file | annotate | diff | comparison | revisions src/HOL/BNF/BNF_GFP.thy file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_def_tactics.ML file | annotate | diff | comparison | revisions src/HOL/BNF/Tools/bnf_gfp_tactics.ML file | annotate | diff | comparison | revisions src/HOL/Relation.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/BNF/BNF_Def.thy	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Sun Jul 28 12:59:59 2013 +0200
@@ -15,15 +15,7 @@
begin

lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
-by (rule ext) (auto simp only: o_apply collect_def)
-
-lemma converse_shift:
-"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
-unfolding converse_def by auto
-
-lemma conversep_shift:
-"R1 \<le> R2 ^--1 \<Longrightarrow> R1 ^--1 \<le> R2"
-unfolding conversep.simps by auto
+  by (rule ext) (auto simp only: o_apply collect_def)

definition convol ("<_ , _>") where
"<f , g> \<equiv> %a. (f a, g a)"```
```--- a/src/HOL/BNF/BNF_GFP.thy	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Sun Jul 28 12:59:59 2013 +0200
@@ -106,15 +106,9 @@
lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
unfolding fun_eq_iff by auto

-lemmas conversep_in_rel_Id_on =
-  trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]
-
lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
unfolding fun_eq_iff by auto

-lemmas relcompp_in_rel_Id_on =
-  trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]
-
lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
unfolding Gr_def Grp_def fun_eq_iff by auto
```
```--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Sun Jul 28 12:59:59 2013 +0200
@@ -42,6 +42,7 @@
open BNF_Tactics

val ord_eq_le_trans = @{thm ord_eq_le_trans};
+val conversep_shift = @{thm conversep_le_swap} RS iffD1;

fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
@@ -146,7 +147,7 @@
end;

fun mk_rel_conversep_tac le_conversep rel_mono =
-  EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac @{thm conversep_shift},
+  EVERY' [rtac @{thm antisym}, rtac le_conversep, rtac @{thm xt1(6)}, rtac conversep_shift,
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
```
```--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Jul 28 12:59:59 2013 +0200
@@ -144,7 +144,12 @@
val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
val rev_bspec = Drule.rotate_prems 1 bspec;
-val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]}
+val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
+val conversep_in_rel_Id_on =
+   @{thm trans[OF conversep_in_rel arg_cong[of _ _ in_rel, OF converse_Id_on]]};
+val relcompp_in_rel_Id_on =
+   @{thm   trans[OF relcompp_in_rel arg_cong[of _ _ in_rel, OF Id_on_Comp[symmetric]]]};
+val converse_shift = @{thm converse_subset_swap} RS iffD1;

fun mk_coalg_set_tac coalg_def =
dtac (coalg_def RS iffD1) 1 THEN
@@ -313,12 +318,12 @@
fun mk_bis_converse_tac m bis_rel rel_congs rel_converseps =
EVERY' [stac bis_rel, dtac (bis_rel RS iffD1),
REPEAT_DETERM o etac conjE, rtac conjI,
-    CONJ_WRAP' (K (EVERY' [rtac @{thm converse_shift}, etac subset_trans,
+    CONJ_WRAP' (K (EVERY' [rtac converse_shift, etac subset_trans,
rtac equalityD2, rtac @{thm converse_Times}])) rel_congs,
CONJ_WRAP' (fn (rel_cong, rel_conversep) =>
EVERY' [rtac allI, rtac allI, rtac impI,
rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac @{thm conversep_in_rel_Id_on},
+        REPEAT_DETERM_N m o rtac conversep_in_rel_Id_on,
REPEAT_DETERM_N (length rel_congs) o rtac @{thm conversep_in_rel},
rtac (rel_conversep RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
REPEAT_DETERM o etac allE,
@@ -331,7 +336,7 @@
CONJ_WRAP' (fn (rel_cong, rel_OO) =>
EVERY' [rtac allI, rtac allI, rtac impI,
rtac (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
-        REPEAT_DETERM_N m o rtac @{thm relcompp_in_rel_Id_on},
+        REPEAT_DETERM_N m o rtac relcompp_in_rel_Id_on,
REPEAT_DETERM_N (length rel_congs) o rtac @{thm relcompp_in_rel},
rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
etac @{thm relcompE},```
```--- a/src/HOL/Relation.thy	Sat Jul 27 22:44:04 2013 +0200
+++ b/src/HOL/Relation.thy	Sun Jul 28 12:59:59 2013 +0200
@@ -705,11 +705,23 @@
lemma converse_UNION: "(UNION S r)^-1 = (UN x:S. (r x)^-1)"
by blast

-lemma converse_mono: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
+lemma converse_mono[simp]: "r^-1 \<subseteq> s ^-1 \<longleftrightarrow> r \<subseteq> s"
+  by auto
+
+lemma conversep_mono[simp]: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
+  by (fact converse_mono[to_pred])
+
+lemma converse_inject[simp]: "r^-1 = s ^-1 \<longleftrightarrow> r = s"
by auto

-lemma conversep_mono: "r^--1 \<le> s ^--1 \<longleftrightarrow> r \<le> s"
-  by (fact converse_mono[to_pred])
+lemma conversep_inject[simp]: "r^--1 = s ^--1 \<longleftrightarrow> r = s"
+  by (fact converse_inject[to_pred])
+
+lemma converse_subset_swap: "r \<subseteq> s ^-1 = (r ^-1 \<subseteq> s)"
+  by auto
+
+lemma conversep_le_swap: "r \<le> s ^--1 = (r ^--1 \<le> s)"
+  by (fact converse_subset_swap[to_pred])

lemma converse_Id [simp]: "Id^-1 = Id"
by blast
@@ -741,18 +753,8 @@
lemma total_on_converse [simp]: "total_on A (r^-1) = total_on A r"
by (auto simp: total_on_def)

-lemma finite_converse [iff]: "finite (r^-1) = finite r"
-  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
-   apply simp
-   apply (rule iffI)
-    apply (erule finite_imageD [unfolded inj_on_def])
-    apply (simp split add: split_split)
-   apply (erule finite_imageI)
-  apply (simp add: set_eq_iff image_def, auto)
-  apply (rule bexI)
-   prefer 2 apply assumption
-  apply simp
-  done
+lemma finite_converse [iff]: "finite (r^-1) = finite r"
+  unfolding converse_def conversep_iff by (auto elim: finite_imageD simp: inj_on_def)

lemma conversep_noteq [simp]: "(op \<noteq>)^--1 = op \<noteq>"
@@ -1075,7 +1077,7 @@
interpret comp_fun_commute "(\<lambda>(x,y) A. if x \<in> S then Set.insert y A else A)"
by (rule comp_fun_commute_Image_fold)
have *: "\<And>x F. Set.insert x F `` S = (if fst x \<in> S then Set.insert (snd x) (F `` S) else (F `` S))"
-    by (auto intro: rev_ImageI)
+    by (force intro: rev_ImageI)
show ?thesis using assms by (induct R) (auto simp: *)
qed

@@ -1119,11 +1121,9 @@
assumes "finite S"
shows "R O S = Finite_Set.fold
(\<lambda>(x,y) A. Finite_Set.fold (\<lambda>(w,z) A'. if y = w then Set.insert (x,z) A' else A') A S) {} R"
-proof -
-  show ?thesis using assms by (induct R)
-    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
+  using assms by (induct R)
+    (auto simp: comp_fun_commute.fold_insert comp_fun_commute_relcomp_fold insert_relcomp_fold
cong: if_cong)
-qed

```