--- a/src/HOLCF/Porder.ML Tue Jul 04 14:58:40 2000 +0200
+++ b/src/HOLCF/Porder.ML Tue Jul 04 15:58:11 2000 +0200
@@ -1,49 +1,48 @@
-(* Title: HOLCF/Porder.thy
+(* Title: HOLCF/Porder
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
-Lemmas for theory Porder.thy
+Conservative extension of theory Porder0 by constant definitions
*)
(* ------------------------------------------------------------------------ *)
(* lubs are unique *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "unique_lub" thy [is_lub, is_ub]
- "[| S <<| x ; S <<| y |] ==> x=y"
-( fn prems =>
- [
- (cut_facts_tac prems 1),
- (etac conjE 1),
- (etac conjE 1),
- (rtac antisym_less 1),
- (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1)),
- (rtac mp 1),((etac allE 1) THEN (atac 1) THEN (atac 1))
- ]);
+
+val prems = goalw thy [is_lub, is_ub]
+ "[| S <<| x ; S <<| y |] ==> x=y";
+by (cut_facts_tac prems 1);
+by (etac conjE 1);
+by (etac conjE 1);
+by (rtac antisym_less 1);
+by (rtac mp 1);
+by ((etac allE 1) THEN (atac 1) THEN (atac 1));
+by (rtac mp 1);
+by ((etac allE 1) THEN (atac 1) THEN (atac 1));
+qed "unique_lub";
(* ------------------------------------------------------------------------ *)
(* chains are monotone functions *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_mono" thy [chain] "chain F ==> x<y --> F x<<F y"
-( fn prems =>
- [
- (cut_facts_tac prems 1),
- (induct_tac "y" 1),
- (rtac impI 1),
- (etac less_zeroE 1),
- (stac less_Suc_eq 1),
- (strip_tac 1),
- (etac disjE 1),
- (rtac trans_less 1),
- (etac allE 2),
- (atac 2),
- (fast_tac HOL_cs 1),
- (hyp_subst_tac 1),
- (etac allE 1),
- (atac 1)
- ]);
+val prems = goalw thy [chain] "chain F ==> x<y --> F x<<F y";
+by (cut_facts_tac prems 1);
+by (induct_tac "y" 1);
+by (rtac impI 1);
+by (etac less_zeroE 1);
+by (stac less_Suc_eq 1);
+by (strip_tac 1);
+by (etac disjE 1);
+by (rtac trans_less 1);
+by (etac allE 2);
+by (atac 2);
+by (fast_tac HOL_cs 1);
+by (hyp_subst_tac 1);
+by (etac allE 1);
+by (atac 1);
+qed "chain_mono";
Goal "[| chain F; x <= y |] ==> F x << F y";
by (rtac (le_imp_less_or_eq RS disjE) 1);
@@ -56,16 +55,16 @@
(* ------------------------------------------------------------------------ *)
-(* The range of a chain is a totaly ordered << *)
+(* The range of a chain is a totally ordered << *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "chain_tord" thy [tord]
-"!!F. chain(F) ==> tord(range(F))"
- (fn _ =>
- [
- Safe_tac,
- (rtac nat_less_cases 1),
- (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])))]);
+val _ = goalw thy [tord]
+"!!F. chain(F) ==> tord(range(F))";
+by (Safe_tac);
+by (rtac nat_less_cases 1);
+by (ALLGOALS (fast_tac (claset() addIs [refl_less, chain_mono RS mp])));
+qed "chain_tord";
+
(* ------------------------------------------------------------------------ *)
(* technical lemmas about lub and is_lub *)
@@ -106,57 +105,47 @@
(* access to some definition as inference rule *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "is_lubE" thy [is_lub]
- "S <<| x ==> S <| x & (! u. S <| u --> x << u)"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (atac 1)
- ]);
+val prems = goalw thy [is_lub]
+ "S <<| x ==> S <| x & (! u. S <| u --> x << u)";
+by (cut_facts_tac prems 1);
+by (atac 1);
+qed "is_lubE";
-qed_goalw "is_lubI" thy [is_lub]
- "S <| x & (! u. S <| u --> x << u) ==> S <<| x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (atac 1)
- ]);
+val prems = goalw thy [is_lub]
+ "S <| x & (! u. S <| u --> x << u) ==> S <<| x";
+by (cut_facts_tac prems 1);
+by (atac 1);
+qed "is_lubI";
-qed_goalw "chainE" thy [chain] "chain F ==> !i. F(i) << F(Suc(i))"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (atac 1)]);
+val prems = goalw thy [chain] "chain F ==> !i. F(i) << F(Suc(i))";
+by (cut_facts_tac prems 1);
+by (atac 1);
+qed "chainE";
-qed_goalw "chainI" thy [chain] "!i. F i << F(Suc i) ==> chain F"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (atac 1)]);
+val prems = goalw thy [chain] "!i. F i << F(Suc i) ==> chain F";
+by (cut_facts_tac prems 1);
+by (atac 1);
+qed "chainI";
(* ------------------------------------------------------------------------ *)
(* technical lemmas about (least) upper bounds of chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "ub_rangeE" thy [is_ub] "range S <| x ==> !i. S(i) << x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (rtac mp 1),
- (etac spec 1),
- (rtac rangeI 1)
- ]);
+val prems = goalw thy [is_ub] "range S <| x ==> !i. S(i) << x";
+by (cut_facts_tac prems 1);
+by (strip_tac 1);
+by (rtac mp 1);
+by (etac spec 1);
+by (rtac rangeI 1);
+qed "ub_rangeE";
-qed_goalw "ub_rangeI" thy [is_ub] "!i. S i << x ==> range S <| x"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (strip_tac 1),
- (etac rangeE 1),
- (hyp_subst_tac 1),
- (etac spec 1)
- ]);
+val prems = goalw thy [is_ub] "!i. S i << x ==> range S <| x";
+by (cut_facts_tac prems 1);
+by (strip_tac 1);
+by (etac rangeE 1);
+by (hyp_subst_tac 1);
+by (etac spec 1);
+qed "ub_rangeI";
bind_thm ("is_ub_lub", is_lubE RS conjunct1 RS ub_rangeE RS spec);
(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *)
@@ -168,38 +157,34 @@
(* results about finite chains *)
(* ------------------------------------------------------------------------ *)
-qed_goalw "lub_finch1" thy [max_in_chain_def]
- "[| chain C; max_in_chain i C|] ==> range C <<| C i"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac is_lubI 1),
- (rtac conjI 1),
- (rtac ub_rangeI 1),
- (rtac allI 1),
- (res_inst_tac [("m","i")] nat_less_cases 1),
- (rtac (antisym_less_inverse RS conjunct2) 1),
- (etac (disjI1 RS less_or_eq_imp_le RS rev_mp) 1),
- (etac spec 1),
- (rtac (antisym_less_inverse RS conjunct2) 1),
- (etac (disjI2 RS less_or_eq_imp_le RS rev_mp) 1),
- (etac spec 1),
- (etac (chain_mono RS mp) 1),
- (atac 1),
- (strip_tac 1),
- (etac (ub_rangeE RS spec) 1)
- ]);
+val prems = goalw thy [max_in_chain_def]
+ "[| chain C; max_in_chain i C|] ==> range C <<| C i";
+by (cut_facts_tac prems 1);
+by (rtac is_lubI 1);
+by (rtac conjI 1);
+by (rtac ub_rangeI 1);
+by (rtac allI 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 RS mp) 1);
+by (atac 1);
+by (strip_tac 1);
+by (etac (ub_rangeE RS spec) 1);
+qed "lub_finch1";
-qed_goalw "lub_finch2" thy [finite_chain_def]
- "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)"
- (fn prems=>
- [
- (cut_facts_tac prems 1),
- (rtac lub_finch1 1),
- (etac conjunct1 1),
- (rtac (select_eq_Ex RS iffD2) 1),
- (etac conjunct2 1)
- ]);
+val prems= goalw thy [finite_chain_def]
+ "finite_chain(C) ==> range(C) <<| C(@ i. max_in_chain i C)";
+by (cut_facts_tac prems 1);
+by (rtac lub_finch1 1);
+by (etac conjunct1 1);
+by (rtac (select_eq_Ex RS iffD2) 1);
+by (etac conjunct2 1);
+qed "lub_finch2";
Goal "x<<y ==> chain (%i. if i=0 then x else y)";
@@ -210,16 +195,14 @@
by (Asm_simp_tac 1);
qed "bin_chain";
-qed_goalw "bin_chainmax" thy [max_in_chain_def,le_def]
- "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)"
-(fn prems =>
- [
- (cut_facts_tac prems 1),
- (rtac allI 1),
- (induct_tac "j" 1),
- (Asm_simp_tac 1),
- (Asm_simp_tac 1)
- ]);
+val prems = goalw thy [max_in_chain_def,le_def]
+ "x<<y ==> max_in_chain (Suc 0) (%i. if (i=0) then x else y)";
+by (cut_facts_tac prems 1);
+by (rtac allI 1);
+by (induct_tac "j" 1);
+by (Asm_simp_tac 1);
+by (Asm_simp_tac 1);
+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