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