src/HOL/Lifting.thy
changeset 60758 d8d85a8172b5
parent 60229 4cd6462c1fda
child 61630 608520e0e8e2
     1.1 --- a/src/HOL/Lifting.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4      Author:     Cezary Kaliszyk and Christian Urban
     1.5  *)
     1.6  
     1.7 -section {* Lifting package *}
     1.8 +section \<open>Lifting package\<close>
     1.9  
    1.10  theory Lifting
    1.11  imports Equiv_Relations Transfer
    1.12 @@ -14,7 +14,7 @@
    1.13    "setup_lifting" "lifting_forget" "lifting_update" :: thy_decl
    1.14  begin
    1.15  
    1.16 -subsection {* Function map *}
    1.17 +subsection \<open>Function map\<close>
    1.18  
    1.19  context
    1.20  begin
    1.21 @@ -24,7 +24,7 @@
    1.22    "(id ---> id) = id"
    1.23    by (simp add: fun_eq_iff)
    1.24  
    1.25 -subsection {* Quotient Predicate *}
    1.26 +subsection \<open>Quotient Predicate\<close>
    1.27  
    1.28  definition
    1.29    "Quotient R Abs Rep T \<longleftrightarrow>
    1.30 @@ -55,7 +55,7 @@
    1.31    by blast
    1.32  
    1.33  lemma Quotient_rel:
    1.34 -  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" -- {* orientation does not loop on rewriting *}
    1.35 +  "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.36    using a unfolding Quotient_def
    1.37    by blast
    1.38  
    1.39 @@ -122,7 +122,7 @@
    1.40  lemma identity_quotient: "Quotient (op =) id id (op =)"
    1.41  unfolding Quotient_def by simp
    1.42  
    1.43 -text {* TODO: Use one of these alternatives as the real definition. *}
    1.44 +text \<open>TODO: Use one of these alternatives as the real definition.\<close>
    1.45  
    1.46  lemma Quotient_alt_def:
    1.47    "Quotient R Abs Rep T \<longleftrightarrow>
    1.48 @@ -195,7 +195,7 @@
    1.49    then show ?thesis using assms(2) by (auto intro: apply_rsp')
    1.50  qed
    1.51  
    1.52 -subsection {* Quotient composition *}
    1.53 +subsection \<open>Quotient composition\<close>
    1.54  
    1.55  lemma Quotient_compose:
    1.56    assumes 1: "Quotient R1 Abs1 Rep1 T1"
    1.57 @@ -207,7 +207,7 @@
    1.58    "equivp R \<Longrightarrow> reflp R"
    1.59    by (erule equivpE)
    1.60  
    1.61 -subsection {* Respects predicate *}
    1.62 +subsection \<open>Respects predicate\<close>
    1.63  
    1.64  definition Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
    1.65    where "Respects R = {x. R x x}"
    1.66 @@ -272,7 +272,7 @@
    1.67  unfolding eq_onp_def by (drule Quotient_rep_reflp) blast
    1.68  
    1.69  
    1.70 -text {* Generating transfer rules for quotients. *}
    1.71 +text \<open>Generating transfer rules for quotients.\<close>
    1.72  
    1.73  context
    1.74    fixes R Abs Rep T
    1.75 @@ -294,7 +294,7 @@
    1.76  
    1.77  end
    1.78  
    1.79 -text {* Generating transfer rules for total quotients. *}
    1.80 +text \<open>Generating transfer rules for total quotients.\<close>
    1.81  
    1.82  context
    1.83    fixes R Abs Rep T
    1.84 @@ -318,7 +318,7 @@
    1.85  
    1.86  end
    1.87  
    1.88 -text {* Generating transfer rules for a type defined with @{text "typedef"}. *}
    1.89 +text \<open>Generating transfer rules for a type defined with @{text "typedef"}.\<close>
    1.90  
    1.91  context
    1.92    fixes Rep Abs A T
    1.93 @@ -349,15 +349,15 @@
    1.94  
    1.95  end
    1.96  
    1.97 -text {* Generating the correspondence rule for a constant defined with
    1.98 -  @{text "lift_definition"}. *}
    1.99 +text \<open>Generating the correspondence rule for a constant defined with
   1.100 +  @{text "lift_definition"}.\<close>
   1.101  
   1.102  lemma Quotient_to_transfer:
   1.103    assumes "Quotient R Abs Rep T" and "R c c" and "c' \<equiv> Abs c"
   1.104    shows "T c c'"
   1.105    using assms by (auto dest: Quotient_cr_rel)
   1.106  
   1.107 -text {* Proving reflexivity *}
   1.108 +text \<open>Proving reflexivity\<close>
   1.109  
   1.110  lemma Quotient_to_left_total:
   1.111    assumes q: "Quotient R Abs Rep T"
   1.112 @@ -383,7 +383,7 @@
   1.113  lemma reflp_ge_eq:
   1.114    "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
   1.115  
   1.116 -text {* Proving a parametrized correspondence relation *}
   1.117 +text \<open>Proving a parametrized correspondence relation\<close>
   1.118  
   1.119  definition POS :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
   1.120  "POS A B \<equiv> A \<le> B"
   1.121 @@ -443,7 +443,7 @@
   1.122    shows "R' f g"
   1.123  using assms unfolding POS_def by auto
   1.124  
   1.125 -text {* Proving a parametrized correspondence relation *}
   1.126 +text \<open>Proving a parametrized correspondence relation\<close>
   1.127  
   1.128  lemma fun_mono:
   1.129    assumes "A \<ge> C"
   1.130 @@ -484,7 +484,7 @@
   1.131    apply (intro choice)
   1.132    by metis
   1.133  
   1.134 -subsection {* Domains *}
   1.135 +subsection \<open>Domains\<close>
   1.136  
   1.137  lemma composed_equiv_rel_eq_onp:
   1.138    assumes "left_unique R"
   1.139 @@ -551,7 +551,7 @@
   1.140    shows "(rel_set A) (Collect (Domainp A)) UNIV"
   1.141    using assms unfolding right_total_def rel_set_def Domainp_iff by blast
   1.142  
   1.143 -subsection {* ML setup *}
   1.144 +subsection \<open>ML setup\<close>
   1.145  
   1.146  ML_file "Tools/Lifting/lifting_util.ML"
   1.147