src/HOL/MicroJava/BV/Convert.thy
changeset 10042 7164dc0d24d8
parent 9941 fe05af7ec816
child 10056 9f84ffa4a8d0
     1.1 --- a/src/HOL/MicroJava/BV/Convert.thy	Wed Sep 20 21:20:41 2000 +0200
     1.2 +++ b/src/HOL/MicroJava/BV/Convert.thy	Thu Sep 21 10:42:49 2000 +0200
     1.3 @@ -19,51 +19,52 @@
     1.4  
     1.5  
     1.6  consts
     1.7 -  strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
     1.8 +  strict  :: "('a => 'b err) => ('a err => 'b err)"
     1.9  primrec
    1.10    "strict f Err    = Err"
    1.11    "strict f (Ok x) = f x"
    1.12  
    1.13 -consts
    1.14 -  opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
    1.15 -primrec
    1.16 -  "opt_map f None     = None"
    1.17 -  "opt_map f (Some x) = Some (f x)"
    1.18  
    1.19  consts
    1.20 -  val :: "'a err \<Rightarrow> 'a"
    1.21 +  val :: "'a err => 'a"
    1.22  primrec
    1.23    "val (Ok s) = s"
    1.24  
    1.25    
    1.26  constdefs
    1.27    (* lifts a relation to err with Err as top element *)
    1.28 -  lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
    1.29 -  "lift_top P a' a \<equiv> case a of 
    1.30 -                       Err  \<Rightarrow> True
    1.31 -                     | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
    1.32 +  lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)"
    1.33 +  "lift_top P a' a == case a of 
    1.34 +                       Err  => True
    1.35 +                     | Ok t => (case a' of Err => False | Ok t' => P t' t)"
    1.36  
    1.37    (* lifts a relation to option with None as bottom element *)
    1.38 -  lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
    1.39 -  "lift_bottom P a' a \<equiv> case a' of 
    1.40 -                          None    \<Rightarrow> True 
    1.41 -                        | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
    1.42 +  lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
    1.43 +  "lift_bottom P a' a == case a' of 
    1.44 +                          None    => True 
    1.45 +                        | Some t' => (case a of None => False | Some t => P t' t)"
    1.46  
    1.47 -  sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
    1.48 -  "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
    1.49 +  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ \<turnstile> _ <=o _" [71,71] 70)
    1.50 +  "sup_ty_opt G == lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
    1.51 +
    1.52 +  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" 
    1.53 +              ("_ \<turnstile> _ <=l _"  [71,71] 70)
    1.54 +  "G \<turnstile> LT <=l LT' == list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
    1.55  
    1.56 -  sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
    1.57 -             ("_ \<turnstile> _ <=l _"  [71,71] 70)
    1.58 -  "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
    1.59 -
    1.60 -  sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
    1.61 +  sup_state :: "['code prog,state_type,state_type] => bool"	  
    1.62                 ("_ \<turnstile> _ <=s _"  [71,71] 70)
    1.63 -  "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'"
    1.64 +  "G \<turnstile> s <=s s' == (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
    1.65 +
    1.66 +  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
    1.67 +                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
    1.68 +  "sup_state_opt G == lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
    1.69  
    1.70 -  sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
    1.71 -                   ("_ \<turnstile> _ <=' _"  [71,71] 70)
    1.72 -  "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
    1.73 -
    1.74 +syntax (HTML output) 
    1.75 +  sup_ty_opt :: "['code prog,ty err,ty err] => bool" ("_ |- _ <=o _")
    1.76 +  sup_loc :: "['code prog,locvars_type,locvars_type] => bool" ("_ |- _ <=l _"  [71,71] 70)
    1.77 +  sup_state :: "['code prog,state_type,state_type] => bool"	("_ |- _ <=s _"  [71,71] 70)
    1.78 +  sup_state_opt :: "['code prog,state_type option,state_type option] => bool" ("_ |- _ <=' _"  [71,71] 70)
    1.79 +                   
    1.80  
    1.81  lemma not_Err_eq [iff]:
    1.82    "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
    1.83 @@ -223,7 +224,7 @@
    1.84    by (simp add: sup_ty_opt_def)
    1.85  
    1.86  theorem sup_ty_opt_Ok:
    1.87 -  "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
    1.88 +  "G \<turnstile> a <=o (Ok b) ==> \<exists> x. a = Ok x"
    1.89    by (clarsimp simp add: sup_ty_opt_def)
    1.90  
    1.91  lemma widen_PrimT_conv1 [simp]:
    1.92 @@ -250,10 +251,10 @@
    1.93  
    1.94  
    1.95  theorem sup_loc_length:
    1.96 -  "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
    1.97 +  "G \<turnstile> a <=l b ==> length a = length b"
    1.98  proof -
    1.99    assume G: "G \<turnstile> a <=l b"
   1.100 -  have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
   1.101 +  have "\<forall> b. (G \<turnstile> a <=l b) --> length a = length b"
   1.102      by (induct a, auto)
   1.103    with G
   1.104    show ?thesis by blast
   1.105 @@ -263,7 +264,7 @@
   1.106    "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
   1.107  proof -
   1.108    assume a: "G \<turnstile> a <=l b" "n < length a"
   1.109 -  have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
   1.110 +  have "\<forall> n b. (G \<turnstile> a <=l b) --> n < length a --> (G \<turnstile> (a!n) <=o (b!n))"
   1.111      (is "?P a")
   1.112    proof (induct a)
   1.113      show "?P []" by simp
   1.114 @@ -285,7 +286,7 @@
   1.115  
   1.116  
   1.117  theorem all_nth_sup_loc:
   1.118 -  "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
   1.119 +  "\<forall>b. length a = length b --> (\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (b!n))) --> 
   1.120         (G \<turnstile> a <=l b)" (is "?P a")
   1.121  proof (induct a)
   1.122    show "?P []" by simp
   1.123 @@ -295,14 +296,14 @@
   1.124    show "?P (l#ls)"
   1.125    proof (intro strip)
   1.126      fix b
   1.127 -    assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
   1.128 +    assume f: "\<forall>n. n < length (l # ls) --> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
   1.129      assume l: "length (l#ls) = length b"
   1.130      
   1.131      then obtain b' bs where b: "b = b'#bs"
   1.132        by - (cases b, simp, simp add: neq_Nil_conv, rule that)
   1.133  
   1.134      with f
   1.135 -    have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
   1.136 +    have "\<forall>n. n < length ls --> (G \<turnstile> (ls!n) <=o (bs!n))"
   1.137        by auto
   1.138  
   1.139      with f b l IH
   1.140 @@ -318,7 +319,7 @@
   1.141  proof -
   1.142    assume l: "length a = length b"
   1.143  
   1.144 -  have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
   1.145 +  have "\<forall>b. length a = length b --> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
   1.146              (G \<turnstile> x <=l y))" (is "?P a") 
   1.147    proof (induct a)
   1.148      show "?P []" by simp
   1.149 @@ -384,7 +385,7 @@
   1.150  
   1.151  
   1.152  theorem sup_loc_update [rule_format]:
   1.153 -  "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
   1.154 +  "\<forall> n y. (G \<turnstile> a <=o b) --> n < length y --> (G \<turnstile> x <=l y) --> 
   1.155            (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
   1.156  proof (induct x)
   1.157    show "?P []" by simp
   1.158 @@ -427,7 +428,7 @@
   1.159    by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
   1.160  
   1.161  theorem sup_state_ignore_fst:  
   1.162 -  "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
   1.163 +  "G \<turnstile> (a, x) <=s (b, y) ==> G \<turnstile> (c, x) <=s (c, y)"
   1.164    by (simp add: sup_state_def)
   1.165  
   1.166  theorem sup_state_rev_fst:
   1.167 @@ -460,15 +461,15 @@
   1.168  
   1.169  
   1.170  theorem sup_ty_opt_trans [trans]:
   1.171 -  "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   1.172 +  "[|G \<turnstile> a <=o b; G \<turnstile> b <=o c|] ==> G \<turnstile> a <=o c"
   1.173    by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
   1.174  
   1.175  theorem sup_loc_trans [trans]:
   1.176 -  "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
   1.177 +  "[|G \<turnstile> a <=l b; G \<turnstile> b <=l c|] ==> G \<turnstile> a <=l c"
   1.178  proof -
   1.179    assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
   1.180   
   1.181 -  hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
   1.182 +  hence "\<forall> n. n < length a --> (G \<turnstile> (a!n) <=o (c!n))"
   1.183    proof (intro strip)
   1.184      fix n 
   1.185      assume n: "n < length a"
   1.186 @@ -490,11 +491,11 @@
   1.187    
   1.188  
   1.189  theorem sup_state_trans [trans]:
   1.190 -  "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   1.191 +  "[|G \<turnstile> a <=s b; G \<turnstile> b <=s c|] ==> G \<turnstile> a <=s c"
   1.192    by (auto intro: sup_loc_trans simp add: sup_state_def)
   1.193  
   1.194  theorem sup_state_opt_trans [trans]:
   1.195 -  "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
   1.196 +  "[|G \<turnstile> a <=' b; G \<turnstile> b <=' c|] ==> G \<turnstile> a <=' c"
   1.197    by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
   1.198  
   1.199