# HG changeset patch # User haftmann # Date 1191873805 -7200 # Node ID fc90277c0dd7b946b912fa35c4ffa7826d08035c # Parent 95cda5dd58d5928c11b347630a54c32f4caa2374 integrated FixedPoint into Inductive diff -r 95cda5dd58d5 -r fc90277c0dd7 src/HOL/FixedPoint.thy --- a/src/HOL/FixedPoint.thy Mon Oct 08 22:03:21 2007 +0200 +++ b/src/HOL/FixedPoint.thy Mon Oct 08 22:03:25 2007 +0200 @@ -1,273 +0,0 @@ -(* Title: HOL/FixedPoint.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Stefan Berghofer, TU Muenchen - Copyright 1992 University of Cambridge -*) - -header {* Fixed Points and the Knaster-Tarski Theorem*} - -theory FixedPoint -imports Lattices -begin - -subsection {* Least and greatest fixed points *} - -definition - lfp :: "('a\complete_lattice \ 'a) \ 'a" where - "lfp f = Inf {u. f u \ u}" --{*least fixed point*} - -definition - gfp :: "('a\complete_lattice \ 'a) \ 'a" where - "gfp f = Sup {u. u \ f u}" --{*greatest fixed point*} - - -subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *} - -text{*@{term "lfp f"} is the least upper bound of - the set @{term "{u. f(u) \ u}"} *} - -lemma lfp_lowerbound: "f A \ A ==> lfp f \ A" - by (auto simp add: lfp_def intro: Inf_lower) - -lemma lfp_greatest: "(!!u. f u \ u ==> A \ u) ==> A \ lfp f" - by (auto simp add: lfp_def intro: Inf_greatest) - -lemma lfp_lemma2: "mono f ==> f (lfp f) \ lfp f" - by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) - -lemma lfp_lemma3: "mono f ==> lfp f \ f (lfp f)" - by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) - -lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)" - by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) - -lemma lfp_const: "lfp (\x. t) = t" - by (rule lfp_unfold) (simp add:mono_def) - - -subsection {* General induction rules for least fixed points *} - -theorem lfp_induct: - assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" - shows "lfp f <= P" -proof - - have "inf (lfp f) P <= lfp f" by (rule inf_le1) - with mono have "f (inf (lfp f) P) <= f (lfp f)" .. - also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) - finally have "f (inf (lfp f) P) <= lfp f" . - from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) - hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) - also have "inf (lfp f) P <= P" by (rule inf_le2) - finally show ?thesis . -qed - -lemma lfp_induct_set: - assumes lfp: "a: lfp(f)" - and mono: "mono(f)" - and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" - shows "P(a)" - by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) - (auto simp: inf_set_eq intro: indhyp) - -lemma lfp_ordinal_induct: - assumes mono: "mono f" - and P_f: "!!S. P S ==> P(f S)" - and P_Union: "!!M. !S:M. P S ==> P(Union M)" - shows "P(lfp f)" -proof - - let ?M = "{S. S \ lfp f & P S}" - have "P (Union ?M)" using P_Union by simp - also have "Union ?M = lfp f" - proof - show "Union ?M \ lfp f" by blast - hence "f (Union ?M) \ f (lfp f)" by (rule mono [THEN monoD]) - hence "f (Union ?M) \ lfp f" using mono [THEN lfp_unfold] by simp - hence "f (Union ?M) \ ?M" using P_f P_Union by simp - hence "f (Union ?M) \ Union ?M" by (rule Union_upper) - thus "lfp f \ Union ?M" by (rule lfp_lowerbound) - qed - finally show ?thesis . -qed - - -text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, - to control unfolding*} - -lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)" -by (auto intro!: lfp_unfold) - -lemma def_lfp_induct: - "[| A == lfp(f); mono(f); - f (inf A P) \ P - |] ==> A \ P" - by (blast intro: lfp_induct) - -lemma def_lfp_induct_set: - "[| A == lfp(f); mono(f); a:A; - !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) - |] ==> P(a)" - by (blast intro: lfp_induct_set) - -(*Monotonicity of lfp!*) -lemma lfp_mono: "(!!Z. f Z \ g Z) ==> lfp f \ lfp g" - by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans) - - -subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *} - -text{*@{term "gfp f"} is the greatest lower bound of - the set @{term "{u. u \ f(u)}"} *} - -lemma gfp_upperbound: "X \ f X ==> X \ gfp f" - by (auto simp add: gfp_def intro: Sup_upper) - -lemma gfp_least: "(!!u. u \ f u ==> u \ X) ==> gfp f \ X" - by (auto simp add: gfp_def intro: Sup_least) - -lemma gfp_lemma2: "mono f ==> gfp f \ f (gfp f)" - by (iprover intro: gfp_least order_trans monoD gfp_upperbound) - -lemma gfp_lemma3: "mono f ==> f (gfp f) \ gfp f" - by (iprover intro: gfp_lemma2 monoD gfp_upperbound) - -lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)" - by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) - - -subsection {* Coinduction rules for greatest fixed points *} - -text{*weak version*} -lemma weak_coinduct: "[| a: X; X \ f(X) |] ==> a : gfp(f)" -by (rule gfp_upperbound [THEN subsetD], auto) - -lemma weak_coinduct_image: "!!X. [| a : X; g`X \ f (g`X) |] ==> g a : gfp f" -apply (erule gfp_upperbound [THEN subsetD]) -apply (erule imageI) -done - -lemma coinduct_lemma: - "[| X \ f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \ f (sup X (gfp f))" - apply (frule gfp_lemma2) - apply (drule mono_sup) - apply (rule le_supI) - apply assumption - apply (rule order_trans) - apply (rule order_trans) - apply assumption - apply (rule sup_ge2) - apply assumption - done - -text{*strong version, thanks to Coen and Frost*} -lemma coinduct_set: "[| mono(f); a: X; X \ f(X Un gfp(f)) |] ==> a : gfp(f)" -by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq]) - -lemma coinduct: "[| mono(f); X \ f (sup X (gfp f)) |] ==> X \ gfp(f)" - apply (rule order_trans) - apply (rule sup_ge1) - apply (erule gfp_upperbound [OF coinduct_lemma]) - apply assumption - done - -lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" -by (blast dest: gfp_lemma2 mono_Un) - - -subsection {* Even Stronger Coinduction Rule, by Martin Coen *} - -text{* Weakens the condition @{term "X \ f(X)"} to one expressed using both - @{term lfp} and @{term gfp}*} - -lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" -by (iprover intro: subset_refl monoI Un_mono monoD) - -lemma coinduct3_lemma: - "[| X \ f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] - ==> lfp(%x. f(x) Un X Un gfp(f)) \ f(lfp(%x. f(x) Un X Un gfp(f)))" -apply (rule subset_trans) -apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) -apply (rule Un_least [THEN Un_least]) -apply (rule subset_refl, assumption) -apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) -apply (rule monoD, assumption) -apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) -done - -lemma coinduct3: - "[| mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" -apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) -apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) -done - - -text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, - to control unfolding*} - -lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)" -by (auto intro!: gfp_unfold) - -lemma def_coinduct: - "[| A==gfp(f); mono(f); X \ f(sup X A) |] ==> X \ A" -by (iprover intro!: coinduct) - -lemma def_coinduct_set: - "[| A==gfp(f); mono(f); a:X; X \ f(X Un A) |] ==> a: A" -by (auto intro!: coinduct_set) - -(*The version used in the induction/coinduction package*) -lemma def_Collect_coinduct: - "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); - a: X; !!z. z: X ==> P (X Un A) z |] ==> - a : A" -apply (erule def_coinduct_set, auto) -done - -lemma def_coinduct3: - "[| A==gfp(f); mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un A)) |] ==> a: A" -by (auto intro!: coinduct3) - -text{*Monotonicity of @{term gfp}!*} -lemma gfp_mono: "(!!Z. f Z \ g Z) ==> gfp f \ gfp g" - by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) - -ML -{* -val lfp_def = thm "lfp_def"; -val lfp_lowerbound = thm "lfp_lowerbound"; -val lfp_greatest = thm "lfp_greatest"; -val lfp_unfold = thm "lfp_unfold"; -val lfp_induct = thm "lfp_induct"; -val lfp_ordinal_induct = thm "lfp_ordinal_induct"; -val def_lfp_unfold = thm "def_lfp_unfold"; -val def_lfp_induct = thm "def_lfp_induct"; -val def_lfp_induct_set = thm "def_lfp_induct_set"; -val lfp_mono = thm "lfp_mono"; -val gfp_def = thm "gfp_def"; -val gfp_upperbound = thm "gfp_upperbound"; -val gfp_least = thm "gfp_least"; -val gfp_unfold = thm "gfp_unfold"; -val weak_coinduct = thm "weak_coinduct"; -val weak_coinduct_image = thm "weak_coinduct_image"; -val coinduct = thm "coinduct"; -val gfp_fun_UnI2 = thm "gfp_fun_UnI2"; -val coinduct3 = thm "coinduct3"; -val def_gfp_unfold = thm "def_gfp_unfold"; -val def_coinduct = thm "def_coinduct"; -val def_Collect_coinduct = thm "def_Collect_coinduct"; -val def_coinduct3 = thm "def_coinduct3"; -val gfp_mono = thm "gfp_mono"; -val le_funI = thm "le_funI"; -val le_boolI = thm "le_boolI"; -val le_boolI' = thm "le_boolI'"; -val inf_fun_eq = thm "inf_fun_eq"; -val inf_bool_eq = thm "inf_bool_eq"; -val le_funE = thm "le_funE"; -val le_funD = thm "le_funD"; -val le_boolE = thm "le_boolE"; -val le_boolD = thm "le_boolD"; -val le_bool_def = thm "le_bool_def"; -val le_fun_def = thm "le_fun_def"; -*} - -end diff -r 95cda5dd58d5 -r fc90277c0dd7 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Mon Oct 08 22:03:21 2007 +0200 +++ b/src/HOL/Inductive.thy Mon Oct 08 22:03:25 2007 +0200 @@ -3,10 +3,10 @@ Author: Markus Wenzel, TU Muenchen *) -header {* Support for inductive sets and types *} +header {* Knaster-Tarski Fixpoint Theorem and inductive definitions *} theory Inductive -imports FixedPoint Sum_Type +imports Lattices Sum_Type uses ("Tools/inductive_package.ML") "Tools/dseq.ML" @@ -20,6 +20,227 @@ ("Tools/primrec_package.ML") begin +subsection {* Least and greatest fixed points *} + +definition + lfp :: "('a\complete_lattice \ 'a) \ 'a" where + "lfp f = Inf {u. f u \ u}" --{*least fixed point*} + +definition + gfp :: "('a\complete_lattice \ 'a) \ 'a" where + "gfp f = Sup {u. u \ f u}" --{*greatest fixed point*} + + +subsection{* Proof of Knaster-Tarski Theorem using @{term lfp} *} + +text{*@{term "lfp f"} is the least upper bound of + the set @{term "{u. f(u) \ u}"} *} + +lemma lfp_lowerbound: "f A \ A ==> lfp f \ A" + by (auto simp add: lfp_def intro: Inf_lower) + +lemma lfp_greatest: "(!!u. f u \ u ==> A \ u) ==> A \ lfp f" + by (auto simp add: lfp_def intro: Inf_greatest) + +lemma lfp_lemma2: "mono f ==> f (lfp f) \ lfp f" + by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) + +lemma lfp_lemma3: "mono f ==> lfp f \ f (lfp f)" + by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) + +lemma lfp_unfold: "mono f ==> lfp f = f (lfp f)" + by (iprover intro: order_antisym lfp_lemma2 lfp_lemma3) + +lemma lfp_const: "lfp (\x. t) = t" + by (rule lfp_unfold) (simp add:mono_def) + + +subsection {* General induction rules for least fixed points *} + +theorem lfp_induct: + assumes mono: "mono f" and ind: "f (inf (lfp f) P) <= P" + shows "lfp f <= P" +proof - + have "inf (lfp f) P <= lfp f" by (rule inf_le1) + with mono have "f (inf (lfp f) P) <= f (lfp f)" .. + also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) + finally have "f (inf (lfp f) P) <= lfp f" . + from this and ind have "f (inf (lfp f) P) <= inf (lfp f) P" by (rule le_infI) + hence "lfp f <= inf (lfp f) P" by (rule lfp_lowerbound) + also have "inf (lfp f) P <= P" by (rule inf_le2) + finally show ?thesis . +qed + +lemma lfp_induct_set: + assumes lfp: "a: lfp(f)" + and mono: "mono(f)" + and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)" + shows "P(a)" + by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) + (auto simp: inf_set_eq intro: indhyp) + +lemma lfp_ordinal_induct: + assumes mono: "mono f" + and P_f: "!!S. P S ==> P(f S)" + and P_Union: "!!M. !S:M. P S ==> P(Union M)" + shows "P(lfp f)" +proof - + let ?M = "{S. S \ lfp f & P S}" + have "P (Union ?M)" using P_Union by simp + also have "Union ?M = lfp f" + proof + show "Union ?M \ lfp f" by blast + hence "f (Union ?M) \ f (lfp f)" by (rule mono [THEN monoD]) + hence "f (Union ?M) \ lfp f" using mono [THEN lfp_unfold] by simp + hence "f (Union ?M) \ ?M" using P_f P_Union by simp + hence "f (Union ?M) \ Union ?M" by (rule Union_upper) + thus "lfp f \ Union ?M" by (rule lfp_lowerbound) + qed + finally show ?thesis . +qed + + +text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, + to control unfolding*} + +lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)" +by (auto intro!: lfp_unfold) + +lemma def_lfp_induct: + "[| A == lfp(f); mono(f); + f (inf A P) \ P + |] ==> A \ P" + by (blast intro: lfp_induct) + +lemma def_lfp_induct_set: + "[| A == lfp(f); mono(f); a:A; + !!x. [| x: f(A Int {x. P(x)}) |] ==> P(x) + |] ==> P(a)" + by (blast intro: lfp_induct_set) + +(*Monotonicity of lfp!*) +lemma lfp_mono: "(!!Z. f Z \ g Z) ==> lfp f \ lfp g" + by (rule lfp_lowerbound [THEN lfp_greatest], blast intro: order_trans) + + +subsection {* Proof of Knaster-Tarski Theorem using @{term gfp} *} + +text{*@{term "gfp f"} is the greatest lower bound of + the set @{term "{u. u \ f(u)}"} *} + +lemma gfp_upperbound: "X \ f X ==> X \ gfp f" + by (auto simp add: gfp_def intro: Sup_upper) + +lemma gfp_least: "(!!u. u \ f u ==> u \ X) ==> gfp f \ X" + by (auto simp add: gfp_def intro: Sup_least) + +lemma gfp_lemma2: "mono f ==> gfp f \ f (gfp f)" + by (iprover intro: gfp_least order_trans monoD gfp_upperbound) + +lemma gfp_lemma3: "mono f ==> f (gfp f) \ gfp f" + by (iprover intro: gfp_lemma2 monoD gfp_upperbound) + +lemma gfp_unfold: "mono f ==> gfp f = f (gfp f)" + by (iprover intro: order_antisym gfp_lemma2 gfp_lemma3) + + +subsection {* Coinduction rules for greatest fixed points *} + +text{*weak version*} +lemma weak_coinduct: "[| a: X; X \ f(X) |] ==> a : gfp(f)" +by (rule gfp_upperbound [THEN subsetD], auto) + +lemma weak_coinduct_image: "!!X. [| a : X; g`X \ f (g`X) |] ==> g a : gfp f" +apply (erule gfp_upperbound [THEN subsetD]) +apply (erule imageI) +done + +lemma coinduct_lemma: + "[| X \ f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \ f (sup X (gfp f))" + apply (frule gfp_lemma2) + apply (drule mono_sup) + apply (rule le_supI) + apply assumption + apply (rule order_trans) + apply (rule order_trans) + apply assumption + apply (rule sup_ge2) + apply assumption + done + +text{*strong version, thanks to Coen and Frost*} +lemma coinduct_set: "[| mono(f); a: X; X \ f(X Un gfp(f)) |] ==> a : gfp(f)" +by (blast intro: weak_coinduct [OF _ coinduct_lemma, simplified sup_set_eq]) + +lemma coinduct: "[| mono(f); X \ f (sup X (gfp f)) |] ==> X \ gfp(f)" + apply (rule order_trans) + apply (rule sup_ge1) + apply (erule gfp_upperbound [OF coinduct_lemma]) + apply assumption + done + +lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))" +by (blast dest: gfp_lemma2 mono_Un) + + +subsection {* Even Stronger Coinduction Rule, by Martin Coen *} + +text{* Weakens the condition @{term "X \ f(X)"} to one expressed using both + @{term lfp} and @{term gfp}*} + +lemma coinduct3_mono_lemma: "mono(f) ==> mono(%x. f(x) Un X Un B)" +by (iprover intro: subset_refl monoI Un_mono monoD) + +lemma coinduct3_lemma: + "[| X \ f(lfp(%x. f(x) Un X Un gfp(f))); mono(f) |] + ==> lfp(%x. f(x) Un X Un gfp(f)) \ f(lfp(%x. f(x) Un X Un gfp(f)))" +apply (rule subset_trans) +apply (erule coinduct3_mono_lemma [THEN lfp_lemma3]) +apply (rule Un_least [THEN Un_least]) +apply (rule subset_refl, assumption) +apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption) +apply (rule monoD, assumption) +apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto) +done + +lemma coinduct3: + "[| mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un gfp(f))) |] ==> a : gfp(f)" +apply (rule coinduct3_lemma [THEN [2] weak_coinduct]) +apply (rule coinduct3_mono_lemma [THEN lfp_unfold, THEN ssubst], auto) +done + + +text{*Definition forms of @{text gfp_unfold} and @{text coinduct}, + to control unfolding*} + +lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)" +by (auto intro!: gfp_unfold) + +lemma def_coinduct: + "[| A==gfp(f); mono(f); X \ f(sup X A) |] ==> X \ A" +by (iprover intro!: coinduct) + +lemma def_coinduct_set: + "[| A==gfp(f); mono(f); a:X; X \ f(X Un A) |] ==> a: A" +by (auto intro!: coinduct_set) + +(*The version used in the induction/coinduction package*) +lemma def_Collect_coinduct: + "[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w))); + a: X; !!z. z: X ==> P (X Un A) z |] ==> + a : A" +apply (erule def_coinduct_set, auto) +done + +lemma def_coinduct3: + "[| A==gfp(f); mono(f); a:X; X \ f(lfp(%x. f(x) Un X Un A)) |] ==> a: A" +by (auto intro!: coinduct3) + +text{*Monotonicity of @{term gfp}!*} +lemma gfp_mono: "(!!Z. f Z \ g Z) ==> gfp f \ gfp g" + by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) + + subsection {* Inductive predicates and sets *} text {* Inversion of injective functions. *} @@ -64,6 +285,24 @@ Ball_def Bex_def induct_rulify_fallback +ML {* +val def_lfp_unfold = @{thm def_lfp_unfold} +val def_gfp_unfold = @{thm def_gfp_unfold} +val def_lfp_induct = @{thm def_lfp_induct} +val def_coinduct = @{thm def_coinduct} +val inf_bool_eq = @{thm inf_bool_eq} +val inf_fun_eq = @{thm inf_fun_eq} +val le_boolI = @{thm le_boolI} +val le_boolI' = @{thm le_boolI'} +val le_funI = @{thm le_funI} +val le_boolE = @{thm le_boolE} +val le_funE = @{thm le_funE} +val le_boolD = @{thm le_boolD} +val le_funD = @{thm le_funD} +val le_bool_def = @{thm le_bool_def} +val le_fun_def = @{thm le_fun_def} +*} + use "Tools/inductive_package.ML" setup InductivePackage.setup @@ -74,26 +313,6 @@ Ball_def Bex_def induct_rulify_fallback -lemma False_meta_all: - "Trueprop False \ (\P\bool. P)" -proof - fix P - assume False - then show P .. -next - assume "\P\bool. P" - then show False . -qed - -lemma not_eq_False: - assumes not_eq: "x \ y" - and eq: "x \ y" - shows False - using not_eq eq by auto - -lemmas not_eq_quodlibet = - not_eq_False [simplified False_meta_all] - subsection {* Inductive datatypes and primitive recursion *} diff -r 95cda5dd58d5 -r fc90277c0dd7 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Oct 08 22:03:21 2007 +0200 +++ b/src/HOL/IsaMakefile Mon Oct 08 22:03:25 2007 +0200 @@ -92,7 +92,7 @@ $(SRC)/Tools/nbe.ML $(SRC)/Tools/rat.ML Tools/TFL/casesplit.ML ATP_Linkup.thy \ Accessible_Part.thy Arith_Tools.thy Code_Setup.thy Datatype.thy \ Dense_Linear_Order.thy Divides.thy Equiv_Relations.thy Extraction.thy \ - Finite_Set.thy FixedPoint.thy Fun.thy FunDef.thy HOL.thy \ + Finite_Set.thy Fun.thy FunDef.thy HOL.thy \ Hilbert_Choice.thy Inductive.thy IntArith.thy IntDef.thy IntDiv.thy \ Lattices.thy List.thy Main.thy Map.thy Nat.thy NatBin.thy \ Numeral.thy OrderedGroup.thy Orderings.thy Power.thy PreList.thy \ diff -r 95cda5dd58d5 -r fc90277c0dd7 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Mon Oct 08 22:03:21 2007 +0200 +++ b/src/HOL/Relation.thy Mon Oct 08 22:03:25 2007 +0200 @@ -7,7 +7,7 @@ header {* Relations *} theory Relation -imports Product_Type FixedPoint +imports Product_Type begin subsection {* Definitions *} diff -r 95cda5dd58d5 -r fc90277c0dd7 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Mon Oct 08 22:03:21 2007 +0200 +++ b/src/HOL/Tools/inductive_package.ML Mon Oct 08 22:03:25 2007 +0200 @@ -589,7 +589,7 @@ fun mk_ind_def alt_name coind cs intr_ts monos params cnames_syn ctxt = let - val fp_name = if coind then @{const_name FixedPoint.gfp} else @{const_name FixedPoint.lfp}; + val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp}; val argTs = fold (fn c => fn Ts => Ts @ (List.drop (binder_types (fastype_of c), length params) \\ Ts)) cs [];