src/HOL/Quotient.thy
changeset 60758 d8d85a8172b5
parent 59028 df7476e79558
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Quotient.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Cezary Kaliszyk and Christian Urban
     1.5  *)
     1.6  
     1.7 -section {* Definition of Quotient Types *}
     1.8 +section \<open>Definition of Quotient Types\<close>
     1.9  
    1.10  theory Quotient
    1.11  imports Lifting
    1.12 @@ -12,12 +12,12 @@
    1.13    "quotient_definition" :: thy_goal
    1.14  begin
    1.15  
    1.16 -text {*
    1.17 +text \<open>
    1.18    Basic definition for equivalence relations
    1.19    that are represented by predicates.
    1.20 -*}
    1.21 +\<close>
    1.22  
    1.23 -text {* Composition of Relations *}
    1.24 +text \<open>Composition of Relations\<close>
    1.25  
    1.26  abbreviation
    1.27    rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
    1.28 @@ -32,7 +32,7 @@
    1.29  begin
    1.30  interpretation lifting_syntax .
    1.31  
    1.32 -subsection {* Quotient Predicate *}
    1.33 +subsection \<open>Quotient Predicate\<close>
    1.34  
    1.35  definition
    1.36    "Quotient3 R Abs Rep \<longleftrightarrow>
    1.37 @@ -64,7 +64,7 @@
    1.38    by blast
    1.39  
    1.40  lemma Quotient3_rel:
    1.41 -  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.42 +  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- \<open>orientation does not loop on rewriting\<close>
    1.43    using a
    1.44    unfolding Quotient3_def
    1.45    by blast
    1.46 @@ -192,12 +192,12 @@
    1.47    using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
    1.48    by simp
    1.49  
    1.50 -text{*
    1.51 +text\<open>
    1.52    In the following theorem R1 can be instantiated with anything,
    1.53    but we know some of the types of the Rep and Abs functions;
    1.54    so by solving Quotient assumptions we can get a unique R1 that
    1.55    will be provable; which is why we need to use @{text apply_rsp} and
    1.56 -  not the primed version *}
    1.57 +  not the primed version\<close>
    1.58  
    1.59  lemma apply_rspQ3:
    1.60    fixes f g::"'a \<Rightarrow> 'c"
    1.61 @@ -215,7 +215,7 @@
    1.62    then show ?thesis using assms(2) by (auto intro: apply_rsp')
    1.63  qed
    1.64  
    1.65 -subsection {* lemmas for regularisation of ball and bex *}
    1.66 +subsection \<open>lemmas for regularisation of ball and bex\<close>
    1.67  
    1.68  lemma ball_reg_eqv:
    1.69    fixes P :: "'a \<Rightarrow> bool"
    1.70 @@ -315,7 +315,7 @@
    1.71    shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
    1.72    using assms by auto
    1.73  
    1.74 -subsection {* Bounded abstraction *}
    1.75 +subsection \<open>Bounded abstraction\<close>
    1.76  
    1.77  definition
    1.78    Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    1.79 @@ -392,7 +392,7 @@
    1.80    using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
    1.81    by metis
    1.82  
    1.83 -subsection {* @{text Bex1_rel} quantifier *}
    1.84 +subsection \<open>@{text Bex1_rel} quantifier\<close>
    1.85  
    1.86  definition
    1.87    Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
    1.88 @@ -506,7 +506,7 @@
    1.89    apply simp
    1.90    done
    1.91  
    1.92 -subsection {* Various respects and preserve lemmas *}
    1.93 +subsection \<open>Various respects and preserve lemmas\<close>
    1.94  
    1.95  lemma quot_rel_rsp:
    1.96    assumes a: "Quotient3 R Abs Rep"
    1.97 @@ -605,7 +605,7 @@
    1.98        have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
    1.99        then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
   1.100        then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
   1.101 -        using part_equivp_transp[OF equivp] by (metis `R (SOME x. x \<in> Rep a) x`)
   1.102 +        using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
   1.103      qed
   1.104      have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
   1.105      then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
   1.106 @@ -624,7 +624,7 @@
   1.107  
   1.108  end
   1.109  
   1.110 -subsection {* Quotient composition *}
   1.111 +subsection \<open>Quotient composition\<close>
   1.112  
   1.113  lemma OOO_quotient3:
   1.114    fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.115 @@ -718,7 +718,7 @@
   1.116  using assms
   1.117  by (rule OOO_quotient3) auto
   1.118  
   1.119 -subsection {* Quotient3 to Quotient *}
   1.120 +subsection \<open>Quotient3 to Quotient\<close>
   1.121  
   1.122  lemma Quotient3_to_Quotient:
   1.123  assumes "Quotient3 R Abs Rep"
   1.124 @@ -744,9 +744,9 @@
   1.125    show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
   1.126  qed
   1.127  
   1.128 -subsection {* ML setup *}
   1.129 +subsection \<open>ML setup\<close>
   1.130  
   1.131 -text {* Auxiliary data for the quotient package *}
   1.132 +text \<open>Auxiliary data for the quotient package\<close>
   1.133  
   1.134  named_theorems quot_equiv "equivalence relation theorems"
   1.135    and quot_respect "respectfulness theorems"
   1.136 @@ -763,7 +763,7 @@
   1.137  lemmas [quot_equiv] = identity_equivp
   1.138  
   1.139  
   1.140 -text {* Lemmas about simplifying id's. *}
   1.141 +text \<open>Lemmas about simplifying id's.\<close>
   1.142  lemmas [id_simps] =
   1.143    id_def[symmetric]
   1.144    map_fun_id
   1.145 @@ -773,22 +773,22 @@
   1.146    eq_comp_r
   1.147    vimage_id
   1.148  
   1.149 -text {* Translation functions for the lifting process. *}
   1.150 +text \<open>Translation functions for the lifting process.\<close>
   1.151  ML_file "Tools/Quotient/quotient_term.ML"
   1.152  
   1.153  
   1.154 -text {* Definitions of the quotient types. *}
   1.155 +text \<open>Definitions of the quotient types.\<close>
   1.156  ML_file "Tools/Quotient/quotient_type.ML"
   1.157  
   1.158  
   1.159 -text {* Definitions for quotient constants. *}
   1.160 +text \<open>Definitions for quotient constants.\<close>
   1.161  ML_file "Tools/Quotient/quotient_def.ML"
   1.162  
   1.163  
   1.164 -text {*
   1.165 +text \<open>
   1.166    An auxiliary constant for recording some information
   1.167    about the lifted theorem in a tactic.
   1.168 -*}
   1.169 +\<close>
   1.170  definition
   1.171    Quot_True :: "'a \<Rightarrow> bool"
   1.172  where
   1.173 @@ -809,55 +809,55 @@
   1.174  begin
   1.175  interpretation lifting_syntax .
   1.176  
   1.177 -text {* Tactics for proving the lifted theorems *}
   1.178 +text \<open>Tactics for proving the lifted theorems\<close>
   1.179  ML_file "Tools/Quotient/quotient_tacs.ML"
   1.180  
   1.181  end
   1.182  
   1.183 -subsection {* Methods / Interface *}
   1.184 +subsection \<open>Methods / Interface\<close>
   1.185  
   1.186  method_setup lifting =
   1.187 -  {* Attrib.thms >> (fn thms => fn ctxt => 
   1.188 -       SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms)) *}
   1.189 -  {* lift theorems to quotient types *}
   1.190 +  \<open>Attrib.thms >> (fn thms => fn ctxt => 
   1.191 +       SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\<close>
   1.192 +  \<open>lift theorems to quotient types\<close>
   1.193  
   1.194  method_setup lifting_setup =
   1.195 -  {* Attrib.thm >> (fn thm => fn ctxt => 
   1.196 -       SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm)) *}
   1.197 -  {* set up the three goals for the quotient lifting procedure *}
   1.198 +  \<open>Attrib.thm >> (fn thm => fn ctxt => 
   1.199 +       SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\<close>
   1.200 +  \<open>set up the three goals for the quotient lifting procedure\<close>
   1.201  
   1.202  method_setup descending =
   1.203 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt [])) *}
   1.204 -  {* decend theorems to the raw level *}
   1.205 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\<close>
   1.206 +  \<open>decend theorems to the raw level\<close>
   1.207  
   1.208  method_setup descending_setup =
   1.209 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt [])) *}
   1.210 -  {* set up the three goals for the decending theorems *}
   1.211 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\<close>
   1.212 +  \<open>set up the three goals for the decending theorems\<close>
   1.213  
   1.214  method_setup partiality_descending =
   1.215 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt [])) *}
   1.216 -  {* decend theorems to the raw level *}
   1.217 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\<close>
   1.218 +  \<open>decend theorems to the raw level\<close>
   1.219  
   1.220  method_setup partiality_descending_setup =
   1.221 -  {* Scan.succeed (fn ctxt => 
   1.222 -       SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt [])) *}
   1.223 -  {* set up the three goals for the decending theorems *}
   1.224 +  \<open>Scan.succeed (fn ctxt => 
   1.225 +       SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\<close>
   1.226 +  \<open>set up the three goals for the decending theorems\<close>
   1.227  
   1.228  method_setup regularize =
   1.229 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt)) *}
   1.230 -  {* prove the regularization goals from the quotient lifting procedure *}
   1.231 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\<close>
   1.232 +  \<open>prove the regularization goals from the quotient lifting procedure\<close>
   1.233  
   1.234  method_setup injection =
   1.235 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt)) *}
   1.236 -  {* prove the rep/abs injection goals from the quotient lifting procedure *}
   1.237 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\<close>
   1.238 +  \<open>prove the rep/abs injection goals from the quotient lifting procedure\<close>
   1.239  
   1.240  method_setup cleaning =
   1.241 -  {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt)) *}
   1.242 -  {* prove the cleaning goals from the quotient lifting procedure *}
   1.243 +  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\<close>
   1.244 +  \<open>prove the cleaning goals from the quotient lifting procedure\<close>
   1.245  
   1.246  attribute_setup quot_lifted =
   1.247 -  {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   1.248 -  {* lift theorems to quotient types *}
   1.249 +  \<open>Scan.succeed Quotient_Tacs.lifted_attrib\<close>
   1.250 +  \<open>lift theorems to quotient types\<close>
   1.251  
   1.252  no_notation
   1.253    rel_conj (infixr "OOO" 75)