--- a/src/HOL/MicroJava/BV/Product.thy Sat Mar 02 12:09:23 2002 +0100
+++ b/src/HOL/MicroJava/BV/Product.thy Sun Mar 03 16:59:08 2002 +0100
@@ -11,16 +11,16 @@
theory Product = Err:
constdefs
- le :: "'a ord => 'b ord => ('a * 'b) ord"
+ le :: "'a ord \<Rightarrow> 'b ord \<Rightarrow> ('a * 'b) ord"
"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
- sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
+ sup :: "'a ebinop \<Rightarrow> 'b ebinop \<Rightarrow> ('a * 'b)ebinop"
"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
- esl :: "'a esl => 'b esl => ('a * 'b ) esl"
+ esl :: "'a esl \<Rightarrow> 'b esl \<Rightarrow> ('a * 'b ) esl"
"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
-syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
+syntax "@lesubprod" :: "'a*'b \<Rightarrow> 'a ord \<Rightarrow> 'b ord \<Rightarrow> 'b \<Rightarrow> bool"
("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
@@ -49,7 +49,7 @@
lemma acc_le_prodI [intro!]:
- "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
+ "\<lbrakk> acc rA; acc rB \<rbrakk> \<Longrightarrow> acc(Product.le rA rB)"
apply (unfold acc_def)
apply (rule wf_subset)
apply (erule wf_lex_prod)
@@ -59,7 +59,7 @@
lemma closed_lift2_sup:
- "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==>
+ "\<lbrakk> closed (err A) (lift2 f); closed (err B) (lift2 g) \<rbrakk> \<Longrightarrow>
closed (err(A<*>B)) (lift2(sup f g))";
apply (unfold closed_def plussub_def lift2_def err_def sup_def)
apply (simp split: err.split)
@@ -72,12 +72,12 @@
lemma plus_eq_Err_conv [simp]:
- "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |]
- ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
+ "\<lbrakk> x:A; y:A; semilat(err A, Err.le r, lift2 f) \<rbrakk>
+ \<Longrightarrow> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
proof -
have plus_le_conv2:
- "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
- OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
+ "\<And>r f z. \<lbrakk> z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
+ OK x +_f OK y <=_r z\<rbrakk> \<Longrightarrow> OK x <=_r z \<and> OK y <=_r z"
by (rule plus_le_conv [THEN iffD1])
case rule_context
thus ?thesis
@@ -110,7 +110,7 @@
qed
lemma err_semilat_Product_esl:
- "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
+ "\<And>L1 L2. \<lbrakk> err_semilat L1; err_semilat L2 \<rbrakk> \<Longrightarrow> err_semilat(Product.esl L1 L2)"
apply (unfold esl_def Err.sl_def)
apply (simp (no_asm_simp) only: split_tupled_all)
apply simp