src/HOL/BNF/BNF_Def.thy
 changeset 51916 eac9e9a45bf5 parent 51909 eb3169abcbd5 child 51917 f964a9887713
```     1.1 --- a/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:39:30 2013 +0200
1.2 +++ b/src/HOL/BNF/BNF_Def.thy	Wed May 08 09:45:30 2013 +0200
1.3 @@ -177,19 +177,14 @@
1.4  lemma Collect_split_mono: "A \<le> B \<Longrightarrow> Collect (split A) \<subseteq> Collect (split B)"
1.5    by auto
1.6
1.7 +lemma Collect_split_mono_strong:
1.8 +  "\<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>
1.9 +  A \<subseteq> Collect (split Q)"
1.10 +  by fastforce
1.11 +
1.12  lemma predicate2_cong: "A = B \<Longrightarrow> A a b \<longleftrightarrow> B a b"
1.13  by metis
1.14
1.15 -lemma fun_cong_pair: "f = g \<Longrightarrow> f {(a, b). R a b} = g {(a, b). R a b}"
1.16 -by (rule fun_cong)
1.17 -
1.18 -lemma flip_as_converse: "{(a, b). R b a} = converse {(a, b). R a b}"
1.19 -unfolding converse_def mem_Collect_eq prod.cases
1.20 -apply (rule arg_cong[of _ _ "\<lambda>x. Collect (prod_case x)"])
1.21 -apply (rule ext)+
1.22 -apply (unfold conversep_iff)
1.23 -by (rule refl)
1.24 -
1.25  ML_file "Tools/bnf_def_tactics.ML"
1.26  ML_file "Tools/bnf_def.ML"
1.27
```