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.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
```