diff -r 3533e3e9267f -r 1024a2d80ac0 src/HOL/MicroJava/BV/Convert.thy
--- a/src/HOL/MicroJava/BV/Convert.thy	Wed Aug 30 21:44:12 2000 +0200
+++ b/src/HOL/MicroJava/BV/Convert.thy	Wed Aug 30 21:47:39 2000 +0200
@@ -1,63 +1,106 @@
 (*  Title:      HOL/MicroJava/BV/Convert.thy
     ID:         $Id$
-    Author:     Cornelia Pusch
+    Author:     Cornelia Pusch and Gerwin Klein
     Copyright   1999 Technische Universitaet Muenchen
+*)
 
-The supertype relation lifted to type options, type lists and state types.
-*)
+header "Lifted Type Relations"
 
 theory Convert = JVMExec:
 
+text "The supertype relation lifted to type err, type lists and state types."
+
+datatype 'a err = Err | Ok 'a
+
 types
- locvars_type = "ty option list"
+ locvars_type = "ty err list"
  opstack_type = "ty list"
  state_type   = "opstack_type \<times> locvars_type"
 
-constdefs
+
+consts
+  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
+primrec
+  "strict f Err    = Err"
+  "strict f (Ok x) = f x"
+
+consts
+  opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
+primrec
+  "opt_map f None     = None"
+  "opt_map f (Some x) = Some (f x)"
+
+consts
+  val :: "'a err \<Rightarrow> 'a"
+primrec
+  "val (Ok s) = s"
 
-  (* lifts a relation to option with None as top element *)
-  lift_top :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'a option \<Rightarrow> bool)"
+  
+constdefs
+  (* lifts a relation to err with Err as top element *)
+  lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
   "lift_top P a' a \<equiv> case a of 
-                       None   \<Rightarrow> True
-                     | Some t \<Rightarrow> (case a' of None \<Rightarrow> False | Some t' \<Rightarrow> P t' t)"
+                       Err  \<Rightarrow> True
+                     | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
+
+  (* lifts a relation to option with None as bottom element *)
+  lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
+  "lift_bottom P a' a \<equiv> case a' of 
+                          None    \<Rightarrow> True 
+                        | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
+
+  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
+  "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+
+  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
+             ("_ \<turnstile> _ <=l _"  [71,71] 70)
+  "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
+
+  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
+               ("_ \<turnstile> _ <=s _"  [71,71] 70)
+  "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+
+  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
+                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
+  "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
 
 
- sup_ty_opt :: "['code prog,ty option,ty option] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
- "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
+lemma not_Err_eq [iff]:
+  "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
+  by (cases x) auto
 
- sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool"	  ("_ \<turnstile> _ <=l _"  [71,71] 70)
- "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
-
- sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  ("_ \<turnstile> _ <=s _"  [71,71] 70)
- "G \<turnstile> s <=s s' \<equiv> (G \<turnstile> map Some (fst s) <=l map Some (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
+lemma not_Some_eq [iff]:
+  "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
+  by (cases x) auto  
 
 
 lemma lift_top_refl [simp]:
   "[| !!x. P x x |] ==> lift_top P x x"
-  by (simp add: lift_top_def split: option.splits)
+  by (simp add: lift_top_def split: err.splits)
 
 lemma lift_top_trans [trans]:
-  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] ==> lift_top P x z"
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
+  ==> lift_top P x z"
 proof -
   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
   assume a: "lift_top P x y"
   assume b: "lift_top P y z"
 
-  { assume "z = None" 
+  { assume "z = Err" 
     hence ?thesis by (simp add: lift_top_def)
   } note z_none = this
 
-  { assume "x = None"
+  { assume "x = Err"
     with a b
     have ?thesis
-      by (simp add: lift_top_def split: option.splits)
+      by (simp add: lift_top_def split: err.splits)
   } note x_none = this
   
   { fix r t
-    assume x: "x = Some r" and z: "z = Some t"    
+    assume x: "x = Ok r" and z: "z = Ok t"    
     with a b
-    obtain s where y: "y = Some s" 
-      by (simp add: lift_top_def split: option.splits)
+    obtain s where y: "y = Ok s" 
+      by (simp add: lift_top_def split: err.splits)
     
     from a x y
     have "P r s" by (simp add: lift_top_def)
@@ -75,21 +118,82 @@
   show ?thesis by blast
 qed
 
-lemma lift_top_None_any [simp]:
-  "lift_top P None any = (any = None)"
-  by (simp add: lift_top_def split: option.splits)
+lemma lift_top_Err_any [simp]:
+  "lift_top P Err any = (any = Err)"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_Ok_Ok [simp]:
+  "lift_top P (Ok a) (Ok b) = P a b"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_any_Ok [simp]:
+  "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
+  by (simp add: lift_top_def split: err.splits)
+
+lemma lift_top_Ok_any:
+  "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
+  by (simp add: lift_top_def split: err.splits)
 
-lemma lift_top_Some_Some [simp]:
-  "lift_top P (Some a) (Some b) = P a b"
-  by (simp add: lift_top_def split: option.splits)
+
+lemma lift_bottom_refl [simp]:
+  "[| !!x. P x x |] ==> lift_bottom P x x"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_trans [trans]:
+  "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
+  ==> lift_bottom P x z"
+proof -
+  assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
+  assume a: "lift_bottom P x y"
+  assume b: "lift_bottom P y z"
+
+  { assume "x = None" 
+    hence ?thesis by (simp add: lift_bottom_def)
+  } note z_none = this
 
-lemma lift_top_any_Some [simp]:
-  "lift_top P any (Some b) = (\<exists>a. any = Some a \<and> P a b)"
-  by (simp add: lift_top_def split: option.splits)
+  { assume "z = None"
+    with a b
+    have ?thesis
+      by (simp add: lift_bottom_def split: option.splits)
+  } note x_none = this
+  
+  { fix r t
+    assume x: "x = Some r" and z: "z = Some t"    
+    with a b
+    obtain s where y: "y = Some s" 
+      by (simp add: lift_bottom_def split: option.splits)
+    
+    from a x y
+    have "P r s" by (simp add: lift_bottom_def)
+    also
+    from b y z
+    have "P s t" by (simp add: lift_bottom_def)
+    finally 
+    have "P r t" .
 
-lemma lift_top_Some_any:
-  "lift_top P (Some a) any = (any = None \<or> (\<exists>b. any = Some b \<and> P a b))"
-  by (simp add: lift_top_def split: option.splits)
+    with x z
+    have ?thesis by (simp add: lift_bottom_def)
+  } 
+
+  with x_none z_none
+  show ?thesis by blast
+qed
+
+lemma lift_bottom_any_None [simp]:
+  "lift_bottom P any None = (any = None)"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_Some_Some [simp]:
+  "lift_bottom P (Some a) (Some b) = P a b"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_any_Some [simp]:
+  "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)"
+  by (simp add: lift_bottom_def split: option.splits)
+
+lemma lift_bottom_Some_any:
+  "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))"
+  by (simp add: lift_bottom_def split: option.splits)
 
 
 
@@ -105,18 +209,21 @@
   "G \<turnstile> s <=s s"
   by (simp add: sup_state_def)
 
+theorem sup_state_opt_refl [simp]:
+  "G \<turnstile> s <=' s"
+  by (simp add: sup_state_opt_def)
 
 
-theorem anyConvNone [simp]:
-  "(G \<turnstile> None <=o any) = (any = None)"
+theorem anyConvErr [simp]:
+  "(G \<turnstile> Err <=o any) = (any = Err)"
   by (simp add: sup_ty_opt_def)
 
-theorem SomeanyConvSome [simp]:
-  "(G \<turnstile> (Some ty') <=o (Some ty)) = (G \<turnstile> ty' \<preceq> ty)"
+theorem OkanyConvOk [simp]:
+  "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
   by (simp add: sup_ty_opt_def)
 
-theorem sup_ty_opt_Some:
-  "G \<turnstile> a <=o (Some b) \<Longrightarrow> \<exists> x. a = Some x"
+theorem sup_ty_opt_Ok:
+  "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
   by (clarsimp simp add: sup_ty_opt_def)
 
 lemma widen_PrimT_conv1 [simp]:
@@ -124,8 +231,8 @@
   by (auto elim: widen.elims)
 
 theorem sup_PTS_eq:
-  "(G \<turnstile> Some (PrimT p) <=o X) = (X=None \<or> X = Some (PrimT p))"
-  by (auto simp add: sup_ty_opt_def lift_top_Some_any)
+  "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
+  by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
 
 
 
@@ -138,7 +245,7 @@
   by (simp add: sup_loc_def list_all2_Cons1)
 
 theorem sup_loc_Cons2:
-  "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))";
+  "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
   by (simp add: sup_loc_def list_all2_Cons2)
 
 
@@ -178,8 +285,8 @@
 
 
 theorem all_nth_sup_loc:
-  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> (G \<turnstile> a <=l b)"
-  (is "?P a")
+  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
+       (G \<turnstile> a <=l b)" (is "?P a")
 proof (induct a)
   show "?P []" by simp
 
@@ -206,12 +313,13 @@
 
 
 theorem sup_loc_append:
-  "[| length a = length b |] ==> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
+  "length a = length b ==> 
+   (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
 proof -
   assume l: "length a = length b"
 
-  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
-    (is "?P a") 
+  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
+            (G \<turnstile> x <=l y))" (is "?P a") 
   proof (induct a)
     show "?P []" by simp
     
@@ -219,7 +327,7 @@
     show "?P (l#ls)" 
     proof (intro strip)
       fix b
-      assume "length (l#ls) = length (b::ty option list)"
+      assume "length (l#ls) = length (b::ty err list)"
       with IH
       show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
         by - (cases b, auto)
@@ -276,8 +384,8 @@
 
 
 theorem sup_loc_update [rulify]:
-  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> (G \<turnstile> x[n := a] <=l y[n := b])"
-  (is "?P x")
+  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
+          (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
 proof (induct x)
   show "?P []" by simp
 
@@ -294,23 +402,28 @@
 
 
 theorem sup_state_length [simp]:
-  "G \<turnstile> s2 <=s s1 \<Longrightarrow> length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
+  "G \<turnstile> s2 <=s s1 ==> 
+   length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
   by (auto dest: sup_loc_length simp add: sup_state_def);
 
 theorem sup_state_append_snd:
-  "length a = length b \<Longrightarrow> (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
+  "length a = length b ==> 
+  (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
   by (auto simp add: sup_state_def sup_loc_append)
 
 theorem sup_state_append_fst:
-  "length a = length b \<Longrightarrow> (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
+  "length a = length b ==> 
+  (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
   by (auto simp add: sup_state_def sup_loc_append)
 
 theorem sup_state_Cons1:
-  "(G \<turnstile> (x#xt, a) <=s (yt, b)) = (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
+  "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
+   (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
   by (auto simp add: sup_state_def map_eq_Cons)
 
 theorem sup_state_Cons2:
-  "(G \<turnstile> (xt, a) <=s (y#yt, b)) = (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
+  "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
+   (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
   by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
 
 theorem sup_state_ignore_fst:  
@@ -324,11 +437,32 @@
   show ?thesis by (simp add: m sup_state_def)
 qed
   
+
+lemma sup_state_opt_None_any [iff]:
+  "(G \<turnstile> None <=' any) = True"
+  by (simp add: sup_state_opt_def lift_bottom_def)
+
+lemma sup_state_opt_any_None [iff]:
+  "(G \<turnstile> any <=' None) = (any = None)"
+  by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_Some [iff]:
+  "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
+  by (simp add: sup_state_opt_def del: split_paired_Ex)
+
+lemma sup_state_opt_any_Some [iff]:
+  "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
+  by (simp add: sup_state_opt_def)
+
+lemma sup_state_opt_Some_any:
+  "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
+  by (simp add: sup_state_opt_def lift_bottom_Some_any)
+
+
 theorem sup_ty_opt_trans [trans]:
   "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
 
-
 theorem sup_loc_trans [trans]:
   "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
 proof -
@@ -359,4 +493,9 @@
   "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   by (auto intro: sup_loc_trans simp add: sup_state_def)
 
+theorem sup_state_opt_trans [trans]:
+  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
+  by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
+
+
 end