src/HOL/MicroJava/BV/Convert.thy
author wenzelm
Tue Sep 12 22:13:23 2000 +0200 (2000-09-12)
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10042 7164dc0d24d8
permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
     1 (*  Title:      HOL/MicroJava/BV/Convert.thy
     2     ID:         $Id$
     3     Author:     Cornelia Pusch and Gerwin Klein
     4     Copyright   1999 Technische Universitaet Muenchen
     5 *)
     6 
     7 header "Lifted Type Relations"
     8 
     9 theory Convert = JVMExec:
    10 
    11 text "The supertype relation lifted to type err, type lists and state types."
    12 
    13 datatype 'a err = Err | Ok 'a
    14 
    15 types
    16  locvars_type = "ty err list"
    17  opstack_type = "ty list"
    18  state_type   = "opstack_type \<times> locvars_type"
    19 
    20 
    21 consts
    22   strict  :: "('a \<Rightarrow> 'b err) \<Rightarrow> ('a err \<Rightarrow> 'b err)"
    23 primrec
    24   "strict f Err    = Err"
    25   "strict f (Ok x) = f x"
    26 
    27 consts
    28   opt_map :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a option \<Rightarrow> 'b option)"
    29 primrec
    30   "opt_map f None     = None"
    31   "opt_map f (Some x) = Some (f x)"
    32 
    33 consts
    34   val :: "'a err \<Rightarrow> 'a"
    35 primrec
    36   "val (Ok s) = s"
    37 
    38   
    39 constdefs
    40   (* lifts a relation to err with Err as top element *)
    41   lift_top :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a err \<Rightarrow> 'b err \<Rightarrow> bool)"
    42   "lift_top P a' a \<equiv> case a of 
    43                        Err  \<Rightarrow> True
    44                      | Ok t \<Rightarrow> (case a' of Err \<Rightarrow> False | Ok t' \<Rightarrow> P t' t)"
    45 
    46   (* lifts a relation to option with None as bottom element *)
    47   lift_bottom :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a option \<Rightarrow> 'b option \<Rightarrow> bool)"
    48   "lift_bottom P a' a \<equiv> case a' of 
    49                           None    \<Rightarrow> True 
    50                         | Some t' \<Rightarrow> (case a of None \<Rightarrow> False | Some t \<Rightarrow> P t' t)"
    51 
    52   sup_ty_opt :: "['code prog,ty err,ty err] \<Rightarrow> bool" ("_ \<turnstile>_ <=o _")
    53   "sup_ty_opt G \<equiv> lift_top (\<lambda>t t'. G \<turnstile> t \<preceq> t')"
    54 
    55   sup_loc :: "['code prog,locvars_type,locvars_type] \<Rightarrow> bool" 
    56              ("_ \<turnstile> _ <=l _"  [71,71] 70)
    57   "G \<turnstile> LT <=l LT' \<equiv> list_all2 (\<lambda>t t'. (G \<turnstile> t <=o t')) LT LT'"
    58 
    59   sup_state :: "['code prog,state_type,state_type] \<Rightarrow> bool"	  
    60                ("_ \<turnstile> _ <=s _"  [71,71] 70)
    61   "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'"
    62 
    63   sup_state_opt :: "['code prog,state_type option,state_type option] \<Rightarrow> bool" 
    64                    ("_ \<turnstile> _ <=' _"  [71,71] 70)
    65   "sup_state_opt G \<equiv> lift_bottom (\<lambda>t t'. G \<turnstile> t <=s t')"
    66 
    67 
    68 lemma not_Err_eq [iff]:
    69   "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
    70   by (cases x) auto
    71 
    72 lemma not_Some_eq [iff]:
    73   "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
    74   by (cases x) auto  
    75 
    76 
    77 lemma lift_top_refl [simp]:
    78   "[| !!x. P x x |] ==> lift_top P x x"
    79   by (simp add: lift_top_def split: err.splits)
    80 
    81 lemma lift_top_trans [trans]:
    82   "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_top P x y; lift_top P y z |] 
    83   ==> lift_top P x z"
    84 proof -
    85   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
    86   assume a: "lift_top P x y"
    87   assume b: "lift_top P y z"
    88 
    89   { assume "z = Err" 
    90     hence ?thesis by (simp add: lift_top_def)
    91   } note z_none = this
    92 
    93   { assume "x = Err"
    94     with a b
    95     have ?thesis
    96       by (simp add: lift_top_def split: err.splits)
    97   } note x_none = this
    98   
    99   { fix r t
   100     assume x: "x = Ok r" and z: "z = Ok t"    
   101     with a b
   102     obtain s where y: "y = Ok s" 
   103       by (simp add: lift_top_def split: err.splits)
   104     
   105     from a x y
   106     have "P r s" by (simp add: lift_top_def)
   107     also
   108     from b y z
   109     have "P s t" by (simp add: lift_top_def)
   110     finally 
   111     have "P r t" .
   112 
   113     with x z
   114     have ?thesis by (simp add: lift_top_def)
   115   } 
   116 
   117   with x_none z_none
   118   show ?thesis by blast
   119 qed
   120 
   121 lemma lift_top_Err_any [simp]:
   122   "lift_top P Err any = (any = Err)"
   123   by (simp add: lift_top_def split: err.splits)
   124 
   125 lemma lift_top_Ok_Ok [simp]:
   126   "lift_top P (Ok a) (Ok b) = P a b"
   127   by (simp add: lift_top_def split: err.splits)
   128 
   129 lemma lift_top_any_Ok [simp]:
   130   "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
   131   by (simp add: lift_top_def split: err.splits)
   132 
   133 lemma lift_top_Ok_any:
   134   "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
   135   by (simp add: lift_top_def split: err.splits)
   136 
   137 
   138 lemma lift_bottom_refl [simp]:
   139   "[| !!x. P x x |] ==> lift_bottom P x x"
   140   by (simp add: lift_bottom_def split: option.splits)
   141 
   142 lemma lift_bottom_trans [trans]:
   143   "[| !!x y z. [| P x y; P y z |] ==> P x z; lift_bottom P x y; lift_bottom P y z |]
   144   ==> lift_bottom P x z"
   145 proof -
   146   assume [trans]: "!!x y z. [| P x y; P y z |] ==> P x z"
   147   assume a: "lift_bottom P x y"
   148   assume b: "lift_bottom P y z"
   149 
   150   { assume "x = None" 
   151     hence ?thesis by (simp add: lift_bottom_def)
   152   } note z_none = this
   153 
   154   { assume "z = None"
   155     with a b
   156     have ?thesis
   157       by (simp add: lift_bottom_def split: option.splits)
   158   } note x_none = this
   159   
   160   { fix r t
   161     assume x: "x = Some r" and z: "z = Some t"    
   162     with a b
   163     obtain s where y: "y = Some s" 
   164       by (simp add: lift_bottom_def split: option.splits)
   165     
   166     from a x y
   167     have "P r s" by (simp add: lift_bottom_def)
   168     also
   169     from b y z
   170     have "P s t" by (simp add: lift_bottom_def)
   171     finally 
   172     have "P r t" .
   173 
   174     with x z
   175     have ?thesis by (simp add: lift_bottom_def)
   176   } 
   177 
   178   with x_none z_none
   179   show ?thesis by blast
   180 qed
   181 
   182 lemma lift_bottom_any_None [simp]:
   183   "lift_bottom P any None = (any = None)"
   184   by (simp add: lift_bottom_def split: option.splits)
   185 
   186 lemma lift_bottom_Some_Some [simp]:
   187   "lift_bottom P (Some a) (Some b) = P a b"
   188   by (simp add: lift_bottom_def split: option.splits)
   189 
   190 lemma lift_bottom_any_Some [simp]:
   191   "lift_bottom P (Some a) any = (\<exists>b. any = Some b \<and> P a b)"
   192   by (simp add: lift_bottom_def split: option.splits)
   193 
   194 lemma lift_bottom_Some_any:
   195   "lift_bottom P any (Some b) = (any = None \<or> (\<exists>a. any = Some a \<and> P a b))"
   196   by (simp add: lift_bottom_def split: option.splits)
   197 
   198 
   199 
   200 theorem sup_ty_opt_refl [simp]:
   201   "G \<turnstile> t <=o t"
   202   by (simp add: sup_ty_opt_def)
   203 
   204 theorem sup_loc_refl [simp]:
   205   "G \<turnstile> t <=l t"
   206   by (induct t, auto simp add: sup_loc_def)
   207 
   208 theorem sup_state_refl [simp]:
   209   "G \<turnstile> s <=s s"
   210   by (simp add: sup_state_def)
   211 
   212 theorem sup_state_opt_refl [simp]:
   213   "G \<turnstile> s <=' s"
   214   by (simp add: sup_state_opt_def)
   215 
   216 
   217 theorem anyConvErr [simp]:
   218   "(G \<turnstile> Err <=o any) = (any = Err)"
   219   by (simp add: sup_ty_opt_def)
   220 
   221 theorem OkanyConvOk [simp]:
   222   "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
   223   by (simp add: sup_ty_opt_def)
   224 
   225 theorem sup_ty_opt_Ok:
   226   "G \<turnstile> a <=o (Ok b) \<Longrightarrow> \<exists> x. a = Ok x"
   227   by (clarsimp simp add: sup_ty_opt_def)
   228 
   229 lemma widen_PrimT_conv1 [simp]:
   230   "[| G \<turnstile> S \<preceq> T; S = PrimT x|] ==> T = PrimT x"
   231   by (auto elim: widen.elims)
   232 
   233 theorem sup_PTS_eq:
   234   "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
   235   by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
   236 
   237 
   238 
   239 theorem sup_loc_Nil [iff]:
   240   "(G \<turnstile> [] <=l XT) = (XT=[])"
   241   by (simp add: sup_loc_def)
   242 
   243 theorem sup_loc_Cons [iff]:
   244   "(G \<turnstile> (Y#YT) <=l XT) = (\<exists>X XT'. XT=X#XT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT <=l XT'))"
   245   by (simp add: sup_loc_def list_all2_Cons1)
   246 
   247 theorem sup_loc_Cons2:
   248   "(G \<turnstile> YT <=l (X#XT)) = (\<exists>Y YT'. YT=Y#YT' \<and> (G \<turnstile> Y <=o X) \<and> (G \<turnstile> YT' <=l XT))"
   249   by (simp add: sup_loc_def list_all2_Cons2)
   250 
   251 
   252 theorem sup_loc_length:
   253   "G \<turnstile> a <=l b \<Longrightarrow> length a = length b"
   254 proof -
   255   assume G: "G \<turnstile> a <=l b"
   256   have "\<forall> b. (G \<turnstile> a <=l b) \<longrightarrow> length a = length b"
   257     by (induct a, auto)
   258   with G
   259   show ?thesis by blast
   260 qed
   261 
   262 theorem sup_loc_nth:
   263   "[| G \<turnstile> a <=l b; n < length a |] ==> G \<turnstile> (a!n) <=o (b!n)"
   264 proof -
   265   assume a: "G \<turnstile> a <=l b" "n < length a"
   266   have "\<forall> n b. (G \<turnstile> a <=l b) \<longrightarrow> n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))"
   267     (is "?P a")
   268   proof (induct a)
   269     show "?P []" by simp
   270     
   271     fix x xs assume IH: "?P xs"
   272 
   273     show "?P (x#xs)"
   274     proof (intro strip)
   275       fix n b
   276       assume "G \<turnstile> (x # xs) <=l b" "n < length (x # xs)"
   277       with IH
   278       show "G \<turnstile> ((x # xs) ! n) <=o (b ! n)"
   279         by - (cases n, auto)
   280     qed
   281   qed
   282   with a
   283   show ?thesis by blast
   284 qed
   285 
   286 
   287 theorem all_nth_sup_loc:
   288   "\<forall>b. length a = length b \<longrightarrow> (\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (b!n))) \<longrightarrow> 
   289        (G \<turnstile> a <=l b)" (is "?P a")
   290 proof (induct a)
   291   show "?P []" by simp
   292 
   293   fix l ls assume IH: "?P ls"
   294   
   295   show "?P (l#ls)"
   296   proof (intro strip)
   297     fix b
   298     assume f: "\<forall>n. n < length (l # ls) \<longrightarrow> (G \<turnstile> ((l # ls) ! n) <=o (b ! n))"
   299     assume l: "length (l#ls) = length b"
   300     
   301     then obtain b' bs where b: "b = b'#bs"
   302       by - (cases b, simp, simp add: neq_Nil_conv, rule that)
   303 
   304     with f
   305     have "\<forall>n. n < length ls \<longrightarrow> (G \<turnstile> (ls!n) <=o (bs!n))"
   306       by auto
   307 
   308     with f b l IH
   309     show "G \<turnstile> (l # ls) <=l b"
   310       by auto
   311   qed
   312 qed
   313 
   314 
   315 theorem sup_loc_append:
   316   "length a = length b ==> 
   317    (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> (G \<turnstile> x <=l y))"
   318 proof -
   319   assume l: "length a = length b"
   320 
   321   have "\<forall>b. length a = length b \<longrightarrow> (G \<turnstile> (a@x) <=l (b@y)) = ((G \<turnstile> a <=l b) \<and> 
   322             (G \<turnstile> x <=l y))" (is "?P a") 
   323   proof (induct a)
   324     show "?P []" by simp
   325     
   326     fix l ls assume IH: "?P ls"    
   327     show "?P (l#ls)" 
   328     proof (intro strip)
   329       fix b
   330       assume "length (l#ls) = length (b::ty err list)"
   331       with IH
   332       show "(G \<turnstile> ((l#ls)@x) <=l (b@y)) = ((G \<turnstile> (l#ls) <=l b) \<and> (G \<turnstile> x <=l y))"
   333         by - (cases b, auto)
   334     qed
   335   qed
   336   with l
   337   show ?thesis by blast
   338 qed
   339 
   340 theorem sup_loc_rev [simp]:
   341   "(G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)"
   342 proof -
   343   have "\<forall>b. (G \<turnstile> (rev a) <=l rev b) = (G \<turnstile> a <=l b)" (is "\<forall>b. ?Q a b" is "?P a")
   344   proof (induct a)
   345     show "?P []" by simp
   346 
   347     fix l ls assume IH: "?P ls"
   348 
   349     { 
   350       fix b
   351       have "?Q (l#ls) b"
   352       proof (cases (open) b)
   353         case Nil
   354         thus ?thesis by (auto dest: sup_loc_length)
   355       next
   356         case Cons 
   357         show ?thesis
   358         proof
   359           assume "G \<turnstile> (l # ls) <=l b"
   360           thus "G \<turnstile> rev (l # ls) <=l rev b"
   361             by (clarsimp simp add: Cons IH sup_loc_length sup_loc_append)
   362         next
   363           assume "G \<turnstile> rev (l # ls) <=l rev b"
   364           hence G: "G \<turnstile> (rev ls @ [l]) <=l (rev list @ [a])"
   365             by (simp add: Cons)          
   366           
   367           hence "length (rev ls) = length (rev list)"
   368             by (auto dest: sup_loc_length)
   369 
   370           from this G
   371           obtain "G \<turnstile> rev ls <=l rev list" "G \<turnstile> l <=o a"
   372             by (simp add: sup_loc_append)
   373 
   374           thus "G \<turnstile> (l # ls) <=l b"
   375             by (simp add: Cons IH)
   376         qed
   377       qed    
   378     }
   379     thus "?P (l#ls)" by blast
   380   qed
   381 
   382   thus ?thesis by blast
   383 qed
   384 
   385 
   386 theorem sup_loc_update [rule_format]:
   387   "\<forall> n y. (G \<turnstile> a <=o b) \<longrightarrow> n < length y \<longrightarrow> (G \<turnstile> x <=l y) \<longrightarrow> 
   388           (G \<turnstile> x[n := a] <=l y[n := b])" (is "?P x")
   389 proof (induct x)
   390   show "?P []" by simp
   391 
   392   fix l ls assume IH: "?P ls"
   393   show "?P (l#ls)"
   394   proof (intro strip)
   395     fix n y
   396     assume "G \<turnstile>a <=o b" "G \<turnstile> (l # ls) <=l y" "n < length y"
   397     with IH
   398     show "G \<turnstile> (l # ls)[n := a] <=l y[n := b]"
   399       by - (cases n, auto simp add: sup_loc_Cons2 list_all2_Cons1)
   400   qed
   401 qed
   402 
   403 
   404 theorem sup_state_length [simp]:
   405   "G \<turnstile> s2 <=s s1 ==> 
   406    length (fst s2) = length (fst s1) \<and> length (snd s2) = length (snd s1)"
   407   by (auto dest: sup_loc_length simp add: sup_state_def);
   408 
   409 theorem sup_state_append_snd:
   410   "length a = length b ==> 
   411   (G \<turnstile> (i,a@x) <=s (j,b@y)) = ((G \<turnstile> (i,a) <=s (j,b)) \<and> (G \<turnstile> (i,x) <=s (j,y)))"
   412   by (auto simp add: sup_state_def sup_loc_append)
   413 
   414 theorem sup_state_append_fst:
   415   "length a = length b ==> 
   416   (G \<turnstile> (a@x,i) <=s (b@y,j)) = ((G \<turnstile> (a,i) <=s (b,j)) \<and> (G \<turnstile> (x,i) <=s (y,j)))"
   417   by (auto simp add: sup_state_def sup_loc_append)
   418 
   419 theorem sup_state_Cons1:
   420   "(G \<turnstile> (x#xt, a) <=s (yt, b)) = 
   421    (\<exists>y yt'. yt=y#yt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt,a) <=s (yt',b)))"
   422   by (auto simp add: sup_state_def map_eq_Cons)
   423 
   424 theorem sup_state_Cons2:
   425   "(G \<turnstile> (xt, a) <=s (y#yt, b)) = 
   426    (\<exists>x xt'. xt=x#xt' \<and> (G \<turnstile> x \<preceq> y) \<and> (G \<turnstile> (xt',a) <=s (yt,b)))"
   427   by (auto simp add: sup_state_def map_eq_Cons sup_loc_Cons2)
   428 
   429 theorem sup_state_ignore_fst:  
   430   "G \<turnstile> (a, x) <=s (b, y) \<Longrightarrow> G \<turnstile> (c, x) <=s (c, y)"
   431   by (simp add: sup_state_def)
   432 
   433 theorem sup_state_rev_fst:
   434   "(G \<turnstile> (rev a, x) <=s (rev b, y)) = (G \<turnstile> (a, x) <=s (b, y))"
   435 proof -
   436   have m: "!!f x. map f (rev x) = rev (map f x)" by (simp add: rev_map)
   437   show ?thesis by (simp add: m sup_state_def)
   438 qed
   439   
   440 
   441 lemma sup_state_opt_None_any [iff]:
   442   "(G \<turnstile> None <=' any) = True"
   443   by (simp add: sup_state_opt_def lift_bottom_def)
   444 
   445 lemma sup_state_opt_any_None [iff]:
   446   "(G \<turnstile> any <=' None) = (any = None)"
   447   by (simp add: sup_state_opt_def)
   448 
   449 lemma sup_state_opt_Some_Some [iff]:
   450   "(G \<turnstile> (Some a) <=' (Some b)) = (G \<turnstile> a <=s b)"
   451   by (simp add: sup_state_opt_def del: split_paired_Ex)
   452 
   453 lemma sup_state_opt_any_Some [iff]:
   454   "(G \<turnstile> (Some a) <=' any) = (\<exists>b. any = Some b \<and> G \<turnstile> a <=s b)"
   455   by (simp add: sup_state_opt_def)
   456 
   457 lemma sup_state_opt_Some_any:
   458   "(G \<turnstile> any <=' (Some b)) = (any = None \<or> (\<exists>a. any = Some a \<and> G \<turnstile> a <=s b))"
   459   by (simp add: sup_state_opt_def lift_bottom_Some_any)
   460 
   461 
   462 theorem sup_ty_opt_trans [trans]:
   463   "\<lbrakk>G \<turnstile> a <=o b; G \<turnstile> b <=o c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=o c"
   464   by (auto intro: lift_top_trans widen_trans simp add: sup_ty_opt_def)
   465 
   466 theorem sup_loc_trans [trans]:
   467   "\<lbrakk>G \<turnstile> a <=l b; G \<turnstile> b <=l c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=l c"
   468 proof -
   469   assume G: "G \<turnstile> a <=l b" "G \<turnstile> b <=l c"
   470  
   471   hence "\<forall> n. n < length a \<longrightarrow> (G \<turnstile> (a!n) <=o (c!n))"
   472   proof (intro strip)
   473     fix n 
   474     assume n: "n < length a"
   475     with G
   476     have "G \<turnstile> (a!n) <=o (b!n)"
   477       by - (rule sup_loc_nth)
   478     also 
   479     from n G
   480     have "G \<turnstile> ... <=o (c!n)"
   481       by - (rule sup_loc_nth, auto dest: sup_loc_length)
   482     finally
   483     show "G \<turnstile> (a!n) <=o (c!n)" .
   484   qed
   485 
   486   with G
   487   show ?thesis 
   488     by (auto intro!: all_nth_sup_loc [rule_format] dest!: sup_loc_length) 
   489 qed
   490   
   491 
   492 theorem sup_state_trans [trans]:
   493   "\<lbrakk>G \<turnstile> a <=s b; G \<turnstile> b <=s c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=s c"
   494   by (auto intro: sup_loc_trans simp add: sup_state_def)
   495 
   496 theorem sup_state_opt_trans [trans]:
   497   "\<lbrakk>G \<turnstile> a <=' b; G \<turnstile> b <=' c\<rbrakk> \<Longrightarrow> G \<turnstile> a <=' c"
   498   by (auto intro: lift_bottom_trans sup_state_trans simp add: sup_state_opt_def)
   499 
   500 
   501 end