author wenzelm
Sat Oct 01 17:16:35 2016 +0200 (2016-10-01)
changeset 63979 95c3ae4baba8
parent 63976 c1a481bb82d3
child 63980 f8e556c8ad6f
permissions -rw-r--r--
clarified lfp/gfp statements and proofs;
     1 (*  Title:      HOL/Inductive.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     5 section \<open>Knaster-Tarski Fixpoint Theorem and inductive definitions\<close>
     7 theory Inductive
     8   imports Complete_Lattices Ctr_Sugar
     9   keywords
    10     "inductive" "coinductive" "inductive_cases" "inductive_simps" :: thy_decl and
    11     "monos" and
    12     "print_inductives" :: diag and
    13     "old_rep_datatype" :: thy_goal and
    14     "primrec" :: thy_decl
    15 begin
    17 subsection \<open>Least fixed points\<close>
    19 context complete_lattice
    20 begin
    22 definition lfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
    23   where "lfp f = Inf {u. f u \<le> u}"
    25 lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
    26   by (auto simp add: lfp_def intro: Inf_lower)
    28 lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
    29   by (auto simp add: lfp_def intro: Inf_greatest)
    31 end
    33 lemma lfp_fixpoint:
    34   assumes "mono f"
    35   shows "f (lfp f) = lfp f"
    36   unfolding lfp_def
    37 proof (rule order_antisym)
    38   let ?H = "{u. f u \<le> u}"
    39   let ?a = "\<Sqinter>?H"
    40   show "f ?a \<le> ?a"
    41   proof (rule Inf_greatest)
    42     fix x
    43     assume "x \<in> ?H"
    44     then have "?a \<le> x" by (rule Inf_lower)
    45     with \<open>mono f\<close> have "f ?a \<le> f x" ..
    46     also from \<open>x \<in> ?H\<close> have "f x \<le> x" ..
    47     finally show "f ?a \<le> x" .
    48   qed
    49   show "?a \<le> f ?a"
    50   proof (rule Inf_lower)
    51     from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..
    52     then show "f ?a \<in> ?H" ..
    53   qed
    54 qed
    56 lemma lfp_unfold: "mono f \<Longrightarrow> lfp f = f (lfp f)"
    57   by (rule lfp_fixpoint [symmetric])
    59 lemma lfp_const: "lfp (\<lambda>x. t) = t"
    60   by (rule lfp_unfold) (simp add: mono_def)
    62 lemma lfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> x \<le> z) \<Longrightarrow> lfp F = x"
    63   by (rule antisym) (simp_all add: lfp_lowerbound lfp_unfold[symmetric])
    66 subsection \<open>General induction rules for least fixed points\<close>
    68 lemma lfp_ordinal_induct [case_names mono step union]:
    69   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
    70   assumes mono: "mono f"
    71     and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    72     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    73   shows "P (lfp f)"
    74 proof -
    75   let ?M = "{S. S \<le> lfp f \<and> P S}"
    76   from P_Union have "P (Sup ?M)" by simp
    77   also have "Sup ?M = lfp f"
    78   proof (rule antisym)
    79     show "Sup ?M \<le> lfp f"
    80       by (blast intro: Sup_least)
    81     then have "f (Sup ?M) \<le> f (lfp f)"
    82       by (rule mono [THEN monoD])
    83     then have "f (Sup ?M) \<le> lfp f"
    84       using mono [THEN lfp_unfold] by simp
    85     then have "f (Sup ?M) \<in> ?M"
    86       using P_Union by simp (intro P_f Sup_least, auto)
    87     then have "f (Sup ?M) \<le> Sup ?M"
    88       by (rule Sup_upper)
    89     then show "lfp f \<le> Sup ?M"
    90       by (rule lfp_lowerbound)
    91   qed
    92   finally show ?thesis .
    93 qed
    95 theorem lfp_induct:
    96   assumes mono: "mono f"
    97     and ind: "f (inf (lfp f) P) \<le> P"
    98   shows "lfp f \<le> P"
    99 proof (induct rule: lfp_ordinal_induct)
   100   case mono
   101   show ?case by fact
   102 next
   103   case (step S)
   104   then show ?case
   105     by (intro order_trans[OF _ ind] monoD[OF mono]) auto
   106 next
   107   case (union M)
   108   then show ?case
   109     by (auto intro: Sup_least)
   110 qed
   112 lemma lfp_induct_set:
   113   assumes lfp: "a \<in> lfp f"
   114     and mono: "mono f"
   115     and hyp: "\<And>x. x \<in> f (lfp f \<inter> {x. P x}) \<Longrightarrow> P x"
   116   shows "P a"
   117   by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) (auto intro: hyp)
   119 lemma lfp_ordinal_induct_set:
   120   assumes mono: "mono f"
   121     and P_f: "\<And>S. P S \<Longrightarrow> P (f S)"
   122     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (\<Union>M)"
   123   shows "P (lfp f)"
   124   using assms by (rule lfp_ordinal_induct)
   127 text \<open>Definition forms of \<open>lfp_unfold\<close> and \<open>lfp_induct\<close>, to control unfolding.\<close>
   129 lemma def_lfp_unfold: "h \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> h = f h"
   130   by (auto intro!: lfp_unfold)
   132 lemma def_lfp_induct: "A \<equiv> lfp f \<Longrightarrow> mono f \<Longrightarrow> f (inf A P) \<le> P \<Longrightarrow> A \<le> P"
   133   by (blast intro: lfp_induct)
   135 lemma def_lfp_induct_set:
   136   "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"
   137   by (blast intro: lfp_induct_set)
   139 text \<open>Monotonicity of \<open>lfp\<close>!\<close>
   140 lemma lfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> lfp f \<le> lfp g"
   141   by (rule lfp_lowerbound [THEN lfp_greatest]) (blast intro: order_trans)
   144 subsection \<open>Greatest fixed points\<close>
   146 context complete_lattice
   147 begin
   149 definition gfp :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a"
   150   where "gfp f = Sup {u. u \<le> f u}"
   152 lemma gfp_upperbound: "X \<le> f X \<Longrightarrow> X \<le> gfp f"
   153   by (auto simp add: gfp_def intro: Sup_upper)
   155 lemma gfp_least: "(\<And>u. u \<le> f u \<Longrightarrow> u \<le> X) \<Longrightarrow> gfp f \<le> X"
   156   by (auto simp add: gfp_def intro: Sup_least)
   158 end
   160 lemma lfp_le_gfp: "mono f \<Longrightarrow> lfp f \<le> gfp f"
   161   by (rule gfp_upperbound) (simp add: lfp_fixpoint)
   163 lemma gfp_fixpoint:
   164   assumes "mono f"
   165   shows "f (gfp f) = gfp f"
   166   unfolding gfp_def
   167 proof (rule order_antisym)
   168   let ?H = "{u. u \<le> f u}"
   169   let ?a = "\<Squnion>?H"
   170   show "?a \<le> f ?a"
   171   proof (rule Sup_least)
   172     fix x
   173     assume "x \<in> ?H"
   174     then have "x \<le> f x" ..
   175     also from \<open>x \<in> ?H\<close> have "x \<le> ?a" by (rule Sup_upper)
   176     with \<open>mono f\<close> have "f x \<le> f ?a" ..
   177     finally show "x \<le> f ?a" .
   178   qed
   179   show "f ?a \<le> ?a"
   180   proof (rule Sup_upper)
   181     from \<open>mono f\<close> and \<open>?a \<le> f ?a\<close> have "f ?a \<le> f (f ?a)" ..
   182     then show "f ?a \<in> ?H" ..
   183   qed
   184 qed
   186 lemma gfp_unfold: "mono f \<Longrightarrow> gfp f = f (gfp f)"
   187   by (rule gfp_fixpoint [symmetric])
   189 lemma gfp_const: "gfp (\<lambda>x. t) = t"
   190   by (rule gfp_unfold) (simp add: mono_def)
   192 lemma gfp_eqI: "mono F \<Longrightarrow> F x = x \<Longrightarrow> (\<And>z. F z = z \<Longrightarrow> z \<le> x) \<Longrightarrow> gfp F = x"
   193   by (rule antisym) (simp_all add: gfp_upperbound gfp_unfold[symmetric])
   196 subsection \<open>Coinduction rules for greatest fixed points\<close>
   198 text \<open>Weak version.\<close>
   199 lemma weak_coinduct: "a \<in> X \<Longrightarrow> X \<subseteq> f X \<Longrightarrow> a \<in> gfp f"
   200   by (rule gfp_upperbound [THEN subsetD]) auto
   202 lemma weak_coinduct_image: "a \<in> X \<Longrightarrow> g`X \<subseteq> f (g`X) \<Longrightarrow> g a \<in> gfp f"
   203   apply (erule gfp_upperbound [THEN subsetD])
   204   apply (erule imageI)
   205   done
   207 lemma coinduct_lemma: "X \<le> f (sup X (gfp f)) \<Longrightarrow> mono f \<Longrightarrow> sup X (gfp f) \<le> f (sup X (gfp f))"
   208   apply (frule gfp_unfold [THEN eq_refl])
   209   apply (drule mono_sup)
   210   apply (rule le_supI)
   211    apply assumption
   212   apply (rule order_trans)
   213    apply (rule order_trans)
   214     apply assumption
   215    apply (rule sup_ge2)
   216   apply assumption
   217   done
   219 text \<open>Strong version, thanks to Coen and Frost.\<close>
   220 lemma coinduct_set: "mono f \<Longrightarrow> a \<in> X \<Longrightarrow> X \<subseteq> f (X \<union> gfp f) \<Longrightarrow> a \<in> gfp f"
   221   by (rule weak_coinduct[rotated], rule coinduct_lemma) blast+
   223 lemma gfp_fun_UnI2: "mono f \<Longrightarrow> a \<in> gfp f \<Longrightarrow> a \<in> f (X \<union> gfp f)"
   224   by (blast dest: gfp_fixpoint mono_Un)
   226 lemma gfp_ordinal_induct[case_names mono step union]:
   227   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   228   assumes mono: "mono f"
   229     and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
   230     and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"
   231   shows "P (gfp f)"
   232 proof -
   233   let ?M = "{S. gfp f \<le> S \<and> P S}"
   234   from P_Union have "P (Inf ?M)" by simp
   235   also have "Inf ?M = gfp f"
   236   proof (rule antisym)
   237     show "gfp f \<le> Inf ?M"
   238       by (blast intro: Inf_greatest)
   239     then have "f (gfp f) \<le> f (Inf ?M)"
   240       by (rule mono [THEN monoD])
   241     then have "gfp f \<le> f (Inf ?M)"
   242       using mono [THEN gfp_unfold] by simp
   243     then have "f (Inf ?M) \<in> ?M"
   244       using P_Union by simp (intro P_f Inf_greatest, auto)
   245     then have "Inf ?M \<le> f (Inf ?M)"
   246       by (rule Inf_lower)
   247     then show "Inf ?M \<le> gfp f"
   248       by (rule gfp_upperbound)
   249   qed
   250   finally show ?thesis .
   251 qed
   253 lemma coinduct:
   254   assumes mono: "mono f"
   255     and ind: "X \<le> f (sup X (gfp f))"
   256   shows "X \<le> gfp f"
   257 proof (induct rule: gfp_ordinal_induct)
   258   case mono
   259   then show ?case by fact
   260 next
   261   case (step S)
   262   then show ?case
   263     by (intro order_trans[OF ind _] monoD[OF mono]) auto
   264 next
   265   case (union M)
   266   then show ?case
   267     by (auto intro: mono Inf_greatest)
   268 qed
   271 subsection \<open>Even Stronger Coinduction Rule, by Martin Coen\<close>
   273 text \<open>Weakens the condition @{term "X \<subseteq> f X"} to one expressed using both
   274   @{term lfp} and @{term gfp}\<close>
   275 lemma coinduct3_mono_lemma: "mono f \<Longrightarrow> mono (\<lambda>x. f x \<union> X \<union> B)"
   276   by (iprover intro: subset_refl monoI Un_mono monoD)
   278 lemma coinduct3_lemma:
   279   "X \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f)) \<Longrightarrow> mono f \<Longrightarrow>
   280     lfp (\<lambda>x. f x \<union> X \<union> gfp f) \<subseteq> f (lfp (\<lambda>x. f x \<union> X \<union> gfp f))"
   281   apply (rule subset_trans)
   282    apply (erule coinduct3_mono_lemma [THEN lfp_unfold [THEN eq_refl]])
   283   apply (rule Un_least [THEN Un_least])
   284     apply (rule subset_refl, assumption)
   285   apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
   286   apply (rule monoD, assumption)
   287   apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
   288   done
   290 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"
   291   apply (rule coinduct3_lemma [THEN [2] weak_coinduct])
   292     apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst])
   293      apply simp_all
   294   done
   296 text  \<open>Definition forms of \<open>gfp_unfold\<close> and \<open>coinduct\<close>, to control unfolding.\<close>
   298 lemma def_gfp_unfold: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> A = f A"
   299   by (auto intro!: gfp_unfold)
   301 lemma def_coinduct: "A \<equiv> gfp f \<Longrightarrow> mono f \<Longrightarrow> X \<le> f (sup X A) \<Longrightarrow> X \<le> A"
   302   by (iprover intro!: coinduct)
   304 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"
   305   by (auto intro!: coinduct_set)
   307 lemma def_Collect_coinduct:
   308   "A \<equiv> gfp (\<lambda>w. Collect (P w)) \<Longrightarrow> mono (\<lambda>w. Collect (P w)) \<Longrightarrow> a \<in> X \<Longrightarrow>
   309     (\<And>z. z \<in> X \<Longrightarrow> P (X \<union> A) z) \<Longrightarrow> a \<in> A"
   310   by (erule def_coinduct_set) auto
   312 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"
   313   by (auto intro!: coinduct3)
   315 text \<open>Monotonicity of @{term gfp}!\<close>
   316 lemma gfp_mono: "(\<And>Z. f Z \<le> g Z) \<Longrightarrow> gfp f \<le> gfp g"
   317   by (rule gfp_upperbound [THEN gfp_least]) (blast intro: order_trans)
   320 subsection \<open>Rules for fixed point calculus\<close>
   322 lemma lfp_rolling:
   323   assumes "mono g" "mono f"
   324   shows "g (lfp (\<lambda>x. f (g x))) = lfp (\<lambda>x. g (f x))"
   325 proof (rule antisym)
   326   have *: "mono (\<lambda>x. f (g x))"
   327     using assms by (auto simp: mono_def)
   328   show "lfp (\<lambda>x. g (f x)) \<le> g (lfp (\<lambda>x. f (g x)))"
   329     by (rule lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
   330   show "g (lfp (\<lambda>x. f (g x))) \<le> lfp (\<lambda>x. g (f x))"
   331   proof (rule lfp_greatest)
   332     fix u
   333     assume u: "g (f u) \<le> u"
   334     then have "g (lfp (\<lambda>x. f (g x))) \<le> g (f u)"
   335       by (intro assms[THEN monoD] lfp_lowerbound)
   336     with u show "g (lfp (\<lambda>x. f (g x))) \<le> u"
   337       by auto
   338   qed
   339 qed
   341 lemma lfp_lfp:
   342   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
   343   shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
   344 proof (rule antisym)
   345   have *: "mono (\<lambda>x. f x x)"
   346     by (blast intro: monoI f)
   347   show "lfp (\<lambda>x. lfp (f x)) \<le> lfp (\<lambda>x. f x x)"
   348     by (intro lfp_lowerbound) (simp add: lfp_unfold[OF *, symmetric])
   349   show "lfp (\<lambda>x. lfp (f x)) \<ge> lfp (\<lambda>x. f x x)" (is "?F \<ge> _")
   350   proof (intro lfp_lowerbound)
   351     have *: "?F = lfp (f ?F)"
   352       by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
   353     also have "\<dots> = f ?F (lfp (f ?F))"
   354       by (rule lfp_unfold) (blast intro: monoI lfp_mono f)
   355     finally show "f ?F ?F \<le> ?F"
   356       by (simp add: *[symmetric])
   357   qed
   358 qed
   360 lemma gfp_rolling:
   361   assumes "mono g" "mono f"
   362   shows "g (gfp (\<lambda>x. f (g x))) = gfp (\<lambda>x. g (f x))"
   363 proof (rule antisym)
   364   have *: "mono (\<lambda>x. f (g x))"
   365     using assms by (auto simp: mono_def)
   366   show "g (gfp (\<lambda>x. f (g x))) \<le> gfp (\<lambda>x. g (f x))"
   367     by (rule gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   368   show "gfp (\<lambda>x. g (f x)) \<le> g (gfp (\<lambda>x. f (g x)))"
   369   proof (rule gfp_least)
   370     fix u
   371     assume u: "u \<le> g (f u)"
   372     then have "g (f u) \<le> g (gfp (\<lambda>x. f (g x)))"
   373       by (intro assms[THEN monoD] gfp_upperbound)
   374     with u show "u \<le> g (gfp (\<lambda>x. f (g x)))"
   375       by auto
   376   qed
   377 qed
   379 lemma gfp_gfp:
   380   assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
   381   shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
   382 proof (rule antisym)
   383   have *: "mono (\<lambda>x. f x x)"
   384     by (blast intro: monoI f)
   385   show "gfp (\<lambda>x. f x x) \<le> gfp (\<lambda>x. gfp (f x))"
   386     by (intro gfp_upperbound) (simp add: gfp_unfold[OF *, symmetric])
   387   show "gfp (\<lambda>x. gfp (f x)) \<le> gfp (\<lambda>x. f x x)" (is "?F \<le> _")
   388   proof (intro gfp_upperbound)
   389     have *: "?F = gfp (f ?F)"
   390       by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
   391     also have "\<dots> = f ?F (gfp (f ?F))"
   392       by (rule gfp_unfold) (blast intro: monoI gfp_mono f)
   393     finally show "?F \<le> f ?F ?F"
   394       by (simp add: *[symmetric])
   395   qed
   396 qed
   399 subsection \<open>Inductive predicates and sets\<close>
   401 text \<open>Package setup.\<close>
   403 lemmas basic_monos =
   404   subset_refl imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   405   Collect_mono in_mono vimage_mono
   407 lemma le_rel_bool_arg_iff: "X \<le> Y \<longleftrightarrow> X False \<le> Y False \<and> X True \<le> Y True"
   408   unfolding le_fun_def le_bool_def using bool_induct by auto
   410 lemma imp_conj_iff: "((P \<longrightarrow> Q) \<and> P) = (P \<and> Q)"
   411   by blast
   413 lemma meta_fun_cong: "P \<equiv> Q \<Longrightarrow> P a \<equiv> Q a"
   414   by auto
   416 ML_file "Tools/inductive.ML"
   418 lemmas [mono] =
   419   imp_refl disj_mono conj_mono ex_mono all_mono if_bool_eq_conj
   420   imp_mono not_mono
   421   Ball_def Bex_def
   422   induct_rulify_fallback
   425 subsection \<open>Inductive datatypes and primitive recursion\<close>
   427 text \<open>Package setup.\<close>
   429 ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
   430 ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
   431 ML_file "Tools/Old_Datatype/old_datatype_data.ML"
   432 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
   433 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
   434 ML_file "Tools/Old_Datatype/old_primrec.ML"
   436 ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
   437 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
   439 text \<open>Lambda-abstractions with pattern matching:\<close>
   440 syntax (ASCII)
   441   "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
   442 syntax
   443   "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
   444 parse_translation \<open>
   445   let
   446     fun fun_tr ctxt [cs] =
   447       let
   448         val x = (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
   449         val ft = Case_Translation.case_tr true ctxt [x, cs];
   450       in lambda x ft end
   451   in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
   452 \<close>
   454 end