src/HOL/Lifting.thy
changeset 51994 82cc2aeb7d13
parent 51956 a4d81cdebf8b
child 52036 1aa2e40df9ff
     1.1 --- a/src/HOL/Lifting.thy	Tue May 14 21:56:19 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Wed May 15 12:10:39 2013 +0200
     1.3 @@ -22,6 +22,23 @@
     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 +definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.22 +  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    1.23 +
    1.24  subsection {* Quotient Predicate *}
    1.25  
    1.26  definition
    1.27 @@ -190,7 +207,7 @@
    1.28    assumes 1: "Quotient R1 Abs1 Rep1 T1"
    1.29    assumes 2: "Quotient R2 Abs2 Rep2 T2"
    1.30    shows "Quotient (T1 OO R2 OO conversep T1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2) (T1 OO T2)"
    1.31 -  using assms unfolding Quotient_alt_def4 by (auto intro!: ext)
    1.32 +  using assms unfolding Quotient_alt_def4 by fastforce
    1.33  
    1.34  lemma equivp_reflp2:
    1.35    "equivp R \<Longrightarrow> reflp R"
    1.36 @@ -323,6 +340,10 @@
    1.37    assumes T_def: "T \<equiv> (\<lambda>(x::'a) (y::'b). x = Rep y)"
    1.38  begin
    1.39  
    1.40 +lemma typedef_left_unique: "left_unique T"
    1.41 +  unfolding left_unique_def T_def
    1.42 +  by (simp add: type_definition.Rep_inject [OF type])
    1.43 +
    1.44  lemma typedef_bi_unique: "bi_unique T"
    1.45    unfolding bi_unique_def T_def
    1.46    by (simp add: type_definition.Rep_inject [OF type])
    1.47 @@ -352,17 +373,7 @@
    1.48  
    1.49  text {* Proving reflexivity *}
    1.50  
    1.51 -definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.52 -  where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
    1.53 -
    1.54 -lemma left_totalI:
    1.55 -  "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
    1.56 -unfolding left_total_def by blast
    1.57 -
    1.58 -lemma left_totalE:
    1.59 -  assumes "left_total R"
    1.60 -  obtains "(\<And>x. \<exists>y. R x y)"
    1.61 -using assms unfolding left_total_def by blast
    1.62 +definition reflp' :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where "reflp' R \<equiv> reflp R"
    1.63  
    1.64  lemma Quotient_to_left_total:
    1.65    assumes q: "Quotient R Abs Rep T"
    1.66 @@ -371,20 +382,30 @@
    1.67  using r_R Quotient_cr_rel[OF q] unfolding left_total_def by (auto elim: reflpE)
    1.68  
    1.69  lemma reflp_Quotient_composition:
    1.70 -  assumes lt_R1: "left_total R1"
    1.71 -  and r_R2: "reflp R2"
    1.72 -  shows "reflp (R1 OO R2 OO R1\<inverse>\<inverse>)"
    1.73 -using assms
    1.74 -proof -
    1.75 -  {
    1.76 -    fix x
    1.77 -    from lt_R1 obtain y where "R1 x y" unfolding left_total_def by blast
    1.78 -    moreover then have "R1\<inverse>\<inverse> y x" by simp
    1.79 -    moreover have "R2 y y" using r_R2 by (auto elim: reflpE)
    1.80 -    ultimately have "(R1 OO R2 OO R1\<inverse>\<inverse>) x x" by auto
    1.81 -  }
    1.82 -  then show ?thesis by (auto intro: reflpI)
    1.83 -qed
    1.84 +  assumes "left_total R"
    1.85 +  assumes "reflp T"
    1.86 +  shows "reflp (R OO T OO R\<inverse>\<inverse>)"
    1.87 +using assms unfolding reflp_def left_total_def by fast
    1.88 +
    1.89 +lemma reflp_fun1:
    1.90 +  assumes "is_equality R"
    1.91 +  assumes "reflp' S"
    1.92 +  shows "reflp (R ===> S)"
    1.93 +using assms unfolding is_equality_def reflp'_def reflp_def fun_rel_def by blast
    1.94 +
    1.95 +lemma reflp_fun2:
    1.96 +  assumes "is_equality R"
    1.97 +  assumes "is_equality S"
    1.98 +  shows "reflp (R ===> S)"
    1.99 +using assms unfolding is_equality_def reflp_def fun_rel_def by blast
   1.100 +
   1.101 +lemma is_equality_Quotient_composition:
   1.102 +  assumes "is_equality T"
   1.103 +  assumes "left_total R"
   1.104 +  assumes "left_unique R"
   1.105 +  shows "is_equality (R OO T OO R\<inverse>\<inverse>)"
   1.106 +using assms unfolding is_equality_def left_total_def left_unique_def OO_def conversep_iff
   1.107 +by fastforce
   1.108  
   1.109  lemma reflp_equality: "reflp (op =)"
   1.110  by (auto intro: reflpI)
   1.111 @@ -400,9 +421,6 @@
   1.112  definition  NEG :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.113  "NEG A B \<equiv> B \<le> A"
   1.114  
   1.115 -definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   1.116 -  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
   1.117 -
   1.118  (*
   1.119    The following two rules are here because we don't have any proper
   1.120    left-unique ant left-total relations. Left-unique and left-total
   1.121 @@ -559,7 +577,18 @@
   1.122  ML_file "Tools/Lifting/lifting_info.ML"
   1.123  setup Lifting_Info.setup
   1.124  
   1.125 -lemmas [reflexivity_rule] = reflp_equality reflp_Quotient_composition
   1.126 +lemmas [reflexivity_rule] = 
   1.127 +  reflp_equality reflp_Quotient_composition is_equality_Quotient_composition
   1.128 +
   1.129 +text {* add @{thm reflp_fun1} and @{thm reflp_fun2} manually through ML
   1.130 +  because we don't want to get reflp' variant of these theorems *}
   1.131 +
   1.132 +setup{*
   1.133 +Context.theory_map 
   1.134 +  (fold
   1.135 +    (snd oo (Thm.apply_attribute Lifting_Info.add_reflexivity_rule_raw_attribute)) 
   1.136 +      [@{thm reflp_fun1}, @{thm reflp_fun2}])
   1.137 +*}
   1.138  
   1.139  (* setup for the function type *)
   1.140  declare fun_quotient[quot_map]
   1.141 @@ -572,6 +601,6 @@
   1.142  
   1.143  ML_file "Tools/Lifting/lifting_setup.ML"
   1.144  
   1.145 -hide_const (open) invariant POS NEG
   1.146 +hide_const (open) invariant POS NEG reflp'
   1.147  
   1.148  end