src/HOL/Lifting.thy
changeset 56518 beb3b6851665
parent 56517 7e8a369eb10d
child 56519 c1048f5bbb45
     1.1 --- a/src/HOL/Lifting.thy	Thu Apr 10 17:48:13 2014 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Apr 10 17:48:14 2014 +0200
     1.3 @@ -24,82 +24,6 @@
     1.4    "(id ---> id) = id"
     1.5    by (simp add: fun_eq_iff)
     1.6  
     1.7 -subsection {* Other predicates on relations *}
     1.8 -
     1.9 -definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.10 -  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    1.11 -
    1.12 -lemma left_totalI:
    1.13 -  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    1.14 -unfolding left_total_def by blast
    1.15 -
    1.16 -lemma left_totalE:
    1.17 -  assumes "left_total R"
    1.18 -  obtains "(\<And>x. \<exists>y. R x y)"
    1.19 -using assms unfolding left_total_def by blast
    1.20 -
    1.21 -lemma bi_total_iff: "bi_total A = (right_total A \<and> left_total A)"
    1.22 -unfolding left_total_def right_total_def bi_total_def by blast
    1.23 -
    1.24 -lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
    1.25 -by(simp add: left_total_def right_total_def bi_total_def)
    1.26 -
    1.27 -definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.28 -  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    1.29 -
    1.30 -lemma left_unique_transfer [transfer_rule]:
    1.31 -  assumes "right_total A"
    1.32 -  assumes "right_total B"
    1.33 -  assumes "bi_unique A"
    1.34 -  shows "((A ===> B ===> op=) ===> implies) left_unique left_unique"
    1.35 -using assms unfolding left_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    1.36 -by metis
    1.37 -
    1.38 -lemma bi_unique_iff: "bi_unique A = (right_unique A \<and> left_unique A)"
    1.39 -unfolding left_unique_def right_unique_def bi_unique_def by blast
    1.40 -
    1.41 -lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
    1.42 -by(auto simp add: left_unique_def right_unique_def bi_unique_def)
    1.43 -
    1.44 -lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
    1.45 -unfolding left_unique_def by blast
    1.46 -
    1.47 -lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
    1.48 -unfolding left_unique_def by blast
    1.49 -
    1.50 -lemma left_total_fun:
    1.51 -  "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
    1.52 -  unfolding left_total_def rel_fun_def
    1.53 -  apply (rule allI, rename_tac f)
    1.54 -  apply (rule_tac x="\<lambda>y. SOME z. B (f (THE x. A x y)) z" in exI)
    1.55 -  apply clarify
    1.56 -  apply (subgoal_tac "(THE x. A x y) = x", simp)
    1.57 -  apply (rule someI_ex)
    1.58 -  apply (simp)
    1.59 -  apply (rule the_equality)
    1.60 -  apply assumption
    1.61 -  apply (simp add: left_unique_def)
    1.62 -  done
    1.63 -
    1.64 -lemma left_unique_fun:
    1.65 -  "\<lbrakk>left_total A; left_unique B\<rbrakk> \<Longrightarrow> left_unique (A ===> B)"
    1.66 -  unfolding left_total_def left_unique_def rel_fun_def
    1.67 -  by (clarify, rule ext, fast)
    1.68 -
    1.69 -lemma left_total_eq: "left_total op=" unfolding left_total_def by blast
    1.70 -
    1.71 -lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
    1.72 -
    1.73 -lemma [simp]:
    1.74 -  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
    1.75 -  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
    1.76 -by(auto simp add: left_unique_def right_unique_def)
    1.77 -
    1.78 -lemma [simp]:
    1.79 -  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
    1.80 -  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
    1.81 -by(simp_all add: left_total_def right_total_def)
    1.82 -
    1.83  subsection {* Quotient Predicate *}
    1.84  
    1.85  definition
    1.86 @@ -391,6 +315,9 @@
    1.87    assumes 1: "Quotient R Abs Rep T" and 2: "reflp R"
    1.88  begin
    1.89  
    1.90 +lemma Quotient_left_total: "left_total T"
    1.91 +  using 1 2 unfolding Quotient_alt_def left_total_def reflp_def by auto
    1.92 +
    1.93  lemma Quotient_bi_total: "bi_total T"
    1.94    using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
    1.95  
    1.96 @@ -464,12 +391,6 @@
    1.97    shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
    1.98  using assms unfolding left_unique_def by blast
    1.99  
   1.100 -lemma left_total_composition: "left_total R \<Longrightarrow> left_total S \<Longrightarrow> left_total (R OO S)"
   1.101 -unfolding left_total_def OO_def by fast
   1.102 -
   1.103 -lemma left_unique_composition: "left_unique R \<Longrightarrow> left_unique S \<Longrightarrow> left_unique (R OO S)"
   1.104 -unfolding left_unique_def OO_def by blast
   1.105 -
   1.106  lemma invariant_le_eq:
   1.107    "invariant P \<le> op=" unfolding invariant_def by blast
   1.108  
   1.109 @@ -487,18 +408,6 @@
   1.110  definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.111  "NEG A B \<equiv> B \<le> A"
   1.112  
   1.113 -(*
   1.114 -  The following two rules are here because we don't have any proper
   1.115 -  left-unique ant left-total relations. Left-unique and left-total
   1.116 -  assumptions show up in distributivity rules for the function type.
   1.117 -*)
   1.118 -
   1.119 -lemma bi_unique_left_unique[transfer_rule]: "bi_unique R \<Longrightarrow> left_unique R"
   1.120 -unfolding bi_unique_def left_unique_def by blast
   1.121 -
   1.122 -lemma bi_total_left_total[transfer_rule]: "bi_total R \<Longrightarrow> left_total R"
   1.123 -unfolding bi_total_def left_total_def by blast
   1.124 -
   1.125  lemma pos_OO_eq:
   1.126    shows "POS (A OO op=) A"
   1.127  unfolding POS_def OO_def by blast
   1.128 @@ -635,10 +544,10 @@
   1.129  using assms by blast
   1.130  
   1.131  lemma pcr_Domainp_total:
   1.132 -  assumes "bi_total B"
   1.133 +  assumes "left_total B"
   1.134    assumes "Domainp A = P"
   1.135    shows "Domainp (A OO B) = P"
   1.136 -using assms unfolding bi_total_def 
   1.137 +using assms unfolding left_total_def 
   1.138  by fast
   1.139  
   1.140  lemma Quotient_to_Domainp:
   1.141 @@ -660,12 +569,6 @@
   1.142  ML_file "Tools/Lifting/lifting_info.ML"
   1.143  setup Lifting_Info.setup
   1.144  
   1.145 -lemmas [reflexivity_rule] = 
   1.146 -  order_refl[of "op="] invariant_le_eq Quotient_composition_le_eq
   1.147 -  Quotient_composition_ge_eq
   1.148 -  left_total_eq left_unique_eq left_total_composition left_unique_composition
   1.149 -  left_total_fun left_unique_fun
   1.150 -
   1.151  (* setup for the function type *)
   1.152  declare fun_quotient[quot_map]
   1.153  declare fun_mono[relator_mono]
   1.154 @@ -676,7 +579,7 @@
   1.155  ML_file "Tools/Lifting/lifting_def.ML"
   1.156  
   1.157  ML_file "Tools/Lifting/lifting_setup.ML"
   1.158 -
   1.159 +                           
   1.160  hide_const (open) invariant POS NEG
   1.161  
   1.162  end