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