# HG changeset patch # User huffman # Date 1109799000 -3600 # Node ID 8455c9671494b447d73ea82a939fe95d4337c23a # Parent 045a07ac35a73eefbd6130e0ccf1dace6f7f3587 converted to new-style theory diff -r 045a07ac35a7 -r 8455c9671494 src/HOLCF/Porder.ML --- a/src/HOLCF/Porder.ML Wed Mar 02 12:06:15 2005 +0100 +++ b/src/HOLCF/Porder.ML Wed Mar 02 22:30:00 2005 +0100 @@ -1,182 +1,46 @@ -(* Title: HOLCF/Porder - ID: $Id$ - Author: Franz Regensburger -Conservative extension of theory Porder0 by constant definitions -*) - -(* ------------------------------------------------------------------------ *) -(* lubs are unique *) -(* ------------------------------------------------------------------------ *) - - -Goalw [is_lub_def, is_ub_def] - "[| S <<| x ; S <<| y |] ==> x=y"; -by (blast_tac (claset() addIs [antisym_less]) 1); -qed "unique_lub"; - -(* ------------------------------------------------------------------------ *) -(* chains are monotone functions *) -(* ------------------------------------------------------------------------ *) - -Goalw [chain_def] "chain F ==> x F x< F x << F y"; -by (dtac le_imp_less_or_eq 1); -by (blast_tac (claset() addIs [chain_mono]) 1); -qed "chain_mono3"; - - -(* ------------------------------------------------------------------------ *) -(* The range of a chain is a totally ordered << *) -(* ------------------------------------------------------------------------ *) - -Goalw [tord_def] "chain(F) ==> tord(range(F))"; -by Safe_tac; -by (rtac nat_less_cases 1); -by (ALLGOALS (fast_tac (claset() addIs [chain_mono]))); -qed "chain_tord"; - - -(* ------------------------------------------------------------------------ *) -(* technical lemmas about lub and is_lub *) -(* ------------------------------------------------------------------------ *) -bind_thm("lub",lub_def RS meta_eq_to_obj_eq); - -Goal "EX x. M <<| x ==> M <<| lub(M)"; -by (asm_full_simp_tac (simpset() addsimps [lub, some_eq_ex]) 1); -bind_thm ("lubI", exI RS result()); - -Goal "M <<| l ==> lub(M) = l"; -by (rtac unique_lub 1); -by (stac lub 1); -by (etac someI 1); -by (atac 1); -qed "thelubI"; - - -Goal "lub{x} = x"; -by (simp_tac (simpset() addsimps [thelubI,is_lub_def,is_ub_def]) 1); -qed "lub_singleton"; -Addsimps [lub_singleton]; - -(* ------------------------------------------------------------------------ *) -(* access to some definition as inference rule *) -(* ------------------------------------------------------------------------ *) - -Goalw [is_lub_def] "S <<| x ==> S <| x"; -by Auto_tac; -qed "is_lubD1"; - -Goalw [is_lub_def] "[| S <<| x; S <| u |] ==> x << u"; -by Auto_tac; -qed "is_lub_lub"; - -val prems = Goalw [is_lub_def] - "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x"; -by (blast_tac (claset() addIs prems) 1); -qed "is_lubI"; - -Goalw [chain_def] "chain F ==> F(i) << F(Suc(i))"; -by Auto_tac; -qed "chainE"; +(* legacy ML bindings *) -val prems = Goalw [chain_def] "(!!i. F i << F(Suc i)) ==> chain F"; -by (blast_tac (claset() addIs prems) 1); -qed "chainI"; - -Goal "chain Y ==> chain (%i. Y (i + j))"; -by (rtac chainI 1); -by (Clarsimp_tac 1); -by (etac chainE 1); -qed "chain_shift"; - -(* ------------------------------------------------------------------------ *) -(* technical lemmas about (least) upper bounds of chains *) -(* ------------------------------------------------------------------------ *) - -Goalw [is_ub_def] "range S <| x ==> S(i) << x"; -by (Blast_tac 1); -qed "ub_rangeD"; - -val prems = Goalw [is_ub_def] "(!!i. S i << x) ==> range S <| x"; -by (blast_tac (claset() addIs prems) 1); -qed "ub_rangeI"; - -bind_thm ("is_ub_lub", is_lubD1 RS ub_rangeD); -(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) - - -(* ------------------------------------------------------------------------ *) -(* results about finite chains *) -(* ------------------------------------------------------------------------ *) - -Goalw [max_in_chain_def] - "[| chain C; max_in_chain i C|] ==> range C <<| C i"; -by (rtac is_lubI 1); -by (rtac ub_rangeI 1); -by (res_inst_tac [("m","i")] nat_less_cases 1); -by (rtac (antisym_less_inverse RS conjunct2) 1); -by (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1); -by (etac spec 1); -by (rtac (antisym_less_inverse RS conjunct2) 1); -by (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1); -by (etac spec 1); -by (etac chain_mono 1); -by (atac 1); -by (etac (ub_rangeD) 1); -qed "lub_finch1"; +val is_ub_def = thm "is_ub_def"; +val is_lub_def = thm "is_lub_def"; +val tord_def = thm "tord_def"; +val chain_def = thm "chain_def"; +val max_in_chain_def = thm "max_in_chain_def"; +val finite_chain_def = thm "finite_chain_def"; +val lub_def = thm "lub_def"; +val unique_lub = thm "unique_lub"; +val chain_mono = thm "chain_mono"; +val chain_mono3 = thm "chain_mono3"; +val chain_tord = thm "chain_tord"; +val lub = thm "lub"; +val lubI = thm "lubI"; +val thelubI = thm "thelubI"; +val lub_singleton = thm "lub_singleton"; +val is_lubD1 = thm "is_lubD1"; +val is_lub_lub = thm "is_lub_lub"; +val is_lubI = thm "is_lubI"; +val chainE = thm "chainE"; +val chainI = thm "chainI"; +val chain_shift = thm "chain_shift"; +val ub_rangeD = thm "ub_rangeD"; +val ub_rangeI = thm "ub_rangeI"; +val is_ub_lub = thm "is_ub_lub"; +val lub_finch1 = thm "lub_finch1"; +val lub_finch2 = thm "lub_finch2"; +val bin_chain = thm "bin_chain"; +val bin_chainmax = thm "bin_chainmax"; +val lub_bin_chain = thm "lub_bin_chain"; +val lub_chain_maxelem = thm "lub_chain_maxelem"; +val lub_const = thm "lub_const"; -Goalw [finite_chain_def] - "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"; -by (rtac lub_finch1 1); -by (best_tac (claset() addIs [someI]) 2); -by (Blast_tac 1); -qed "lub_finch2"; - - -Goal "x< chain (%i. if i=0 then x else y)"; -by (rtac chainI 1); -by (induct_tac "i" 1); -by Auto_tac; -qed "bin_chain"; - -Goalw [max_in_chain_def,le_def] - "x< max_in_chain (Suc 0) (%i. if (i=0) then x else y)"; -by (rtac allI 1); -by (induct_tac "j" 1); -by Auto_tac; -qed "bin_chainmax"; - -Goal "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y"; -by (res_inst_tac [("s","if (Suc 0) = 0 then x else y")] subst 1 - THEN rtac lub_finch1 2); -by (etac bin_chain 2); -by (etac bin_chainmax 2); -by (Simp_tac 1); -qed "lub_bin_chain"; - -(* ------------------------------------------------------------------------ *) -(* the maximal element in a chain is its lub *) -(* ------------------------------------------------------------------------ *) - -Goal "[| Y i = c; ALL i. Y i< lub(range Y) = c"; -by (blast_tac (claset() addDs [ub_rangeD] - addIs [thelubI, is_lubI, ub_rangeI]) 1); -qed "lub_chain_maxelem"; - -(* ------------------------------------------------------------------------ *) -(* the lub of a constant chain is the constant *) -(* ------------------------------------------------------------------------ *) - -Goal "range(%x. c) <<| c"; -by (blast_tac (claset() addDs [ub_rangeD] addIs [is_lubI, ub_rangeI]) 1); -qed "lub_const"; - - - +structure Porder = +struct + val thy = the_context (); + val is_ub_def = is_ub_def; + val is_lub_def = is_lub_def; + val tord_def = tord_def; + val chain_def = chain_def; + val max_in_chain_def = max_in_chain_def; + val finite_chain_def = finite_chain_def; + val lub_def = lub_def; +end; diff -r 045a07ac35a7 -r 8455c9671494 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Wed Mar 02 12:06:15 2005 +0100 +++ b/src/HOLCF/Porder.thy Wed Mar 02 22:30:00 2005 +0100 @@ -1,11 +1,12 @@ (* Title: HOLCF/porder.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Conservative extension of theory Porder0 by constant definitions *) -Porder = Porder0 + +theory Porder = Porder0: consts "<|" :: "['a set,'a::po] => bool" (infixl 55) @@ -25,25 +26,217 @@ syntax (xsymbols) - "LUB " :: "[idts, 'a] => 'a" ("(3\\_./ _)"[0,10] 10) + "LUB " :: "[idts, 'a] => 'a" ("(3\_./ _)"[0,10] 10) defs (* class definitions *) -is_ub_def "S <| x == ! y. y:S --> y< x << u)" +is_ub_def: "S <| x == ! y. y:S --> y< x << u)" (* Arbitrary chains are total orders *) -tord_def "tord S == !x y. x:S & y:S --> (x< (x< C(i) = C(j)" -finite_chain_def "finite_chain C == chain(C) & (? i. max_in_chain i C)" +max_in_chain_def: "max_in_chain i C == ! j. i <= j --> C(i) = C(j)" +finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" + +lub_def: "lub S == (@x. S <<| x)" + +(* Title: HOLCF/Porder + ID: $Id$ + Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Conservative extension of theory Porder0 by constant definitions +*) + +(* ------------------------------------------------------------------------ *) +(* lubs are unique *) +(* ------------------------------------------------------------------------ *) + + +lemma unique_lub: + "[| S <<| x ; S <<| y |] ==> x=y" +apply (unfold is_lub_def is_ub_def) +apply (blast intro: antisym_less) +done + +(* ------------------------------------------------------------------------ *) +(* chains are monotone functions *) +(* ------------------------------------------------------------------------ *) + +lemma chain_mono [rule_format]: "chain F ==> x F x< F x << F y" +apply (drule le_imp_less_or_eq) +apply (blast intro: chain_mono) +done + + +(* ------------------------------------------------------------------------ *) +(* The range of a chain is a totally ordered << *) +(* ------------------------------------------------------------------------ *) + +lemma chain_tord: "chain(F) ==> tord(range(F))" +apply (unfold tord_def) +apply safe +apply (rule nat_less_cases) +apply (fast intro: chain_mono)+ +done + + +(* ------------------------------------------------------------------------ *) +(* technical lemmas about lub and is_lub *) +(* ------------------------------------------------------------------------ *) +lemmas lub = lub_def [THEN meta_eq_to_obj_eq, standard] + +lemma lubI[OF exI]: "EX x. M <<| x ==> M <<| lub(M)" +apply (simp add: lub some_eq_ex) +done + +lemma thelubI: "M <<| l ==> lub(M) = l" +apply (rule unique_lub) +apply (subst lub) +apply (erule someI) +apply assumption +done + + +lemma lub_singleton: "lub{x} = x" +apply (simp (no_asm) add: thelubI is_lub_def is_ub_def) +done +declare lub_singleton [simp] + +(* ------------------------------------------------------------------------ *) +(* access to some definition as inference rule *) +(* ------------------------------------------------------------------------ *) + +lemma is_lubD1: "S <<| x ==> S <| x" +apply (unfold is_lub_def) +apply auto +done + +lemma is_lub_lub: "[| S <<| x; S <| u |] ==> x << u" +apply (unfold is_lub_def) +apply auto +done + +lemma is_lubI: + "[| S <| x; !!u. S <| u ==> x << u |] ==> S <<| x" +apply (unfold is_lub_def) +apply blast +done -lub_def "lub S == (@x. S <<| x)" +lemma chainE: "chain F ==> F(i) << F(Suc(i))" +apply (unfold chain_def) +apply auto +done + +lemma chainI: "(!!i. F i << F(Suc i)) ==> chain F" +apply (unfold chain_def) +apply blast +done + +lemma chain_shift: "chain Y ==> chain (%i. Y (i + j))" +apply (rule chainI) +apply clarsimp +apply (erule chainE) +done + +(* ------------------------------------------------------------------------ *) +(* technical lemmas about (least) upper bounds of chains *) +(* ------------------------------------------------------------------------ *) + +lemma ub_rangeD: "range S <| x ==> S(i) << x" +apply (unfold is_ub_def) +apply blast +done + +lemma ub_rangeI: "(!!i. S i << x) ==> range S <| x" +apply (unfold is_ub_def) +apply blast +done + +lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] +(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) + + +(* ------------------------------------------------------------------------ *) +(* results about finite chains *) +(* ------------------------------------------------------------------------ *) + +lemma lub_finch1: + "[| chain C; max_in_chain i C|] ==> range C <<| C i" +apply (unfold max_in_chain_def) +apply (rule is_lubI) +apply (rule ub_rangeI) +apply (rule_tac m = "i" in nat_less_cases) +apply (rule antisym_less_inverse [THEN conjunct2]) +apply (erule disjI1 [THEN less_or_eq_imp_le, THEN rev_mp]) +apply (erule spec) +apply (rule antisym_less_inverse [THEN conjunct2]) +apply (erule disjI2 [THEN less_or_eq_imp_le, THEN rev_mp]) +apply (erule spec) +apply (erule chain_mono) +apply assumption +apply (erule ub_rangeD) +done + +lemma lub_finch2: + "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)" +apply (unfold finite_chain_def) +apply (rule lub_finch1) +prefer 2 apply (best intro: someI) +apply blast +done + + +lemma bin_chain: "x< chain (%i. if i=0 then x else y)" +apply (rule chainI) +apply (induct_tac "i") +apply auto +done + +lemma bin_chainmax: + "x< max_in_chain (Suc 0) (%i. if (i=0) then x else y)" +apply (unfold max_in_chain_def le_def) +apply (rule allI) +apply (induct_tac "j") +apply auto +done + +lemma lub_bin_chain: "x << y ==> range(%i::nat. if (i=0) then x else y) <<| y" +apply (rule_tac s = "if (Suc 0) = 0 then x else y" in subst , rule_tac [2] lub_finch1) +apply (erule_tac [2] bin_chain) +apply (erule_tac [2] bin_chainmax) +apply (simp (no_asm)) +done + +(* ------------------------------------------------------------------------ *) +(* the maximal element in a chain is its lub *) +(* ------------------------------------------------------------------------ *) + +lemma lub_chain_maxelem: "[| Y i = c; ALL i. Y i< lub(range Y) = c" +apply (blast dest: ub_rangeD intro: thelubI is_lubI ub_rangeI) +done + +(* ------------------------------------------------------------------------ *) +(* the lub of a constant chain is the constant *) +(* ------------------------------------------------------------------------ *) + +lemma lub_const: "range(%x. c) <<| c" +apply (blast dest: ub_rangeD intro: is_lubI ub_rangeI) +done end diff -r 045a07ac35a7 -r 8455c9671494 src/HOLCF/Porder0.ML --- a/src/HOLCF/Porder0.ML Wed Mar 02 12:06:15 2005 +0100 +++ b/src/HOLCF/Porder0.ML Wed Mar 02 22:30:00 2005 +0100 @@ -1,34 +1,10 @@ -(* Title: HOLCF/Porder0.ML - ID: $Id$ - Author: Oscar Slotosch -derive the characteristic axioms for the characteristic constants -*) - -AddIffs [refl_less]; - -(* ------------------------------------------------------------------------ *) -(* minimal fixes least element *) -(* ------------------------------------------------------------------------ *) -Goal "!x::'a::po. uu< uu=(@u.!y. u< x << y & y << x"; -by (Blast_tac 1); -qed "antisym_less_inverse"; - - -Goal "[| (a::'a::po) << b; c << a; b << d|] ==> c << d"; -by (etac trans_less 1); -by (etac trans_less 1); -by (atac 1); -qed "box_less"; - -Goal "((x::'a::po)=y) = (x << y & y << x)"; -by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1); -qed "po_eq_conv"; +val refl_less = thm "refl_less"; +val antisym_less = thm "antisym_less"; +val trans_less = thm "trans_less"; +val minimal2UU = thm "minimal2UU"; +val antisym_less_inverse = thm "antisym_less_inverse"; +val box_less = thm "box_less"; +val po_eq_conv = thm "po_eq_conv"; diff -r 045a07ac35a7 -r 8455c9671494 src/HOLCF/Porder0.thy --- a/src/HOLCF/Porder0.thy Wed Mar 02 12:06:15 2005 +0100 +++ b/src/HOLCF/Porder0.thy Wed Mar 02 22:30:00 2005 +0100 @@ -1,11 +1,12 @@ (* Title: HOLCF/Porder0.thy ID: $Id$ Author: Franz Regensburger + License: GPL (GNU GENERAL PUBLIC LICENSE) Definition of class porder (partial order). *) -Porder0 = Main + +theory Porder0 = Main: (* introduce a (syntactic) class for the constant << *) axclass sq_ord < type @@ -15,14 +16,41 @@ "<<" :: "['a,'a::sq_ord] => bool" (infixl 55) syntax (xsymbols) - "op <<" :: "['a,'a::sq_ord] => bool" (infixl "\\" 55) + "op <<" :: "['a,'a::sq_ord] => bool" (infixl "\" 55) axclass po < sq_ord (* class axioms: *) -refl_less "x << x" -antisym_less "[|x << y; y << x |] ==> x = y" -trans_less "[|x << y; y << z |] ==> x << z" - +refl_less: "x << x" +antisym_less: "[|x << y; y << x |] ==> x = y" +trans_less: "[|x << y; y << z |] ==> x << z" + +declare refl_less [iff] + +(* ------------------------------------------------------------------------ *) +(* minimal fixes least element *) +(* ------------------------------------------------------------------------ *) +lemma minimal2UU[OF allI] : "!x::'a::po. uu< uu=(@u.!y. u< x << y & y << x" +apply blast +done + + +lemma box_less: "[| (a::'a::po) << b; c << a; b << d|] ==> c << d" +apply (erule trans_less) +apply (erule trans_less) +apply assumption +done + +lemma po_eq_conv: "((x::'a::po)=y) = (x << y & y << x)" +apply (fast elim!: antisym_less_inverse intro!: antisym_less) +done end