src/HOL/Inductive.thy
author wenzelm
Tue, 02 Aug 2016 21:05:34 +0200
changeset 63588 d0e2bad67bd4
parent 63561 fba08009ff3e
child 63863 d14e580c3b8f
permissions -rw-r--r--
misc tuning and modernization;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7700
38b6d2643630 load / setup datatype package;
wenzelm
parents: 7357
diff changeset
     1
(*  Title:      HOL/Inductive.thy
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
     3
*)
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
     5
section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
1187
bc94f00e47ba Includes Sum.thy as a parent for mutual recursion
lcp
parents: 923
diff changeset
     6
54398
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents: 52143
diff changeset
     7
theory Inductive
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
     8
  imports Complete_Lattices Ctr_Sugar
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
     9
  keywords
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    10
    "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    11
    "monos" and
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    12
    "print_inductives" :: diag and
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    13
    "old_rep_datatype" :: thy_goal and
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    14
    "primrec" :: thy_decl
15131
c69542757a4d New theory header syntax.
nipkow
parents: 14981
diff changeset
    15
begin
10727
2ccafccb81c0 added inductive_conj;
wenzelm
parents: 10434
diff changeset
    16
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
    17
subsection \<open>Least and greatest fixed points\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    18
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    19
context complete_lattice
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    20
begin
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    21
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    22
definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>least fixed point\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    23
  where "lfp f = Inf {u. f u \<le> u}"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    24
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    25
definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"  \<comment> \<open>greatest fixed point\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    26
  where "gfp f = Sup {u. u \<le> f u}"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    27
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    28
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    29
subsection \<open>Proof of Knaster-Tarski Theorem using @{term lfp}\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    30
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    31
text \<open>@{term "lfp f"} is the least upper bound of the set @{term "{u. f u \<le> u}"}\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    32
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    33
lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    34
  by (auto simp add: lfp_def intro: Inf_lower)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    35
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    36
lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    37
  by (auto simp add: lfp_def intro: Inf_greatest)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    38
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    39
end
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    40
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    41
lemma lfp_lemma2: "mono f \<Longrightarrow> f (lfp f) \<le> lfp f"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    42
  by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    43
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    44
lemma lfp_lemma3: "mono f \<Longrightarrow> lfp f \<le> f (lfp f)"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    45
  by (iprover intro: lfp_lemma2 monoD lfp_lowerbound)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    46
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    47
lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    48
  by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    49
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    50
lemma lfp_const: "lfp (\<lambda>x. t) = t"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    51
  by (rule lfp_unfold) (simp add: mono_def)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    52
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    53
lemma lfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> x \<le> z) \<Longrightarrow> lfp F = x"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    54
  by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric])
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 63540
diff changeset
    55
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    56
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
    57
subsection \<open>General induction rules for least fixed points\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
    58
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    59
lemma lfp_ordinal_induct [case_names mono step union]:
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
    60
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    61
  assumes mono: "mono f"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    62
    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    63
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    64
  shows "P (lfp f)"
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    65
proof -
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    66
  let ?M = "{S. S \<le> lfp f \<and> P S}"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    67
  from P_Union have "P (Sup ?M)" by simp
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    68
  also have "Sup ?M = lfp f"
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    69
  proof (rule antisym)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    70
    show "Sup ?M \<le> lfp f"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    71
      by (blast intro: Sup_least)
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    72
    then have "f (Sup ?M) \<le> f (lfp f)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    73
      by (rule mono [THEN monoD])
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    74
    then have "f (Sup ?M) \<le> lfp f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    75
      using mono [THEN lfp_unfold] by simp
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    76
    then have "f (Sup ?M) \<in> ?M"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    77
      using P_Union by simp (intro P_f Sup_least, auto)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    78
    then have "f (Sup ?M) \<le> Sup ?M"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    79
      by (rule Sup_upper)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    80
    then show "lfp f \<le> Sup ?M"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    81
      by (rule lfp_lowerbound)
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    82
  qed
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    83
  finally show ?thesis .
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    84
qed
26013
8764a1f1253b Theorem Inductive.lfp_ordinal_induct generalized to complete lattices
haftmann
parents: 25557
diff changeset
    85
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
    86
theorem lfp_induct:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    87
  assumes mono: "mono f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    88
    and ind: "f (inf (lfp f) P) \<le> P"
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
    89
  shows "lfp f \<le> P"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    90
proof (induct rule: lfp_ordinal_induct)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    91
  case mono
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    92
  show ?case by fact
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    93
next
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    94
  case (step S)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
    95
  then show ?case
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
    96
    by (intro order_trans[OF _ ind] monoD[OF mono]) auto
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    97
next
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    98
  case (union M)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
    99
  then show ?case
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   100
    by (auto intro: Sup_least)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   101
qed
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   102
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   103
lemma lfp_induct_set:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   104
  assumes lfp: "a \<in> lfp f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   105
    and mono: "mono f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   106
    and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   107
  shows "P a"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   108
  by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   109
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   110
lemma lfp_ordinal_induct_set:
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   111
  assumes mono: "mono f"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   112
    and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   113
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   114
  shows "P (lfp f)"
46008
c296c75f4cf4 reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents: 45907
diff changeset
   115
  using assms by (rule lfp_ordinal_induct)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   116
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   117
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   118
text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   119
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   120
lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   121
  by (auto intro!: lfp_unfold)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   122
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   123
lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   124
  by (blast intro: lfp_induct)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   125
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   126
lemma def_lfp_induct_set:
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   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"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   128
  by (blast intro: lfp_induct_set)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   129
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   130
text \<open>Monotonicity of \<open>lfp\<close>!\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   131
lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   132
  by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   133
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   134
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   135
subsection \<open>Proof of Knaster-Tarski Theorem using \<open>gfp\<close>\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   136
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   137
text \<open>@{term "gfp f"} is the greatest lower bound of the set @{term "{u. u \<le> f u}"}\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   138
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   139
lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   140
  by (auto simp add: gfp_def intro: Sup_upper)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   141
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   142
lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   143
  by (auto simp add: gfp_def intro: Sup_least)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   144
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   145
lemma gfp_lemma2: "mono f \<Longrightarrow> gfp f \<le> f (gfp f)"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   146
  by (iprover intro: gfp_least order_trans monoD gfp_upperbound)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   147
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   148
lemma gfp_lemma3: "mono f \<Longrightarrow> f (gfp f) \<le> gfp f"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   149
  by (iprover intro: gfp_lemma2 monoD gfp_upperbound)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   150
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   151
lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   152
  by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   153
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 63540
diff changeset
   154
lemma gfp_const: "gfp (\<lambda>x. t) = t"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   155
  by (rule gfp_unfold) (simp add: mono_def)
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 63540
diff changeset
   156
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   157
lemma gfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> z \<le> x) \<Longrightarrow> gfp F = x"
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   158
  by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
63561
fba08009ff3e add lemmas contributed by Peter Gammie
Andreas Lochbihler
parents: 63540
diff changeset
   159
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   160
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   161
subsection \<open>Coinduction rules for greatest fixed points\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   162
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   163
text \<open>Weak version.\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   164
lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   165
  by (rule gfp_upperbound [THEN subsetD]) auto
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   166
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   167
lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   168
  apply (erule gfp_upperbound [THEN subsetD])
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   169
  apply (erule imageI)
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   170
  done
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   171
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   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))"
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   173
  apply (frule gfp_lemma2)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   174
  apply (drule mono_sup)
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   175
  apply (rule le_supI)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   176
   apply assumption
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   177
  apply (rule order_trans)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   178
   apply (rule order_trans)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   179
    apply assumption
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   180
   apply (rule sup_ge2)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   181
  apply assumption
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   182
  done
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   183
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   184
text \<open>Strong version, thanks to Coen and Frost.\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   185
lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
55604
42e4e8c2e8dc less flex-flex pairs
noschinl
parents: 55575
diff changeset
   186
  by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   187
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   188
lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   189
  by (blast dest: gfp_lemma2 mono_Un)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   190
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   191
lemma gfp_ordinal_induct[case_names mono step union]:
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60758
diff changeset
   192
  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   193
  assumes mono: "mono f"
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   194
    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   195
    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   196
  shows "P (gfp f)"
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   197
proof -
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   198
  let ?M = "{S. gfp f \<le> S \<and> P S}"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   199
  from P_Union have "P (Inf ?M)" by simp
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   200
  also have "Inf ?M = gfp f"
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   201
  proof (rule antisym)
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   202
    show "gfp f \<le> Inf ?M"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   203
      by (blast intro: Inf_greatest)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   204
    then have "f (gfp f) \<le> f (Inf ?M)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   205
      by (rule mono [THEN monoD])
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   206
    then have "gfp f \<le> f (Inf ?M)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   207
      using mono [THEN gfp_unfold] by simp
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   208
    then have "f (Inf ?M) \<in> ?M"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   209
      using P_Union by simp (intro P_f Inf_greatest, auto)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   210
    then have "Inf ?M \<le> f (Inf ?M)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   211
      by (rule Inf_lower)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   212
    then show "Inf ?M \<le> gfp f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   213
      by (rule gfp_upperbound)
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   214
  qed
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   215
  finally show ?thesis .
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   216
qed
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   217
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   218
lemma coinduct:
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   219
  assumes mono: "mono f"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   220
    and ind: "X \<le> f (sup X (gfp f))"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   221
  shows "X \<le> gfp f"
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   222
proof (induct rule: gfp_ordinal_induct)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   223
  case mono
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   224
  then show ?case by fact
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   225
next
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   226
  case (step S)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   227
  then show ?case
60174
70d8f7abde8f strengthened lfp_ordinal_induct; added dual gfp variant
hoelzl
parents: 60173
diff changeset
   228
    by (intro order_trans[OF ind _] monoD[OF mono]) auto
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   229
next
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   230
  case (union M)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   231
  then show ?case
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   232
    by (auto intro: mono Inf_greatest)
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   233
qed
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   234
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   235
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   236
subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   237
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   238
text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   239
  @{term lfp} and @{term gfp}\<close>
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   240
lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   241
  by (iprover intro: subset_refl monoI Un_mono monoD)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   242
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   243
lemma coinduct3_lemma:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   244
  "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   245
    lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   246
  apply (rule subset_trans)
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   247
   apply (erule coinduct3_mono_lemma [THEN lfp_lemma3])
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   248
  apply (rule Un_least [THEN Un_least])
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   249
    apply (rule subset_refl, assumption)
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   250
  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   251
  apply (rule monoD, assumption)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   252
  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   253
  done
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   254
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   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"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   256
  apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
63588
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   257
    apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
d0e2bad67bd4 misc tuning and modernization;
wenzelm
parents: 63561
diff changeset
   258
     apply simp_all
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   259
  done
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   260
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   261
text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   262
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   263
lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   264
  by (auto intro!: gfp_unfold)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   265
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   266
lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   267
  by (iprover intro!: coinduct)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   268
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   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"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   270
  by (auto intro!: coinduct_set)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   271
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   272
lemma def_Collect_coinduct:
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   273
  "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   274
    (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   275
  by (erule def_coinduct_set) auto
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   276
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   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"
45899
df887263a379 prefer Name.context operations;
wenzelm
parents: 45897
diff changeset
   278
  by (auto intro!: coinduct3)
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   279
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   280
text \<open>Monotonicity of @{term gfp}!\<close>
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   281
lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   282
  by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   283
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   284
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   285
subsection \<open>Rules for fixed point calculus\<close>
60173
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   286
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   287
lemma lfp_rolling:
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   288
  assumes "mono g" "mono f"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   289
  shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   290
proof (rule antisym)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   291
  have *: "mono (\<lambda>x. f (g x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   292
    using assms by (auto simp: mono_def)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   293
  show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   294
    by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   295
  show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   296
  proof (rule lfp_greatest)
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   297
    fix u
63540
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   298
    assume u: "g (f u) \<le> u"
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   299
    then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
60173
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   300
      by (intro assms[THEN monoD] lfp_lowerbound)
63540
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   301
    with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
60173
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   302
      by auto
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   303
  qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   304
qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   305
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   306
lemma lfp_lfp:
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   307
  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   308
  shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   309
proof (rule antisym)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   310
  have *: "mono (\<lambda>x. f x x)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   311
    by (blast intro: monoI f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   312
  show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   313
    by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   314
  show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _")
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   315
  proof (intro lfp_lowerbound)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   316
    have *: "?F = lfp (f ?F)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   317
      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   318
    also have "\<dots> = f ?F (lfp (f ?F))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   319
      by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   320
    finally show "f ?F ?F \<le> ?F"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   321
      by (simp add: *[symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   322
  qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   323
qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   324
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   325
lemma gfp_rolling:
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   326
  assumes "mono g" "mono f"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   327
  shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   328
proof (rule antisym)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   329
  have *: "mono (\<lambda>x. f (g x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   330
    using assms by (auto simp: mono_def)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   331
  show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   332
    by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   333
  show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   334
  proof (rule gfp_least)
63540
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   335
    fix u
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   336
    assume u: "u \<le> g (f u)"
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   337
    then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
60173
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   338
      by (intro assms[THEN monoD] gfp_upperbound)
63540
f8652d0534fa tuned proofs -- avoid unstructured calculation;
wenzelm
parents: 63400
diff changeset
   339
    with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
60173
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   340
      by auto
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   341
  qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   342
qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   343
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   344
lemma gfp_gfp:
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   345
  assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   346
  shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   347
proof (rule antisym)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   348
  have *: "mono (\<lambda>x. f x x)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   349
    by (blast intro: monoI f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   350
  show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   351
    by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   352
  show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _")
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   353
  proof (intro gfp_upperbound)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   354
    have *: "?F = gfp (f ?F)"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   355
      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   356
    also have "\<dots> = f ?F (gfp (f ?F))"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   357
      by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   358
    finally show "?F \<le> f ?F ?F"
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   359
      by (simp add: *[symmetric])
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   360
  qed
6a61bb577d5b add rules for least/greatest fixed point calculus
hoelzl
parents: 58889
diff changeset
   361
qed
24915
fc90277c0dd7 integrated FixedPoint into Inductive
haftmann
parents: 24845
diff changeset
   362
63400
249fa34faba2 misc tuning and modernization;
wenzelm
parents: 61955
diff changeset
   363
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   364
subsection \<open>Inductive predicates and sets\<close>
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   365
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   366
text \<open>Package setup.\<close>
10402
5e82d6cafb5f inductive_atomize, inductive_rulify;
wenzelm
parents: 10312
diff changeset
   367
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 61076
diff changeset
   368
lemmas basic_monos =
22218
30a8890d2967 dropped lemma duplicates in HOL.thy
haftmann
parents: 21018
diff changeset
   369
  subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   370
  Collect_mono in_mono vimage_mono
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   371
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48357
diff changeset
   372
ML_file "Tools/inductive.ML"
21018
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
   373
61337
4645502c3c64 fewer aliases for toplevel theorem statements;
wenzelm
parents: 61076
diff changeset
   374
lemmas [mono] =
22218
30a8890d2967 dropped lemma duplicates in HOL.thy
haftmann
parents: 21018
diff changeset
   375
  imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
33934
25d6a8982e37 Streamlined setup for monotonicity rules (no longer requires classical rules).
berghofe
parents: 32701
diff changeset
   376
  imp_mono not_mono
21018
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
   377
  Ball_def Bex_def
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
   378
  induct_rulify_fallback
e6b8d6784792 Added new package for inductive definitions, moved old package
berghofe
parents: 20604
diff changeset
   379
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   380
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   381
subsection \<open>Inductive datatypes and primitive recursion\<close>
11688
56833637db2a generic induct_method.ML;
wenzelm
parents: 11439
diff changeset
   382
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   383
text \<open>Package setup.\<close>
11825
ef7d619e2c88 moved InductMethod.setup to theory HOL;
wenzelm
parents: 11688
diff changeset
   384
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 56146
diff changeset
   385
ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 56146
diff changeset
   386
ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
58187
d2ddd401d74d fixed infinite loops in 'register' functions + more uniform API
blanchet
parents: 58112
diff changeset
   387
ML_file "Tools/Old_Datatype/old_datatype_data.ML"
58112
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 56146
diff changeset
   388
ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 56146
diff changeset
   389
ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
blanchet
parents: 56146
diff changeset
   390
ML_file "Tools/Old_Datatype/old_primrec.ML"
12437
6d4e02b6dd43 Moved code generator setup from Recdef to Inductive.
berghofe
parents: 12023
diff changeset
   391
55575
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55534
diff changeset
   392
ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55534
diff changeset
   393
ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
a5e33e18fb5c moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
blanchet
parents: 55534
diff changeset
   394
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61952
diff changeset
   395
text \<open>Lambda-abstractions with pattern matching:\<close>
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61952
diff changeset
   396
syntax (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61952
diff changeset
   397
  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   398
syntax
61955
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents: 61952
diff changeset
   399
  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   400
parse_translation \<open>
52143
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   401
  let
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   402
    fun fun_tr ctxt [cs] =
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   403
      let
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   404
        val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   405
        val ft = Case_Translation.case_tr true ctxt [x, cs];
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   406
      in lambda x ft end
36ffe23b25f8 syntax translations always depend on context;
wenzelm
parents: 51692
diff changeset
   407
  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 60636
diff changeset
   408
\<close>
23526
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   409
936dc616a7fb Added pattern maatching for lambda abstraction
nipkow
parents: 23389
diff changeset
   410
end