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