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