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