# HG changeset patch # User traytel # Date 1375009199 -7200 # Node ID ed416f4ac34e1ef30b1536ddf08f76916a83d6ce # Parent 8e398d9bedf34282d5fff771d686544d25ad8b32 more converse(p) theorems; tuned proofs; diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/BNF/BNF_Def.thy --- 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 ((\f. f o g) ` F)" -by (rule ext) (auto simp only: o_apply collect_def) - -lemma converse_shift: -"R1 \ R2 ^-1 \ R1 ^-1 \ R2" -unfolding converse_def by auto - -lemma conversep_shift: -"R1 \ R2 ^--1 \ R1 ^--1 \ R2" -unfolding conversep.simps by auto + by (rule ext) (auto simp only: o_apply collect_def) definition convol ("<_ , _>") where " \ %a. (f a, g a)" diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/BNF/BNF_GFP.thy --- 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)\\ = in_rel (R\)" 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 diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/BNF/Tools/bnf_def_tactics.ML --- 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; diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- 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 \"]} +val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \"]}; +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}, diff -r 8e398d9bedf3 -r ed416f4ac34e src/HOL/Relation.thy --- 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 \ s ^-1 \ r \ s" +lemma converse_mono[simp]: "r^-1 \ s ^-1 \ r \ s" + by auto + +lemma conversep_mono[simp]: "r^--1 \ s ^--1 \ r \ s" + by (fact converse_mono[to_pred]) + +lemma converse_inject[simp]: "r^-1 = s ^-1 \ r = s" by auto -lemma conversep_mono: "r^--1 \ s ^--1 \ r \ s" - by (fact converse_mono[to_pred]) +lemma conversep_inject[simp]: "r^--1 = s ^--1 \ r = s" + by (fact converse_inject[to_pred]) + +lemma converse_subset_swap: "r \ s ^-1 = (r ^-1 \ s)" + by auto + +lemma conversep_le_swap: "r \ s ^--1 = (r ^--1 \ 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 \)^--1 = op \" by (auto simp add: fun_eq_iff) @@ -1075,7 +1077,7 @@ interpret comp_fun_commute "(\(x,y) A. if x \ S then Set.insert y A else A)" by (rule comp_fun_commute_Image_fold) have *: "\x F. Set.insert x F `` S = (if fst x \ 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 (\(x,y) A. Finite_Set.fold (\(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