added parentheses made necessary by change of constrain's precedence
authorclasohm
Wed Jun 29 12:03:41 1994 +0200 (1994-06-29)
changeset 44213ac1fd0a14d
parent 441 2b97bd6415b7
child 443 10884e64c241
added parentheses made necessary by change of constrain's precedence
src/CCL/Fix.ML
src/HOLCF/Cfun2.thy
src/HOLCF/Cfun3.thy
src/HOLCF/Cprod2.thy
src/HOLCF/Cprod3.thy
src/HOLCF/Fix.ML
src/HOLCF/Fix.thy
src/HOLCF/Fun2.thy
src/HOLCF/Fun3.thy
src/HOLCF/Lift2.thy
src/HOLCF/Lift3.thy
src/HOLCF/Pcpo.ML
src/HOLCF/Pcpo.thy
src/HOLCF/Porder.ML
src/HOLCF/Porder0.thy
src/HOLCF/Sprod2.thy
src/HOLCF/Sprod3.thy
src/HOLCF/Ssum2.thy
src/HOLCF/Ssum3.thy
src/HOLCF/ex/Hoare.ML
src/LCF/LCF.ML
src/LCF/fix.ML
src/LCF/pair.ML
     1.1 --- a/src/CCL/Fix.ML	Wed Jun 29 12:01:17 1994 +0200
     1.2 +++ b/src/CCL/Fix.ML	Wed Jun 29 12:03:41 1994 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  by (fast_tac (set_cs addSIs ([inclI] @ (prems RL [inclD]))) 1);;
     1.5  val ball_INCL = result();
     1.6  
     1.7 -goal Fix.thy "INCL(%x.a(x) = b(x)::'a::prog)";
     1.8 +goal Fix.thy "INCL(%x.a(x) = (b(x)::'a::prog))";
     1.9  by (simp_tac (term_ss addsimps [eq_iff]) 1);
    1.10  by (REPEAT (resolve_tac [conj_INCL,po_INCL] 1));
    1.11  val eq_INCL = result();
     2.1 --- a/src/HOLCF/Cfun2.thy	Wed Jun 29 12:01:17 1994 +0200
     2.2 +++ b/src/HOLCF/Cfun2.thy	Wed Jun 29 12:03:41 1994 +0200
     2.3 @@ -19,7 +19,7 @@
     2.4  
     2.5  (* instance of << for type ['a -> 'b]  *)
     2.6  
     2.7 -inst_cfun_po	"(op <<)::['a->'b,'a->'b]=>bool = less_cfun"
     2.8 +inst_cfun_po	"((op <<)::['a->'b,'a->'b]=>bool) = less_cfun"
     2.9  
    2.10  (* definitions *)
    2.11  (* The least element in type 'a->'b *)
     3.1 --- a/src/HOLCF/Cfun3.thy	Wed Jun 29 12:01:17 1994 +0200
     3.2 +++ b/src/HOLCF/Cfun3.thy	Wed Jun 29 12:03:41 1994 +0200
     3.3 @@ -17,7 +17,7 @@
     3.4  
     3.5  rules 
     3.6  
     3.7 -inst_cfun_pcpo	"UU::'a->'b = UU_cfun"
     3.8 +inst_cfun_pcpo	"(UU::'a->'b) = UU_cfun"
     3.9  
    3.10  Istrictify_def	"Istrictify(f,x) == (@z.\
    3.11  \			  ( x=UU --> z = UU)\
     4.1 --- a/src/HOLCF/Cprod2.thy	Wed Jun 29 12:01:17 1994 +0200
     4.2 +++ b/src/HOLCF/Cprod2.thy	Wed Jun 29 12:03:41 1994 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4  
     4.5  (* instance of << for type ['a * 'b]  *)
     4.6  
     4.7 -inst_cprod_po	"(op <<)::['a * 'b,'a * 'b]=>bool = less_cprod"
     4.8 +inst_cprod_po	"((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod"
     4.9  
    4.10  end
    4.11  
     5.1 --- a/src/HOLCF/Cprod3.thy	Wed Jun 29 12:01:17 1994 +0200
     5.2 +++ b/src/HOLCF/Cprod3.thy	Wed Jun 29 12:03:41 1994 +0200
     5.3 @@ -22,7 +22,7 @@
     5.4  
     5.5  rules 
     5.6  
     5.7 -inst_cprod_pcpo	"UU::'a*'b = <UU,UU>"
     5.8 +inst_cprod_pcpo	"(UU::'a*'b) = <UU,UU>"
     5.9  
    5.10  cpair_def	"cpair  == (LAM x y.<x,y>)"
    5.11  cfst_def	"cfst   == (LAM p.fst(p))"
     6.1 --- a/src/HOLCF/Fix.ML	Wed Jun 29 12:01:17 1994 +0200
     6.2 +++ b/src/HOLCF/Fix.ML	Wed Jun 29 12:03:41 1994 +0200
     6.3 @@ -1138,17 +1138,17 @@
     6.4  (* ------------------------------------------------------------------------- *)
     6.5  
     6.6  val flat_codom = prove_goalw Fix.thy [flat_def]
     6.7 -"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
     6.8 +"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
     6.9   (fn prems =>
    6.10  	[
    6.11  	(cut_facts_tac prems 1),
    6.12 -	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
    6.13 +	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
    6.14  	(rtac disjI1 1),
    6.15  	(rtac UU_I 1),
    6.16  	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
    6.17  	(atac 1),
    6.18  	(rtac (minimal RS monofun_cfun_arg) 1),
    6.19 -	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
    6.20 +	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
    6.21  	(etac disjI1 1),
    6.22  	(rtac disjI2 1),
    6.23  	(rtac allI 1),
     7.1 --- a/src/HOLCF/Fix.thy	Wed Jun 29 12:01:17 1994 +0200
     7.2 +++ b/src/HOLCF/Fix.thy	Wed Jun 29 12:03:41 1994 +0200
     7.3 @@ -36,7 +36,7 @@
     7.4  \                        !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))"
     7.5  
     7.6  flat_def          "flat(x::'a) ==\
     7.7 -\                        ! x y. x::'a << y --> (x = UU) | (x=y)"
     7.8 +\                        ! x y. (x::'a) << y --> (x = UU) | (x=y)"
     7.9  
    7.10  end
    7.11  
     8.1 --- a/src/HOLCF/Fun2.thy	Wed Jun 29 12:01:17 1994 +0200
     8.2 +++ b/src/HOLCF/Fun2.thy	Wed Jun 29 12:03:41 1994 +0200
     8.3 @@ -22,7 +22,7 @@
     8.4  
     8.5  (* instance of << for type ['a::term => 'b::po]  *)
     8.6  
     8.7 -inst_fun_po	"(op <<)::['a=>'b::po,'a=>'b::po ]=>bool = less_fun"
     8.8 +inst_fun_po	"((op <<)::['a=>'b::po,'a=>'b::po ]=>bool) = less_fun"
     8.9  
    8.10  (* definitions *)
    8.11  (* The least element in type 'a::term => 'b::pcpo *)
     9.1 --- a/src/HOLCF/Fun3.thy	Wed Jun 29 12:01:17 1994 +0200
     9.2 +++ b/src/HOLCF/Fun3.thy	Wed Jun 29 12:03:41 1994 +0200
     9.3 @@ -15,7 +15,7 @@
     9.4  
     9.5  rules 
     9.6  
     9.7 -inst_fun_pcpo	"UU::'a=>'b::pcpo = UU_fun"
     9.8 +inst_fun_pcpo	"(UU::'a=>'b::pcpo) = UU_fun"
     9.9  
    9.10  end
    9.11  
    10.1 --- a/src/HOLCF/Lift2.thy	Wed Jun 29 12:01:17 1994 +0200
    10.2 +++ b/src/HOLCF/Lift2.thy	Wed Jun 29 12:03:41 1994 +0200
    10.3 @@ -17,7 +17,7 @@
    10.4  
    10.5  (* instance of << for type ('a)u  *)
    10.6  
    10.7 -inst_lift_po	"(op <<)::[('a)u,('a)u]=>bool = less_lift"
    10.8 +inst_lift_po	"((op <<)::[('a)u,('a)u]=>bool) = less_lift"
    10.9  
   10.10  end
   10.11  
    11.1 --- a/src/HOLCF/Lift3.thy	Wed Jun 29 12:01:17 1994 +0200
    11.2 +++ b/src/HOLCF/Lift3.thy	Wed Jun 29 12:03:41 1994 +0200
    11.3 @@ -18,7 +18,7 @@
    11.4  
    11.5  rules 
    11.6  
    11.7 -inst_lift_pcpo	"UU::('a)u = UU_lift"
    11.8 +inst_lift_pcpo	"(UU::('a)u) = UU_lift"
    11.9  
   11.10  up_def		"up     == (LAM x.Iup(x))"
   11.11  lift_def	"lift   == (LAM f p.Ilift(f)(p))"
    12.1 --- a/src/HOLCF/Pcpo.ML	Wed Jun 29 12:01:17 1994 +0200
    12.2 +++ b/src/HOLCF/Pcpo.ML	Wed Jun 29 12:03:41 1994 +0200
    12.3 @@ -13,7 +13,7 @@
    12.4  (* ------------------------------------------------------------------------ *)
    12.5  
    12.6  val thelubE = prove_goal  Pcpo.thy 
    12.7 -	"[| is_chain(S);lub(range(S)) = l::'a::pcpo|] ==> range(S) <<| l "
    12.8 +	"[| is_chain(S);lub(range(S)) = (l::'a::pcpo)|] ==> range(S) <<| l "
    12.9  (fn prems =>
   12.10  	[
   12.11  	(cut_facts_tac prems 1), 
   12.12 @@ -256,7 +256,7 @@
   12.13  (* uniqueness in void                                                       *)
   12.14  (* ------------------------------------------------------------------------ *)
   12.15  
   12.16 -val unique_void2 = prove_goal Pcpo.thy "x::void=UU"
   12.17 +val unique_void2 = prove_goal Pcpo.thy "(x::void)=UU"
   12.18   (fn prems =>
   12.19  	[
   12.20  	(rtac (inst_void_pcpo RS ssubst) 1),
    13.1 --- a/src/HOLCF/Pcpo.thy	Wed Jun 29 12:01:17 1994 +0200
    13.2 +++ b/src/HOLCF/Pcpo.thy	Wed Jun 29 12:03:41 1994 +0200
    13.3 @@ -28,12 +28,12 @@
    13.4  
    13.5  minimal		"UU << x"			(* witness is minimal_void *)
    13.6  
    13.7 -cpo		"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
    13.8 +cpo		"is_chain(S) ==> ? x. range(S) <<| (x::('a::pcpo))" 
    13.9  						(* witness is cpo_void     *)
   13.10  						(* needs explicit type     *)
   13.11  
   13.12  (* instance of UU for the prototype void *)
   13.13  
   13.14 -inst_void_pcpo	"UU::void = UU_void"
   13.15 +inst_void_pcpo	"(UU::void) = UU_void"
   13.16  
   13.17  end 
    14.1 --- a/src/HOLCF/Porder.ML	Wed Jun 29 12:01:17 1994 +0200
    14.2 +++ b/src/HOLCF/Porder.ML	Wed Jun 29 12:03:41 1994 +0200
    14.3 @@ -77,7 +77,7 @@
    14.4  (* ------------------------------------------------------------------------ *)
    14.5  
    14.6  val nat_less_cases = prove_goal Porder.thy 
    14.7 -	"[| m::nat < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
    14.8 +	"[| (m::nat) < n ==> P(n,m); m=n ==> P(n,m);n < m ==> P(n,m)|]==>P(n,m)"
    14.9  ( fn prems =>
   14.10  	[
   14.11  	(res_inst_tac [("m1","n"),("n1","m")] (less_linear RS disjE) 1),
   14.12 @@ -236,7 +236,7 @@
   14.13  (* a technical argument about << on void                                    *)
   14.14  (* ------------------------------------------------------------------------ *)
   14.15  
   14.16 -val less_void = prove_goal Porder.thy "(u1::void << u2) = (u1 = u2)"
   14.17 +val less_void = prove_goal Porder.thy "((u1::void) << u2) = (u1 = u2)"
   14.18  (fn prems =>
   14.19  	[
   14.20  	(rtac (inst_void_po RS ssubst) 1),
   14.21 @@ -289,7 +289,7 @@
   14.22  (* ------------------------------------------------------------------------ *)
   14.23  
   14.24  val cpo_void = prove_goal Porder.thy
   14.25 -	"is_chain(S::nat=>void) ==> ? x. range(S) <<| x "
   14.26 +	"is_chain((S::nat=>void)) ==> ? x. range(S) <<| x "
   14.27  (fn prems =>
   14.28  	[
   14.29  	(cut_facts_tac prems 1),
    15.1 --- a/src/HOLCF/Porder0.thy	Wed Jun 29 12:01:17 1994 +0200
    15.2 +++ b/src/HOLCF/Porder0.thy	Wed Jun 29 12:03:41 1994 +0200
    15.3 @@ -37,6 +37,6 @@
    15.4  
    15.5  (* instance of << for the prototype void *)
    15.6  
    15.7 -inst_void_po	"(op <<)::[void,void]=>bool = less_void"
    15.8 +inst_void_po	"((op <<)::[void,void]=>bool) = less_void"
    15.9  
   15.10  end 
    16.1 --- a/src/HOLCF/Sprod2.thy	Wed Jun 29 12:01:17 1994 +0200
    16.2 +++ b/src/HOLCF/Sprod2.thy	Wed Jun 29 12:03:41 1994 +0200
    16.3 @@ -16,7 +16,7 @@
    16.4  
    16.5  (* instance of << for type ['a ** 'b]  *)
    16.6  
    16.7 -inst_sprod_po	"(op <<)::['a ** 'b,'a ** 'b]=>bool = less_sprod"
    16.8 +inst_sprod_po	"((op <<)::['a ** 'b,'a ** 'b]=>bool) = less_sprod"
    16.9  
   16.10  end
   16.11  
    17.1 --- a/src/HOLCF/Sprod3.thy	Wed Jun 29 12:01:17 1994 +0200
    17.2 +++ b/src/HOLCF/Sprod3.thy	Wed Jun 29 12:03:41 1994 +0200
    17.3 @@ -20,7 +20,7 @@
    17.4  
    17.5  rules 
    17.6  
    17.7 -inst_sprod_pcpo	"UU::'a**'b = Ispair(UU,UU)"
    17.8 +inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
    17.9  spair_def	"spair  == (LAM x y.Ispair(x,y))"
   17.10  sfst_def	"sfst   == (LAM p.Isfst(p))"
   17.11  ssnd_def	"ssnd   == (LAM p.Issnd(p))"	
    18.1 --- a/src/HOLCF/Ssum2.thy	Wed Jun 29 12:01:17 1994 +0200
    18.2 +++ b/src/HOLCF/Ssum2.thy	Wed Jun 29 12:03:41 1994 +0200
    18.3 @@ -15,7 +15,7 @@
    18.4  
    18.5  (* instance of << for type ['a ++ 'b]  *)
    18.6  
    18.7 -inst_ssum_po	"(op <<)::['a ++ 'b,'a ++ 'b]=>bool = less_ssum"
    18.8 +inst_ssum_po	"((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum"
    18.9  
   18.10  end
   18.11  
    19.1 --- a/src/HOLCF/Ssum3.thy	Wed Jun 29 12:01:17 1994 +0200
    19.2 +++ b/src/HOLCF/Ssum3.thy	Wed Jun 29 12:03:41 1994 +0200
    19.3 @@ -17,7 +17,7 @@
    19.4  
    19.5  rules 
    19.6  
    19.7 -inst_ssum_pcpo	"UU::'a++'b = Isinl(UU)"
    19.8 +inst_ssum_pcpo	"(UU::'a++'b) = Isinl(UU)"
    19.9  
   19.10  sinl_def	"sinl   == (LAM x.Isinl(x))"
   19.11  sinr_def	"sinr   == (LAM x.Isinr(x))"
    20.1 --- a/src/HOLCF/ex/Hoare.ML	Wed Jun 29 12:01:17 1994 +0200
    20.2 +++ b/src/HOLCF/ex/Hoare.ML	Wed Jun 29 12:03:41 1994 +0200
    20.3 @@ -90,7 +90,7 @@
    20.4  	]);
    20.5  
    20.6  val hoare_lemma28 = prove_goal HOLCF.thy 
    20.7 -"b1[y::'a]=UU::tr ==> b1[UU] = UU"
    20.8 +"b1[y::'a]=(UU::tr) ==> b1[UU] = UU"
    20.9   (fn prems =>
   20.10  	[
   20.11  	(cut_facts_tac prems 1),
    21.1 --- a/src/LCF/LCF.ML	Wed Jun 29 12:01:17 1994 +0200
    21.2 +++ b/src/LCF/LCF.ML	Wed Jun 29 12:03:41 1994 +0200
    21.3 @@ -65,7 +65,7 @@
    21.4  		      REPEAT(rstac(conjI::prems)1)]);
    21.5  
    21.6  val ext = prove_goal thy
    21.7 -	"(!!x::'a::cpo. f(x)=g(x)::'b::cpo) ==> (%x.f(x))=(%x.g(x))"
    21.8 +	"(!!x::'a::cpo. f(x)=(g(x)::'b::cpo)) ==> (%x.f(x))=(%x.g(x))"
    21.9  	(fn [prem] => [REPEAT(rstac[less_anti_sym, less_ext, allI,
   21.10  				    prem RS eq_imp_less1,
   21.11  				    prem RS eq_imp_less2]1)]);
    22.1 --- a/src/LCF/fix.ML	Wed Jun 29 12:01:17 1994 +0200
    22.2 +++ b/src/LCF/fix.ML	Wed Jun 29 12:03:41 1994 +0200
    22.3 @@ -14,7 +14,7 @@
    22.4  structure Fix:FIX =
    22.5  struct
    22.6  
    22.7 -val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=u(x)::'a::cpo)"
    22.8 +val adm_eq = prove_goal LCF.thy "adm(%x.t(x)=(u(x)::'a::cpo))"
    22.9  	(fn _ => [rewrite_goals_tac [eq_def],
   22.10  		  REPEAT(rstac[adm_conj,adm_less]1)]);
   22.11  
    23.1 --- a/src/LCF/pair.ML	Wed Jun 29 12:01:17 1994 +0200
    23.2 +++ b/src/LCF/pair.ML	Wed Jun 29 12:03:41 1994 +0200
    23.3 @@ -8,7 +8,7 @@
    23.4  val qpair = read_instantiate [("z","q::'a*'b")] surj_pairing;
    23.5  in
    23.6  val PROD_less = prove_goal LCF.thy
    23.7 -	"p::'a*'b << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
    23.8 +	"(p::'a*'b) << q <-> FST(p) << FST(q) & SND(p) << SND(q)"
    23.9  	(fn _ => [EVERY1[rtac iffI,
   23.10  		  rtac conjI, etac less_ap_term, etac less_ap_term,
   23.11  		  rtac (ppair RS subst), rtac (qpair RS subst),