src/HOL/Quotient.thy
changeset 35222 4f1fba00f66d
child 35236 fd8231b16203
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quotient.thy	Fri Feb 19 13:54:19 2010 +0100
     1.3 @@ -0,0 +1,797 @@
     1.4 +(*  Title:      Quotient.thy
     1.5 +    Author:     Cezary Kaliszyk and Christian Urban
     1.6 +*)
     1.7 +
     1.8 +theory Quotient
     1.9 +imports Plain ATP_Linkup
    1.10 +uses
    1.11 +  ("~~/src/HOL/Tools/Quotient/quotient_info.ML")
    1.12 +  ("~~/src/HOL/Tools/Quotient/quotient_typ.ML")
    1.13 +  ("~~/src/HOL/Tools/Quotient/quotient_def.ML")
    1.14 +  ("~~/src/HOL/Tools/Quotient/quotient_term.ML")
    1.15 +  ("~~/src/HOL/Tools/Quotient/quotient_tacs.ML")
    1.16 +begin
    1.17 +
    1.18 +
    1.19 +text {*
    1.20 +  Basic definition for equivalence relations
    1.21 +  that are represented by predicates.
    1.22 +*}
    1.23 +
    1.24 +definition
    1.25 +  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
    1.26 +
    1.27 +definition
    1.28 +  "reflp E \<equiv> \<forall>x. E x x"
    1.29 +
    1.30 +definition
    1.31 +  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
    1.32 +
    1.33 +definition
    1.34 +  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
    1.35 +
    1.36 +lemma equivp_reflp_symp_transp:
    1.37 +  shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
    1.38 +  unfolding equivp_def reflp_def symp_def transp_def expand_fun_eq
    1.39 +  by blast
    1.40 +
    1.41 +lemma equivp_reflp:
    1.42 +  shows "equivp E \<Longrightarrow> E x x"
    1.43 +  by (simp only: equivp_reflp_symp_transp reflp_def)
    1.44 +
    1.45 +lemma equivp_symp:
    1.46 +  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
    1.47 +  by (metis equivp_reflp_symp_transp symp_def)
    1.48 +
    1.49 +lemma equivp_transp:
    1.50 +  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
    1.51 +  by (metis equivp_reflp_symp_transp transp_def)
    1.52 +
    1.53 +lemma equivpI:
    1.54 +  assumes "reflp R" "symp R" "transp R"
    1.55 +  shows "equivp R"
    1.56 +  using assms by (simp add: equivp_reflp_symp_transp)
    1.57 +
    1.58 +lemma identity_equivp:
    1.59 +  shows "equivp (op =)"
    1.60 +  unfolding equivp_def
    1.61 +  by auto
    1.62 +
    1.63 +text {* Partial equivalences: not yet used anywhere *}
    1.64 +
    1.65 +definition
    1.66 +  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
    1.67 +
    1.68 +lemma equivp_implies_part_equivp:
    1.69 +  assumes a: "equivp E"
    1.70 +  shows "part_equivp E"
    1.71 +  using a
    1.72 +  unfolding equivp_def part_equivp_def
    1.73 +  by auto
    1.74 +
    1.75 +text {* Composition of Relations *}
    1.76 +
    1.77 +abbreviation
    1.78 +  rel_conj (infixr "OOO" 75)
    1.79 +where
    1.80 +  "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
    1.81 +
    1.82 +lemma eq_comp_r:
    1.83 +  shows "((op =) OOO R) = R"
    1.84 +  by (auto simp add: expand_fun_eq)
    1.85 +
    1.86 +section {* Respects predicate *}
    1.87 +
    1.88 +definition
    1.89 +  Respects
    1.90 +where
    1.91 +  "Respects R x \<equiv> R x x"
    1.92 +
    1.93 +lemma in_respects:
    1.94 +  shows "(x \<in> Respects R) = R x x"
    1.95 +  unfolding mem_def Respects_def
    1.96 +  by simp
    1.97 +
    1.98 +section {* Function map and function relation *}
    1.99 +
   1.100 +definition
   1.101 +  fun_map (infixr "--->" 55)
   1.102 +where
   1.103 +[simp]: "fun_map f g h x = g (h (f x))"
   1.104 +
   1.105 +definition
   1.106 +  fun_rel (infixr "===>" 55)
   1.107 +where
   1.108 +[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
   1.109 +
   1.110 +
   1.111 +lemma fun_map_id:
   1.112 +  shows "(id ---> id) = id"
   1.113 +  by (simp add: expand_fun_eq id_def)
   1.114 +
   1.115 +lemma fun_rel_eq:
   1.116 +  shows "((op =) ===> (op =)) = (op =)"
   1.117 +  by (simp add: expand_fun_eq)
   1.118 +
   1.119 +lemma fun_rel_id:
   1.120 +  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
   1.121 +  shows "(R1 ===> R2) f g"
   1.122 +  using a by simp
   1.123 +
   1.124 +lemma fun_rel_id_asm:
   1.125 +  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
   1.126 +  shows "A \<longrightarrow> (R1 ===> R2) f g"
   1.127 +  using a by auto
   1.128 +
   1.129 +
   1.130 +section {* Quotient Predicate *}
   1.131 +
   1.132 +definition
   1.133 +  "Quotient E Abs Rep \<equiv>
   1.134 +     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
   1.135 +     (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
   1.136 +
   1.137 +lemma Quotient_abs_rep:
   1.138 +  assumes a: "Quotient E Abs Rep"
   1.139 +  shows "Abs (Rep a) = a"
   1.140 +  using a
   1.141 +  unfolding Quotient_def
   1.142 +  by simp
   1.143 +
   1.144 +lemma Quotient_rep_reflp:
   1.145 +  assumes a: "Quotient E Abs Rep"
   1.146 +  shows "E (Rep a) (Rep a)"
   1.147 +  using a
   1.148 +  unfolding Quotient_def
   1.149 +  by blast
   1.150 +
   1.151 +lemma Quotient_rel:
   1.152 +  assumes a: "Quotient E Abs Rep"
   1.153 +  shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
   1.154 +  using a
   1.155 +  unfolding Quotient_def
   1.156 +  by blast
   1.157 +
   1.158 +lemma Quotient_rel_rep:
   1.159 +  assumes a: "Quotient R Abs Rep"
   1.160 +  shows "R (Rep a) (Rep b) = (a = b)"
   1.161 +  using a
   1.162 +  unfolding Quotient_def
   1.163 +  by metis
   1.164 +
   1.165 +lemma Quotient_rep_abs:
   1.166 +  assumes a: "Quotient R Abs Rep"
   1.167 +  shows "R r r \<Longrightarrow> R (Rep (Abs r)) r"
   1.168 +  using a unfolding Quotient_def
   1.169 +  by blast
   1.170 +
   1.171 +lemma Quotient_rel_abs:
   1.172 +  assumes a: "Quotient E Abs Rep"
   1.173 +  shows "E r s \<Longrightarrow> Abs r = Abs s"
   1.174 +  using a unfolding Quotient_def
   1.175 +  by blast
   1.176 +
   1.177 +lemma Quotient_symp:
   1.178 +  assumes a: "Quotient E Abs Rep"
   1.179 +  shows "symp E"
   1.180 +  using a unfolding Quotient_def symp_def
   1.181 +  by metis
   1.182 +
   1.183 +lemma Quotient_transp:
   1.184 +  assumes a: "Quotient E Abs Rep"
   1.185 +  shows "transp E"
   1.186 +  using a unfolding Quotient_def transp_def
   1.187 +  by metis
   1.188 +
   1.189 +lemma identity_quotient:
   1.190 +  shows "Quotient (op =) id id"
   1.191 +  unfolding Quotient_def id_def
   1.192 +  by blast
   1.193 +
   1.194 +lemma fun_quotient:
   1.195 +  assumes q1: "Quotient R1 abs1 rep1"
   1.196 +  and     q2: "Quotient R2 abs2 rep2"
   1.197 +  shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.198 +proof -
   1.199 +  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   1.200 +    using q1 q2
   1.201 +    unfolding Quotient_def
   1.202 +    unfolding expand_fun_eq
   1.203 +    by simp
   1.204 +  moreover
   1.205 +  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   1.206 +    using q1 q2
   1.207 +    unfolding Quotient_def
   1.208 +    by (simp (no_asm)) (metis)
   1.209 +  moreover
   1.210 +  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.211 +        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   1.212 +    unfolding expand_fun_eq
   1.213 +    apply(auto)
   1.214 +    using q1 q2 unfolding Quotient_def
   1.215 +    apply(metis)
   1.216 +    using q1 q2 unfolding Quotient_def
   1.217 +    apply(metis)
   1.218 +    using q1 q2 unfolding Quotient_def
   1.219 +    apply(metis)
   1.220 +    using q1 q2 unfolding Quotient_def
   1.221 +    apply(metis)
   1.222 +    done
   1.223 +  ultimately
   1.224 +  show "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.225 +    unfolding Quotient_def by blast
   1.226 +qed
   1.227 +
   1.228 +lemma abs_o_rep:
   1.229 +  assumes a: "Quotient R Abs Rep"
   1.230 +  shows "Abs o Rep = id"
   1.231 +  unfolding expand_fun_eq
   1.232 +  by (simp add: Quotient_abs_rep[OF a])
   1.233 +
   1.234 +lemma equals_rsp:
   1.235 +  assumes q: "Quotient R Abs Rep"
   1.236 +  and     a: "R xa xb" "R ya yb"
   1.237 +  shows "R xa ya = R xb yb"
   1.238 +  using a Quotient_symp[OF q] Quotient_transp[OF q]
   1.239 +  unfolding symp_def transp_def
   1.240 +  by blast
   1.241 +
   1.242 +lemma lambda_prs:
   1.243 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.244 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.245 +  shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   1.246 +  unfolding expand_fun_eq
   1.247 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.248 +  by simp
   1.249 +
   1.250 +lemma lambda_prs1:
   1.251 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.252 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.253 +  shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   1.254 +  unfolding expand_fun_eq
   1.255 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.256 +  by simp
   1.257 +
   1.258 +lemma rep_abs_rsp:
   1.259 +  assumes q: "Quotient R Abs Rep"
   1.260 +  and     a: "R x1 x2"
   1.261 +  shows "R x1 (Rep (Abs x2))"
   1.262 +  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   1.263 +  by metis
   1.264 +
   1.265 +lemma rep_abs_rsp_left:
   1.266 +  assumes q: "Quotient R Abs Rep"
   1.267 +  and     a: "R x1 x2"
   1.268 +  shows "R (Rep (Abs x1)) x2"
   1.269 +  using a Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]
   1.270 +  by metis
   1.271 +
   1.272 +text{*
   1.273 +  In the following theorem R1 can be instantiated with anything,
   1.274 +  but we know some of the types of the Rep and Abs functions;
   1.275 +  so by solving Quotient assumptions we can get a unique R1 that
   1.276 +  will be provable; which is why we need to use apply_rsp and
   1.277 +  not the primed version *}
   1.278 +
   1.279 +lemma apply_rsp:
   1.280 +  fixes f g::"'a \<Rightarrow> 'c"
   1.281 +  assumes q: "Quotient R1 Abs1 Rep1"
   1.282 +  and     a: "(R1 ===> R2) f g" "R1 x y"
   1.283 +  shows "R2 (f x) (g y)"
   1.284 +  using a by simp
   1.285 +
   1.286 +lemma apply_rsp':
   1.287 +  assumes a: "(R1 ===> R2) f g" "R1 x y"
   1.288 +  shows "R2 (f x) (g y)"
   1.289 +  using a by simp
   1.290 +
   1.291 +section {* lemmas for regularisation of ball and bex *}
   1.292 +
   1.293 +lemma ball_reg_eqv:
   1.294 +  fixes P :: "'a \<Rightarrow> bool"
   1.295 +  assumes a: "equivp R"
   1.296 +  shows "Ball (Respects R) P = (All P)"
   1.297 +  using a
   1.298 +  unfolding equivp_def
   1.299 +  by (auto simp add: in_respects)
   1.300 +
   1.301 +lemma bex_reg_eqv:
   1.302 +  fixes P :: "'a \<Rightarrow> bool"
   1.303 +  assumes a: "equivp R"
   1.304 +  shows "Bex (Respects R) P = (Ex P)"
   1.305 +  using a
   1.306 +  unfolding equivp_def
   1.307 +  by (auto simp add: in_respects)
   1.308 +
   1.309 +lemma ball_reg_right:
   1.310 +  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
   1.311 +  shows "All P \<longrightarrow> Ball R Q"
   1.312 +  using a by (metis COMBC_def Collect_def Collect_mem_eq)
   1.313 +
   1.314 +lemma bex_reg_left:
   1.315 +  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
   1.316 +  shows "Bex R Q \<longrightarrow> Ex P"
   1.317 +  using a by (metis COMBC_def Collect_def Collect_mem_eq)
   1.318 +
   1.319 +lemma ball_reg_left:
   1.320 +  assumes a: "equivp R"
   1.321 +  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
   1.322 +  using a by (metis equivp_reflp in_respects)
   1.323 +
   1.324 +lemma bex_reg_right:
   1.325 +  assumes a: "equivp R"
   1.326 +  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
   1.327 +  using a by (metis equivp_reflp in_respects)
   1.328 +
   1.329 +lemma ball_reg_eqv_range:
   1.330 +  fixes P::"'a \<Rightarrow> bool"
   1.331 +  and x::"'a"
   1.332 +  assumes a: "equivp R2"
   1.333 +  shows   "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
   1.334 +  apply(rule iffI)
   1.335 +  apply(rule allI)
   1.336 +  apply(drule_tac x="\<lambda>y. f x" in bspec)
   1.337 +  apply(simp add: in_respects)
   1.338 +  apply(rule impI)
   1.339 +  using a equivp_reflp_symp_transp[of "R2"]
   1.340 +  apply(simp add: reflp_def)
   1.341 +  apply(simp)
   1.342 +  apply(simp)
   1.343 +  done
   1.344 +
   1.345 +lemma bex_reg_eqv_range:
   1.346 +  assumes a: "equivp R2"
   1.347 +  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
   1.348 +  apply(auto)
   1.349 +  apply(rule_tac x="\<lambda>y. f x" in bexI)
   1.350 +  apply(simp)
   1.351 +  apply(simp add: Respects_def in_respects)
   1.352 +  apply(rule impI)
   1.353 +  using a equivp_reflp_symp_transp[of "R2"]
   1.354 +  apply(simp add: reflp_def)
   1.355 +  done
   1.356 +
   1.357 +(* Next four lemmas are unused *)
   1.358 +lemma all_reg:
   1.359 +  assumes a: "!x :: 'a. (P x --> Q x)"
   1.360 +  and     b: "All P"
   1.361 +  shows "All Q"
   1.362 +  using a b by (metis)
   1.363 +
   1.364 +lemma ex_reg:
   1.365 +  assumes a: "!x :: 'a. (P x --> Q x)"
   1.366 +  and     b: "Ex P"
   1.367 +  shows "Ex Q"
   1.368 +  using a b by metis
   1.369 +
   1.370 +lemma ball_reg:
   1.371 +  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   1.372 +  and     b: "Ball R P"
   1.373 +  shows "Ball R Q"
   1.374 +  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
   1.375 +
   1.376 +lemma bex_reg:
   1.377 +  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
   1.378 +  and     b: "Bex R P"
   1.379 +  shows "Bex R Q"
   1.380 +  using a b by (metis COMBC_def Collect_def Collect_mem_eq)
   1.381 +
   1.382 +
   1.383 +lemma ball_all_comm:
   1.384 +  assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
   1.385 +  shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
   1.386 +  using assms by auto
   1.387 +
   1.388 +lemma bex_ex_comm:
   1.389 +  assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
   1.390 +  shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
   1.391 +  using assms by auto
   1.392 +
   1.393 +section {* Bounded abstraction *}
   1.394 +
   1.395 +definition
   1.396 +  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.397 +where
   1.398 +  "x \<in> p \<Longrightarrow> Babs p m x = m x"
   1.399 +
   1.400 +lemma babs_rsp:
   1.401 +  assumes q: "Quotient R1 Abs1 Rep1"
   1.402 +  and     a: "(R1 ===> R2) f g"
   1.403 +  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   1.404 +  apply (auto simp add: Babs_def in_respects)
   1.405 +  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.406 +  using a apply (simp add: Babs_def)
   1.407 +  apply (simp add: in_respects)
   1.408 +  using Quotient_rel[OF q]
   1.409 +  by metis
   1.410 +
   1.411 +lemma babs_prs:
   1.412 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.413 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.414 +  shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   1.415 +  apply (rule ext)
   1.416 +  apply (simp)
   1.417 +  apply (subgoal_tac "Rep1 x \<in> Respects R1")
   1.418 +  apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   1.419 +  apply (simp add: in_respects Quotient_rel_rep[OF q1])
   1.420 +  done
   1.421 +
   1.422 +lemma babs_simp:
   1.423 +  assumes q: "Quotient R1 Abs Rep"
   1.424 +  shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   1.425 +  apply(rule iffI)
   1.426 +  apply(simp_all only: babs_rsp[OF q])
   1.427 +  apply(auto simp add: Babs_def)
   1.428 +  apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.429 +  apply(metis Babs_def)
   1.430 +  apply (simp add: in_respects)
   1.431 +  using Quotient_rel[OF q]
   1.432 +  by metis
   1.433 +
   1.434 +(* If a user proves that a particular functional relation
   1.435 +   is an equivalence this may be useful in regularising *)
   1.436 +lemma babs_reg_eqv:
   1.437 +  shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   1.438 +  by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
   1.439 +
   1.440 +
   1.441 +(* 3 lemmas needed for proving repabs_inj *)
   1.442 +lemma ball_rsp:
   1.443 +  assumes a: "(R ===> (op =)) f g"
   1.444 +  shows "Ball (Respects R) f = Ball (Respects R) g"
   1.445 +  using a by (simp add: Ball_def in_respects)
   1.446 +
   1.447 +lemma bex_rsp:
   1.448 +  assumes a: "(R ===> (op =)) f g"
   1.449 +  shows "(Bex (Respects R) f = Bex (Respects R) g)"
   1.450 +  using a by (simp add: Bex_def in_respects)
   1.451 +
   1.452 +lemma bex1_rsp:
   1.453 +  assumes a: "(R ===> (op =)) f g"
   1.454 +  shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   1.455 +  using a
   1.456 +  by (simp add: Ex1_def in_respects) auto
   1.457 +
   1.458 +(* 2 lemmas needed for cleaning of quantifiers *)
   1.459 +lemma all_prs:
   1.460 +  assumes a: "Quotient R absf repf"
   1.461 +  shows "Ball (Respects R) ((absf ---> id) f) = All f"
   1.462 +  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
   1.463 +  by metis
   1.464 +
   1.465 +lemma ex_prs:
   1.466 +  assumes a: "Quotient R absf repf"
   1.467 +  shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   1.468 +  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   1.469 +  by metis
   1.470 +
   1.471 +section {* Bex1_rel quantifier *}
   1.472 +
   1.473 +definition
   1.474 +  Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   1.475 +where
   1.476 +  "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
   1.477 +
   1.478 +lemma bex1_rel_aux:
   1.479 +  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
   1.480 +  unfolding Bex1_rel_def
   1.481 +  apply (erule conjE)+
   1.482 +  apply (erule bexE)
   1.483 +  apply rule
   1.484 +  apply (rule_tac x="xa" in bexI)
   1.485 +  apply metis
   1.486 +  apply metis
   1.487 +  apply rule+
   1.488 +  apply (erule_tac x="xaa" in ballE)
   1.489 +  prefer 2
   1.490 +  apply (metis)
   1.491 +  apply (erule_tac x="ya" in ballE)
   1.492 +  prefer 2
   1.493 +  apply (metis)
   1.494 +  apply (metis in_respects)
   1.495 +  done
   1.496 +
   1.497 +lemma bex1_rel_aux2:
   1.498 +  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
   1.499 +  unfolding Bex1_rel_def
   1.500 +  apply (erule conjE)+
   1.501 +  apply (erule bexE)
   1.502 +  apply rule
   1.503 +  apply (rule_tac x="xa" in bexI)
   1.504 +  apply metis
   1.505 +  apply metis
   1.506 +  apply rule+
   1.507 +  apply (erule_tac x="xaa" in ballE)
   1.508 +  prefer 2
   1.509 +  apply (metis)
   1.510 +  apply (erule_tac x="ya" in ballE)
   1.511 +  prefer 2
   1.512 +  apply (metis)
   1.513 +  apply (metis in_respects)
   1.514 +  done
   1.515 +
   1.516 +lemma bex1_rel_rsp:
   1.517 +  assumes a: "Quotient R absf repf"
   1.518 +  shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   1.519 +  apply simp
   1.520 +  apply clarify
   1.521 +  apply rule
   1.522 +  apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
   1.523 +  apply (erule bex1_rel_aux2)
   1.524 +  apply assumption
   1.525 +  done
   1.526 +
   1.527 +
   1.528 +lemma ex1_prs:
   1.529 +  assumes a: "Quotient R absf repf"
   1.530 +  shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
   1.531 +apply simp
   1.532 +apply (subst Bex1_rel_def)
   1.533 +apply (subst Bex_def)
   1.534 +apply (subst Ex1_def)
   1.535 +apply simp
   1.536 +apply rule
   1.537 + apply (erule conjE)+
   1.538 + apply (erule_tac exE)
   1.539 + apply (erule conjE)
   1.540 + apply (subgoal_tac "\<forall>y. R y y \<longrightarrow> f (absf y) \<longrightarrow> R x y")
   1.541 +  apply (rule_tac x="absf x" in exI)
   1.542 +  apply (simp)
   1.543 +  apply rule+
   1.544 +  using a unfolding Quotient_def
   1.545 +  apply metis
   1.546 + apply rule+
   1.547 + apply (erule_tac x="x" in ballE)
   1.548 +  apply (erule_tac x="y" in ballE)
   1.549 +   apply simp
   1.550 +  apply (simp add: in_respects)
   1.551 + apply (simp add: in_respects)
   1.552 +apply (erule_tac exE)
   1.553 + apply rule
   1.554 + apply (rule_tac x="repf x" in exI)
   1.555 + apply (simp only: in_respects)
   1.556 +  apply rule
   1.557 + apply (metis Quotient_rel_rep[OF a])
   1.558 +using a unfolding Quotient_def apply (simp)
   1.559 +apply rule+
   1.560 +using a unfolding Quotient_def in_respects
   1.561 +apply metis
   1.562 +done
   1.563 +
   1.564 +lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
   1.565 +  apply (simp add: Ex1_def Bex1_rel_def in_respects)
   1.566 +  apply clarify
   1.567 +  apply auto
   1.568 +  apply (rule bexI)
   1.569 +  apply assumption
   1.570 +  apply (simp add: in_respects)
   1.571 +  apply (simp add: in_respects)
   1.572 +  apply auto
   1.573 +  done
   1.574 +
   1.575 +section {* Various respects and preserve lemmas *}
   1.576 +
   1.577 +lemma quot_rel_rsp:
   1.578 +  assumes a: "Quotient R Abs Rep"
   1.579 +  shows "(R ===> R ===> op =) R R"
   1.580 +  apply(rule fun_rel_id)+
   1.581 +  apply(rule equals_rsp[OF a])
   1.582 +  apply(assumption)+
   1.583 +  done
   1.584 +
   1.585 +lemma o_prs:
   1.586 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.587 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.588 +  and     q3: "Quotient R3 Abs3 Rep3"
   1.589 +  shows "(Rep1 ---> Abs3) (((Abs2 ---> Rep3) f) o ((Abs1 ---> Rep2) g)) = f o g"
   1.590 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
   1.591 +  unfolding o_def expand_fun_eq by simp
   1.592 +
   1.593 +lemma o_rsp:
   1.594 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.595 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.596 +  and     q3: "Quotient R3 Abs3 Rep3"
   1.597 +  and     a1: "(R2 ===> R3) f1 f2"
   1.598 +  and     a2: "(R1 ===> R2) g1 g2"
   1.599 +  shows "(R1 ===> R3) (f1 o g1) (f2 o g2)"
   1.600 +  using a1 a2 unfolding o_def expand_fun_eq
   1.601 +  by (auto)
   1.602 +
   1.603 +lemma cond_prs:
   1.604 +  assumes a: "Quotient R absf repf"
   1.605 +  shows "absf (if a then repf b else repf c) = (if a then b else c)"
   1.606 +  using a unfolding Quotient_def by auto
   1.607 +
   1.608 +lemma if_prs:
   1.609 +  assumes q: "Quotient R Abs Rep"
   1.610 +  shows "Abs (If a (Rep b) (Rep c)) = If a b c"
   1.611 +  using Quotient_abs_rep[OF q] by auto
   1.612 +
   1.613 +(* q not used *)
   1.614 +lemma if_rsp:
   1.615 +  assumes q: "Quotient R Abs Rep"
   1.616 +  and     a: "a1 = a2" "R b1 b2" "R c1 c2"
   1.617 +  shows "R (If a1 b1 c1) (If a2 b2 c2)"
   1.618 +  using a by auto
   1.619 +
   1.620 +lemma let_prs:
   1.621 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.622 +  and     q2: "Quotient R2 Abs2 Rep2"
   1.623 +  shows "Abs2 (Let (Rep1 x) ((Abs1 ---> Rep2) f)) = Let x f"
   1.624 +  using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] by auto
   1.625 +
   1.626 +lemma let_rsp:
   1.627 +  assumes q1: "Quotient R1 Abs1 Rep1"
   1.628 +  and     a1: "(R1 ===> R2) f g"
   1.629 +  and     a2: "R1 x y"
   1.630 +  shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
   1.631 +  using apply_rsp[OF q1 a1] a2 by auto
   1.632 +
   1.633 +locale quot_type =
   1.634 +  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.635 +  and   Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b"
   1.636 +  and   Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)"
   1.637 +  assumes equivp: "equivp R"
   1.638 +  and     rep_prop: "\<And>y. \<exists>x. Rep y = R x"
   1.639 +  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
   1.640 +  and     abs_inverse: "\<And>x. (Rep (Abs (R x))) = (R x)"
   1.641 +  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
   1.642 +begin
   1.643 +
   1.644 +definition
   1.645 +  abs::"'a \<Rightarrow> 'b"
   1.646 +where
   1.647 +  "abs x \<equiv> Abs (R x)"
   1.648 +
   1.649 +definition
   1.650 +  rep::"'b \<Rightarrow> 'a"
   1.651 +where
   1.652 +  "rep a = Eps (Rep a)"
   1.653 +
   1.654 +lemma homeier_lem9:
   1.655 +  shows "R (Eps (R x)) = R x"
   1.656 +proof -
   1.657 +  have a: "R x x" using equivp by (simp add: equivp_reflp_symp_transp reflp_def)
   1.658 +  then have "R x (Eps (R x))" by (rule someI)
   1.659 +  then show "R (Eps (R x)) = R x"
   1.660 +    using equivp unfolding equivp_def by simp
   1.661 +qed
   1.662 +
   1.663 +theorem homeier_thm10:
   1.664 +  shows "abs (rep a) = a"
   1.665 +  unfolding abs_def rep_def
   1.666 +proof -
   1.667 +  from rep_prop
   1.668 +  obtain x where eq: "Rep a = R x" by auto
   1.669 +  have "Abs (R (Eps (Rep a))) = Abs (R (Eps (R x)))" using eq by simp
   1.670 +  also have "\<dots> = Abs (R x)" using homeier_lem9 by simp
   1.671 +  also have "\<dots> = Abs (Rep a)" using eq by simp
   1.672 +  also have "\<dots> = a" using rep_inverse by simp
   1.673 +  finally
   1.674 +  show "Abs (R (Eps (Rep a))) = a" by simp
   1.675 +qed
   1.676 +
   1.677 +lemma homeier_lem7:
   1.678 +  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
   1.679 +proof -
   1.680 +  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
   1.681 +  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
   1.682 +  finally show "?LHS = ?RHS" by simp
   1.683 +qed
   1.684 +
   1.685 +theorem homeier_thm11:
   1.686 +  shows "R r r' = (abs r = abs r')"
   1.687 +  unfolding abs_def
   1.688 +  by (simp only: equivp[simplified equivp_def] homeier_lem7)
   1.689 +
   1.690 +lemma rep_refl:
   1.691 +  shows "R (rep a) (rep a)"
   1.692 +  unfolding rep_def
   1.693 +  by (simp add: equivp[simplified equivp_def])
   1.694 +
   1.695 +
   1.696 +lemma rep_abs_rsp:
   1.697 +  shows "R f (rep (abs g)) = R f g"
   1.698 +  and   "R (rep (abs g)) f = R g f"
   1.699 +  by (simp_all add: homeier_thm10 homeier_thm11)
   1.700 +
   1.701 +lemma Quotient:
   1.702 +  shows "Quotient R abs rep"
   1.703 +  unfolding Quotient_def
   1.704 +  apply(simp add: homeier_thm10)
   1.705 +  apply(simp add: rep_refl)
   1.706 +  apply(subst homeier_thm11[symmetric])
   1.707 +  apply(simp add: equivp[simplified equivp_def])
   1.708 +  done
   1.709 +
   1.710 +end
   1.711 +
   1.712 +section {* ML setup *}
   1.713 +
   1.714 +text {* Auxiliary data for the quotient package *}
   1.715 +
   1.716 +use "~~/src/HOL/Tools/Quotient/quotient_info.ML"
   1.717 +
   1.718 +declare [[map "fun" = (fun_map, fun_rel)]]
   1.719 +
   1.720 +lemmas [quot_thm] = fun_quotient
   1.721 +lemmas [quot_respect] = quot_rel_rsp
   1.722 +lemmas [quot_equiv] = identity_equivp
   1.723 +
   1.724 +
   1.725 +text {* Lemmas about simplifying id's. *}
   1.726 +lemmas [id_simps] =
   1.727 +  id_def[symmetric]
   1.728 +  fun_map_id
   1.729 +  id_apply
   1.730 +  id_o
   1.731 +  o_id
   1.732 +  eq_comp_r
   1.733 +
   1.734 +text {* Translation functions for the lifting process. *}
   1.735 +use "~~/src/HOL/Tools/Quotient/quotient_term.ML"
   1.736 +
   1.737 +
   1.738 +text {* Definitions of the quotient types. *}
   1.739 +use "~~/src/HOL/Tools/Quotient/quotient_typ.ML"
   1.740 +
   1.741 +
   1.742 +text {* Definitions for quotient constants. *}
   1.743 +use "~~/src/HOL/Tools/Quotient/quotient_def.ML"
   1.744 +
   1.745 +
   1.746 +text {*
   1.747 +  An auxiliary constant for recording some information
   1.748 +  about the lifted theorem in a tactic.
   1.749 +*}
   1.750 +definition
   1.751 +  "Quot_True x \<equiv> True"
   1.752 +
   1.753 +lemma
   1.754 +  shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   1.755 +  and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
   1.756 +  and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
   1.757 +  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
   1.758 +  and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
   1.759 +  by (simp_all add: Quot_True_def ext)
   1.760 +
   1.761 +lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
   1.762 +  by (simp add: Quot_True_def)
   1.763 +
   1.764 +
   1.765 +text {* Tactics for proving the lifted theorems *}
   1.766 +use "~~/src/HOL/Tools/Quotient/quotient_tacs.ML"
   1.767 +
   1.768 +section {* Methods / Interface *}
   1.769 +
   1.770 +method_setup lifting =
   1.771 +  {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt thms))) *}
   1.772 +  {* lifts theorems to quotient types *}
   1.773 +
   1.774 +method_setup lifting_setup =
   1.775 +  {* Attrib.thm >> (fn thms => fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.procedure_tac ctxt thms))) *}
   1.776 +  {* sets up the three goals for the quotient lifting procedure *}
   1.777 +
   1.778 +method_setup regularize =
   1.779 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   1.780 +  {* proves the regularization goals from the quotient lifting procedure *}
   1.781 +
   1.782 +method_setup injection =
   1.783 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
   1.784 +  {* proves the rep/abs injection goals from the quotient lifting procedure *}
   1.785 +
   1.786 +method_setup cleaning =
   1.787 +  {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
   1.788 +  {* proves the cleaning goals from the quotient lifting procedure *}
   1.789 +
   1.790 +attribute_setup quot_lifted =
   1.791 +  {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   1.792 +  {* lifts theorems to quotient types *}
   1.793 +
   1.794 +no_notation
   1.795 +  rel_conj (infixr "OOO" 75) and
   1.796 +  fun_map (infixr "--->" 55) and
   1.797 +  fun_rel (infixr "===>" 55)
   1.798 +
   1.799 +end
   1.800 +