src/HOL/Inductive.thy
 changeset 60758 d8d85a8172b5 parent 60636 ee18efe9b246 child 61076 bdc1e2f0a86a
```     1.1 --- a/src/HOL/Inductive.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/Inductive.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -2,7 +2,7 @@
1.4      Author:     Markus Wenzel, TU Muenchen
1.5  *)
1.6
1.7 -section {* Knaster-Tarski Fixpoint Theorem and inductive definitions *}
1.8 +section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
1.9
1.10  theory Inductive
1.11  imports Complete_Lattices Ctr_Sugar
1.12 @@ -14,24 +14,24 @@
1.13    "primrec" :: thy_decl
1.14  begin
1.15
1.16 -subsection {* Least and greatest fixed points *}
1.17 +subsection \<open>Least and greatest fixed points\<close>
1.18
1.19  context complete_lattice
1.20  begin
1.21
1.22  definition
1.23    lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.24 -  "lfp f = Inf {u. f u \<le> u}"    --{*least fixed point*}
1.25 +  "lfp f = Inf {u. f u \<le> u}"    --\<open>least fixed point\<close>
1.26
1.27  definition
1.28    gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.29 -  "gfp f = Sup {u. u \<le> f u}"    --{*greatest fixed point*}
1.30 +  "gfp f = Sup {u. u \<le> f u}"    --\<open>greatest fixed point\<close>
1.31
1.32
1.33 -subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *}
1.34 +subsection\<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
1.35
1.36 -text{*@{term "lfp f"} is the least upper bound of
1.37 -      the set @{term "{u. f(u) \<le> u}"} *}
1.38 +text\<open>@{term "lfp f"} is the least upper bound of
1.39 +      the set @{term "{u. f(u) \<le> u}"}\<close>
1.40
1.41  lemma lfp_lowerbound: "f A \<le> A ==> lfp f \<le> A"
1.42    by (auto simp add: lfp_def intro: Inf_lower)
1.43 @@ -54,7 +54,7 @@
1.44    by (rule lfp_unfold) (simp add:mono_def)
1.45
1.46
1.47 -subsection {* General induction rules for least fixed points *}
1.48 +subsection \<open>General induction rules for least fixed points\<close>
1.49
1.50  lemma lfp_ordinal_induct[case_names mono step union]:
1.51    fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
1.52 @@ -101,8 +101,8 @@
1.53    using assms by (rule lfp_ordinal_induct)
1.54
1.55
1.56 -text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct},
1.57 -    to control unfolding*}
1.58 +text\<open>Definition forms of @{text lfp_unfold} and @{text lfp_induct},
1.59 +    to control unfolding\<close>
1.60
1.61  lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
1.62    by (auto intro!: lfp_unfold)
1.63 @@ -124,10 +124,10 @@
1.64    by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans)
1.65
1.66
1.67 -subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *}
1.68 +subsection \<open>Proof of Knaster-Tarski Theorem using @{term gfp}\<close>
1.69
1.70 -text{*@{term "gfp f"} is the greatest lower bound of
1.71 -      the set @{term "{u. u \<le> f(u)}"} *}
1.72 +text\<open>@{term "gfp f"} is the greatest lower bound of
1.73 +      the set @{term "{u. u \<le> f(u)}"}\<close>
1.74
1.75  lemma gfp_upperbound: "X \<le> f X ==> X \<le> gfp f"
1.76    by (auto simp add: gfp_def intro: Sup_upper)
1.77 @@ -145,9 +145,9 @@
1.78    by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
1.79
1.80
1.81 -subsection {* Coinduction rules for greatest fixed points *}
1.82 +subsection \<open>Coinduction rules for greatest fixed points\<close>
1.83
1.84 -text{*weak version*}
1.85 +text\<open>weak version\<close>
1.86  lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
1.87    by (rule gfp_upperbound [THEN subsetD]) auto
1.88
1.89 @@ -169,7 +169,7 @@
1.90    apply assumption
1.91    done
1.92
1.93 -text{*strong version, thanks to Coen and Frost*}
1.94 +text\<open>strong version, thanks to Coen and Frost\<close>
1.95  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
1.96    by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
1.97
1.98 @@ -203,10 +203,10 @@
1.99      by (intro order_trans[OF ind _] monoD[OF mono]) auto
1.100  qed (auto intro: mono Inf_greatest)
1.101
1.102 -subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
1.103 +subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
1.104
1.105 -text{* Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
1.106 -  @{term lfp} and @{term gfp}*}
1.107 +text\<open>Weakens the condition @{term "X \<subseteq> f(X)"} to one expressed using both
1.108 +  @{term lfp} and @{term gfp}\<close>
1.109
1.110  lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)"
1.111  by (iprover intro: subset_refl monoI Un_mono monoD)
1.112 @@ -230,8 +230,8 @@
1.113  apply (simp_all)
1.114  done
1.115
1.116 -text{*Definition forms of @{text gfp_unfold} and @{text coinduct},
1.117 -    to control unfolding*}
1.118 +text\<open>Definition forms of @{text gfp_unfold} and @{text coinduct},
1.119 +    to control unfolding\<close>
1.120
1.121  lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
1.122    by (auto intro!: gfp_unfold)
1.123 @@ -255,11 +255,11 @@
1.124      "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
1.125    by (auto intro!: coinduct3)
1.126
1.127 -text{*Monotonicity of @{term gfp}!*}
1.128 +text\<open>Monotonicity of @{term gfp}!\<close>
1.129  lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
1.130    by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans)
1.131
1.132 -subsection {* Rules for fixed point calculus *}
1.133 +subsection \<open>Rules for fixed point calculus\<close>
1.134
1.135
1.136  lemma lfp_rolling:
1.137 @@ -339,9 +339,9 @@
1.138    qed
1.139  qed
1.140
1.141 -subsection {* Inductive predicates and sets *}
1.142 +subsection \<open>Inductive predicates and sets\<close>
1.143
1.144 -text {* Package setup. *}
1.145 +text \<open>Package setup.\<close>
1.146
1.147  theorems basic_monos =
1.148    subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
1.149 @@ -356,9 +356,9 @@
1.150    induct_rulify_fallback
1.151
1.152
1.153 -subsection {* Inductive datatypes and primitive recursion *}
1.154 +subsection \<open>Inductive datatypes and primitive recursion\<close>
1.155
1.156 -text {* Package setup. *}
1.157 +text \<open>Package setup.\<close>
1.158
1.159  ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
1.160  ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
1.161 @@ -370,14 +370,14 @@
1.162  ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
1.163  ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
1.164
1.165 -text{* Lambda-abstractions with pattern matching: *}
1.166 +text\<open>Lambda-abstractions with pattern matching:\<close>
1.167
1.168  syntax
1.169    "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
1.170  syntax (xsymbols)
1.171    "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
1.172
1.173 -parse_translation {*
1.174 +parse_translation \<open>
1.175    let
1.176      fun fun_tr ctxt [cs] =
1.177        let
1.178 @@ -385,6 +385,6 @@
1.179          val ft = Case_Translation.case_tr true ctxt [x, cs];
1.180        in lambda x ft end
1.181    in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
1.182 -*}
1.183 +\<close>
1.184
1.185  end
```