src/HOL/Inductive.thy
author wenzelm
Fri Jul 22 11:00:43 2016 +0200 (2016-07-22)
changeset 63540 f8652d0534fa
parent 63400 249fa34faba2
child 63561 fba08009ff3e
permissions -rw-r--r--
tuned proofs -- avoid unstructured calculation;
wenzelm@7700
     1
(*  Title:      HOL/Inductive.thy
wenzelm@10402
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@11688
     3
*)
wenzelm@10727
     4
wenzelm@60758
     5
section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
lcp@1187
     6
blanchet@54398
     7
theory Inductive
blanchet@54398
     8
imports Complete_Lattices Ctr_Sugar
wenzelm@46950
     9
keywords
wenzelm@56146
    10
  "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
wenzelm@56146
    11
  "monos" and
blanchet@54398
    12
  "print_inductives" :: diag and
blanchet@58306
    13
  "old_rep_datatype" :: thy_goal and
blanchet@55575
    14
  "primrec" :: thy_decl
nipkow@15131
    15
begin
wenzelm@10727
    16
wenzelm@60758
    17
subsection \<open>Least and greatest fixed points\<close>
haftmann@24915
    18
haftmann@26013
    19
context complete_lattice
haftmann@26013
    20
begin
haftmann@26013
    21
wenzelm@63400
    22
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
wenzelm@63400
    23
  where "lfp f = Inf {u. f u \<le> u}"
haftmann@24915
    24
wenzelm@63400
    25
definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
wenzelm@63400
    26
  where "gfp f = Sup {u. u \<le> f u}"
haftmann@24915
    27
haftmann@24915
    28
wenzelm@63400
    29
subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
haftmann@24915
    30
wenzelm@63400
    31
text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
haftmann@24915
    32
wenzelm@63400
    33
lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
haftmann@24915
    34
  by (auto simp add: lfp_def intro: Inf_lower)
haftmann@24915
    35
wenzelm@63400
    36
lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
haftmann@24915
    37
  by (auto simp add: lfp_def intro: Inf_greatest)
haftmann@24915
    38
haftmann@26013
    39
end
haftmann@26013
    40
wenzelm@63400
    41
lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
haftmann@24915
    42
  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
haftmann@24915
    43
wenzelm@63400
    44
lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
haftmann@24915
    45
  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
haftmann@24915
    46
wenzelm@63400
    47
lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
haftmann@24915
    48
  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
haftmann@24915
    49
haftmann@24915
    50
lemma lfp_const: "lfp (\<lambda>x. t) = t"
wenzelm@63400
    51
  by (rule lfp_unfold) (simp add: mono_def)
haftmann@24915
    52
haftmann@24915
    53
wenzelm@60758
    54
subsection \<open>General induction rules for least fixed points\<close>
haftmann@24915
    55
wenzelm@63400
    56
lemma lfp_ordinal_induct [case_names mono step union]:
wenzelm@61076
    57
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
haftmann@26013
    58
  assumes mono: "mono f"
wenzelm@63400
    59
    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
wenzelm@63400
    60
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
haftmann@26013
    61
  shows "P (lfp f)"
haftmann@26013
    62
proof -
haftmann@26013
    63
  let ?M = "{S. S \<le> lfp f \<and> P S}"
haftmann@26013
    64
  have "P (Sup ?M)" using P_Union by simp
haftmann@26013
    65
  also have "Sup ?M = lfp f"
haftmann@26013
    66
  proof (rule antisym)
haftmann@26013
    67
    show "Sup ?M \<le> lfp f" by (blast intro: Sup_least)
wenzelm@63400
    68
    then have "f (Sup ?M) \<le> f (lfp f)"
wenzelm@63400
    69
      by (rule mono [THEN monoD])
wenzelm@63400
    70
    then have "f (Sup ?M) \<le> lfp f"
wenzelm@63400
    71
      using mono [THEN lfp_unfold] by simp
wenzelm@63400
    72
    then have "f (Sup ?M) \<in> ?M"
wenzelm@63400
    73
      using P_Union by simp (intro P_f Sup_least, auto)
wenzelm@63400
    74
    then have "f (Sup ?M) \<le> Sup ?M"
wenzelm@63400
    75
      by (rule Sup_upper)
wenzelm@63400
    76
    then show "lfp f \<le> Sup ?M"
wenzelm@63400
    77
      by (rule lfp_lowerbound)
haftmann@26013
    78
  qed
haftmann@26013
    79
  finally show ?thesis .
wenzelm@63400
    80
qed
haftmann@26013
    81
hoelzl@60174
    82
theorem lfp_induct:
wenzelm@63400
    83
  assumes mono: "mono f"
wenzelm@63400
    84
    and ind: "f (inf (lfp f) P) \<le> P"
hoelzl@60174
    85
  shows "lfp f \<le> P"
hoelzl@60174
    86
proof (induction rule: lfp_ordinal_induct)
wenzelm@63400
    87
  case (step S)
wenzelm@63400
    88
  then show ?case
hoelzl@60174
    89
    by (intro order_trans[OF _ ind] monoD[OF mono]) auto
hoelzl@60174
    90
qed (auto intro: mono Sup_least)
hoelzl@60174
    91
hoelzl@60174
    92
lemma lfp_induct_set:
wenzelm@63400
    93
  assumes lfp: "a \<in> lfp f"
wenzelm@63400
    94
    and mono: "mono f"
wenzelm@63400
    95
    and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
wenzelm@63400
    96
  shows "P a"
wenzelm@63400
    97
  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
hoelzl@60174
    98
wenzelm@63400
    99
lemma lfp_ordinal_induct_set:
haftmann@24915
   100
  assumes mono: "mono f"
wenzelm@63400
   101
    and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
wenzelm@63400
   102
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
wenzelm@63400
   103
  shows "P (lfp f)"
wenzelm@46008
   104
  using assms by (rule lfp_ordinal_induct)
haftmann@24915
   105
haftmann@24915
   106
wenzelm@63400
   107
text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
haftmann@24915
   108
wenzelm@63400
   109
lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
wenzelm@45899
   110
  by (auto intro!: lfp_unfold)
haftmann@24915
   111
wenzelm@63400
   112
lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
haftmann@24915
   113
  by (blast intro: lfp_induct)
haftmann@24915
   114
wenzelm@63400
   115
lemma def_lfp_induct_set:
wenzelm@63400
   116
  "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> A \<Longrightarrow> (\<And>x. x \<in> f (A \<inter> {x. P x}) \<Longrightarrow> P x) \<Longrightarrow> P a"
haftmann@24915
   117
  by (blast intro: lfp_induct_set)
haftmann@24915
   118
wenzelm@63400
   119
text \<open>Monotonicity of \<open>lfp\<close>!\<close>
wenzelm@63400
   120
lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
wenzelm@63400
   121
  by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
haftmann@24915
   122
haftmann@24915
   123
wenzelm@63400
   124
subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
haftmann@24915
   125
wenzelm@63400
   126
text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
haftmann@24915
   127
wenzelm@63400
   128
lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
haftmann@24915
   129
  by (auto simp add: gfp_def intro: Sup_upper)
haftmann@24915
   130
wenzelm@63400
   131
lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
haftmann@24915
   132
  by (auto simp add: gfp_def intro: Sup_least)
haftmann@24915
   133
wenzelm@63400
   134
lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
haftmann@24915
   135
  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
haftmann@24915
   136
wenzelm@63400
   137
lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
haftmann@24915
   138
  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
haftmann@24915
   139
wenzelm@63400
   140
lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
haftmann@24915
   141
  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
haftmann@24915
   142
haftmann@24915
   143
wenzelm@60758
   144
subsection \<open>Coinduction rules for greatest fixed points\<close>
haftmann@24915
   145
wenzelm@63400
   146
text \<open>Weak version.\<close>
wenzelm@63400
   147
lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
wenzelm@45899
   148
  by (rule gfp_upperbound [THEN subsetD]) auto
haftmann@24915
   149
wenzelm@63400
   150
lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
wenzelm@45899
   151
  apply (erule gfp_upperbound [THEN subsetD])
wenzelm@45899
   152
  apply (erule imageI)
wenzelm@45899
   153
  done
haftmann@24915
   154
wenzelm@63400
   155
lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
haftmann@24915
   156
  apply (frule gfp_lemma2)
haftmann@24915
   157
  apply (drule mono_sup)
haftmann@24915
   158
  apply (rule le_supI)
haftmann@24915
   159
  apply assumption
haftmann@24915
   160
  apply (rule order_trans)
haftmann@24915
   161
  apply (rule order_trans)
haftmann@24915
   162
  apply assumption
haftmann@24915
   163
  apply (rule sup_ge2)
haftmann@24915
   164
  apply assumption
haftmann@24915
   165
  done
haftmann@24915
   166
wenzelm@63400
   167
text \<open>Strong version, thanks to Coen and Frost.\<close>
wenzelm@63400
   168
lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
noschinl@55604
   169
  by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
haftmann@24915
   170
wenzelm@63400
   171
lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
wenzelm@45899
   172
  by (blast dest: gfp_lemma2 mono_Un)
haftmann@24915
   173
hoelzl@60174
   174
lemma gfp_ordinal_induct[case_names mono step union]:
wenzelm@61076
   175
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
hoelzl@60174
   176
  assumes mono: "mono f"
wenzelm@63400
   177
    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
wenzelm@63400
   178
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
hoelzl@60174
   179
  shows "P (gfp f)"
hoelzl@60174
   180
proof -
hoelzl@60174
   181
  let ?M = "{S. gfp f \<le> S \<and> P S}"
hoelzl@60174
   182
  have "P (Inf ?M)" using P_Union by simp
hoelzl@60174
   183
  also have "Inf ?M = gfp f"
hoelzl@60174
   184
  proof (rule antisym)
wenzelm@63400
   185
    show "gfp f \<le> Inf ?M"
wenzelm@63400
   186
      by (blast intro: Inf_greatest)
wenzelm@63400
   187
    then have "f (gfp f) \<le> f (Inf ?M)"
wenzelm@63400
   188
      by (rule mono [THEN monoD])
wenzelm@63400
   189
    then have "gfp f \<le> f (Inf ?M)"
wenzelm@63400
   190
      using mono [THEN gfp_unfold] by simp
wenzelm@63400
   191
    then have "f (Inf ?M) \<in> ?M"
wenzelm@63400
   192
      using P_Union by simp (intro P_f Inf_greatest, auto)
wenzelm@63400
   193
    then have "Inf ?M \<le> f (Inf ?M)"
wenzelm@63400
   194
      by (rule Inf_lower)
wenzelm@63400
   195
    then show "Inf ?M \<le> gfp f"
wenzelm@63400
   196
      by (rule gfp_upperbound)
hoelzl@60174
   197
  qed
hoelzl@60174
   198
  finally show ?thesis .
wenzelm@63400
   199
qed
hoelzl@60174
   200
wenzelm@63400
   201
lemma coinduct:
wenzelm@63400
   202
  assumes mono: "mono f"
wenzelm@63400
   203
    and ind: "X \<le> f (sup X (gfp f))"
wenzelm@63400
   204
  shows "X \<le> gfp f"
hoelzl@60174
   205
proof (induction rule: gfp_ordinal_induct)
hoelzl@60174
   206
  case (step S) then show ?case
hoelzl@60174
   207
    by (intro order_trans[OF ind _] monoD[OF mono]) auto
hoelzl@60174
   208
qed (auto intro: mono Inf_greatest)
haftmann@24915
   209
wenzelm@63400
   210
wenzelm@60758
   211
subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
haftmann@24915
   212
wenzelm@63400
   213
text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
wenzelm@60758
   214
  @{term lfp} and @{term gfp}\<close>
wenzelm@63400
   215
lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
wenzelm@63400
   216
  by (iprover intro: subset_refl monoI Un_mono monoD)
haftmann@24915
   217
haftmann@24915
   218
lemma coinduct3_lemma:
wenzelm@63400
   219
  "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
wenzelm@63400
   220
    lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
wenzelm@63400
   221
  apply (rule subset_trans)
wenzelm@63400
   222
  apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
wenzelm@63400
   223
  apply (rule Un_least [THEN Un_least])
wenzelm@63400
   224
  apply (rule subset_refl, assumption)
wenzelm@63400
   225
  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
wenzelm@63400
   226
  apply (rule monoD, assumption)
wenzelm@63400
   227
  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
wenzelm@63400
   228
  done
haftmann@24915
   229
wenzelm@63400
   230
lemma coinduct3: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> a \<in> gfp f"
wenzelm@63400
   231
  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
wenzelm@63400
   232
  apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
wenzelm@63400
   233
  apply simp_all
wenzelm@63400
   234
  done
haftmann@24915
   235
wenzelm@63400
   236
text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
haftmann@24915
   237
wenzelm@63400
   238
lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
wenzelm@45899
   239
  by (auto intro!: gfp_unfold)
haftmann@24915
   240
wenzelm@63400
   241
lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
wenzelm@45899
   242
  by (iprover intro!: coinduct)
haftmann@24915
   243
wenzelm@63400
   244
lemma def_coinduct_set: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> A) \<Longrightarrow> a \<in> A"
wenzelm@45899
   245
  by (auto intro!: coinduct_set)
haftmann@24915
   246
haftmann@24915
   247
lemma def_Collect_coinduct:
wenzelm@63400
   248
  "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
wenzelm@63400
   249
    (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
wenzelm@45899
   250
  by (erule def_coinduct_set) auto
haftmann@24915
   251
wenzelm@63400
   252
lemma def_coinduct3: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> A)) \<Longrightarrow> a \<in> A"
wenzelm@45899
   253
  by (auto intro!: coinduct3)
haftmann@24915
   254
wenzelm@63400
   255
text \<open>Monotonicity of @{term gfp}!\<close>
wenzelm@63400
   256
lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
wenzelm@63400
   257
  by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
wenzelm@63400
   258
haftmann@24915
   259
wenzelm@60758
   260
subsection \<open>Rules for fixed point calculus\<close>
hoelzl@60173
   261
hoelzl@60173
   262
lemma lfp_rolling:
hoelzl@60173
   263
  assumes "mono g" "mono f"
hoelzl@60173
   264
  shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
hoelzl@60173
   265
proof (rule antisym)
hoelzl@60173
   266
  have *: "mono (\<lambda>x. f (g x))"
hoelzl@60173
   267
    using assms by (auto simp: mono_def)
hoelzl@60173
   268
  show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
hoelzl@60173
   269
    by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
hoelzl@60173
   270
  show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
hoelzl@60173
   271
  proof (rule lfp_greatest)
wenzelm@63400
   272
    fix u
wenzelm@63540
   273
    assume u: "g (f u) \<le> u"
wenzelm@63540
   274
    then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
hoelzl@60173
   275
      by (intro assms[THEN monoD] lfp_lowerbound)
wenzelm@63540
   276
    with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
hoelzl@60173
   277
      by auto
hoelzl@60173
   278
  qed
hoelzl@60173
   279
qed
hoelzl@60173
   280
hoelzl@60173
   281
lemma lfp_lfp:
hoelzl@60173
   282
  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
hoelzl@60173
   283
  shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
hoelzl@60173
   284
proof (rule antisym)
hoelzl@60173
   285
  have *: "mono (\<lambda>x. f x x)"
hoelzl@60173
   286
    by (blast intro: monoI f)
hoelzl@60173
   287
  show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)"
hoelzl@60173
   288
    by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
hoelzl@60173
   289
  show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _")
hoelzl@60173
   290
  proof (intro lfp_lowerbound)
hoelzl@60173
   291
    have *: "?F = lfp (f ?F)"
hoelzl@60173
   292
      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
hoelzl@60173
   293
    also have "\<dots> = f ?F (lfp (f ?F))"
hoelzl@60173
   294
      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
hoelzl@60173
   295
    finally show "f ?F ?F \<le> ?F"
hoelzl@60173
   296
      by (simp add: *[symmetric])
hoelzl@60173
   297
  qed
hoelzl@60173
   298
qed
hoelzl@60173
   299
hoelzl@60173
   300
lemma gfp_rolling:
hoelzl@60173
   301
  assumes "mono g" "mono f"
hoelzl@60173
   302
  shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
hoelzl@60173
   303
proof (rule antisym)
hoelzl@60173
   304
  have *: "mono (\<lambda>x. f (g x))"
hoelzl@60173
   305
    using assms by (auto simp: mono_def)
hoelzl@60173
   306
  show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
hoelzl@60173
   307
    by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
hoelzl@60173
   308
  show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
hoelzl@60173
   309
  proof (rule gfp_least)
wenzelm@63540
   310
    fix u
wenzelm@63540
   311
    assume u: "u \<le> g (f u)"
wenzelm@63540
   312
    then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
hoelzl@60173
   313
      by (intro assms[THEN monoD] gfp_upperbound)
wenzelm@63540
   314
    with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
hoelzl@60173
   315
      by auto
hoelzl@60173
   316
  qed
hoelzl@60173
   317
qed
hoelzl@60173
   318
hoelzl@60173
   319
lemma gfp_gfp:
hoelzl@60173
   320
  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
hoelzl@60173
   321
  shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
hoelzl@60173
   322
proof (rule antisym)
hoelzl@60173
   323
  have *: "mono (\<lambda>x. f x x)"
hoelzl@60173
   324
    by (blast intro: monoI f)
hoelzl@60173
   325
  show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))"
hoelzl@60173
   326
    by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
hoelzl@60173
   327
  show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _")
hoelzl@60173
   328
  proof (intro gfp_upperbound)
hoelzl@60173
   329
    have *: "?F = gfp (f ?F)"
hoelzl@60173
   330
      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
hoelzl@60173
   331
    also have "\<dots> = f ?F (gfp (f ?F))"
hoelzl@60173
   332
      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
hoelzl@60173
   333
    finally show "?F \<le> f ?F ?F"
hoelzl@60173
   334
      by (simp add: *[symmetric])
hoelzl@60173
   335
  qed
hoelzl@60173
   336
qed
haftmann@24915
   337
wenzelm@63400
   338
wenzelm@60758
   339
subsection \<open>Inductive predicates and sets\<close>
wenzelm@11688
   340
wenzelm@60758
   341
text \<open>Package setup.\<close>
wenzelm@10402
   342
wenzelm@61337
   343
lemmas basic_monos =
haftmann@22218
   344
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
wenzelm@11688
   345
  Collect_mono in_mono vimage_mono
wenzelm@11688
   346
wenzelm@48891
   347
ML_file "Tools/inductive.ML"
berghofe@21018
   348
wenzelm@61337
   349
lemmas [mono] =
haftmann@22218
   350
  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
berghofe@33934
   351
  imp_mono not_mono
berghofe@21018
   352
  Ball_def Bex_def
berghofe@21018
   353
  induct_rulify_fallback
berghofe@21018
   354
wenzelm@11688
   355
wenzelm@60758
   356
subsection \<open>Inductive datatypes and primitive recursion\<close>
wenzelm@11688
   357
wenzelm@60758
   358
text \<open>Package setup.\<close>
wenzelm@11825
   359
blanchet@58112
   360
ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
blanchet@58112
   361
ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
blanchet@58187
   362
ML_file "Tools/Old_Datatype/old_datatype_data.ML"
blanchet@58112
   363
ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
blanchet@58112
   364
ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
blanchet@58112
   365
ML_file "Tools/Old_Datatype/old_primrec.ML"
berghofe@12437
   366
blanchet@55575
   367
ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
blanchet@55575
   368
ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
blanchet@55575
   369
wenzelm@61955
   370
text \<open>Lambda-abstractions with pattern matching:\<close>
wenzelm@61955
   371
syntax (ASCII)
wenzelm@61955
   372
  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
nipkow@23526
   373
syntax
wenzelm@61955
   374
  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
wenzelm@60758
   375
parse_translation \<open>
wenzelm@52143
   376
  let
wenzelm@52143
   377
    fun fun_tr ctxt [cs] =
wenzelm@52143
   378
      let
wenzelm@52143
   379
        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
wenzelm@52143
   380
        val ft = Case_Translation.case_tr true ctxt [x, cs];
wenzelm@52143
   381
      in lambda x ft end
wenzelm@52143
   382
  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
wenzelm@60758
   383
\<close>
nipkow@23526
   384
nipkow@23526
   385
end