# HG changeset patch # User berghofe # Date 1160755816 -7200 # Node ID 5693e4471c2b22f9af6fce6fb701ced9d77b1f4f # Parent 430b35c9cd27e92c77f186f2d31daaed716e0da6 Generalized gfp and lfp to arbitrary complete lattices. diff -r 430b35c9cd27 -r 5693e4471c2b src/HOL/FixedPoint.thy --- a/src/HOL/FixedPoint.thy Fri Oct 13 18:08:48 2006 +0200 +++ b/src/HOL/FixedPoint.thy Fri Oct 13 18:10:16 2006 +0200 @@ -1,6 +1,7 @@ (* Title: HOL/FixedPoint.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Stefan Berghofer, TU Muenchen Copyright 1992 University of Cambridge *) @@ -10,53 +11,347 @@ imports Product_Type begin +subsection {* Complete lattices *} + +consts + Meet :: "'a::order set \ 'a" + Join :: "'a::order set \ 'a" + +defs Join_def: "Join A == Meet {b. \a \ A. a <= b}" + +axclass comp_lat < order + Meet_lower: "x \ A \ Meet A <= x" + Meet_greatest: "(\x. x \ A \ z <= x) \ z <= Meet A" + +theorem Join_upper: "(x::'a::comp_lat) \ A \ x <= Join A" + by (auto simp: Join_def intro: Meet_greatest) + +theorem Join_least: "(\x::'a::comp_lat. x \ A \ x <= z) \ Join A <= z" + by (auto simp: Join_def intro: Meet_lower) + +text {* A complete lattice is a lattice *} + +lemma is_meet_Meet: "is_meet (\(x::'a::comp_lat) y. Meet {x, y})" + by (auto simp: is_meet_def intro: Meet_lower Meet_greatest) + +lemma is_join_Join: "is_join (\(x::'a::comp_lat) y. Join {x, y})" + by (auto simp: is_join_def intro: Join_upper Join_least) + +instance comp_lat < lorder +proof + from is_meet_Meet show "\m::'a\'a\'a. is_meet m" by iprover + from is_join_Join show "\j::'a\'a\'a. is_join j" by iprover +qed + +lemma mono_join: "mono f \ join (f A) (f B) <= f (join A B)" + by (auto simp add: mono_def intro: join_imp_le join_left_le join_right_le) + +lemma mono_meet: "mono f \ f (meet A B) <= meet (f A) (f B)" + by (auto simp add: mono_def intro: meet_imp_le meet_left_le meet_right_le) + + +subsection {* Some instances of the type class of complete lattices *} + +subsubsection {* Booleans *} + +instance bool :: ord .. + +defs + le_bool_def: "P <= Q == P \ Q" + less_bool_def: "P < Q == (P::bool) <= Q \ P \ Q" + +theorem le_boolI: "(P \ Q) \ P <= Q" + by (simp add: le_bool_def) + +theorem le_boolI': "P \ Q \ P <= Q" + by (simp add: le_bool_def) + +theorem le_boolE: "P <= Q \ P \ (Q \ R) \ R" + by (simp add: le_bool_def) + +theorem le_boolD: "P <= Q \ P \ Q" + by (simp add: le_bool_def) + +instance bool :: order + apply intro_classes + apply (unfold le_bool_def less_bool_def) + apply iprover+ + done + +defs Meet_bool_def: "Meet A == ALL x:A. x" + +instance bool :: comp_lat + apply intro_classes + apply (unfold Meet_bool_def) + apply (iprover intro!: le_boolI elim: ballE) + apply (iprover intro!: ballI le_boolI elim: ballE le_boolE) + done + +theorem meet_bool_eq: "meet P Q = (P \ Q)" + apply (rule order_antisym) + apply (rule le_boolI) + apply (rule conjI) + apply (rule le_boolE) + apply (rule meet_left_le) + apply assumption+ + apply (rule le_boolE) + apply (rule meet_right_le) + apply assumption+ + apply (rule meet_imp_le) + apply (rule le_boolI) + apply (erule conjunct1) + apply (rule le_boolI) + apply (erule conjunct2) + done + +theorem join_bool_eq: "join P Q = (P \ Q)" + apply (rule order_antisym) + apply (rule join_imp_le) + apply (rule le_boolI) + apply (erule disjI1) + apply (rule le_boolI) + apply (erule disjI2) + apply (rule le_boolI) + apply (erule disjE) + apply (rule le_boolE) + apply (rule join_left_le) + apply assumption+ + apply (rule le_boolE) + apply (rule join_right_le) + apply assumption+ + done + +theorem Join_bool_eq: "Join A = (EX x:A. x)" + apply (rule order_antisym) + apply (rule Join_least) + apply (rule le_boolI) + apply (erule bexI, assumption) + apply (rule le_boolI) + apply (erule bexE) + apply (rule le_boolE) + apply (rule Join_upper) + apply assumption+ + done + +subsubsection {* Functions *} + +instance "fun" :: (type, ord) ord .. + +defs + le_fun_def: "f <= g == \x. f x <= g x" + less_fun_def: "f < g == (f::'a\'b::ord) <= g \ f \ g" + +theorem le_funI: "(\x. f x <= g x) \ f <= g" + by (simp add: le_fun_def) + +theorem le_funE: "f <= g \ (f x <= g x \ P) \ P" + by (simp add: le_fun_def) + +theorem le_funD: "f <= g \ f x <= g x" + by (simp add: le_fun_def) + +text {* +Handy introduction and elimination rules for @{text "\"} +on unary and binary predicates +*} + +lemma predicate1I [intro]: + assumes PQ: "\x. P x \ Q x" + shows "P \ Q" + apply (rule le_funI) + apply (rule le_boolI) + apply (rule PQ) + apply assumption + done + +lemma predicate1D [elim]: "P \ Q \ P x \ Q x" + apply (erule le_funE) + apply (erule le_boolE) + apply assumption+ + done + +lemma predicate2I [intro]: + assumes PQ: "\x y. P x y \ Q x y" + shows "P \ Q" + apply (rule le_funI)+ + apply (rule le_boolI) + apply (rule PQ) + apply assumption + done + +lemma predicate2D [elim]: "P \ Q \ P x y \ Q x y" + apply (erule le_funE)+ + apply (erule le_boolE) + apply assumption+ + done + +instance "fun" :: (type, order) order + apply intro_classes + apply (rule le_funI) + apply (rule order_refl) + apply (rule le_funI) + apply (erule le_funE)+ + apply (erule order_trans) + apply assumption + apply (rule ext) + apply (erule le_funE)+ + apply (erule order_antisym) + apply assumption + apply (simp add: less_fun_def) + done + +defs Meet_fun_def: "Meet A == (\x. Meet {y. EX f:A. y = f x})" + +instance "fun" :: (type, comp_lat) comp_lat + apply intro_classes + apply (unfold Meet_fun_def) + apply (rule le_funI) + apply (rule Meet_lower) + apply (rule CollectI) + apply (rule bexI) + apply (rule refl) + apply assumption + apply (rule le_funI) + apply (rule Meet_greatest) + apply (erule CollectE) + apply (erule bexE) + apply (iprover elim: le_funE) + done + +theorem meet_fun_eq: "meet f g = (\x. meet (f x) (g x))" + apply (rule order_antisym) + apply (rule le_funI) + apply (rule meet_imp_le) + apply (rule le_funD [OF meet_left_le]) + apply (rule le_funD [OF meet_right_le]) + apply (rule meet_imp_le) + apply (rule le_funI) + apply (rule meet_left_le) + apply (rule le_funI) + apply (rule meet_right_le) + done + +theorem join_fun_eq: "join f g = (\x. join (f x) (g x))" + apply (rule order_antisym) + apply (rule join_imp_le) + apply (rule le_funI) + apply (rule join_left_le) + apply (rule le_funI) + apply (rule join_right_le) + apply (rule le_funI) + apply (rule join_imp_le) + apply (rule le_funD [OF join_left_le]) + apply (rule le_funD [OF join_right_le]) + done + +theorem Join_fun_eq: "Join A = (\x. Join {y::'a::comp_lat. EX f:A. y = f x})" + apply (rule order_antisym) + apply (rule Join_least) + apply (rule le_funI) + apply (rule Join_upper) + apply fast + apply (rule le_funI) + apply (rule Join_least) + apply (erule CollectE) + apply (erule bexE) + apply (drule le_funD [OF Join_upper]) + apply simp + done + +subsubsection {* Sets *} + +defs Meet_set_def: "Meet S == \S" + +instance set :: (type) comp_lat + by intro_classes (auto simp add: Meet_set_def) + +theorem meet_set_eq: "meet A B = A \ B" + apply (rule subset_antisym) + apply (rule Int_greatest) + apply (rule meet_left_le) + apply (rule meet_right_le) + apply (rule meet_imp_le) + apply (rule Int_lower1) + apply (rule Int_lower2) + done + +theorem join_set_eq: "join A B = A \ B" + apply (rule subset_antisym) + apply (rule join_imp_le) + apply (rule Un_upper1) + apply (rule Un_upper2) + apply (rule Un_least) + apply (rule join_left_le) + apply (rule join_right_le) + done + +theorem Join_set_eq: "Join S = \S" + apply (rule subset_antisym) + apply (rule Join_least) + apply (erule Union_upper) + apply (rule Union_least) + apply (erule Join_upper) + done + + +subsection {* Least and greatest fixed points *} + constdefs - lfp :: "['a set \ 'a set] \ 'a set" - "lfp(f) == Inter({u. f(u) \ u})" --{*least fixed point*} + lfp :: "(('a::comp_lat) => 'a) => 'a" + "lfp f == Meet {u. f u <= u}" --{*least fixed point*} - gfp :: "['a set=>'a set] => 'a set" - "gfp(f) == Union({u. u \ f(u)})" + gfp :: "(('a::comp_lat) => 'a) => 'a" + "gfp f == Join {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}"} *} + the set @{term "{u. f(u) \ u}"} *} + +lemma lfp_lowerbound: "f A \ A ==> lfp f \ A" + by (auto simp add: lfp_def intro: Meet_lower) + +lemma lfp_greatest: "(!!u. f u \ u ==> A \ u) ==> A \ lfp f" + by (auto simp add: lfp_def intro: Meet_greatest) -lemma lfp_lowerbound: "f(A) \ A ==> lfp(f) \ A" -by (auto simp add: lfp_def) +lemma lfp_lemma2: "mono f ==> f (lfp f) \ lfp f" + by (iprover intro: lfp_greatest order_trans monoD lfp_lowerbound) -lemma lfp_greatest: "[| !!u. f(u) \ u ==> A\u |] ==> A \ lfp(f)" -by (auto simp add: lfp_def) +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_lemma2: "mono(f) ==> f(lfp(f)) \ lfp(f)" -by (iprover intro: lfp_greatest subset_trans monoD lfp_lowerbound) - -lemma lfp_lemma3: "mono(f) ==> lfp(f) \ f(lfp(f))" -by (iprover intro: lfp_lemma2 monoD lfp_lowerbound) +subsection{*General induction rules for least fixed points*} -lemma lfp_unfold: "mono(f) ==> lfp(f) = f(lfp(f))" -by (iprover intro: equalityI lfp_lemma2 lfp_lemma3) +theorem lfp_induct: + assumes mono: "mono f" and ind: "f (meet (lfp f) P) <= P" + shows "lfp f <= P" +proof - + have "meet (lfp f) P <= lfp f" by (rule meet_left_le) + with mono have "f (meet (lfp f) P) <= f (lfp f)" .. + also from mono have "f (lfp f) = lfp f" by (rule lfp_unfold [symmetric]) + finally have "f (meet (lfp f) P) <= lfp f" . + from this and ind have "f (meet (lfp f) P) <= meet (lfp f) P" by (rule meet_imp_le) + hence "lfp f <= meet (lfp f) P" by (rule lfp_lowerbound) + also have "meet (lfp f) P <= P" by (rule meet_right_le) + finally show ?thesis . +qed -subsection{*General induction rules for greatest fixed points*} - -lemma lfp_induct: +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)" -apply (rule_tac a=a in Int_lower2 [THEN subsetD, THEN CollectD]) -apply (rule lfp [THEN [2] lfp_lowerbound [THEN subsetD]]) -apply (rule Int_greatest) - apply (rule subset_trans [OF Int_lower1 [THEN mono [THEN monoD]] - mono [THEN lfp_lemma2]]) -apply (blast intro: indhyp) -done + by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp]) + (auto simp: meet_set_eq intro: indhyp) text{*Version of induction for binary relations*} -lemmas lfp_induct2 = lfp_induct [of "(a,b)", split_format (complete)] +lemmas lfp_induct2 = lfp_induct_set [of "(a,b)", split_format (complete)] lemma lfp_ordinal_induct: @@ -82,36 +377,42 @@ by (auto intro!: lfp_unfold) lemma def_lfp_induct: + "[| A == lfp(f); mono(f); + f (meet 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) + 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) +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)}"} *} + the set @{term "{u. u \ f(u)}"} *} -lemma gfp_upperbound: "[| X \ f(X) |] ==> X \ gfp(f)" -by (auto simp add: gfp_def) +lemma gfp_upperbound: "X \ f X ==> X \ gfp f" + by (auto simp add: gfp_def intro: Join_upper) -lemma gfp_least: "[| !!u. u \ f(u) ==> u\X |] ==> gfp(f) \ X" -by (auto simp add: gfp_def) +lemma gfp_least: "(!!u. u \ f u ==> u \ X) ==> gfp f \ X" + by (auto simp add: gfp_def intro: Join_least) -lemma gfp_lemma2: "mono(f) ==> gfp(f) \ f(gfp(f))" -by (iprover intro: gfp_least subset_trans monoD gfp_upperbound) +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_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: equalityI gfp_lemma2 gfp_lemma3) +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*} @@ -125,12 +426,28 @@ done lemma coinduct_lemma: - "[| X \ f(X Un gfp(f)); mono(f) |] ==> X Un gfp(f) \ f(X Un gfp(f))" -by (blast dest: gfp_lemma2 mono_Un) + "[| X \ f (join X (gfp f)); mono f |] ==> join X (gfp f) \ f (join X (gfp f))" + apply (frule gfp_lemma2) + apply (drule mono_join) + apply (rule join_imp_le) + apply assumption + apply (rule order_trans) + apply (rule order_trans) + apply assumption + apply (rule join_right_le) + apply assumption + done text{*strong version, thanks to Coen and Frost*} -lemma coinduct: "[| mono(f); a: X; X \ f(X Un gfp(f)) |] ==> a : gfp(f)" -by (blast intro: weak_coinduct [OF _ coinduct_lemma]) +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 join_set_eq]) + +lemma coinduct: "[| mono(f); X \ f (join X (gfp f)) |] ==> X \ gfp(f)" + apply (rule order_trans) + apply (rule join_left_le) + 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) @@ -169,15 +486,19 @@ by (auto intro!: gfp_unfold) lemma def_coinduct: + "[| A==gfp(f); mono(f); X \ f(join 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) +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, auto) +apply (erule def_coinduct_set, auto) done lemma def_coinduct3: @@ -185,8 +506,8 @@ 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) +lemma gfp_mono: "(!!Z. f Z \ g Z) ==> gfp f \ gfp g" + by (rule gfp_upperbound [THEN gfp_least], blast intro: order_trans) ML @@ -200,6 +521,7 @@ 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"; @@ -215,6 +537,16 @@ 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 meet_fun_eq = thm "meet_fun_eq"; +val meet_bool_eq = thm "meet_bool_eq"; +val le_funE = thm "le_funE"; +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