src/HOLCF/Sprod2.ML
changeset 892 d0dc8d057929
parent 243 c22b85994e17
child 1168 74be52691d62
     1.1 --- a/src/HOLCF/Sprod2.ML	Fri Feb 03 12:32:14 1995 +0100
     1.2 +++ b/src/HOLCF/Sprod2.ML	Tue Feb 07 11:59:32 1995 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  (* access to less_sprod in class po                                         *)
     1.5  (* ------------------------------------------------------------------------ *)
     1.6  
     1.7 -val less_sprod3a = prove_goal Sprod2.thy 
     1.8 +qed_goal "less_sprod3a" Sprod2.thy 
     1.9  	"p1=Ispair(UU,UU) ==> p1 << p2"
    1.10  (fn prems =>
    1.11  	[
    1.12 @@ -23,7 +23,7 @@
    1.13  	]);
    1.14  
    1.15  
    1.16 -val less_sprod3b = prove_goal Sprod2.thy
    1.17 +qed_goal "less_sprod3b" Sprod2.thy
    1.18   "~p1=Ispair(UU,UU) ==>\
    1.19  \	(p1<<p2) = (Isfst(p1)<<Isfst(p2) & Issnd(p1)<<Issnd(p2))" 
    1.20  (fn prems =>
    1.21 @@ -33,7 +33,7 @@
    1.22  	(etac less_sprod1b 1)
    1.23  	]);
    1.24  
    1.25 -val less_sprod4b = prove_goal Sprod2.thy 
    1.26 +qed_goal "less_sprod4b" Sprod2.thy 
    1.27  	"p << Ispair(UU,UU) ==> p = Ispair(UU,UU)"
    1.28  (fn prems =>
    1.29  	[
    1.30 @@ -45,7 +45,7 @@
    1.31  val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
    1.32  (* Ispair(?a,?b) << Ispair(UU,UU) ==> ?a = UU | ?b = UU *)
    1.33  
    1.34 -val less_sprod4c = prove_goal Sprod2.thy
    1.35 +qed_goal "less_sprod4c" Sprod2.thy
    1.36   "[|Ispair(xa,ya)<<Ispair(x,y);~xa=UU;~ya=UU;~x=UU;~y=UU|] ==>\
    1.37  \		xa<<x & ya << y"
    1.38  (fn prems =>
    1.39 @@ -60,7 +60,7 @@
    1.40  (* type sprod is pointed                                                    *)
    1.41  (* ------------------------------------------------------------------------ *)
    1.42  
    1.43 -val minimal_sprod = prove_goal Sprod2.thy  "Ispair(UU,UU)<<p"
    1.44 +qed_goal "minimal_sprod" Sprod2.thy  "Ispair(UU,UU)<<p"
    1.45  (fn prems =>
    1.46  	[
    1.47  	(rtac less_sprod3a 1),
    1.48 @@ -71,7 +71,7 @@
    1.49  (* Ispair is monotone in both arguments                                     *)
    1.50  (* ------------------------------------------------------------------------ *)
    1.51  
    1.52 -val monofun_Ispair1 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair)"
    1.53 +qed_goalw "monofun_Ispair1" Sprod2.thy [monofun] "monofun(Ispair)"
    1.54  (fn prems =>
    1.55  	[
    1.56  	(strip_tac 1),
    1.57 @@ -111,7 +111,7 @@
    1.58  	]);
    1.59  
    1.60  
    1.61 -val monofun_Ispair2 = prove_goalw Sprod2.thy [monofun] "monofun(Ispair(x))"
    1.62 +qed_goalw "monofun_Ispair2" Sprod2.thy [monofun] "monofun(Ispair(x))"
    1.63  (fn prems =>
    1.64  	[
    1.65  	(strip_tac 1),
    1.66 @@ -148,7 +148,7 @@
    1.67  	(etac (strict_Ispair_rev RS  conjunct2) 1)
    1.68  	]);
    1.69  
    1.70 -val  monofun_Ispair = prove_goal Sprod2.thy 
    1.71 +qed_goal " monofun_Ispair" Sprod2.thy 
    1.72   "[|x1<<x2; y1<<y2|] ==> Ispair(x1,y1)<<Ispair(x2,y2)"
    1.73  (fn prems =>
    1.74  	[
    1.75 @@ -166,7 +166,7 @@
    1.76  (* Isfst and Issnd are monotone                                             *)
    1.77  (* ------------------------------------------------------------------------ *)
    1.78  
    1.79 -val  monofun_Isfst = prove_goalw Sprod2.thy [monofun] "monofun(Isfst)"
    1.80 +qed_goalw " monofun_Isfst" Sprod2.thy [monofun] "monofun(Isfst)"
    1.81  (fn prems =>
    1.82  	[
    1.83  	(strip_tac 1),
    1.84 @@ -193,7 +193,7 @@
    1.85  	(REPEAT (atac 1))
    1.86  	]);
    1.87  
    1.88 -val monofun_Issnd = prove_goalw Sprod2.thy [monofun] "monofun(Issnd)"
    1.89 +qed_goalw "monofun_Issnd" Sprod2.thy [monofun] "monofun(Issnd)"
    1.90  (fn prems =>
    1.91  	[
    1.92  	(strip_tac 1),
    1.93 @@ -225,7 +225,7 @@
    1.94  (* the type 'a ** 'b is a cpo                                               *)
    1.95  (* ------------------------------------------------------------------------ *)
    1.96  
    1.97 -val lub_sprod = prove_goal Sprod2.thy 
    1.98 +qed_goal "lub_sprod" Sprod2.thy 
    1.99  "[|is_chain(S)|] ==> range(S) <<| \
   1.100  \ Ispair(lub(range(%i.Isfst(S(i)))),lub(range(%i.Issnd(S(i)))))"
   1.101  (fn prems =>
   1.102 @@ -256,7 +256,7 @@
   1.103  (* is_chain(?S1) ==> lub(range(?S1)) =                                     *)
   1.104  (* Ispair(lub(range(%i. Isfst(?S1(i)))),lub(range(%i. Issnd(?S1(i)))))     *)
   1.105  
   1.106 -val cpo_sprod = prove_goal Sprod2.thy 
   1.107 +qed_goal "cpo_sprod" Sprod2.thy 
   1.108  	"is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
   1.109  (fn prems =>
   1.110  	[