BCV integration (first step)
authorkleing
Mon Nov 20 16:37:42 2000 +0100 (2000-11-20)
changeset 10496f2d304bdf3cc
parent 10495 284ee538991c
child 10497 7c6985b4de40
BCV integration (first step)
src/HOL/MicroJava/BV/BVSpec.thy
src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
src/HOL/MicroJava/BV/Convert.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/BV/DFA_Framework.thy
src/HOL/MicroJava/BV/DFA_err.thy
src/HOL/MicroJava/BV/Err.thy
src/HOL/MicroJava/BV/Kildall.thy
src/HOL/MicroJava/BV/LBVComplete.thy
src/HOL/MicroJava/BV/LBVCorrect.thy
src/HOL/MicroJava/BV/LBVSpec.thy
src/HOL/MicroJava/BV/Listn.thy
src/HOL/MicroJava/BV/Opt.thy
src/HOL/MicroJava/BV/Product.thy
src/HOL/MicroJava/BV/Semilat.thy
src/HOL/MicroJava/BV/Step.thy
src/HOL/MicroJava/BV/StepMono.thy
     1.1 --- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Nov 18 19:48:34 2000 +0100
     1.2 +++ b/src/HOL/MicroJava/BV/BVSpec.thy	Mon Nov 20 16:37:42 2000 +0100
     1.3 @@ -9,11 +9,6 @@
     1.4  
     1.5  theory BVSpec = Step:
     1.6  
     1.7 -types
     1.8 - method_type = "state_type option list"
     1.9 - class_type	 = "sig => method_type"
    1.10 - prog_type	 = "cname => class_type"
    1.11 -
    1.12  constdefs
    1.13  wt_instr :: "[instr,jvm_prog,ty,method_type,p_count,p_count] => bool"
    1.14  "wt_instr i G rT phi max_pc pc == 
    1.15 @@ -22,7 +17,7 @@
    1.16  
    1.17  wt_start :: "[jvm_prog,cname,ty list,nat,method_type] => bool"
    1.18  "wt_start G C pTs mxl phi == 
    1.19 -    G \<turnstile> Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err)) <=' phi!0"
    1.20 +    G \<turnstile> Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)) <=' phi!0"
    1.21  
    1.22  
    1.23  wt_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,method_type] => bool"
     2.1 --- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Sat Nov 18 19:48:34 2000 +0100
     2.2 +++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Mon Nov 20 16:37:42 2000 +0100
     2.3 @@ -274,7 +274,7 @@
     2.4    from a_stk
     2.5    obtain opTs stk' oX where
     2.6      opTs:   "approx_stk G hp opTs (rev apTs)" and
     2.7 -    oX:     "approx_val G hp oX (Ok X)" and
     2.8 +    oX:     "approx_val G hp oX (OK X)" and
     2.9      a_stk': "approx_stk G hp stk' ST" and
    2.10      stk':   "stk = opTs @ oX # stk'" and
    2.11      l_o:    "length opTs = length apTs" 
    2.12 @@ -377,7 +377,7 @@
    2.13      proof -
    2.14        from start LT0
    2.15        have sup_loc: 
    2.16 -        "G \<turnstile> (Ok (Class D'') # map Ok pTs @ replicate mxl' Err) <=l LT0"
    2.17 +        "G \<turnstile> (OK (Class D'') # map OK pTs @ replicate mxl' Err) <=l LT0"
    2.18          (is "G \<turnstile> ?LT <=l LT0")
    2.19          by (simp add: wt_start_def sup_state_def)
    2.20  
    2.21 @@ -389,14 +389,14 @@
    2.22        have "G \<turnstile> Class D \<preceq> Class D''"
    2.23          by (auto dest: method_wf_mdecl)
    2.24        with obj_ty loc
    2.25 -      have a: "approx_val G hp (Addr ref) (Ok (Class D''))"
    2.26 +      have a: "approx_val G hp (Addr ref) (OK (Class D''))"
    2.27          by (simp add: approx_val_def conf_def)
    2.28  
    2.29        from w l
    2.30        have "\<forall>x\<in>set (zip (rev apTs) (rev pTs)). x \<in> widen G"
    2.31          by (auto simp add: zip_rev)
    2.32        with wfprog l l_o opTs
    2.33 -      have "approx_loc G hp opTs (map Ok (rev pTs))"
    2.34 +      have "approx_loc G hp opTs (map OK (rev pTs))"
    2.35          by (auto intro: assConv_approx_stk_imp_approx_loc)
    2.36        hence "approx_stk G hp opTs (rev pTs)"
    2.37          by (simp add: approx_stk_def)
    2.38 @@ -427,7 +427,7 @@
    2.39          by (rule approx_loc_imp_approx_loc_sup)
    2.40        moreover
    2.41        from s s' mC' step l
    2.42 -      have  "G \<turnstile> map Ok ST <=l map Ok (tl ST')"
    2.43 +      have  "G \<turnstile> map OK ST <=l map OK (tl ST')"
    2.44          by (auto simp add: step_def sup_state_def map_eq_Cons)
    2.45        with wfprog a_stk'
    2.46        have "approx_stk G hp stk' (tl ST')"
     3.1 --- a/src/HOL/MicroJava/BV/Convert.thy	Sat Nov 18 19:48:34 2000 +0100
     3.2 +++ b/src/HOL/MicroJava/BV/Convert.thy	Mon Nov 20 16:37:42 2000 +0100
     3.3 @@ -6,29 +6,23 @@
     3.4  
     3.5  header "Lifted Type Relations"
     3.6  
     3.7 -theory Convert = JVMExec:
     3.8 +theory Convert = Err + JVMExec:
     3.9  
    3.10  text "The supertype relation lifted to type err, type lists and state types."
    3.11  
    3.12 -datatype 'a err = Err | Ok 'a
    3.13 -
    3.14  types
    3.15   locvars_type = "ty err list"
    3.16   opstack_type = "ty list"
    3.17   state_type   = "opstack_type \<times> locvars_type"
    3.18 -
    3.19 + method_type  = "state_type option list"
    3.20 + class_type	  = "sig => method_type"
    3.21 + prog_type	  = "cname => class_type"
    3.22  
    3.23  consts
    3.24    strict  :: "('a => 'b err) => ('a err => 'b err)"
    3.25  primrec
    3.26    "strict f Err    = Err"
    3.27 -  "strict f (Ok x) = f x"
    3.28 -
    3.29 -
    3.30 -consts
    3.31 -  val :: "'a err => 'a"
    3.32 -primrec
    3.33 -  "val (Ok s) = s"
    3.34 +  "strict f (OK x) = f x"
    3.35  
    3.36    
    3.37  constdefs
    3.38 @@ -36,7 +30,7 @@
    3.39    lift_top :: "('a => 'b => bool) => ('a err => 'b err => bool)"
    3.40    "lift_top P a' a == case a of 
    3.41                         Err  => True
    3.42 -                     | Ok t => (case a' of Err => False | Ok t' => P t' t)"
    3.43 +                     | OK t => (case a' of Err => False | OK t' => P t' t)"
    3.44  
    3.45    (* lifts a relation to option with None as bottom element *)
    3.46    lift_bottom :: "('a => 'b => bool) => ('a option => 'b option => bool)"
    3.47 @@ -56,7 +50,7 @@
    3.48    sup_state :: "['code prog,state_type,state_type] => bool"	  
    3.49                 ("_ \<turnstile> _ <=s _"  [71,71] 70)
    3.50    "G \<turnstile> s <=s s' == 
    3.51 -   (G \<turnstile> map Ok (fst s) <=l map Ok (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
    3.52 +   (G \<turnstile> map OK (fst s) <=l map OK (fst s')) \<and> G \<turnstile> snd s <=l snd s'"
    3.53  
    3.54    sup_state_opt :: "['code prog,state_type option,state_type option] => bool" 
    3.55                     ("_ \<turnstile> _ <=' _"  [71,71] 70)
    3.56 @@ -73,14 +67,7 @@
    3.57                     ("_ |- _ <=' _"  [71,71] 70)
    3.58                     
    3.59  
    3.60 -lemma not_Err_eq [iff]:
    3.61 -  "(x \<noteq> Err) = (\<exists>a. x = Ok a)" 
    3.62 -  by (cases x) auto
    3.63 -
    3.64 -lemma not_Some_eq [iff]:
    3.65 -  "(\<forall>y. x \<noteq> Ok y) = (x = Err)"
    3.66 -  by (cases x) auto  
    3.67 -
    3.68 +lemmas [iff] = not_Err_eq not_OK_eq
    3.69  
    3.70  lemma lift_top_refl [simp]:
    3.71    "[| !!x. P x x |] ==> lift_top P x x"
    3.72 @@ -105,9 +92,9 @@
    3.73    } note x_none = this
    3.74    
    3.75    { fix r t
    3.76 -    assume x: "x = Ok r" and z: "z = Ok t"    
    3.77 +    assume x: "x = OK r" and z: "z = OK t"    
    3.78      with a b
    3.79 -    obtain s where y: "y = Ok s" 
    3.80 +    obtain s where y: "y = OK s" 
    3.81        by (simp add: lift_top_def split: err.splits)
    3.82      
    3.83      from a x y
    3.84 @@ -130,16 +117,16 @@
    3.85    "lift_top P Err any = (any = Err)"
    3.86    by (simp add: lift_top_def split: err.splits)
    3.87  
    3.88 -lemma lift_top_Ok_Ok [simp]:
    3.89 -  "lift_top P (Ok a) (Ok b) = P a b"
    3.90 +lemma lift_top_OK_OK [simp]:
    3.91 +  "lift_top P (OK a) (OK b) = P a b"
    3.92    by (simp add: lift_top_def split: err.splits)
    3.93  
    3.94 -lemma lift_top_any_Ok [simp]:
    3.95 -  "lift_top P any (Ok b) = (\<exists>a. any = Ok a \<and> P a b)"
    3.96 +lemma lift_top_any_OK [simp]:
    3.97 +  "lift_top P any (OK b) = (\<exists>a. any = OK a \<and> P a b)"
    3.98    by (simp add: lift_top_def split: err.splits)
    3.99  
   3.100 -lemma lift_top_Ok_any:
   3.101 -  "lift_top P (Ok a) any = (any = Err \<or> (\<exists>b. any = Ok b \<and> P a b))"
   3.102 +lemma lift_top_OK_any:
   3.103 +  "lift_top P (OK a) any = (any = Err \<or> (\<exists>b. any = OK b \<and> P a b))"
   3.104    by (simp add: lift_top_def split: err.splits)
   3.105  
   3.106  
   3.107 @@ -227,12 +214,12 @@
   3.108    "(G \<turnstile> Err <=o any) = (any = Err)"
   3.109    by (simp add: sup_ty_opt_def)
   3.110  
   3.111 -theorem OkanyConvOk [simp]:
   3.112 -  "(G \<turnstile> (Ok ty') <=o (Ok ty)) = (G \<turnstile> ty' \<preceq> ty)"
   3.113 +theorem OKanyConvOK [simp]:
   3.114 +  "(G \<turnstile> (OK ty') <=o (OK ty)) = (G \<turnstile> ty' \<preceq> ty)"
   3.115    by (simp add: sup_ty_opt_def)
   3.116  
   3.117 -theorem sup_ty_opt_Ok:
   3.118 -  "G \<turnstile> a <=o (Ok b) ==> \<exists> x. a = Ok x"
   3.119 +theorem sup_ty_opt_OK:
   3.120 +  "G \<turnstile> a <=o (OK b) ==> \<exists> x. a = OK x"
   3.121    by (clarsimp simp add: sup_ty_opt_def)
   3.122  
   3.123  lemma widen_PrimT_conv1 [simp]:
   3.124 @@ -240,8 +227,8 @@
   3.125    by (auto elim: widen.elims)
   3.126  
   3.127  theorem sup_PTS_eq:
   3.128 -  "(G \<turnstile> Ok (PrimT p) <=o X) = (X=Err \<or> X = Ok (PrimT p))"
   3.129 -  by (auto simp add: sup_ty_opt_def lift_top_Ok_any)
   3.130 +  "(G \<turnstile> OK (PrimT p) <=o X) = (X=Err \<or> X = OK (PrimT p))"
   3.131 +  by (auto simp add: sup_ty_opt_def lift_top_OK_any)
   3.132  
   3.133  
   3.134  
     4.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Sat Nov 18 19:48:34 2000 +0100
     4.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Mon Nov 20 16:37:42 2000 +0100
     4.3 @@ -12,13 +12,13 @@
     4.4  
     4.5  constdefs
     4.6    approx_val :: "[jvm_prog,aheap,val,ty err] => bool"
     4.7 -  "approx_val G h v any == case any of Err => True | Ok T => G,h\<turnstile>v::\<preceq>T"
     4.8 +  "approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T"
     4.9  
    4.10    approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool"
    4.11    "approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT"
    4.12  
    4.13    approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool"
    4.14 -  "approx_stk G hp stk ST == approx_loc G hp stk (map Ok ST)"
    4.15 +  "approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)"
    4.16  
    4.17    correct_frame  :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool"
    4.18    "correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc).
    4.19 @@ -96,12 +96,12 @@
    4.20  by (simp add: approx_val_def)
    4.21  
    4.22  lemma approx_val_Null:
    4.23 -  "approx_val G hp Null (Ok (RefT x))"
    4.24 +  "approx_val G hp Null (OK (RefT x))"
    4.25  by (auto intro: null simp add: approx_val_def)
    4.26  
    4.27  lemma approx_val_imp_approx_val_assConvertible [rule_format]: 
    4.28 -  "wf_prog wt G ==> approx_val G hp v (Ok T) --> G\<turnstile> T\<preceq>T' 
    4.29 -  --> approx_val G hp v (Ok T')"
    4.30 +  "wf_prog wt G ==> approx_val G hp v (OK T) --> G\<turnstile> T\<preceq>T' 
    4.31 +  --> approx_val G hp v (OK T')"
    4.32  by (cases T) (auto intro: conf_widen simp add: approx_val_def)
    4.33  
    4.34  lemma approx_val_imp_approx_val_sup_heap [rule_format]:
    4.35 @@ -143,7 +143,7 @@
    4.36  lemma assConv_approx_stk_imp_approx_loc [rule_format]:
    4.37    "wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) 
    4.38    --> length tys_n = length ts --> approx_stk G hp s tys_n --> 
    4.39 -  approx_loc G hp s (map Ok ts)"
    4.40 +  approx_loc G hp s (map OK ts)"
    4.41  apply (unfold approx_stk_def approx_loc_def list_all2_def)
    4.42  apply (clarsimp simp add: all_set_conv_all_nth)
    4.43  apply (rule approx_val_imp_approx_val_assConvertible)
    4.44 @@ -212,7 +212,7 @@
    4.45  by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def)
    4.46  
    4.47  lemma approx_stk_imp_approx_stk_sup [rule_format]:
    4.48 -  "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map Ok st <=l (map Ok st')) 
    4.49 +  "wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map OK st <=l (map OK st')) 
    4.50    --> approx_stk G hp lvars st'" 
    4.51  by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def)
    4.52  
    4.53 @@ -222,12 +222,12 @@
    4.54  
    4.55  lemma approx_stk_Cons [iff]:
    4.56    "approx_stk G hp (x # stk) (S#ST) = 
    4.57 -   (approx_val G hp x (Ok S) \<and> approx_stk G hp stk ST)"
    4.58 +   (approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)"
    4.59  by (simp add: approx_stk_def approx_loc_def)
    4.60  
    4.61  lemma approx_stk_Cons_lemma [iff]:
    4.62    "approx_stk G hp stk (S#ST') = 
    4.63 -  (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (Ok S) \<and> approx_stk G hp stk' ST')"
    4.64 +  (\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')"
    4.65  by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def)
    4.66  
    4.67  lemma approx_stk_append_lemma:
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/MicroJava/BV/DFA_Framework.thy	Mon Nov 20 16:37:42 2000 +0100
     5.3 @@ -0,0 +1,76 @@
     5.4 +(*  Title:      HOL/BCV/DFA_Framework.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Tobias Nipkow
     5.7 +    Copyright   2000 TUM
     5.8 +
     5.9 +The relationship between dataflow analysis and a welltyped-insruction predicate.
    5.10 +*)
    5.11 +
    5.12 +header "Dataflow Analysis Framework"
    5.13 +
    5.14 +theory DFA_Framework = Listn:
    5.15 +
    5.16 +constdefs
    5.17 +
    5.18 + stable :: "'s ord =>
    5.19 +           (nat => 's => 's)
    5.20 +           => (nat => nat list) => 's list => nat => bool"
    5.21 +"stable r step succs ss p == !q:set(succs p). step p (ss!p) <=_r ss!q"
    5.22 +
    5.23 + stables :: "'s ord => (nat => 's => 's)
    5.24 +            => (nat => nat list) => 's list => bool"
    5.25 +"stables r step succs ss == !p<size ss. stable r step succs ss p"
    5.26 +
    5.27 + is_dfa :: "'s ord
    5.28 +           => ('s list => 's list)
    5.29 +           => (nat => 's => 's)
    5.30 +           => (nat => nat list)
    5.31 +           => nat => 's set => bool"
    5.32 +"is_dfa r dfa step succs n A == !ss : list n A.
    5.33 +   dfa ss : list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss &
    5.34 +   (!ts: list n A. ss <=[r] ts & stables r step succs ts
    5.35 +                     --> dfa ss <=[r] ts)"
    5.36 +
    5.37 + is_bcv :: "'s ord => 's => (nat => 's => 's) => (nat => nat list)
    5.38 +           => nat => 's set => ('s list => 's list) => bool"
    5.39 +"is_bcv r T step succs n A bcv == !ss : list n A.
    5.40 +   (!p<n. (bcv ss)!p ~= T) =
    5.41 +   (? ts: list n A. ss <=[r] ts & welltyping r T step succs ts)"
    5.42 +
    5.43 + welltyping ::
    5.44 +"'s ord => 's => (nat => 's => 's) => (nat => nat list) => 's list => bool"
    5.45 +"welltyping r T step succs ts ==
    5.46 + !p<size(ts). ts!p ~= T & stable r step succs ts p"
    5.47 +
    5.48 +
    5.49 +lemma is_dfaD:
    5.50 + "[| is_dfa r dfa step succs n A; ss : list n A |] ==> 
    5.51 +  dfa ss:list n A & stables r step succs (dfa ss) & ss <=[r] dfa ss & 
    5.52 +  (!ts: list n A. stables r step succs ts & ss <=[r] ts 
    5.53 +  --> dfa ss <=[r] ts)"
    5.54 +  by (simp add: is_dfa_def)
    5.55 +
    5.56 +
    5.57 +lemma is_bcv_dfa:
    5.58 +  "[| order r; top r T; is_dfa r dfa step succs n A |] 
    5.59 +  ==> is_bcv r T step succs n A dfa"
    5.60 +apply (unfold is_bcv_def welltyping_def stables_def)
    5.61 +apply clarify
    5.62 +apply (drule is_dfaD)
    5.63 +apply assumption
    5.64 +apply clarify
    5.65 +apply (rule iffI)
    5.66 + apply (rule bexI)
    5.67 +  apply (rule conjI)
    5.68 +   apply assumption
    5.69 +  apply (simp add: stables_def)
    5.70 + apply assumption
    5.71 +apply clarify
    5.72 +apply (simp add: imp_conjR all_conj_distrib stables_def 
    5.73 +            cong: conj_cong)
    5.74 +apply (drule_tac x = ts in bspec)
    5.75 + apply assumption
    5.76 +apply (force dest: le_listD)
    5.77 +done
    5.78 +
    5.79 +end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/MicroJava/BV/DFA_err.thy	Mon Nov 20 16:37:42 2000 +0100
     6.3 @@ -0,0 +1,121 @@
     6.4 +(*  Title:      HOL/BCV/DFA_err.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Gerwin Klein
     6.7 +    Copyright   2000 TUM
     6.8 +
     6.9 +static and dynamic welltyping 
    6.10 +*)
    6.11 +
    6.12 +header "Static and Dynamic Welltyping"
    6.13 +
    6.14 +theory DFA_err = DFA_Framework:
    6.15 +
    6.16 +constdefs
    6.17 +
    6.18 +dynamic_wt :: "'s ord => (nat => 's err => 's err) => (nat => nat list) => 
    6.19 +               's err list => bool"
    6.20 +"dynamic_wt r step succs ts == welltyping (Err.le r) Err step succs ts"
    6.21 +
    6.22 +static_wt :: "'s ord => (nat => 's => bool) => 
    6.23 +              (nat => 's => 's) => (nat => nat list) =>  's list => bool"
    6.24 +"static_wt r app step succs ts == 
    6.25 +  !p < size ts. app p (ts!p) & (!q:set(succs p). step p (ts!p) <=_r ts!q)"
    6.26 +
    6.27 +err_step :: "(nat => 's => bool) => (nat => 's => 's) => 
    6.28 +             (nat => 's err => 's err)"
    6.29 +"err_step app step p == lift (%t. if app p t then OK (step p t) else Err)"
    6.30 +
    6.31 +bounded :: "(nat => nat list) => nat => bool"
    6.32 +"bounded succs n == !p<n. !q:set(succs p). q<n"
    6.33 +
    6.34 +non_empty :: "(nat => nat list) => bool"
    6.35 +"non_empty succs == !p. succs p ~= []"
    6.36 +
    6.37 +
    6.38 +lemma non_emptyD:
    6.39 +  "non_empty succs ==> ? q. q:set(succs p)"
    6.40 +proof (unfold non_empty_def)
    6.41 +  assume "!p. succs p ~= []"
    6.42 +  hence "succs p ~= []" ..
    6.43 +  then obtain x xs where "succs p = x#xs"
    6.44 +    by (auto simp add: neq_Nil_conv)
    6.45 +  thus ?thesis 
    6.46 +    by auto
    6.47 +qed
    6.48 +
    6.49 +text_raw {* \newpage *}
    6.50 +lemma dynamic_imp_static:
    6.51 +  "[| bounded succs (size ts); non_empty succs;
    6.52 +      dynamic_wt r (err_step app step) succs ts |] 
    6.53 +  ==> static_wt r app step succs (map ok_val ts)"
    6.54 +proof (unfold static_wt_def, intro strip, rule conjI)
    6.55 +
    6.56 +  assume b:  "bounded succs (size ts)"
    6.57 +  assume n:  "non_empty succs"
    6.58 +  assume wt: "dynamic_wt r (err_step app step) succs ts"
    6.59 +
    6.60 +  fix p 
    6.61 +  assume "p < length (map ok_val ts)"
    6.62 +  hence lp: "p < length ts" by simp
    6.63 +
    6.64 +  from wt lp
    6.65 +  have [intro?]: "!!p. p < length ts ==> ts ! p ~= Err" 
    6.66 +    by (unfold dynamic_wt_def welltyping_def) simp
    6.67 +
    6.68 +  show app: "app p (map ok_val ts ! p)"
    6.69 +  proof -
    6.70 +    from n
    6.71 +    obtain q where q: "q:set(succs p)"
    6.72 +      by (auto dest: non_emptyD)
    6.73 +
    6.74 +    from wt lp q
    6.75 +    obtain s where
    6.76 +      OKp:  "ts ! p = OK s" and
    6.77 +      less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
    6.78 +      by (unfold dynamic_wt_def welltyping_def stable_def) 
    6.79 +         (auto iff: not_Err_eq)
    6.80 +
    6.81 +    from lp b q
    6.82 +    have lq: "q < length ts"
    6.83 +      by (unfold bounded_def) blast
    6.84 +    hence "ts!q ~= Err" ..
    6.85 +    then
    6.86 +    obtain s' where OKq: "ts ! q = OK s'"
    6.87 +      by (auto iff: not_Err_eq)      
    6.88 +
    6.89 +    with OKp less
    6.90 +    have "app p s"
    6.91 +      by (simp add: err_step_def lift_def split: err.split_asm split_if_asm)
    6.92 +
    6.93 +    with lp OKp
    6.94 +    show ?thesis
    6.95 +      by simp
    6.96 +  qed
    6.97 +  
    6.98 +  show "!q:set(succs p). step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
    6.99 +  proof (intro strip)
   6.100 +    fix q
   6.101 +    assume q: "q:set (succs p)"
   6.102 +
   6.103 +    from wt lp q
   6.104 +    obtain s where
   6.105 +      OKp:  "ts ! p = OK s" and
   6.106 +      less: "err_step app step p (ts ! p) <=_(Err.le r) ts ! q"
   6.107 +      by (unfold dynamic_wt_def welltyping_def stable_def) 
   6.108 +         (auto iff: not_Err_eq)
   6.109 +
   6.110 +    from lp b q
   6.111 +    have lq: "q < length ts"
   6.112 +      by (unfold bounded_def) blast
   6.113 +    hence "ts!q ~= Err" ..
   6.114 +    then
   6.115 +    obtain s' where OKq: "ts ! q = OK s'"
   6.116 +      by (auto iff: not_Err_eq)      
   6.117 +
   6.118 +    from lp lq OKp OKq app less
   6.119 +    show "step p (map ok_val ts ! p) <=_r map ok_val ts ! q"
   6.120 +      by (simp add: err_step_def lift_def)
   6.121 +  qed
   6.122 +qed
   6.123 +
   6.124 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/MicroJava/BV/Err.thy	Mon Nov 20 16:37:42 2000 +0100
     7.3 @@ -0,0 +1,336 @@
     7.4 +(*  Title:      HOL/BCV/Err.thy
     7.5 +    ID:         $Id$
     7.6 +    Author:     Tobias Nipkow
     7.7 +    Copyright   2000 TUM
     7.8 +
     7.9 +The error type
    7.10 +*)
    7.11 +
    7.12 +header "The Error Type"
    7.13 +
    7.14 +theory Err = Semilat:
    7.15 +
    7.16 +datatype 'a err = Err | OK 'a
    7.17 +
    7.18 +types 'a ebinop = "'a => 'a => 'a err"
    7.19 +      'a esl =    "'a set * 'a ord * 'a ebinop"
    7.20 +
    7.21 +
    7.22 +consts
    7.23 +  ok_val :: "'a err => 'a"
    7.24 +primrec
    7.25 +  "ok_val (OK x) = x"
    7.26 +
    7.27 +
    7.28 +constdefs
    7.29 + lift :: "('a => 'b err) => ('a err => 'b err)"
    7.30 +"lift f e == case e of Err => Err | OK x => f x"
    7.31 +
    7.32 + lift2 :: "('a => 'b => 'c err) => 'a err => 'b err => 'c err"
    7.33 +"lift2 f e1 e2 ==
    7.34 + case e1 of Err  => Err
    7.35 +          | OK x => (case e2 of Err => Err | OK y => f x y)"
    7.36 +
    7.37 + le :: "'a ord => 'a err ord"
    7.38 +"le r e1 e2 ==
    7.39 +        case e2 of Err => True |
    7.40 +                   OK y => (case e1 of Err => False | OK x => x <=_r y)"
    7.41 +
    7.42 + sup :: "('a => 'b => 'c) => ('a err => 'b err => 'c err)"
    7.43 +"sup f == lift2(%x y. OK(x +_f y))"
    7.44 +
    7.45 + err :: "'a set => 'a err set"
    7.46 +"err A == insert Err {x . ? y:A. x = OK y}"
    7.47 +
    7.48 + esl :: "'a sl => 'a esl"
    7.49 +"esl == %(A,r,f). (A,r, %x y. OK(f x y))"
    7.50 +
    7.51 + sl :: "'a esl => 'a err sl"
    7.52 +"sl == %(A,r,f). (err A, le r, lift2 f)"
    7.53 +
    7.54 +syntax
    7.55 + err_semilat :: "'a esl => bool"
    7.56 +translations
    7.57 +"err_semilat L" == "semilat(Err.sl L)"
    7.58 +
    7.59 +
    7.60 +lemma not_Err_eq:
    7.61 +  "(x \<noteq> Err) = (\<exists>a. x = OK a)" 
    7.62 +  by (cases x) auto
    7.63 +
    7.64 +lemma not_OK_eq:
    7.65 +  "(\<forall>y. x \<noteq> OK y) = (x = Err)"
    7.66 +  by (cases x) auto  
    7.67 +
    7.68 +
    7.69 +lemma unfold_lesub_err:
    7.70 +  "e1 <=_(le r) e2 == le r e1 e2"
    7.71 +  by (simp add: lesub_def)
    7.72 +
    7.73 +lemma le_err_refl:
    7.74 +  "!x. x <=_r x ==> e <=_(Err.le r) e"
    7.75 +apply (unfold lesub_def Err.le_def)
    7.76 +apply (simp split: err.split)
    7.77 +done 
    7.78 +
    7.79 +lemma le_err_trans [rule_format]:
    7.80 +  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e3 --> e1 <=_(le r) e3"
    7.81 +apply (unfold unfold_lesub_err le_def)
    7.82 +apply (simp split: err.split)
    7.83 +apply (blast intro: order_trans)
    7.84 +done
    7.85 +
    7.86 +lemma le_err_antisym [rule_format]:
    7.87 +  "order r ==> e1 <=_(le r) e2 --> e2 <=_(le r) e1 --> e1=e2"
    7.88 +apply (unfold unfold_lesub_err le_def)
    7.89 +apply (simp split: err.split)
    7.90 +apply (blast intro: order_antisym)
    7.91 +done 
    7.92 +
    7.93 +lemma OK_le_err_OK:
    7.94 +  "(OK x <=_(le r) OK y) = (x <=_r y)"
    7.95 +  by (simp add: unfold_lesub_err le_def)
    7.96 +
    7.97 +lemma order_le_err [iff]:
    7.98 +  "order(le r) = order r"
    7.99 +apply (rule iffI)
   7.100 + apply (subst order_def)
   7.101 + apply (blast dest: order_antisym OK_le_err_OK [THEN iffD2]
   7.102 +              intro: order_trans OK_le_err_OK [THEN iffD1])
   7.103 +apply (subst order_def)
   7.104 +apply (blast intro: le_err_refl le_err_trans le_err_antisym
   7.105 +             dest: order_refl)
   7.106 +done 
   7.107 +
   7.108 +lemma le_Err [iff]:  "e <=_(le r) Err"
   7.109 +  by (simp add: unfold_lesub_err le_def)
   7.110 +
   7.111 +lemma Err_le_conv [iff]:
   7.112 + "Err <=_(le r) e  = (e = Err)"
   7.113 +  by (simp add: unfold_lesub_err le_def  split: err.split)
   7.114 +
   7.115 +lemma le_OK_conv [iff]:
   7.116 +  "e <=_(le r) OK x  =  (? y. e = OK y & y <=_r x)"
   7.117 +  by (simp add: unfold_lesub_err le_def split: err.split)
   7.118 +
   7.119 +lemma OK_le_conv:
   7.120 + "OK x <=_(le r) e  =  (e = Err | (? y. e = OK y & x <=_r y))"
   7.121 +  by (simp add: unfold_lesub_err le_def split: err.split)
   7.122 +
   7.123 +lemma top_Err [iff]: "top (le r) Err";
   7.124 +  by (simp add: top_def)
   7.125 +
   7.126 +lemma OK_less_conv [rule_format, iff]:
   7.127 +  "OK x <_(le r) e = (e=Err | (? y. e = OK y & x <_r y))"
   7.128 +  by (simp add: lesssub_def lesub_def le_def split: err.split)
   7.129 +
   7.130 +lemma not_Err_less [rule_format, iff]:
   7.131 +  "~(Err <_(le r) x)"
   7.132 +  by (simp add: lesssub_def lesub_def le_def split: err.split)
   7.133 +
   7.134 +lemma semilat_errI:
   7.135 +  "semilat(A,r,f) ==> semilat(err A, Err.le r, lift2(%x y. OK(f x y)))"
   7.136 +apply (unfold semilat_Def closed_def plussub_def lesub_def lift2_def Err.le_def err_def)
   7.137 +apply (simp split: err.split)
   7.138 +apply blast
   7.139 +done
   7.140 +
   7.141 +lemma err_semilat_eslI: 
   7.142 +  "!!L. semilat L ==> err_semilat(esl L)"
   7.143 +apply (unfold sl_def esl_def)
   7.144 +apply (simp (no_asm_simp) only: split_tupled_all)
   7.145 +apply (simp add: semilat_errI)
   7.146 +done
   7.147 +
   7.148 +lemma acc_err [simp, intro!]:  "acc r ==> acc(le r)"
   7.149 +apply (unfold acc_def lesub_def le_def lesssub_def)
   7.150 +apply (simp add: wf_eq_minimal split: err.split)
   7.151 +apply clarify
   7.152 +apply (case_tac "Err : Q")
   7.153 + apply blast
   7.154 +apply (erule_tac x = "{a . OK a : Q}" in allE)
   7.155 +apply (case_tac "x")
   7.156 + apply fast
   7.157 +apply blast
   7.158 +done 
   7.159 +
   7.160 +lemma Err_in_err [iff]: "Err : err A"
   7.161 +  by (simp add: err_def)
   7.162 +
   7.163 +lemma Ok_in_err [iff]: "(OK x : err A) = (x:A)"
   7.164 +  by (auto simp add: err_def)
   7.165 +
   7.166 +(** lift **)
   7.167 +
   7.168 +lemma lift_in_errI:
   7.169 +  "[| e : err S; !x:S. e = OK x --> f x : err S |] ==> lift f e : err S"
   7.170 +apply (unfold lift_def)
   7.171 +apply (simp split: err.split)
   7.172 +apply blast
   7.173 +done 
   7.174 +
   7.175 +(** lift2 **)
   7.176 +
   7.177 +lemma Err_lift2 [simp]: 
   7.178 +  "Err +_(lift2 f) x = Err"
   7.179 +  by (simp add: lift2_def plussub_def)
   7.180 +
   7.181 +lemma lift2_Err [simp]: 
   7.182 +  "x +_(lift2 f) Err = Err"
   7.183 +  by (simp add: lift2_def plussub_def split: err.split)
   7.184 +
   7.185 +lemma OK_lift2_OK [simp]:
   7.186 +  "OK x +_(lift2 f) OK y = x +_f y"
   7.187 +  by (simp add: lift2_def plussub_def split: err.split)
   7.188 +
   7.189 +(** sup **)
   7.190 +
   7.191 +lemma Err_sup_Err [simp]:
   7.192 +  "Err +_(Err.sup f) x = Err"
   7.193 +  by (simp add: plussub_def Err.sup_def Err.lift2_def)
   7.194 +
   7.195 +lemma Err_sup_Err2 [simp]:
   7.196 +  "x +_(Err.sup f) Err = Err"
   7.197 +  by (simp add: plussub_def Err.sup_def Err.lift2_def split: err.split)
   7.198 +
   7.199 +lemma Err_sup_OK [simp]:
   7.200 +  "OK x +_(Err.sup f) OK y = OK(x +_f y)"
   7.201 +  by (simp add: plussub_def Err.sup_def Err.lift2_def)
   7.202 +
   7.203 +lemma Err_sup_eq_OK_conv [iff]:
   7.204 +  "(Err.sup f ex ey = OK z) = (? x y. ex = OK x & ey = OK y & f x y = z)"
   7.205 +apply (unfold Err.sup_def lift2_def plussub_def)
   7.206 +apply (rule iffI)
   7.207 + apply (simp split: err.split_asm)
   7.208 +apply clarify
   7.209 +apply simp
   7.210 +done
   7.211 +
   7.212 +lemma Err_sup_eq_Err [iff]:
   7.213 +  "(Err.sup f ex ey = Err) = (ex=Err | ey=Err)"
   7.214 +apply (unfold Err.sup_def lift2_def plussub_def)
   7.215 +apply (simp split: err.split)
   7.216 +done 
   7.217 +
   7.218 +(*** semilat (err A) (le r) f ***)
   7.219 +
   7.220 +lemma semilat_le_err_Err_plus [simp]:
   7.221 +  "[| x: err A; semilat(err A, le r, f) |] ==> Err +_f x = Err"
   7.222 +  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
   7.223 +
   7.224 +lemma semilat_le_err_plus_Err [simp]:
   7.225 +  "[| x: err A; semilat(err A, le r, f) |] ==> x +_f Err = Err"
   7.226 +  by (blast intro: le_iff_plus_unchanged [THEN iffD1] le_iff_plus_unchanged2 [THEN iffD1])
   7.227 +
   7.228 +lemma semilat_le_err_OK1:
   7.229 +  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
   7.230 +  ==> x <=_r z";
   7.231 +apply (rule OK_le_err_OK [THEN iffD1])
   7.232 +apply (erule subst)
   7.233 +apply simp
   7.234 +done 
   7.235 +
   7.236 +lemma semilat_le_err_OK2:
   7.237 +  "[| x:A; y:A; semilat(err A, le r, f); OK x +_f OK y = OK z |] 
   7.238 +  ==> y <=_r z"
   7.239 +apply (rule OK_le_err_OK [THEN iffD1])
   7.240 +apply (erule subst)
   7.241 +apply simp
   7.242 +done 
   7.243 +
   7.244 +lemma eq_order_le:
   7.245 +  "[| x=y; order r |] ==> x <=_r y"
   7.246 +apply (unfold order_def)
   7.247 +apply blast
   7.248 +done
   7.249 +
   7.250 +lemma OK_plus_OK_eq_Err_conv [simp]:
   7.251 +  "[| x:A; y:A; semilat(err A, le r, fe) |] ==> 
   7.252 +  ((OK x) +_fe (OK y) = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   7.253 +proof -
   7.254 +  have plus_le_conv3: "!!A x y z f r. 
   7.255 +    [| semilat (A,r,f); x +_f y <=_r z; x:A; y:A; z:A |] 
   7.256 +    ==> x <=_r z \<and> y <=_r z"
   7.257 +    by (rule plus_le_conv [THEN iffD1])
   7.258 +  case antecedent
   7.259 +  thus ?thesis
   7.260 +  apply (rule_tac iffI)
   7.261 +   apply clarify
   7.262 +   apply (drule OK_le_err_OK [THEN iffD2])
   7.263 +   apply (drule OK_le_err_OK [THEN iffD2])
   7.264 +   apply (drule semilat_lub)
   7.265 +        apply assumption
   7.266 +       apply assumption
   7.267 +      apply simp
   7.268 +     apply simp
   7.269 +    apply simp
   7.270 +   apply simp
   7.271 +  apply (case_tac "(OK x) +_fe (OK y)")
   7.272 +   apply assumption
   7.273 +  apply (rename_tac z)
   7.274 +  apply (subgoal_tac "OK z: err A")
   7.275 +  apply (drule eq_order_le)
   7.276 +    apply blast
   7.277 +   apply (blast dest: plus_le_conv3) 
   7.278 +  apply (erule subst)
   7.279 +  apply (blast intro: closedD)
   7.280 +  done 
   7.281 +qed
   7.282 +
   7.283 +(*** semilat (err(Union AS)) ***)
   7.284 +
   7.285 +(* FIXME? *)
   7.286 +lemma all_bex_swap_lemma [iff]:
   7.287 +  "(!x. (? y:A. x = f y) --> P x) = (!y:A. P(f y))"
   7.288 +  by blast
   7.289 +
   7.290 +lemma closed_err_Union_lift2I: 
   7.291 +  "[| !A:AS. closed (err A) (lift2 f); AS ~= {}; 
   7.292 +      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. a +_f b = Err) |] 
   7.293 +  ==> closed (err(Union AS)) (lift2 f)"
   7.294 +apply (unfold closed_def err_def)
   7.295 +apply simp
   7.296 +apply clarify
   7.297 +apply simp
   7.298 +apply fast
   7.299 +done 
   7.300 +
   7.301 +(* If AS = {} the thm collapses to
   7.302 +   order r & closed {Err} f & Err +_f Err = Err
   7.303 +   which may not hold *)
   7.304 +lemma err_semilat_UnionI:
   7.305 +  "[| !A:AS. err_semilat(A, r, f); AS ~= {}; 
   7.306 +      !A:AS.!B:AS. A~=B --> (!a:A.!b:B. ~ a <=_r b & a +_f b = Err) |] 
   7.307 +  ==> err_semilat(Union AS, r, f)"
   7.308 +apply (unfold semilat_def sl_def)
   7.309 +apply (simp add: closed_err_Union_lift2I)
   7.310 +apply (rule conjI)
   7.311 + apply blast
   7.312 +apply (simp add: err_def)
   7.313 +apply (rule conjI)
   7.314 + apply clarify
   7.315 + apply (rename_tac A a u B b)
   7.316 + apply (case_tac "A = B")
   7.317 +  apply simp
   7.318 + apply simp
   7.319 +apply (rule conjI)
   7.320 + apply clarify
   7.321 + apply (rename_tac A a u B b)
   7.322 + apply (case_tac "A = B")
   7.323 +  apply simp
   7.324 + apply simp
   7.325 +apply clarify
   7.326 +apply (rename_tac A ya yb B yd z C c a b)
   7.327 +apply (case_tac "A = B")
   7.328 + apply (case_tac "A = C")
   7.329 +  apply simp
   7.330 + apply (rotate_tac -1)
   7.331 + apply simp
   7.332 +apply (rotate_tac -1)
   7.333 +apply (case_tac "B = C")
   7.334 + apply simp
   7.335 +apply (rotate_tac -1)
   7.336 +apply simp
   7.337 +done 
   7.338 +
   7.339 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/MicroJava/BV/Kildall.thy	Mon Nov 20 16:37:42 2000 +0100
     8.3 @@ -0,0 +1,445 @@
     8.4 +(*  Title:      HOL/BCV/Kildall.thy
     8.5 +    ID:         $Id$
     8.6 +    Author:     Tobias Nipkow
     8.7 +    Copyright   2000 TUM
     8.8 +
     8.9 +Kildall's algorithm
    8.10 +*)
    8.11 +
    8.12 +header "Kildall's Algorithm"
    8.13 +
    8.14 +theory Kildall = DFA_Framework:
    8.15 +
    8.16 +constdefs
    8.17 + bounded :: "(nat => nat list) => nat => bool"
    8.18 +"bounded succs n == !p<n. !q:set(succs p). q<n"
    8.19 +
    8.20 + pres_type :: "(nat => 's => 's) => nat => 's set => bool"
    8.21 +"pres_type step n A == !s:A. !p<n. step p s : A"
    8.22 +
    8.23 + mono :: "'s ord => (nat => 's => 's) => nat => 's set => bool"
    8.24 +"mono r step n A ==
    8.25 + !s p t. s : A & p < n & s <=_r t --> step p s <=_r step p t"
    8.26 +
    8.27 +consts
    8.28 + iter :: "('s sl * (nat => 's => 's) * (nat => nat list))
    8.29 +          * 's list * nat set => 's list"
    8.30 + propa :: "'s binop => nat list => 's => 's list => nat set => 's list * nat set"
    8.31 +
    8.32 +primrec
    8.33 +"propa f []     t ss w = (ss,w)"
    8.34 +"propa f (q#qs) t ss w = (let u = t +_f ss!q;
    8.35 +                              w' = (if u = ss!q then w else insert q w)
    8.36 +                          in propa f qs t (ss[q := u]) w')"
    8.37 +
    8.38 +recdef iter
    8.39 + "same_fst (%((A,r,f),step,succs). semilat(A,r,f) & acc r)
    8.40 +         (%((A,r,f),step,succs).
    8.41 +  {(ss',ss) . ss <[r] ss'} <*lex*> finite_psubset)"
    8.42 +"iter(((A,r,f),step,succs),ss,w) =
    8.43 +  (if semilat(A,r,f) & acc r & (!p:w. p < size ss) &
    8.44 +      bounded succs (size ss) & set ss <= A & pres_type step (size ss) A
    8.45 +   then if w={} then ss
    8.46 +        else let p = SOME p. p : w
    8.47 +             in iter(((A,r,f),step,succs),
    8.48 +                     propa f (succs p) (step p (ss!p)) ss (w-{p}))
    8.49 +   else arbitrary)"
    8.50 +
    8.51 +constdefs
    8.52 + unstables ::
    8.53 + "'s binop => (nat => 's => 's) => (nat => nat list) => 's list => nat set"
    8.54 +"unstables f step succs ss ==
    8.55 + {p. p < size ss & (? q:set(succs p). step p (ss!p) +_f ss!q ~= ss!q)}"
    8.56 +
    8.57 + kildall :: "'s sl => (nat => 's => 's) => (nat => nat list)
    8.58 +             => 's list => 's list"
    8.59 +"kildall Arf step succs ss ==
    8.60 + iter((Arf,step,succs),ss,unstables (snd(snd Arf)) step succs ss)"
    8.61 +
    8.62 +consts merges :: "'s binop => 's => nat list => 's list => 's list"
    8.63 +primrec
    8.64 +"merges f s []     ss = ss"
    8.65 +"merges f s (p#ps) ss = merges f s ps (ss[p := s +_f ss!p])"
    8.66 +
    8.67 +
    8.68 +lemmas [simp] = Let_def le_iff_plus_unchanged [symmetric];
    8.69 +
    8.70 +
    8.71 +lemma pres_typeD:
    8.72 +  "[| pres_type step n A; s:A; p<n |] ==> step p s : A"
    8.73 +  by (unfold pres_type_def, blast)
    8.74 +
    8.75 +lemma boundedD:
    8.76 +  "[| bounded succs n; p < n; q : set(succs p) |] ==> q < n"
    8.77 +  by (unfold bounded_def, blast)
    8.78 +
    8.79 +lemma monoD:
    8.80 +  "[| mono r step n A; p < n; s:A; s <=_r t |] ==> step p s <=_r step p t"
    8.81 +  by (unfold mono_def, blast)
    8.82 +
    8.83 +(** merges **)
    8.84 +
    8.85 +lemma length_merges [rule_format, simp]:
    8.86 +  "!ss. size(merges f t ps ss) = size ss"
    8.87 +  by (induct_tac ps, auto)
    8.88 +
    8.89 +lemma merges_preserves_type [rule_format, simp]:
    8.90 +  "[| semilat(A,r,f) |] ==> 
    8.91 +     !xs. xs : list n A --> x : A --> (!p : set ps. p<n) 
    8.92 +          --> merges f x ps xs : list n A"
    8.93 +  apply (frule semilatDclosedI)
    8.94 +  apply (unfold closed_def)
    8.95 +  apply (induct_tac ps)
    8.96 +  apply auto
    8.97 +  done
    8.98 +
    8.99 +lemma merges_incr [rule_format]:
   8.100 +  "[| semilat(A,r,f) |] ==> 
   8.101 +     !xs. xs : list n A --> x : A --> (!p:set ps. p<size xs) --> xs <=[r] merges f x ps xs"
   8.102 +  apply (induct_tac ps)
   8.103 +   apply simp
   8.104 +  apply simp
   8.105 +  apply clarify
   8.106 +  apply (rule order_trans)
   8.107 +    apply simp
   8.108 +   apply (erule list_update_incr)
   8.109 +     apply assumption
   8.110 +    apply simp
   8.111 +   apply simp
   8.112 +  apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
   8.113 +  done
   8.114 +
   8.115 +lemma merges_same_conv [rule_format]:
   8.116 +  "[| semilat(A,r,f) |] ==> 
   8.117 +     (!xs. xs : list n A --> x:A --> (!p:set ps. p<size xs) --> 
   8.118 +     (merges f x ps xs = xs) = (!p:set ps. x <=_r xs!p))"
   8.119 +  apply (induct_tac ps)
   8.120 +   apply simp
   8.121 +  apply clarsimp
   8.122 +  apply (rename_tac p ps xs)
   8.123 +  apply (rule iffI)
   8.124 +   apply (rule context_conjI)
   8.125 +    apply (subgoal_tac "xs[p := x +_f xs!p] <=[r] xs")
   8.126 +     apply (force dest!: le_listD simp add: nth_list_update)
   8.127 +    apply (erule subst, rule merges_incr)
   8.128 +        apply assumption
   8.129 +       apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in])
   8.130 +     apply assumption
   8.131 +    apply simp
   8.132 +   apply clarify
   8.133 +   apply (rotate_tac -2)
   8.134 +   apply (erule allE)
   8.135 +   apply (erule impE)
   8.136 +    apply assumption
   8.137 +   apply (erule impE)
   8.138 +    apply assumption
   8.139 +   apply (drule bspec)
   8.140 +    apply assumption
   8.141 +   apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
   8.142 +  apply clarify 
   8.143 +  apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2])
   8.144 +  done
   8.145 +
   8.146 +
   8.147 +lemma list_update_le_listI [rule_format]:
   8.148 +  "set xs <= A --> set ys <= A --> xs <=[r] ys --> p < size xs -->  
   8.149 +   x <=_r ys!p --> semilat(A,r,f) --> x:A --> 
   8.150 +   xs[p := x +_f xs!p] <=[r] ys"
   8.151 +  apply (unfold Listn.le_def lesub_def semilat_def)
   8.152 +  apply (simp add: list_all2_conv_all_nth nth_list_update)
   8.153 +  done
   8.154 +
   8.155 +lemma merges_pres_le_ub:
   8.156 +  "[| semilat(A,r,f); t:A; set ts <= A; set ss <= A; 
   8.157 +     !p. p:set ps --> t <=_r ts!p; 
   8.158 +     !p. p:set ps --> p<size ts; 
   8.159 +     ss <=[r] ts |] 
   8.160 +  ==> merges f t ps ss <=[r] ts"
   8.161 +proof -
   8.162 +  { fix A r f t ts ps
   8.163 +    have
   8.164 +    "!!qs. [| semilat(A,r,f); set ts <= A; t:A; 
   8.165 +       !p. p:set ps --> t <=_r ts!p; 
   8.166 +       !p. p:set ps --> p<size ts |] ==> 
   8.167 +    set qs <= set ps  --> 
   8.168 +    (!ss. set ss <= A --> ss <=[r] ts --> merges f t qs ss <=[r] ts)"
   8.169 +    apply (induct_tac qs)
   8.170 +     apply simp
   8.171 +    apply (simp (no_asm_simp))
   8.172 +    apply clarify
   8.173 +    apply (rotate_tac -2)
   8.174 +    apply simp
   8.175 +    apply (erule allE, erule impE, erule_tac [2] mp)
   8.176 +     apply (simp (no_asm_simp) add: closedD)
   8.177 +    apply (simp add: list_update_le_listI)
   8.178 +    done
   8.179 +  } note this [dest]
   8.180 +  
   8.181 +  case antecedent
   8.182 +  thus ?thesis by blast
   8.183 +qed
   8.184 +
   8.185 +
   8.186 +lemma nth_merges [rule_format]:
   8.187 +  "[| semilat (A, r, f); t:A; p < n |] ==> !ss. ss : list n A --> 
   8.188 +     (!p:set ps. p<n) --> 
   8.189 +     (merges f t ps ss)!p = (if p : set ps then t +_f ss!p else ss!p)"
   8.190 +  apply (induct_tac "ps")
   8.191 +   apply simp
   8.192 +  apply (simp add: nth_list_update closedD listE_nth_in) 
   8.193 +  done
   8.194 +
   8.195 +
   8.196 +(** propa **)
   8.197 +
   8.198 +lemma decomp_propa [rule_format]:
   8.199 +  "!ss w. (!q:set qs. q < size ss) --> 
   8.200 +   propa f qs t ss w = 
   8.201 +   (merges f t qs ss, {q. q:set qs & t +_f ss!q ~= ss!q} Un w)"
   8.202 +  apply (induct_tac qs)
   8.203 +   apply simp
   8.204 +  apply (simp (no_asm))
   8.205 +  apply clarify
   8.206 +  apply (rule conjI)
   8.207 +   apply (simp add: nth_list_update)
   8.208 +   apply blast
   8.209 +  apply (simp add: nth_list_update)
   8.210 +  apply blast
   8.211 +  done 
   8.212 +
   8.213 +(** iter **)
   8.214 +
   8.215 +ML_setup {*
   8.216 +let
   8.217 +val thy = the_context ()
   8.218 +val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
   8.219 +in
   8.220 +goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_wf));
   8.221 +by (REPEAT(rtac wf_same_fstI 1));
   8.222 +by (split_all_tac 1);
   8.223 +by (asm_full_simp_tac (simpset() addsimps [thm "lesssub_def"]) 1);
   8.224 +by (REPEAT(rtac wf_same_fstI 1));
   8.225 +by (rtac wf_lex_prod 1);
   8.226 + by (rtac wf_finite_psubset 2);
   8.227 +by (Clarify_tac 1);
   8.228 +by (dtac (thm "semilatDorderI" RS (thm "acc_le_listI")) 1);
   8.229 + by (assume_tac 1);
   8.230 +by (rewrite_goals_tac [thm "acc_def",thm "lesssub_def"]);
   8.231 +by (assume_tac 1);
   8.232 +qed "iter_wf"
   8.233 +end
   8.234 +*}
   8.235 +
   8.236 +lemma inter_tc_lemma:  
   8.237 +  "[| semilat(A,r,f); ss : list n A; t:A; ! q:set qs. q < n; p:w |] ==> 
   8.238 +      ss <[r] merges f t qs ss | 
   8.239 +  merges f t qs ss = ss & {q. q:set qs & t +_f ss!q ~= ss!q} Un (w-{p}) < w"
   8.240 +  apply (unfold lesssub_def)
   8.241 +  apply (simp (no_asm_simp) add: merges_incr)
   8.242 +  apply (rule impI)
   8.243 +  apply (rule merges_same_conv [THEN iffD1, elim_format]) 
   8.244 +  apply assumption+
   8.245 +    defer
   8.246 +    apply (rule sym, assumption)
   8.247 +   apply (simp cong add: conj_cong add: le_iff_plus_unchanged [symmetric])
   8.248 +   apply (blast intro!: psubsetI elim: equalityE)
   8.249 +  apply simp
   8.250 +  done
   8.251 +
   8.252 +ML_setup {*
   8.253 +let
   8.254 +val thy = the_context ()
   8.255 +val [iter_wf,iter_tc] = RecdefPackage.tcs_of thy "iter";
   8.256 +in
   8.257 +goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop iter_tc)); 
   8.258 +by (asm_simp_tac (simpset() addsimps [same_fst_def,thm "pres_type_def"]) 1);
   8.259 +by (clarify_tac (claset() delrules [disjCI]) 1);
   8.260 +by (subgoal_tac "(@p. p:w) : w" 1);
   8.261 + by (fast_tac (claset() addIs [someI]) 2);
   8.262 +by (subgoal_tac "ss : list (size ss) A" 1);
   8.263 + by (blast_tac (claset() addSIs [thm "listI"]) 2);
   8.264 +by (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss" 1);
   8.265 + by (blast_tac (claset() addDs [thm "boundedD"]) 2);
   8.266 +by (rotate_tac 1 1);
   8.267 +by (asm_full_simp_tac (simpset() delsimps [thm "listE_length"]
   8.268 +      addsimps [thm "decomp_propa",finite_psubset_def,thm "inter_tc_lemma",
   8.269 +                bounded_nat_set_is_finite]) 1);
   8.270 +qed "iter_tc"
   8.271 +end
   8.272 +*}
   8.273 +
   8.274 +
   8.275 +lemma iter_induct:
   8.276 +  "(!!A r f step succs ss w. 
   8.277 +    (!p. p = (@ p. p : w) & w ~= {} & semilat(A,r,f) & acc r & 
   8.278 +      (!p:w. p < length ss) & bounded succs (length ss) & 
   8.279 +         set ss <= A & pres_type step (length ss) A 
   8.280 +         --> P A r f step succs (merges f (step p (ss!p)) (succs p) ss) 
   8.281 +             ({q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))
   8.282 +  ==> P A r f step succs ss w) ==> P A r f step succs ss w"
   8.283 +proof -
   8.284 +  case antecedent
   8.285 +  show ?thesis
   8.286 +    apply (rule_tac P = P in iter_tc [THEN iter_wf [THEN iter.induct]])
   8.287 +    apply (rule antecedent)
   8.288 +    apply clarify
   8.289 +    apply simp
   8.290 +    apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
   8.291 +     apply (rotate_tac -1)
   8.292 +     apply (simp add: decomp_propa)
   8.293 +    apply (subgoal_tac "(@p. p:w) : w")
   8.294 +     apply (blast dest: boundedD)
   8.295 +    apply (fast intro: someI)
   8.296 +    done
   8.297 +qed
   8.298 +
   8.299 +lemma iter_unfold:
   8.300 + "[| semilat(A,r,f); acc r; set ss <= A; pres_type step (length ss) A; 
   8.301 +    bounded succs (size ss); !p:w. p<size ss |] ==> 
   8.302 + iter(((A,r,f),step,succs),ss,w) = 
   8.303 + (if w={} then ss 
   8.304 +  else let p = SOME p. p : w 
   8.305 +       in iter(((A,r,f),step,succs),merges f (step p (ss!p)) (succs p) ss, 
   8.306 +        {q. q:set(succs p) & step p (ss!p) +_f ss!q ~= ss!q} Un (w-{p})))"
   8.307 +  apply (rule iter_tc [THEN iter_wf [THEN iter.simps [THEN trans]]])
   8.308 +  apply simp
   8.309 +  apply (rule impI)
   8.310 +  apply (subst decomp_propa)
   8.311 +   apply (subgoal_tac "(@p. p:w) : w")
   8.312 +    apply (blast dest: boundedD)
   8.313 +   apply (fast intro: someI)
   8.314 +  apply simp
   8.315 +  done
   8.316 +
   8.317 +lemma stable_pres_lemma:
   8.318 +  "[| semilat (A,r,f); pres_type step n A; bounded succs n; 
   8.319 +     ss : list n A; p : w; ! q:w. q < n; 
   8.320 +     ! q. q < n --> q ~: w --> stable r step succs ss q; q < n; 
   8.321 +     q : set (succs p) --> step p (ss ! p) +_f ss ! q = ss ! q; 
   8.322 +     q ~: w | q = p  |] 
   8.323 +  ==> stable r step succs (merges f (step p (ss!p)) (succs p) ss) q"
   8.324 +  apply (unfold stable_def)
   8.325 +  apply (subgoal_tac "step p (ss!p) : A")
   8.326 +   defer
   8.327 +   apply (blast intro: listE_nth_in pres_typeD)     
   8.328 +  apply simp
   8.329 +  apply clarify
   8.330 +  apply (subst nth_merges)
   8.331 +       apply assumption
   8.332 +      apply assumption
   8.333 +     prefer 2
   8.334 +     apply assumption
   8.335 +    apply (blast dest: boundedD)
   8.336 +   apply (blast dest: boundedD)  
   8.337 +  apply (subst nth_merges)
   8.338 +       apply assumption
   8.339 +      apply assumption
   8.340 +     prefer 2
   8.341 +     apply assumption
   8.342 +    apply (blast dest: boundedD)
   8.343 +   apply (blast dest: boundedD)  
   8.344 +  apply simp
   8.345 +  apply (rule conjI)
   8.346 +   apply clarify
   8.347 +   apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
   8.348 +                intro: order_trans dest: boundedD)
   8.349 +  apply (blast intro!: semilat_ub1 semilat_ub2 listE_nth_in
   8.350 +               intro: order_trans dest: boundedD)
   8.351 +  done
   8.352 +
   8.353 +lemma merges_bounded_lemma [rule_format]:
   8.354 +  "[| semilat (A,r,f); mono r step n A; bounded succs n; 
   8.355 +     step p (ss!p) : A; ss : list n A; ts : list n A; p < n; 
   8.356 +     ss <=[r] ts; ! p. p < n --> stable r step succs ts p |] 
   8.357 +  ==> merges f (step p (ss!p)) (succs p) ss <=[r] ts"
   8.358 +  apply (unfold stable_def)
   8.359 +  apply (blast intro!: listE_set monoD listE_nth_in le_listD less_lengthI
   8.360 +               intro: merges_pres_le_ub order_trans
   8.361 +               dest: pres_typeD boundedD)
   8.362 +  done
   8.363 +
   8.364 +ML_setup {*
   8.365 +Unify.trace_bound := 80;
   8.366 +Unify.search_bound := 90;
   8.367 +*}
   8.368 +
   8.369 +lemma iter_properties [rule_format]:
   8.370 +  "semilat(A,r,f) & acc r & pres_type step n A & mono r step n A & 
   8.371 +  bounded succs n & (! p:w. p < n) & ss:list n A & 
   8.372 +  (!p<n. p~:w --> stable r step succs ss p) 
   8.373 +  --> iter(((A,r,f),step,succs),ss,w) : list n A & 
   8.374 +      stables r step succs (iter(((A,r,f),step,succs),ss,w)) & 
   8.375 +      ss <=[r] iter(((A,r,f),step,succs),ss,w) & 
   8.376 +      (! ts:list n A. 
   8.377 +           ss <=[r] ts & stables r step succs ts --> 
   8.378 +           iter(((A,r,f),step,succs),ss,w) <=[r] ts)"
   8.379 +  apply (unfold stables_def)
   8.380 +  apply (rule_tac A = A and r = r and f = f and step = step and ss = ss and w = w in iter_induct)
   8.381 +  apply clarify
   8.382 +  apply (frule listE_length)
   8.383 +  apply hypsubst
   8.384 +  apply (subst iter_unfold)
   8.385 +        apply assumption
   8.386 +       apply assumption
   8.387 +      apply (simp (no_asm_simp))
   8.388 +     apply assumption
   8.389 +    apply assumption
   8.390 +   apply assumption
   8.391 +  apply (simp (no_asm_simp) del: listE_length)
   8.392 +  apply (rule impI)
   8.393 +  apply (erule allE)
   8.394 +  apply (erule impE)
   8.395 +   apply (simp (no_asm_simp) del: listE_length)   
   8.396 +  apply (subgoal_tac "(@p. p:w) : w")
   8.397 +   prefer 2
   8.398 +   apply (fast intro: someI)
   8.399 +  apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
   8.400 +   prefer 2
   8.401 +   apply (blast intro: pres_typeD listE_nth_in)
   8.402 +  apply (erule impE)
   8.403 +   apply (simp (no_asm_simp) del: listE_length le_iff_plus_unchanged [symmetric])
   8.404 +   apply (rule conjI)
   8.405 +    apply (blast dest: boundedD)
   8.406 +   apply (rule conjI)
   8.407 +    apply (blast intro: merges_preserves_type dest: boundedD)
   8.408 +   apply clarify
   8.409 +   apply (blast intro!: stable_pres_lemma)
   8.410 +  apply (simp (no_asm_simp) del: listE_length)
   8.411 +  apply (subgoal_tac "!q:set(succs (@ p. p : w)). q < size ss")
   8.412 +   prefer 2
   8.413 +   apply (blast dest: boundedD)
   8.414 +  apply (subgoal_tac "step (@ p. p : w) (ss ! (@ p. p : w)) : A")
   8.415 +   prefer 2
   8.416 +   apply (blast intro: pres_typeD)
   8.417 +  apply (rule conjI)
   8.418 +   apply (blast intro!: merges_incr intro: le_list_trans)
   8.419 +  apply clarify
   8.420 +  apply (drule bspec, assumption, erule mp)
   8.421 +  apply (simp del: listE_length)
   8.422 +  apply (blast intro: merges_bounded_lemma)
   8.423 +  done
   8.424 +
   8.425 +
   8.426 +lemma is_dfa_kildall:
   8.427 +  "[| semilat(A,r,f); acc r; pres_type step n A; 
   8.428 +     mono r step n A; bounded succs n|] 
   8.429 +  ==> is_dfa r (kildall (A,r,f) step succs) step succs n A"
   8.430 +  apply (unfold is_dfa_def kildall_def)
   8.431 +  apply clarify
   8.432 +  apply simp
   8.433 +  apply (rule iter_properties)
   8.434 +  apply (simp add: unstables_def stable_def)
   8.435 +  apply (blast intro!: le_iff_plus_unchanged [THEN iffD2] listE_nth_in
   8.436 +               dest: boundedD pres_typeD)
   8.437 +  done
   8.438 +
   8.439 +lemma is_bcv_kildall:
   8.440 +  "[| semilat(A,r,f); acc r; top r T; 
   8.441 +      pres_type step n A; bounded succs n; 
   8.442 +      mono r step n A |]
   8.443 +  ==> is_bcv r T step succs n A (kildall (A,r,f) step succs)"
   8.444 +  apply (intro is_bcv_dfa is_dfa_kildall semilatDorderI)
   8.445 +  apply assumption+
   8.446 +  done
   8.447 +
   8.448 +end
     9.1 --- a/src/HOL/MicroJava/BV/LBVComplete.thy	Sat Nov 18 19:48:34 2000 +0100
     9.2 +++ b/src/HOL/MicroJava/BV/LBVComplete.thy	Mon Nov 20 16:37:42 2000 +0100
     9.3 @@ -83,44 +83,41 @@
     9.4                             
     9.5  
     9.6  lemma wtl_inst_mono:
     9.7 -  "[| wtl_inst i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
     9.8 +  "[| wtl_inst i G rT s1 cert mpc pc = OK s1'; fits ins cert phi; 
     9.9        pc < length ins;  G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
    9.10 -  \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
    9.11 +  \<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
    9.12  proof -
    9.13    assume pc:   "pc < length ins" "i = ins!pc"
    9.14 -  assume wtl:  "wtl_inst i G rT s1 cert mpc pc = Ok s1'"
    9.15 +  assume wtl:  "wtl_inst i G rT s1 cert mpc pc = OK s1'"
    9.16    assume fits: "fits ins cert phi"
    9.17    assume G:    "G \<turnstile> s2 <=' s1"
    9.18    
    9.19    let "?step s" = "step i G s"
    9.20  
    9.21    from wtl G
    9.22 -  have app: "app i G rT s2" by (auto simp add: wtl_inst_Ok app_mono)
    9.23 +  have app: "app i G rT s2" by (auto simp add: wtl_inst_OK app_mono)
    9.24    
    9.25    from wtl G
    9.26 -  have step: "succs i pc \<noteq> [] ==> G \<turnstile> ?step s2 <=' ?step s1" 
    9.27 -    by - (drule step_mono, auto simp add: wtl_inst_Ok)
    9.28 +  have step: "G \<turnstile> ?step s2 <=' ?step s1" 
    9.29 +    by (auto intro: step_mono simp add: wtl_inst_OK)
    9.30  
    9.31 -  {
    9.32 +  { also
    9.33      fix pc'
    9.34 -    assume 0: "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
    9.35 -    hence "succs i pc \<noteq> []" by auto
    9.36 -    hence "G \<turnstile> ?step s2 <=' ?step s1" by (rule step)
    9.37 -    also 
    9.38 -    from wtl 0
    9.39 +    assume "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1"
    9.40 +    with wtl 
    9.41      have "G \<turnstile> ?step s1 <=' cert!pc'"
    9.42 -      by (auto simp add: wtl_inst_Ok) 
    9.43 +      by (auto simp add: wtl_inst_OK) 
    9.44      finally
    9.45      have "G\<turnstile> ?step s2 <=' cert!pc'" .
    9.46    } note cert = this
    9.47      
    9.48 -  have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = Ok s2' \<and> G \<turnstile> s2' <=' s1'"
    9.49 +  have "\<exists>s2'. wtl_inst i G rT s2 cert mpc pc = OK s2' \<and> G \<turnstile> s2' <=' s1'"
    9.50    proof (cases "pc+1 \<in> set (succs i pc)")
    9.51      case True
    9.52      with wtl
    9.53 -    have s1': "s1' = ?step s1" by (simp add: wtl_inst_Ok)
    9.54 +    have s1': "s1' = ?step s1" by (simp add: wtl_inst_OK)
    9.55  
    9.56 -    have "wtl_inst i G rT s2 cert mpc pc = Ok (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'" 
    9.57 +    have "wtl_inst i G rT s2 cert mpc pc = OK (?step s2) \<and> G \<turnstile> ?step s2 <=' s1'" 
    9.58        (is "?wtl \<and> ?G")
    9.59      proof
    9.60        from True s1'
    9.61 @@ -128,17 +125,17 @@
    9.62  
    9.63        from True app wtl
    9.64        show ?wtl
    9.65 -        by (clarsimp intro!: cert simp add: wtl_inst_Ok)
    9.66 +        by (clarsimp intro!: cert simp add: wtl_inst_OK)
    9.67      qed
    9.68      thus ?thesis by blast
    9.69    next
    9.70      case False
    9.71      with wtl
    9.72 -    have "s1' = cert ! Suc pc" by (simp add: wtl_inst_Ok)
    9.73 +    have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK)
    9.74  
    9.75      with False app wtl
    9.76 -    have "wtl_inst i G rT s2 cert mpc pc = Ok s1' \<and> G \<turnstile> s1' <=' s1'"
    9.77 -      by (clarsimp intro!: cert simp add: wtl_inst_Ok)
    9.78 +    have "wtl_inst i G rT s2 cert mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'"
    9.79 +      by (clarsimp intro!: cert simp add: wtl_inst_OK)
    9.80  
    9.81      thus ?thesis by blast
    9.82    qed
    9.83 @@ -148,11 +145,11 @@
    9.84  
    9.85  
    9.86  lemma wtl_cert_mono:
    9.87 -  "[| wtl_cert i G rT s1 cert mpc pc = Ok s1'; fits ins cert phi; 
    9.88 +  "[| wtl_cert i G rT s1 cert mpc pc = OK s1'; fits ins cert phi; 
    9.89        pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc |] ==>
    9.90 -  \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = Ok s2' \<and> (G \<turnstile> s2' <=' s1')"
    9.91 +  \<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')"
    9.92  proof -
    9.93 -  assume wtl:  "wtl_cert i G rT s1 cert mpc pc = Ok s1'" and
    9.94 +  assume wtl:  "wtl_cert i G rT s1 cert mpc pc = OK s1'" and
    9.95           fits: "fits ins cert phi" "pc < length ins"
    9.96                 "G \<turnstile> s2 <=' s1" "i = ins!pc"
    9.97  
    9.98 @@ -170,11 +167,11 @@
    9.99        by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits)
   9.100  
   9.101      from Some wtl
   9.102 -    have "wtl_inst i G rT (Some a) cert mpc pc = Ok s1'" 
   9.103 +    have "wtl_inst i G rT (Some a) cert mpc pc = OK s1'" 
   9.104        by (simp add: wtl_cert_def split: if_splits)
   9.105  
   9.106      with G fits
   9.107 -    have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = Ok s2' \<and> 
   9.108 +    have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mpc pc = OK s2' \<and> 
   9.109                   (G \<turnstile> s2' <=' s1')"
   9.110        by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+)
   9.111      
   9.112 @@ -209,23 +206,23 @@
   9.113  
   9.114    from app pc cert pc'
   9.115    show ?thesis
   9.116 -    by (auto simp add: wtl_inst_Ok)
   9.117 +    by (auto simp add: wtl_inst_OK)
   9.118  qed
   9.119  
   9.120  lemma wt_less_wtl:
   9.121    "[| wt_instr (ins!pc) G rT phi max_pc pc; 
   9.122 -      wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
   9.123 +      wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
   9.124        fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
   9.125    G \<turnstile> s <=' phi ! Suc pc"
   9.126  proof -
   9.127    assume wt:   "wt_instr (ins!pc) G rT phi max_pc pc" 
   9.128 -  assume wtl:  "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   9.129 +  assume wtl:  "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
   9.130    assume fits: "fits ins cert phi"
   9.131    assume pc:   "Suc pc < length ins" "length ins = max_pc"
   9.132  
   9.133    { assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)"
   9.134      with wtl         have "s = step (ins!pc) G (phi!pc)"
   9.135 -      by (simp add: wtl_inst_Ok)
   9.136 +      by (simp add: wtl_inst_OK)
   9.137      also from suc wt have "G \<turnstile> ... <=' phi!Suc pc"
   9.138        by (simp add: wt_instr_def)
   9.139      finally have ?thesis .
   9.140 @@ -236,7 +233,7 @@
   9.141      
   9.142      with wtl
   9.143      have "s = cert!Suc pc" 
   9.144 -      by (simp add: wtl_inst_Ok)
   9.145 +      by (simp add: wtl_inst_OK)
   9.146      with fits pc
   9.147      have ?thesis
   9.148        by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp)
   9.149 @@ -281,11 +278,11 @@
   9.150  
   9.151  lemma wt_less_wtl_cert:
   9.152    "[| wt_instr (ins!pc) G rT phi max_pc pc; 
   9.153 -      wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s;
   9.154 +      wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s;
   9.155        fits ins cert phi; Suc pc < length ins; length ins = max_pc |] ==> 
   9.156    G \<turnstile> s <=' phi ! Suc pc"
   9.157  proof -
   9.158 -  assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   9.159 +  assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
   9.160  
   9.161    assume wti: "wt_instr (ins!pc) G rT phi max_pc pc"
   9.162                "fits ins cert phi" 
   9.163 @@ -293,7 +290,7 @@
   9.164    
   9.165    { assume "cert!pc = None"
   9.166      with wtl
   9.167 -    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   9.168 +    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
   9.169        by (simp add: wtl_cert_def)
   9.170      with wti
   9.171      have ?thesis
   9.172 @@ -306,7 +303,7 @@
   9.173      have "cert!pc = phi!pc"
   9.174        by - (rule fitsD2, simp+)
   9.175      with c wtl
   9.176 -    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = Ok s"
   9.177 +    have "wtl_inst (ins!pc) G rT (phi!pc) cert max_pc pc = OK s"
   9.178        by (simp add: wtl_cert_def)
   9.179      with wti
   9.180      have ?thesis
   9.181 @@ -378,13 +375,13 @@
   9.182  
   9.183        from c wti fits l True
   9.184        obtain s'' where
   9.185 -        "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = Ok s''"
   9.186 +        "wtl_cert (all_ins!pc) G rT (phi!pc) cert (length all_ins) pc = OK s''"
   9.187          "G \<turnstile> s'' <=' phi ! Suc pc"
   9.188          by clarsimp (drule wt_less_wtl_cert, auto)
   9.189        moreover
   9.190        from calculation fits G l
   9.191        obtain s' where
   9.192 -        c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = Ok s'" and
   9.193 +        c': "wtl_cert (all_ins!pc) G rT s cert (length all_ins) pc = OK s'" and
   9.194          "G \<turnstile> s' <=' s''"
   9.195          by - (drule wtl_cert_mono, auto)
   9.196        ultimately
    10.1 --- a/src/HOL/MicroJava/BV/LBVCorrect.thy	Sat Nov 18 19:48:34 2000 +0100
    10.2 +++ b/src/HOL/MicroJava/BV/LBVCorrect.thy	Mon Nov 20 16:37:42 2000 +0100
    10.3 @@ -14,7 +14,7 @@
    10.4  fits :: "[method_type,instr list,jvm_prog,ty,state_type option,certificate] => bool"
    10.5  "fits phi is G rT s0 cert == 
    10.6    (\<forall>pc s1. pc < length is -->
    10.7 -    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1 -->
    10.8 +    (wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1 -->
    10.9      (case cert!pc of None   => phi!pc = s1
   10.10                     | Some t => phi!pc = Some t)))"
   10.11  
   10.12 @@ -22,19 +22,19 @@
   10.13  make_phi :: "[instr list,jvm_prog,ty,state_type option,certificate] => method_type"
   10.14  "make_phi is G rT s0 cert == 
   10.15     map (\<lambda>pc. case cert!pc of 
   10.16 -               None   => val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
   10.17 +               None   => ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0) 
   10.18               | Some t => Some t) [0..length is(]"
   10.19  
   10.20  
   10.21  lemma fitsD_None:
   10.22    "[|fits phi is G rT s0 cert; pc < length is;
   10.23 -    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
   10.24 +    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; 
   10.25      cert ! pc = None|] ==> phi!pc = s1"
   10.26    by (auto simp add: fits_def)
   10.27  
   10.28  lemma fitsD_Some:
   10.29    "[|fits phi is G rT s0 cert; pc < length is;
   10.30 -    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = Ok s1; 
   10.31 +    wtl_inst_list (take pc is) G rT cert (length is) 0 s0 = OK s1; 
   10.32      cert ! pc = Some t|] ==> phi!pc = Some t"
   10.33    by (auto simp add: fits_def)
   10.34  
   10.35 @@ -46,7 +46,7 @@
   10.36  lemma make_phi_None:
   10.37    "[| pc < length is; cert!pc = None |] ==> 
   10.38    make_phi is G rT s0 cert ! pc = 
   10.39 -  val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
   10.40 +  ok_val (wtl_inst_list (take pc is) G rT cert (length is) 0 s0)"
   10.41    by (simp add: make_phi_def)
   10.42  
   10.43  lemma exists_phi:
   10.44 @@ -61,14 +61,14 @@
   10.45  qed
   10.46    
   10.47  lemma fits_lemma1:
   10.48 -  "[| wtl_inst_list is G rT cert (length is) 0 s = Ok s'; fits phi is G rT s cert |]
   10.49 +  "[| wtl_inst_list is G rT cert (length is) 0 s = OK s'; fits phi is G rT s cert |]
   10.50    ==> \<forall>pc t. pc < length is --> cert!pc = Some t --> phi!pc = Some t"
   10.51  proof (intro strip)
   10.52    fix pc t 
   10.53 -  assume "wtl_inst_list is G rT cert (length is) 0 s = Ok s'"
   10.54 +  assume "wtl_inst_list is G rT cert (length is) 0 s = OK s'"
   10.55    then 
   10.56    obtain s'' where
   10.57 -    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s''"
   10.58 +    "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s''"
   10.59      by (blast dest: wtl_take)
   10.60    moreover
   10.61    assume "fits phi is G rT s cert" 
   10.62 @@ -81,8 +81,8 @@
   10.63  
   10.64  lemma wtl_suc_pc:
   10.65   "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
   10.66 -     wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s';
   10.67 -     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
   10.68 +     wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s';
   10.69 +     wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
   10.70       fits phi is G rT s cert; Suc pc < length is |] ==>
   10.71    G \<turnstile> s'' <=' phi ! Suc pc"
   10.72  proof -
   10.73 @@ -90,11 +90,11 @@
   10.74    assume all:  "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
   10.75    assume fits: "fits phi is G rT s cert"
   10.76  
   10.77 -  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
   10.78 -         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''" and
   10.79 +  assume wtl:  "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
   10.80 +         wtc:  "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''" and
   10.81           pc:   "Suc pc < length is"
   10.82  
   10.83 -  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = Ok s''"
   10.84 +  hence wts: "wtl_inst_list (take (Suc pc) is) G rT cert (length is) 0 s = OK s''"
   10.85      by (rule wtl_Suc)
   10.86  
   10.87    from all
   10.88 @@ -111,7 +111,7 @@
   10.89      by (auto simp add: neq_Nil_conv simp del: length_drop)
   10.90    with app wts pc
   10.91    obtain x where 
   10.92 -    "wtl_cert l G rT s'' cert (length is) (Suc pc) = Ok x"
   10.93 +    "wtl_cert l G rT s'' cert (length is) (Suc pc) = OK x"
   10.94      by (auto simp add: wtl_append min_def simp del: append_take_drop_id)
   10.95  
   10.96    hence c1: "!!t. cert!Suc pc = Some t ==> G \<turnstile> s'' <=' cert!Suc pc"
   10.97 @@ -144,8 +144,8 @@
   10.98          
   10.99    then
  10.100    obtain s' s'' where
  10.101 -    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'" and
  10.102 -    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
  10.103 +    w: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'" and
  10.104 +    c: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
  10.105      by - (drule wtl_all, auto)
  10.106  
  10.107    from fits wtl pc
  10.108 @@ -158,7 +158,7 @@
  10.109      by - (drule fitsD_None)
  10.110    
  10.111    from pc c cert_None cert_Some
  10.112 -  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = Ok s''"
  10.113 +  have wti: "wtl_inst (is ! pc) G rT (phi!pc) cert (length is) pc = OK s''"
  10.114      by (auto simp add: wtl_cert_def split: if_splits option.splits)
  10.115  
  10.116    { fix pc'
  10.117 @@ -166,14 +166,14 @@
  10.118  
  10.119      with wti
  10.120      have less: "pc' < length is"  
  10.121 -      by (simp add: wtl_inst_Ok)
  10.122 +      by (simp add: wtl_inst_OK)
  10.123  
  10.124      have "G \<turnstile> step (is!pc) G (phi!pc) <=' phi ! pc'" 
  10.125      proof (cases "pc' = Suc pc")
  10.126        case False          
  10.127        with wti pc'
  10.128        have G: "G \<turnstile> step (is ! pc) G (phi ! pc) <=' cert ! pc'" 
  10.129 -        by (simp add: wtl_inst_Ok)
  10.130 +        by (simp add: wtl_inst_OK)
  10.131  
  10.132        hence "cert!pc' = None ==> step (is ! pc) G (phi ! pc) = None"
  10.133          by simp
  10.134 @@ -197,7 +197,7 @@
  10.135        case True
  10.136        with pc' wti
  10.137        have "step (is ! pc) G (phi ! pc) = s''"  
  10.138 -        by (simp add: wtl_inst_Ok)
  10.139 +        by (simp add: wtl_inst_OK)
  10.140        also
  10.141        from w c fits pc wtl 
  10.142        have "Suc pc < length is ==> G \<turnstile> s'' <=' phi ! Suc pc"
  10.143 @@ -213,7 +213,7 @@
  10.144    
  10.145    with wti
  10.146    show ?thesis
  10.147 -    by (auto simp add: wtl_inst_Ok wt_instr_def)
  10.148 +    by (auto simp add: wtl_inst_OK wt_instr_def)
  10.149  qed
  10.150  
  10.151  
  10.152 @@ -228,7 +228,7 @@
  10.153    assume pc:   "0 < length is"
  10.154  
  10.155    from wtl
  10.156 -  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = Ok s"
  10.157 +  have wt0: "wtl_inst_list (take 0 is) G rT cert (length is) 0 s = OK s"
  10.158      by simp
  10.159    
  10.160    with fits pc
  10.161 @@ -244,7 +244,7 @@
  10.162      by (simp add: neq_Nil_conv) (elim, rule that)
  10.163    with wtl
  10.164    obtain s' where
  10.165 -    "wtl_cert x G rT s cert (length is) 0 = Ok s'"
  10.166 +    "wtl_cert x G rT s cert (length is) 0 = OK s'"
  10.167      by simp (elim, rule that, simp)
  10.168    hence 
  10.169      "!!t. cert!0 = Some t ==> G \<turnstile> s <=' cert!0"
  10.170 @@ -259,7 +259,7 @@
  10.171  lemma wtl_method_correct:
  10.172  "wtl_method G C pTs rT mxl ins cert ==> \<exists> phi. wt_method G C pTs rT mxl ins phi"
  10.173  proof (unfold wtl_method_def, simp only: Let_def, elim conjE)
  10.174 -  let "?s0" = "Some ([], Ok (Class C) # map Ok pTs @ replicate mxl Err)"
  10.175 +  let "?s0" = "Some ([], OK (Class C) # map OK pTs @ replicate mxl Err)"
  10.176    assume pc:  "0 < length ins"
  10.177    assume wtl: "wtl_inst_list ins G rT cert (length ins) 0 ?s0 \<noteq> Err"
  10.178  
    11.1 --- a/src/HOL/MicroJava/BV/LBVSpec.thy	Sat Nov 18 19:48:34 2000 +0100
    11.2 +++ b/src/HOL/MicroJava/BV/LBVSpec.thy	Mon Nov 20 16:37:42 2000 +0100
    11.3 @@ -25,7 +25,7 @@
    11.4                 => state_type option err" 
    11.5    "wtl_inst i G rT s cert max_pc pc == 
    11.6       if app i G rT s \<and> check_cert i G s cert pc max_pc then 
    11.7 -       if pc+1 mem (succs i pc) then Ok (step i G s) else Ok (cert!(pc+1))
    11.8 +       if pc+1 mem (succs i pc) then OK (step i G s) else OK (cert!(pc+1))
    11.9       else Err";
   11.10  
   11.11  constdefs
   11.12 @@ -42,7 +42,7 @@
   11.13    wtl_inst_list :: "[instr list,jvm_prog,ty,certificate,p_count,p_count, 
   11.14                       state_type option] => state_type option err"
   11.15  primrec
   11.16 -  "wtl_inst_list []     G rT cert max_pc pc s = Ok s"
   11.17 +  "wtl_inst_list []     G rT cert max_pc pc s = OK s"
   11.18    "wtl_inst_list (i#is) G rT cert max_pc pc s = 
   11.19      (let s' = wtl_cert i G rT s cert max_pc pc in
   11.20       strict (wtl_inst_list is G rT cert max_pc (pc+1)) s')";
   11.21 @@ -55,7 +55,7 @@
   11.22    in 
   11.23    0 < max_pc \<and>   
   11.24    wtl_inst_list ins G rT cert max_pc 0 
   11.25 -                (Some ([],(Ok (Class C))#((map Ok pTs))@(replicate mxl Err))) \<noteq> Err"
   11.26 +                (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) \<noteq> Err"
   11.27  
   11.28   wtl_jvm_prog :: "[jvm_prog,prog_certificate] => bool" 
   11.29   "wtl_jvm_prog G cert ==  
   11.30 @@ -63,27 +63,27 @@
   11.31  
   11.32  
   11.33  
   11.34 -lemma wtl_inst_Ok:
   11.35 -"(wtl_inst i G rT s cert max_pc pc = Ok s') =
   11.36 +lemma wtl_inst_OK:
   11.37 +"(wtl_inst i G rT s cert max_pc pc = OK s') =
   11.38   (app i G rT s \<and> (\<forall>pc' \<in> set (succs i pc). 
   11.39                     pc' < max_pc \<and> (pc' \<noteq> pc+1 --> G \<turnstile> step i G s <=' cert!pc')) \<and> 
   11.40   (if pc+1 \<in> set (succs i pc) then s' = step i G s else s' = cert!(pc+1)))"
   11.41    by (auto simp add: wtl_inst_def check_cert_def set_mem_eq);
   11.42  
   11.43  lemma strict_Some [simp]: 
   11.44 -"(strict f x = Ok y) = (\<exists> z. x = Ok z \<and> f z = Ok y)"
   11.45 +"(strict f x = OK y) = (\<exists> z. x = OK z \<and> f z = OK y)"
   11.46    by (cases x, auto)
   11.47  
   11.48  lemma wtl_Cons:
   11.49    "wtl_inst_list (i#is) G rT cert max_pc pc s \<noteq> Err = 
   11.50 -  (\<exists>s'. wtl_cert i G rT s cert max_pc pc = Ok s' \<and> 
   11.51 +  (\<exists>s'. wtl_cert i G rT s cert max_pc pc = OK s' \<and> 
   11.52          wtl_inst_list is G rT cert max_pc (pc+1) s' \<noteq> Err)"
   11.53  by (auto simp del: split_paired_Ex)
   11.54  
   11.55  lemma wtl_append:
   11.56 -"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = Ok s') =
   11.57 -   (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = Ok s'' \<and> 
   11.58 -          wtl_inst_list b G rT cert mpc (pc+length a) s'' = Ok s')" 
   11.59 +"\<forall> s pc. (wtl_inst_list (a@b) G rT cert mpc pc s = OK s') =
   11.60 +   (\<exists>s''. wtl_inst_list a G rT cert mpc pc s = OK s'' \<and> 
   11.61 +          wtl_inst_list b G rT cert mpc (pc+length a) s'' = OK s')" 
   11.62    (is "\<forall> s pc. ?C s pc a" is "?P a")
   11.63  proof (induct ?P a)
   11.64  
   11.65 @@ -101,24 +101,24 @@
   11.66        case Err thus ?thesis by simp
   11.67      next
   11.68        fix s0
   11.69 -      assume Ok: "wtl_cert x G rT s cert mpc pc = Ok s0"
   11.70 +      assume OK: "wtl_cert x G rT s cert mpc pc = OK s0"
   11.71  
   11.72        with IH
   11.73        have "?C s0 (Suc pc) xs" by blast
   11.74        
   11.75 -      with Ok
   11.76 +      with OK
   11.77        show ?thesis by simp
   11.78      qed
   11.79    qed
   11.80  qed
   11.81  
   11.82  lemma wtl_take:
   11.83 -  "wtl_inst_list is G rT cert mpc pc s = Ok s'' ==>
   11.84 -   \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = Ok s'"
   11.85 +  "wtl_inst_list is G rT cert mpc pc s = OK s'' ==>
   11.86 +   \<exists>s'. wtl_inst_list (take pc' is) G rT cert mpc pc s = OK s'"
   11.87  proof -
   11.88 -  assume "wtl_inst_list is G rT cert mpc pc s = Ok s''"
   11.89 +  assume "wtl_inst_list is G rT cert mpc pc s = OK s''"
   11.90  
   11.91 -  hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = Ok s''"
   11.92 +  hence "wtl_inst_list (take pc' is @ drop pc' is) G rT cert mpc pc s = OK s''"
   11.93      by simp
   11.94  
   11.95    thus ?thesis 
   11.96 @@ -144,13 +144,13 @@
   11.97  qed
   11.98  
   11.99  lemma wtl_Suc:
  11.100 - "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'; 
  11.101 -     wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s'';
  11.102 + "[| wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'; 
  11.103 +     wtl_cert (is!pc) G rT s' cert (length is) pc = OK s'';
  11.104       Suc pc < length is |] ==>
  11.105 -  wtl_inst_list (take (Suc pc) is)  G rT cert (length is) 0 s = Ok s''" 
  11.106 +  wtl_inst_list (take (Suc pc) is)  G rT cert (length is) 0 s = OK s''" 
  11.107  proof -
  11.108 -  assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s'"
  11.109 -  assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
  11.110 +  assume wtt: "wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s'"
  11.111 +  assume wtc: "wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
  11.112    assume pc: "Suc pc < length is"
  11.113  
  11.114    hence "take (Suc pc) is = (take pc is)@[is!pc]" 
  11.115 @@ -164,8 +164,8 @@
  11.116  lemma wtl_all:
  11.117    "[| wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err;
  11.118        pc < length is |] ==> 
  11.119 -   \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = Ok s' \<and> 
  11.120 -            wtl_cert (is!pc) G rT s' cert (length is) pc = Ok s''"
  11.121 +   \<exists>s' s''. wtl_inst_list (take pc is) G rT cert (length is) 0 s = OK s' \<and> 
  11.122 +            wtl_cert (is!pc) G rT s' cert (length is) pc = OK s''"
  11.123  proof -
  11.124    assume all: "wtl_inst_list is G rT cert (length is) 0 s \<noteq> Err"
  11.125  
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/MicroJava/BV/Listn.thy	Mon Nov 20 16:37:42 2000 +0100
    12.3 @@ -0,0 +1,495 @@
    12.4 +(*  Title:      HOL/BCV/Listn.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Tobias Nipkow
    12.7 +    Copyright   2000 TUM
    12.8 +
    12.9 +Lists of a fixed length
   12.10 +*)
   12.11 +
   12.12 +header "Fixed Length Lists"
   12.13 +
   12.14 +theory Listn = Err:
   12.15 +
   12.16 +constdefs
   12.17 +
   12.18 + list :: "nat => 'a set => 'a list set"
   12.19 +"list n A == {xs. length xs = n & set xs <= A}"
   12.20 +
   12.21 + le :: "'a ord => ('a list)ord"
   12.22 +"le r == list_all2 (%x y. x <=_r y)"
   12.23 +
   12.24 +syntax "@lesublist" :: "'a list => 'a ord => 'a list => bool"
   12.25 +       ("(_ /<=[_] _)" [50, 0, 51] 50)
   12.26 +syntax "@lesssublist" :: "'a list => 'a ord => 'a list => bool"
   12.27 +       ("(_ /<[_] _)" [50, 0, 51] 50)
   12.28 +translations
   12.29 + "x <=[r] y" == "x <=_(Listn.le r) y"
   12.30 + "x <[r] y"  == "x <_(Listn.le r) y"
   12.31 +
   12.32 +constdefs
   12.33 + map2 :: "('a => 'b => 'c) => 'a list => 'b list => 'c list"
   12.34 +"map2 f == (%xs ys. map (split f) (zip xs ys))"
   12.35 +
   12.36 +syntax "@plussublist" :: "'a list => ('a => 'b => 'c) => 'b list => 'c list"
   12.37 +       ("(_ /+[_] _)" [65, 0, 66] 65)
   12.38 +translations  "x +[f] y" == "x +_(map2 f) y"
   12.39 +
   12.40 +consts coalesce :: "'a err list => 'a list err"
   12.41 +primrec
   12.42 +"coalesce [] = OK[]"
   12.43 +"coalesce (ex#exs) = Err.sup (op #) ex (coalesce exs)"
   12.44 +
   12.45 +constdefs
   12.46 + sl :: "nat => 'a sl => 'a list sl"
   12.47 +"sl n == %(A,r,f). (list n A, le r, map2 f)"
   12.48 +
   12.49 + sup :: "('a => 'b => 'c err) => 'a list => 'b list => 'c list err"
   12.50 +"sup f == %xs ys. if size xs = size ys then coalesce(xs +[f] ys) else Err"
   12.51 +
   12.52 + upto_esl :: "nat => 'a esl => 'a list esl"
   12.53 +"upto_esl m == %(A,r,f). (Union{list n A |n. n <= m}, le r, sup f)"
   12.54 +
   12.55 +lemmas [simp] = set_update_subsetI
   12.56 +
   12.57 +lemma unfold_lesub_list:
   12.58 +  "xs <=[r] ys == Listn.le r xs ys"
   12.59 +  by (simp add: lesub_def)
   12.60 +
   12.61 +lemma Nil_le_conv [iff]:
   12.62 +  "([] <=[r] ys) = (ys = [])"
   12.63 +apply (unfold lesub_def Listn.le_def)
   12.64 +apply simp
   12.65 +done
   12.66 +
   12.67 +lemma Cons_notle_Nil [iff]: 
   12.68 +  "~ x#xs <=[r] []"
   12.69 +apply (unfold lesub_def Listn.le_def)
   12.70 +apply simp
   12.71 +done
   12.72 +
   12.73 +
   12.74 +lemma Cons_le_Cons [iff]:
   12.75 +  "x#xs <=[r] y#ys = (x <=_r y & xs <=[r] ys)"
   12.76 +apply (unfold lesub_def Listn.le_def)
   12.77 +apply simp
   12.78 +done
   12.79 +
   12.80 +lemma Cons_less_Conss [simp]:
   12.81 +  "order r ==> 
   12.82 +  x#xs <_(Listn.le r) y#ys = 
   12.83 +  (x <_r y & xs <=[r] ys  |  x = y & xs <_(Listn.le r) ys)"
   12.84 +apply (unfold lesssub_def)
   12.85 +apply blast
   12.86 +done  
   12.87 +
   12.88 +lemma list_update_le_cong:
   12.89 +  "[| i<size xs; xs <=[r] ys; x <=_r y |] ==> xs[i:=x] <=[r] ys[i:=y]";
   12.90 +apply (unfold unfold_lesub_list)
   12.91 +apply (unfold Listn.le_def)
   12.92 +apply (simp add: list_all2_conv_all_nth nth_list_update)
   12.93 +done
   12.94 +
   12.95 +
   12.96 +lemma le_listD:
   12.97 +  "[| xs <=[r] ys; p < size xs |] ==> xs!p <=_r ys!p"
   12.98 +apply (unfold Listn.le_def lesub_def)
   12.99 +apply (simp add: list_all2_conv_all_nth)
  12.100 +done
  12.101 +
  12.102 +lemma le_list_refl:
  12.103 +  "!x. x <=_r x ==> xs <=[r] xs"
  12.104 +apply (unfold unfold_lesub_list)
  12.105 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.106 +done
  12.107 +
  12.108 +lemma le_list_trans:
  12.109 +  "[| order r; xs <=[r] ys; ys <=[r] zs |] ==> xs <=[r] zs"
  12.110 +apply (unfold unfold_lesub_list)
  12.111 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.112 +apply clarify
  12.113 +apply simp
  12.114 +apply (blast intro: order_trans)
  12.115 +done
  12.116 +
  12.117 +lemma le_list_antisym:
  12.118 +  "[| order r; xs <=[r] ys; ys <=[r] xs |] ==> xs = ys"
  12.119 +apply (unfold unfold_lesub_list)
  12.120 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.121 +apply (rule nth_equalityI)
  12.122 + apply blast
  12.123 +apply clarify
  12.124 +apply simp
  12.125 +apply (blast intro: order_antisym)
  12.126 +done
  12.127 +
  12.128 +lemma order_listI [simp, intro!]:
  12.129 +  "order r ==> order(Listn.le r)"
  12.130 +apply (subst order_def)
  12.131 +apply (blast intro: le_list_refl le_list_trans le_list_antisym
  12.132 +             dest: order_refl)
  12.133 +done
  12.134 +
  12.135 +
  12.136 +lemma lesub_list_impl_same_size [simp]:
  12.137 +  "xs <=[r] ys ==> size ys = size xs"  
  12.138 +apply (unfold Listn.le_def lesub_def)
  12.139 +apply (simp add: list_all2_conv_all_nth)
  12.140 +done 
  12.141 +
  12.142 +lemma lesssub_list_impl_same_size:
  12.143 +  "xs <_(Listn.le r) ys ==> size ys = size xs"
  12.144 +apply (unfold lesssub_def)
  12.145 +apply auto
  12.146 +done  
  12.147 +
  12.148 +lemma listI:
  12.149 +  "[| length xs = n; set xs <= A |] ==> xs : list n A"
  12.150 +apply (unfold list_def)
  12.151 +apply blast
  12.152 +done
  12.153 +
  12.154 +lemma listE_length [simp]:
  12.155 +   "xs : list n A ==> length xs = n"
  12.156 +apply (unfold list_def)
  12.157 +apply blast
  12.158 +done 
  12.159 +
  12.160 +lemma less_lengthI:
  12.161 +  "[| xs : list n A; p < n |] ==> p < length xs"
  12.162 +  by simp
  12.163 +
  12.164 +lemma listE_set [simp]:
  12.165 +  "xs : list n A ==> set xs <= A"
  12.166 +apply (unfold list_def)
  12.167 +apply blast
  12.168 +done 
  12.169 +
  12.170 +lemma list_0 [simp]:
  12.171 +  "list 0 A = {[]}"
  12.172 +apply (unfold list_def)
  12.173 +apply auto
  12.174 +done 
  12.175 +
  12.176 +lemma in_list_Suc_iff: 
  12.177 +  "(xs : list (Suc n) A) = (? y:A. ? ys:list n A. xs = y#ys)"
  12.178 +apply (unfold list_def)
  12.179 +apply (case_tac "xs")
  12.180 +apply auto
  12.181 +done 
  12.182 +
  12.183 +lemma Cons_in_list_Suc [iff]:
  12.184 +  "(x#xs : list (Suc n) A) = (x:A & xs : list n A)";
  12.185 +apply (simp add: in_list_Suc_iff)
  12.186 +apply blast
  12.187 +done 
  12.188 +
  12.189 +lemma list_not_empty:
  12.190 +  "? a. a:A ==> ? xs. xs : list n A";
  12.191 +apply (induct "n")
  12.192 + apply simp
  12.193 +apply (simp add: in_list_Suc_iff)
  12.194 +apply blast
  12.195 +done
  12.196 +
  12.197 +
  12.198 +lemma nth_in [rule_format, simp]:
  12.199 +  "!i n. length xs = n --> set xs <= A --> i < n --> (xs!i) : A"
  12.200 +apply (induct "xs")
  12.201 + apply simp
  12.202 +apply (simp add: nth_Cons split: nat.split)
  12.203 +done
  12.204 +
  12.205 +lemma listE_nth_in:
  12.206 +  "[| xs : list n A; i < n |] ==> (xs!i) : A"
  12.207 +  by auto
  12.208 +
  12.209 +lemma listt_update_in_list [simp, intro!]:
  12.210 +  "[| xs : list n A; x:A |] ==> xs[i := x] : list n A"
  12.211 +apply (unfold list_def)
  12.212 +apply simp
  12.213 +done 
  12.214 +
  12.215 +lemma plus_list_Nil [simp]:
  12.216 +  "[] +[f] xs = []"
  12.217 +apply (unfold plussub_def map2_def)
  12.218 +apply simp
  12.219 +done 
  12.220 +
  12.221 +lemma plus_list_Cons [simp]:
  12.222 +  "(x#xs) +[f] ys = (case ys of [] => [] | y#ys => (x +_f y)#(xs +[f] ys))"
  12.223 +  by (simp add: plussub_def map2_def split: list.split)
  12.224 +
  12.225 +lemma length_plus_list [rule_format, simp]:
  12.226 +  "!ys. length(xs +[f] ys) = min(length xs) (length ys)"
  12.227 +apply (induct xs)
  12.228 + apply simp
  12.229 +apply clarify
  12.230 +apply (simp (no_asm_simp) split: list.split)
  12.231 +done
  12.232 +
  12.233 +lemma nth_plus_list [rule_format, simp]:
  12.234 +  "!xs ys i. length xs = n --> length ys = n --> i<n --> 
  12.235 +  (xs +[f] ys)!i = (xs!i) +_f (ys!i)"
  12.236 +apply (induct n)
  12.237 + apply simp
  12.238 +apply clarify
  12.239 +apply (case_tac xs)
  12.240 + apply simp
  12.241 +apply (force simp add: nth_Cons split: list.split nat.split)
  12.242 +done
  12.243 +
  12.244 +
  12.245 +lemma plus_list_ub1 [rule_format]:
  12.246 +  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |] 
  12.247 +  ==> xs <=[r] xs +[f] ys"
  12.248 +apply (unfold unfold_lesub_list)
  12.249 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.250 +done
  12.251 +
  12.252 +lemma plus_list_ub2:
  12.253 +  "[| semilat(A,r,f); set xs <= A; set ys <= A; size xs = size ys |]
  12.254 +  ==> ys <=[r] xs +[f] ys"
  12.255 +apply (unfold unfold_lesub_list)
  12.256 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.257 +done 
  12.258 +
  12.259 +lemma plus_list_lub [rule_format]:
  12.260 +  "semilat(A,r,f) ==> !xs ys zs. set xs <= A --> set ys <= A --> set zs <= A 
  12.261 +  --> size xs = n & size ys = n --> 
  12.262 +  xs <=[r] zs & ys <=[r] zs --> xs +[f] ys <=[r] zs"
  12.263 +apply (unfold unfold_lesub_list)
  12.264 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.265 +done 
  12.266 +
  12.267 +lemma list_update_incr [rule_format]:
  12.268 +  "[| semilat(A,r,f); x:A |] ==> set xs <= A --> 
  12.269 +  (!i. i<size xs --> xs <=[r] xs[i := x +_f xs!i])"
  12.270 +apply (unfold unfold_lesub_list)
  12.271 +apply (simp add: Listn.le_def list_all2_conv_all_nth)
  12.272 +apply (induct xs)
  12.273 + apply simp
  12.274 +apply (simp add: in_list_Suc_iff)
  12.275 +apply clarify
  12.276 +apply (simp add: nth_Cons split: nat.split)
  12.277 +done 
  12.278 +
  12.279 +lemma acc_le_listI [intro!]:
  12.280 +  "[| order r; acc r |] ==> acc(Listn.le r)"
  12.281 +apply (unfold acc_def)
  12.282 +apply (subgoal_tac
  12.283 + "wf(UN n. {(ys,xs). size xs = n & size ys = n & xs <_(Listn.le r) ys})")
  12.284 + apply (erule wf_subset)
  12.285 + apply (blast intro: lesssub_list_impl_same_size)
  12.286 +apply (rule wf_UN)
  12.287 + prefer 2
  12.288 + apply clarify
  12.289 + apply (rename_tac m n)
  12.290 + apply (case_tac "m=n")
  12.291 +  apply simp
  12.292 + apply (rule conjI)
  12.293 +  apply (fast intro!: equals0I dest: not_sym)
  12.294 + apply (fast intro!: equals0I dest: not_sym)
  12.295 +apply clarify
  12.296 +apply (rename_tac n)
  12.297 +apply (induct_tac n)
  12.298 + apply (simp add: lesssub_def cong: conj_cong)
  12.299 +apply (rename_tac k)
  12.300 +apply (simp add: wf_eq_minimal)
  12.301 +apply (simp (no_asm) add: length_Suc_conv cong: conj_cong)
  12.302 +apply clarify
  12.303 +apply (rename_tac M m)
  12.304 +apply (case_tac "? x xs. size xs = k & x#xs : M")
  12.305 + prefer 2
  12.306 + apply (erule thin_rl)
  12.307 + apply (erule thin_rl)
  12.308 + apply blast
  12.309 +apply (erule_tac x = "{a. ? xs. size xs = k & a#xs:M}" in allE)
  12.310 +apply (erule impE)
  12.311 + apply blast
  12.312 +apply (thin_tac "? x xs. ?P x xs")
  12.313 +apply clarify
  12.314 +apply (rename_tac maxA xs)
  12.315 +apply (erule_tac x = "{ys. size ys = size xs & maxA#ys : M}" in allE)
  12.316 +apply (erule impE)
  12.317 + apply blast
  12.318 +apply clarify
  12.319 +apply (thin_tac "m : M")
  12.320 +apply (thin_tac "maxA#xs : M")
  12.321 +apply (rule bexI)
  12.322 + prefer 2
  12.323 + apply assumption
  12.324 +apply clarify
  12.325 +apply simp
  12.326 +apply blast
  12.327 +done 
  12.328 +
  12.329 +lemma closed_listI:
  12.330 +  "closed S f ==> closed (list n S) (map2 f)"
  12.331 +apply (unfold closed_def)
  12.332 +apply (induct n)
  12.333 + apply simp
  12.334 +apply clarify
  12.335 +apply (simp add: in_list_Suc_iff)
  12.336 +apply clarify
  12.337 +apply simp
  12.338 +apply blast
  12.339 +done 
  12.340 +
  12.341 +
  12.342 +lemma semilat_Listn_sl:
  12.343 +  "!!L. semilat L ==> semilat (Listn.sl n L)"
  12.344 +apply (unfold Listn.sl_def)
  12.345 +apply (simp (no_asm_simp) only: split_tupled_all)
  12.346 +apply (simp (no_asm) only: semilat_Def Product_Type.split)
  12.347 +apply (rule conjI)
  12.348 + apply simp
  12.349 +apply (rule conjI)
  12.350 + apply (simp only: semilatDclosedI closed_listI)
  12.351 +apply (simp (no_asm) only: list_def)
  12.352 +apply (simp (no_asm_simp) add: plus_list_ub1 plus_list_ub2 plus_list_lub)
  12.353 +done  
  12.354 +
  12.355 +
  12.356 +lemma coalesce_in_err_list [rule_format]:
  12.357 +  "!xes. xes : list n (err A) --> coalesce xes : err(list n A)"
  12.358 +apply (induct n)
  12.359 + apply simp
  12.360 +apply clarify
  12.361 +apply (simp add: in_list_Suc_iff)
  12.362 +apply clarify
  12.363 +apply (simp (no_asm) add: plussub_def Err.sup_def lift2_def split: err.split)
  12.364 +apply force
  12.365 +done 
  12.366 +
  12.367 +lemma lem: "!!x xs. x +_(op #) xs = x#xs"
  12.368 +  by (simp add: plussub_def)
  12.369 +
  12.370 +lemma coalesce_eq_OK1_D [rule_format]:
  12.371 +  "semilat(err A, Err.le r, lift2 f) ==> 
  12.372 +  !xs. xs : list n A --> (!ys. ys : list n A --> 
  12.373 +  (!zs. coalesce (xs +[f] ys) = OK zs --> xs <=[r] zs))"
  12.374 +apply (induct n)
  12.375 +  apply simp
  12.376 +apply clarify
  12.377 +apply (simp add: in_list_Suc_iff)
  12.378 +apply clarify
  12.379 +apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
  12.380 +apply (force simp add: semilat_le_err_OK1)
  12.381 +done
  12.382 +
  12.383 +lemma coalesce_eq_OK2_D [rule_format]:
  12.384 +  "semilat(err A, Err.le r, lift2 f) ==> 
  12.385 +  !xs. xs : list n A --> (!ys. ys : list n A --> 
  12.386 +  (!zs. coalesce (xs +[f] ys) = OK zs --> ys <=[r] zs))"
  12.387 +apply (induct n)
  12.388 + apply simp
  12.389 +apply clarify
  12.390 +apply (simp add: in_list_Suc_iff)
  12.391 +apply clarify
  12.392 +apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
  12.393 +apply (force simp add: semilat_le_err_OK2)
  12.394 +done 
  12.395 +
  12.396 +lemma lift2_le_ub:
  12.397 +  "[| semilat(err A, Err.le r, lift2 f); x:A; y:A; x +_f y = OK z; 
  12.398 +      u:A; x <=_r u; y <=_r u |] ==> z <=_r u"
  12.399 +apply (unfold semilat_Def plussub_def err_def)
  12.400 +apply (simp add: lift2_def)
  12.401 +apply clarify
  12.402 +apply (rotate_tac -3)
  12.403 +apply (erule thin_rl)
  12.404 +apply (erule thin_rl)
  12.405 +apply force
  12.406 +done 
  12.407 +
  12.408 +lemma coalesce_eq_OK_ub_D [rule_format]:
  12.409 +  "semilat(err A, Err.le r, lift2 f) ==> 
  12.410 +  !xs. xs : list n A --> (!ys. ys : list n A --> 
  12.411 +  (!zs us. coalesce (xs +[f] ys) = OK zs & xs <=[r] us & ys <=[r] us 
  12.412 +           & us : list n A --> zs <=[r] us))"
  12.413 +apply (induct n)
  12.414 + apply simp
  12.415 +apply clarify
  12.416 +apply (simp add: in_list_Suc_iff)
  12.417 +apply clarify
  12.418 +apply (simp (no_asm_use) split: err.split_asm add: lem Err.sup_def lift2_def)
  12.419 +apply clarify
  12.420 +apply (rule conjI)
  12.421 + apply (blast intro: lift2_le_ub)
  12.422 +apply blast
  12.423 +done 
  12.424 +
  12.425 +lemma lift2_eq_ErrD:
  12.426 +  "[| x +_f y = Err; semilat(err A, Err.le r, lift2 f); x:A; y:A |] 
  12.427 +  ==> ~(? u:A. x <=_r u & y <=_r u)"
  12.428 +  by (simp add: OK_plus_OK_eq_Err_conv [THEN iffD1])
  12.429 +
  12.430 +
  12.431 +lemma coalesce_eq_Err_D [rule_format]:
  12.432 +  "[| semilat(err A, Err.le r, lift2 f) |] 
  12.433 +  ==> !xs. xs:list n A --> (!ys. ys:list n A --> 
  12.434 +      coalesce (xs +[f] ys) = Err --> 
  12.435 +      ~(? zs:list n A. xs <=[r] zs & ys <=[r] zs))"
  12.436 +apply (induct n)
  12.437 + apply simp
  12.438 +apply clarify
  12.439 +apply (simp add: in_list_Suc_iff)
  12.440 +apply clarify
  12.441 +apply (simp split: err.split_asm add: lem Err.sup_def lift2_def)
  12.442 + apply (blast dest: lift2_eq_ErrD)
  12.443 +apply blast
  12.444 +done 
  12.445 +
  12.446 +lemma closed_err_lift2_conv:
  12.447 +  "closed (err A) (lift2 f) = (!x:A. !y:A. x +_f y : err A)"
  12.448 +apply (unfold closed_def)
  12.449 +apply (simp add: err_def)
  12.450 +done 
  12.451 +
  12.452 +lemma closed_map2_list [rule_format]:
  12.453 +  "closed (err A) (lift2 f) ==> 
  12.454 +  !xs. xs : list n A --> (!ys. ys : list n A --> 
  12.455 +  map2 f xs ys : list n (err A))"
  12.456 +apply (unfold map2_def)
  12.457 +apply (induct n)
  12.458 + apply simp
  12.459 +apply clarify
  12.460 +apply (simp add: in_list_Suc_iff)
  12.461 +apply clarify
  12.462 +apply (simp add: plussub_def closed_err_lift2_conv)
  12.463 +apply blast
  12.464 +done 
  12.465 +
  12.466 +lemma closed_lift2_sup:
  12.467 +  "closed (err A) (lift2 f) ==> 
  12.468 +  closed (err (list n A)) (lift2 (sup f))"
  12.469 +  by (fastsimp  simp add: closed_def plussub_def sup_def lift2_def
  12.470 +                          coalesce_in_err_list closed_map2_list
  12.471 +                split: err.split)
  12.472 +
  12.473 +lemma err_semilat_sup:
  12.474 +  "err_semilat (A,r,f) ==> 
  12.475 +  err_semilat (list n A, Listn.le r, sup f)"
  12.476 +apply (unfold Err.sl_def)
  12.477 +apply (simp only: Product_Type.split)
  12.478 +apply (simp (no_asm) only: semilat_Def plussub_def)
  12.479 +apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
  12.480 +apply (rule conjI)
  12.481 + apply (drule semilatDorderI)
  12.482 + apply simp
  12.483 +apply (simp (no_asm) only: unfold_lesub_err Err.le_def err_def sup_def lift2_def)
  12.484 +apply (simp (no_asm_simp) add: coalesce_eq_OK1_D coalesce_eq_OK2_D split: err.split)
  12.485 +apply (blast intro: coalesce_eq_OK_ub_D dest: coalesce_eq_Err_D)
  12.486 +done 
  12.487 +
  12.488 +lemma err_semilat_upto_esl:
  12.489 +  "!!L. err_semilat L ==> err_semilat(upto_esl m L)"
  12.490 +apply (unfold Listn.upto_esl_def)
  12.491 +apply (simp (no_asm_simp) only: split_tupled_all)
  12.492 +apply simp
  12.493 +apply (fastsimp intro!: err_semilat_UnionI err_semilat_sup
  12.494 +                dest: lesub_list_impl_same_size 
  12.495 +                simp add: plussub_def Listn.sup_def)
  12.496 +done
  12.497 +
  12.498 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/MicroJava/BV/Opt.thy	Mon Nov 20 16:37:42 2000 +0100
    13.3 @@ -0,0 +1,359 @@
    13.4 +(*  Title:      HOL/BCV/Opt.thy
    13.5 +    ID:         $Id$
    13.6 +    Author:     Tobias Nipkow
    13.7 +    Copyright   2000 TUM
    13.8 +
    13.9 +More about options
   13.10 +*)
   13.11 +
   13.12 +header "More about Options"
   13.13 +
   13.14 +theory Opt = Err:
   13.15 +
   13.16 +constdefs
   13.17 + le :: "'a ord => 'a option ord"
   13.18 +"le r o1 o2 == case o2 of None => o1=None |
   13.19 +                              Some y => (case o1 of None => True |
   13.20 +                                                    Some x => x <=_r y)"
   13.21 +
   13.22 + opt :: "'a set => 'a option set"
   13.23 +"opt A == insert None {x . ? y:A. x = Some y}"
   13.24 +
   13.25 + sup :: "'a ebinop => 'a option ebinop"
   13.26 +"sup f o1 o2 ==  
   13.27 + case o1 of None => OK o2 | Some x => (case o2 of None => OK o1
   13.28 +                                              | Some y => (case f x y of Err => Err | OK z => OK (Some z)))"
   13.29 +
   13.30 + esl :: "'a esl => 'a option esl"
   13.31 +"esl == %(A,r,f). (opt A, le r, sup f)"
   13.32 +
   13.33 +lemma unfold_le_opt:
   13.34 +  "o1 <=_(le r) o2 = 
   13.35 +  (case o2 of None => o1=None | 
   13.36 +              Some y => (case o1 of None => True | Some x => x <=_r y))"
   13.37 +apply (unfold lesub_def le_def)
   13.38 +apply (rule refl)
   13.39 +done
   13.40 +
   13.41 +lemma le_opt_refl:
   13.42 +  "order r ==> o1 <=_(le r) o1"
   13.43 +by (simp add: unfold_le_opt split: option.split)
   13.44 +
   13.45 +lemma le_opt_trans [rule_format]:
   13.46 +  "order r ==> 
   13.47 +   o1 <=_(le r) o2 --> o2 <=_(le r) o3 --> o1 <=_(le r) o3"
   13.48 +apply (simp add: unfold_le_opt split: option.split)
   13.49 +apply (blast intro: order_trans)
   13.50 +done
   13.51 +
   13.52 +lemma le_opt_antisym [rule_format]:
   13.53 +  "order r ==> o1 <=_(le r) o2 --> o2 <=_(le r) o1 --> o1=o2"
   13.54 +apply (simp add: unfold_le_opt split: option.split)
   13.55 +apply (blast intro: order_antisym)
   13.56 +done
   13.57 +
   13.58 +lemma order_le_opt [intro!,simp]:
   13.59 +  "order r ==> order(le r)"
   13.60 +apply (subst order_def)
   13.61 +apply (blast intro: le_opt_refl le_opt_trans le_opt_antisym)
   13.62 +done 
   13.63 +
   13.64 +lemma None_bot [iff]: 
   13.65 +  "None <=_(le r) ox"
   13.66 +apply (unfold lesub_def le_def)
   13.67 +apply (simp split: option.split)
   13.68 +done 
   13.69 +
   13.70 +lemma Some_le [iff]:
   13.71 +  "(Some x <=_(le r) ox) = (? y. ox = Some y & x <=_r y)"
   13.72 +apply (unfold lesub_def le_def)
   13.73 +apply (simp split: option.split)
   13.74 +done 
   13.75 +
   13.76 +lemma le_None [iff]:
   13.77 +  "(ox <=_(le r) None) = (ox = None)";
   13.78 +apply (unfold lesub_def le_def)
   13.79 +apply (simp split: option.split)
   13.80 +done 
   13.81 +
   13.82 +
   13.83 +lemma OK_None_bot [iff]:
   13.84 +  "OK None <=_(Err.le (le r)) x"
   13.85 +  by (simp add: lesub_def Err.le_def le_def split: option.split err.split)
   13.86 +
   13.87 +lemma sup_None1 [iff]:
   13.88 +  "x +_(sup f) None = OK x"
   13.89 +  by (simp add: plussub_def sup_def split: option.split)
   13.90 +
   13.91 +lemma sup_None2 [iff]:
   13.92 +  "None +_(sup f) x = OK x"
   13.93 +  by (simp add: plussub_def sup_def split: option.split)
   13.94 +
   13.95 +
   13.96 +lemma None_in_opt [iff]:
   13.97 +  "None : opt A"
   13.98 +by (simp add: opt_def)
   13.99 +
  13.100 +lemma Some_in_opt [iff]:
  13.101 +  "(Some x : opt A) = (x:A)"
  13.102 +apply (unfold opt_def)
  13.103 +apply auto
  13.104 +done 
  13.105 +
  13.106 +
  13.107 +lemma semilat_opt:
  13.108 +  "!!L. err_semilat L ==> err_semilat (Opt.esl L)"
  13.109 +proof (unfold Opt.esl_def Err.sl_def, simp add: split_tupled_all)
  13.110 +  
  13.111 +  fix A r f
  13.112 +  assume s: "semilat (err A, Err.le r, lift2 f)"
  13.113 + 
  13.114 +  let ?A0 = "err A"
  13.115 +  let ?r0 = "Err.le r"
  13.116 +  let ?f0 = "lift2 f"
  13.117 +
  13.118 +  from s
  13.119 +  obtain
  13.120 +    ord: "order ?r0" and
  13.121 +    clo: "closed ?A0 ?f0" and
  13.122 +    ub1: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. x <=_?r0 x +_?f0 y" and
  13.123 +    ub2: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. y <=_?r0 x +_?f0 y" and
  13.124 +    lub: "\<forall>x\<in>?A0. \<forall>y\<in>?A0. \<forall>z\<in>?A0. x <=_?r0 z \<and> y <=_?r0 z \<longrightarrow> x +_?f0 y <=_?r0 z"
  13.125 +    by (unfold semilat_def) simp
  13.126 +
  13.127 +  let ?A = "err (opt A)" 
  13.128 +  let ?r = "Err.le (Opt.le r)"
  13.129 +  let ?f = "lift2 (Opt.sup f)"
  13.130 +
  13.131 +  from ord
  13.132 +  have "order ?r"
  13.133 +    by simp
  13.134 +
  13.135 +  moreover
  13.136 +
  13.137 +  have "closed ?A ?f"
  13.138 +  proof (unfold closed_def, intro strip)
  13.139 +    fix x y    
  13.140 +    assume x: "x : ?A" 
  13.141 +    assume y: "y : ?A" 
  13.142 +
  13.143 +    {
  13.144 +      fix a b
  13.145 +      assume ab: "x = OK a" "y = OK b"
  13.146 +      
  13.147 +      with x 
  13.148 +      have a: "!!c. a = Some c ==> c : A"
  13.149 +        by (clarsimp simp add: opt_def)
  13.150 +
  13.151 +      from ab y
  13.152 +      have b: "!!d. b = Some d ==> d : A"
  13.153 +        by (clarsimp simp add: opt_def)
  13.154 +      
  13.155 +      { fix c d assume "a = Some c" "b = Some d"
  13.156 +        with ab x y
  13.157 +        have "c:A & d:A"
  13.158 +          by (simp add: err_def opt_def Bex_def)
  13.159 +        with clo
  13.160 +        have "f c d : err A"
  13.161 +          by (simp add: closed_def plussub_def err_def lift2_def)
  13.162 +        moreover
  13.163 +        fix z assume "f c d = OK z"
  13.164 +        ultimately
  13.165 +        have "z : A" by simp
  13.166 +      } note f_closed = this    
  13.167 +
  13.168 +      have "sup f a b : ?A"
  13.169 +      proof (cases a)
  13.170 +        case None
  13.171 +        thus ?thesis
  13.172 +          by (simp add: sup_def opt_def) (cases b, simp, simp add: b Bex_def)
  13.173 +      next
  13.174 +        case Some
  13.175 +        thus ?thesis
  13.176 +          by (auto simp add: sup_def opt_def Bex_def a b f_closed split: err.split option.split)
  13.177 +      qed
  13.178 +    }
  13.179 +
  13.180 +    thus "x +_?f y : ?A"
  13.181 +      by (simp add: plussub_def lift2_def split: err.split)
  13.182 +  qed
  13.183 +    
  13.184 +  moreover
  13.185 +
  13.186 +  have "\<forall>x\<in>?A. \<forall>y\<in>?A. x <=_?r x +_?f y"
  13.187 +  proof (intro strip)
  13.188 +    fix x y
  13.189 +    assume x: "x : ?A"
  13.190 +    assume y: "y : ?A"
  13.191 +
  13.192 +    show "x <=_?r x +_?f y"
  13.193 +    proof -
  13.194 +      from ord 
  13.195 +      have order_r: "order r" by simp
  13.196 +
  13.197 +      { fix a b 
  13.198 +        assume ok: "x = OK a" "y = OK b"
  13.199 +        
  13.200 +        { fix c d 
  13.201 +          assume some: "a = Some c" "b = Some d"
  13.202 +
  13.203 +          with x y ok
  13.204 +          obtain "c:A" "d:A" by simp
  13.205 +          then
  13.206 +          obtain "OK c : err A" "OK d : err A" by simp
  13.207 +          with ub1
  13.208 +          have OK: "OK c <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
  13.209 +            by blast        
  13.210 +          
  13.211 +          { fix e assume  "f c d = OK e"
  13.212 +            with OK
  13.213 +            have "c <=_r e"
  13.214 +              by (simp add: lesub_def Err.le_def plussub_def lift2_def)
  13.215 +          }
  13.216 +          with ok some
  13.217 +          have ?thesis
  13.218 +            by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def 
  13.219 +                     split: err.split)
  13.220 +        } note this [intro!]
  13.221 +
  13.222 +        from ok
  13.223 +        have ?thesis
  13.224 +          by - (cases a, simp, cases b, simp add: order_r, blast)
  13.225 +      }
  13.226 +      thus ?thesis
  13.227 +        by - (cases x, simp, cases y, simp+)
  13.228 +    qed
  13.229 +  qed
  13.230 +
  13.231 +  moreover
  13.232 +
  13.233 +  have "\<forall>x\<in>?A. \<forall>y\<in>?A. y <=_?r x +_?f y" 
  13.234 +  proof (intro strip)
  13.235 +    fix x y
  13.236 +    assume x: "x : ?A"
  13.237 +    assume y: "y : ?A"
  13.238 +
  13.239 +    show "y <=_?r x +_?f y"
  13.240 +    proof -
  13.241 +      from ord 
  13.242 +      have order_r: "order r" by simp
  13.243 +
  13.244 +      { fix a b 
  13.245 +        assume ok: "x = OK a" "y = OK b"
  13.246 +        
  13.247 +        { fix c d 
  13.248 +          assume some: "a = Some c" "b = Some d"
  13.249 +
  13.250 +          with x y ok
  13.251 +          obtain "c:A" "d:A" by simp
  13.252 +          then
  13.253 +          obtain "OK c : err A" "OK d : err A" by simp
  13.254 +          with ub2
  13.255 +          have OK: "OK d <=_(Err.le r) (OK c) +_(lift2 f) (OK d)"
  13.256 +            by blast        
  13.257 +          
  13.258 +          { fix e assume  "f c d = OK e"
  13.259 +            with OK
  13.260 +            have "d <=_r e"
  13.261 +              by (simp add: lesub_def Err.le_def plussub_def lift2_def)
  13.262 +          }
  13.263 +          with ok some
  13.264 +          have ?thesis
  13.265 +            by (simp add: plussub_def sup_def lesub_def le_def lift2_def Err.le_def 
  13.266 +                     split: err.split)
  13.267 +        } note this [intro!]
  13.268 +
  13.269 +        from ok
  13.270 +        have ?thesis
  13.271 +          by - (cases a, simp add: order_r, cases b, simp, blast)
  13.272 +      }
  13.273 +      thus ?thesis
  13.274 +        by - (cases x, simp, cases y, simp+)
  13.275 +    qed
  13.276 +  qed
  13.277 +
  13.278 +  moreover
  13.279 +
  13.280 +  have "\<forall>x\<in>?A. \<forall>y\<in>?A. \<forall>z\<in>?A. x <=_?r z \<and> y <=_?r z \<longrightarrow> x +_?f y <=_?r z"
  13.281 +  proof (intro strip, elim conjE)
  13.282 +    fix x y z
  13.283 +    assume xyz: "x : ?A" "y : ?A" "z : ?A"
  13.284 +    assume xz: "x <=_?r z"
  13.285 +    assume yz: "y <=_?r z"
  13.286 +
  13.287 +    { fix a b c
  13.288 +      assume ok: "x = OK a" "y = OK b" "z = OK c"
  13.289 +
  13.290 +      { fix d e g
  13.291 +        assume some: "a = Some d" "b = Some e" "c = Some g"
  13.292 +        
  13.293 +        with ok xyz
  13.294 +        obtain "OK d:err A" "OK e:err A" "OK g:err A"
  13.295 +          by simp
  13.296 +        with lub
  13.297 +        have "[| (OK d) <=_(Err.le r) (OK g); (OK e) <=_(Err.le r) (OK g) |]
  13.298 +          ==> (OK d) +_(lift2 f) (OK e) <=_(Err.le r) (OK g)"
  13.299 +          by blast
  13.300 +        hence "[| d <=_r g; e <=_r g |] ==> \<exists>y. d +_f e = OK y \<and> y <=_r g"
  13.301 +          by simp
  13.302 +
  13.303 +        with ok some xyz xz yz
  13.304 +        have "x +_?f y <=_?r z"
  13.305 +          by (auto simp add: sup_def le_def lesub_def lift2_def plussub_def Err.le_def)
  13.306 +      } note this [intro!]
  13.307 +
  13.308 +      from ok xyz xz yz
  13.309 +      have "x +_?f y <=_?r z"
  13.310 +        by - (cases a, simp, cases b, simp, cases c, simp, blast)
  13.311 +    }
  13.312 +    
  13.313 +    with xyz xz yz
  13.314 +    show "x +_?f y <=_?r z"
  13.315 +      by - (cases x, simp, cases y, simp, cases z, simp+)
  13.316 +  qed
  13.317 +
  13.318 +  ultimately
  13.319 +
  13.320 +  show "semilat (?A,?r,?f)"
  13.321 +    by (unfold semilat_def) simp
  13.322 +qed 
  13.323 +
  13.324 +lemma top_le_opt_Some [iff]: 
  13.325 +  "top (le r) (Some T) = top r T"
  13.326 +apply (unfold top_def)
  13.327 +apply (rule iffI)
  13.328 + apply blast
  13.329 +apply (rule allI)
  13.330 +apply (case_tac "x")
  13.331 +apply simp+
  13.332 +done 
  13.333 +
  13.334 +lemma Top_le_conv:
  13.335 +  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
  13.336 +apply (unfold top_def)
  13.337 +apply (blast intro: order_antisym)
  13.338 +done 
  13.339 +
  13.340 +
  13.341 +lemma acc_le_optI [intro!]:
  13.342 +  "acc r ==> acc(le r)"
  13.343 +apply (unfold acc_def lesub_def le_def lesssub_def)
  13.344 +apply (simp add: wf_eq_minimal split: option.split)
  13.345 +apply clarify
  13.346 +apply (case_tac "? a. Some a : Q")
  13.347 + apply (erule_tac x = "{a . Some a : Q}" in allE)
  13.348 + apply blast
  13.349 +apply (case_tac "x")
  13.350 + apply blast
  13.351 +apply blast
  13.352 +done 
  13.353 +
  13.354 +lemma option_map_in_optionI:
  13.355 +  "[| ox : opt S; !x:S. ox = Some x --> f x : S |] 
  13.356 +  ==> option_map f ox : opt S";
  13.357 +apply (unfold option_map_def)
  13.358 +apply (simp split: option.split)
  13.359 +apply blast
  13.360 +done 
  13.361 +
  13.362 +end
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/MicroJava/BV/Product.thy	Mon Nov 20 16:37:42 2000 +0100
    14.3 @@ -0,0 +1,144 @@
    14.4 +(*  Title:      HOL/BCV/Product.thy
    14.5 +    ID:         $Id$
    14.6 +    Author:     Tobias Nipkow
    14.7 +    Copyright   2000 TUM
    14.8 +
    14.9 +Products as semilattices
   14.10 +*)
   14.11 +
   14.12 +header "Products as Semilattices"
   14.13 +
   14.14 +theory Product = Err:
   14.15 +
   14.16 +constdefs
   14.17 + le :: "'a ord => 'b ord => ('a * 'b) ord"
   14.18 +"le rA rB == %(a,b) (a',b'). a <=_rA a' & b <=_rB b'"
   14.19 +
   14.20 + sup :: "'a ebinop => 'b ebinop => ('a * 'b)ebinop"
   14.21 +"sup f g == %(a1,b1)(a2,b2). Err.sup Pair (a1 +_f a2) (b1 +_g b2)"
   14.22 +
   14.23 + esl :: "'a esl => 'b esl => ('a * 'b ) esl"
   14.24 +"esl == %(A,rA,fA) (B,rB,fB). (A <*> B, le rA rB, sup fA fB)"
   14.25 +
   14.26 +syntax "@lesubprod" :: "'a*'b => 'a ord => 'b ord => 'b => bool"
   14.27 +       ("(_ /<='(_,_') _)" [50, 0, 0, 51] 50)
   14.28 +translations "p <=(rA,rB) q" == "p <=_(Product.le rA rB) q"
   14.29 +
   14.30 +lemma unfold_lesub_prod:
   14.31 +  "p <=(rA,rB) q == le rA rB p q"
   14.32 +  by (simp add: lesub_def)
   14.33 +
   14.34 +lemma le_prod_Pair_conv [iff]:
   14.35 +  "((a1,b1) <=(rA,rB) (a2,b2)) = (a1 <=_rA a2 & b1 <=_rB b2)"
   14.36 +  by (simp add: lesub_def le_def)
   14.37 +
   14.38 +lemma less_prod_Pair_conv:
   14.39 +  "((a1,b1) <_(Product.le rA rB) (a2,b2)) = 
   14.40 +  (a1 <_rA a2 & b1 <=_rB b2 | a1 <=_rA a2 & b1 <_rB b2)"
   14.41 +apply (unfold lesssub_def)
   14.42 +apply simp
   14.43 +apply blast
   14.44 +done
   14.45 +
   14.46 +lemma order_le_prod [iff]:
   14.47 +  "order(Product.le rA rB) = (order rA & order rB)"
   14.48 +apply (unfold order_def)
   14.49 +apply simp
   14.50 +apply blast
   14.51 +done 
   14.52 +
   14.53 +
   14.54 +lemma acc_le_prodI [intro!]:
   14.55 +  "[| acc rA; acc rB |] ==> acc(Product.le rA rB)"
   14.56 +apply (unfold acc_def)
   14.57 +apply (rule wf_subset)
   14.58 + apply (erule wf_lex_prod)
   14.59 + apply assumption
   14.60 +apply (auto simp add: lesssub_def less_prod_Pair_conv lex_prod_def)
   14.61 +done
   14.62 +
   14.63 +
   14.64 +lemma closed_lift2_sup:
   14.65 +  "[| closed (err A) (lift2 f); closed (err B) (lift2 g) |] ==> 
   14.66 +  closed (err(A<*>B)) (lift2(sup f g))";
   14.67 +apply (unfold closed_def plussub_def lift2_def err_def sup_def)
   14.68 +apply (simp split: err.split)
   14.69 +apply blast
   14.70 +done 
   14.71 +
   14.72 +lemma unfold_plussub_lift2:
   14.73 +  "e1 +_(lift2 f) e2 == lift2 f e1 e2"
   14.74 +  by (simp add: plussub_def)
   14.75 +
   14.76 +
   14.77 +lemma plus_eq_Err_conv [simp]:
   14.78 +  "[| x:A; y:A; semilat(err A, Err.le r, lift2 f) |] 
   14.79 +  ==> (x +_f y = Err) = (~(? z:A. x <=_r z & y <=_r z))"
   14.80 +proof -
   14.81 +  have plus_le_conv2:
   14.82 +    "!!r f z. [| z : err A; semilat (err A, r, f); OK x : err A; OK y : err A;
   14.83 +                 OK x +_f OK y <=_r z|] ==> OK x <=_r z \<and> OK y <=_r z"
   14.84 +    by (rule plus_le_conv [THEN iffD1])
   14.85 +  case antecedent
   14.86 +  thus ?thesis
   14.87 +  apply (rule_tac iffI)
   14.88 +   apply clarify
   14.89 +   apply (drule OK_le_err_OK [THEN iffD2])
   14.90 +   apply (drule OK_le_err_OK [THEN iffD2])
   14.91 +   apply (drule semilat_lub)
   14.92 +        apply assumption
   14.93 +       apply assumption
   14.94 +      apply simp
   14.95 +     apply simp
   14.96 +    apply simp
   14.97 +   apply simp
   14.98 +  apply (case_tac "x +_f y")
   14.99 +   apply assumption
  14.100 +  apply (rename_tac "z")
  14.101 +  apply (subgoal_tac "OK z: err A")
  14.102 +  apply (frule plus_le_conv2)
  14.103 +       apply assumption
  14.104 +      apply simp
  14.105 +      apply blast
  14.106 +     apply simp
  14.107 +    apply (blast dest: semilatDorderI order_refl)
  14.108 +   apply blast
  14.109 +  apply (erule subst)
  14.110 +  apply (unfold semilat_def err_def closed_def)
  14.111 +  apply simp
  14.112 +  done
  14.113 +qed
  14.114 +
  14.115 +lemma err_semilat_Product_esl:
  14.116 +  "!!L1 L2. [| err_semilat L1; err_semilat L2 |] ==> err_semilat(Product.esl L1 L2)"
  14.117 +apply (unfold esl_def Err.sl_def)
  14.118 +apply (simp (no_asm_simp) only: split_tupled_all)
  14.119 +apply simp
  14.120 +apply (simp (no_asm) only: semilat_Def)
  14.121 +apply (simp (no_asm_simp) only: semilatDclosedI closed_lift2_sup)
  14.122 +apply (simp (no_asm) only: unfold_lesub_err Err.le_def unfold_plussub_lift2 sup_def)
  14.123 +apply (auto elim: semilat_le_err_OK1 semilat_le_err_OK2
  14.124 +            simp add: lift2_def  split: err.split)
  14.125 +apply (blast dest: semilatDorderI)
  14.126 +apply (blast dest: semilatDorderI)
  14.127 +
  14.128 +apply (rule OK_le_err_OK [THEN iffD1])
  14.129 +apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
  14.130 +apply simp
  14.131 +apply simp
  14.132 +apply simp
  14.133 +apply simp
  14.134 +apply simp
  14.135 +apply simp
  14.136 +
  14.137 +apply (rule OK_le_err_OK [THEN iffD1])
  14.138 +apply (erule subst, subst OK_lift2_OK [symmetric], rule semilat_lub)
  14.139 +apply simp
  14.140 +apply simp
  14.141 +apply simp
  14.142 +apply simp
  14.143 +apply simp
  14.144 +apply simp
  14.145 +done 
  14.146 +
  14.147 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/MicroJava/BV/Semilat.thy	Mon Nov 20 16:37:42 2000 +0100
    15.3 @@ -0,0 +1,235 @@
    15.4 +(*  Title:      HOL/BCV/Semilat.thy
    15.5 +    ID:         $Id$
    15.6 +    Author:     Tobias Nipkow
    15.7 +    Copyright   2000 TUM
    15.8 +
    15.9 +Semilattices
   15.10 +*)
   15.11 +
   15.12 +header "Semilattices"
   15.13 +
   15.14 +theory Semilat = Main:
   15.15 +
   15.16 +types 'a ord    = "'a => 'a => bool"
   15.17 +      'a binop  = "'a => 'a => 'a"
   15.18 +      'a sl     = "'a set * 'a ord * 'a binop"
   15.19 +
   15.20 +consts
   15.21 + "@lesub"   :: "'a => 'a ord => 'a => bool" ("(_ /<='__ _)" [50, 1000, 51] 50)
   15.22 + "@lesssub" :: "'a => 'a ord => 'a => bool" ("(_ /<'__ _)" [50, 1000, 51] 50)
   15.23 +defs
   15.24 +lesub_def:   "x <=_r y == r x y"
   15.25 +lesssub_def: "x <_r y  == x <=_r y & x ~= y"
   15.26 +
   15.27 +consts
   15.28 + "@plussub" :: "'a => ('a => 'b => 'c) => 'b => 'c" ("(_ /+'__ _)" [65, 1000, 66] 65)
   15.29 +defs
   15.30 +plussub_def: "x +_f y == f x y"
   15.31 +
   15.32 +
   15.33 +constdefs
   15.34 + ord :: "('a*'a)set => 'a ord"
   15.35 +"ord r == %x y. (x,y):r"
   15.36 +
   15.37 + order :: "'a ord => bool"
   15.38 +"order r == (!x. x <=_r x) &
   15.39 +            (!x y. x <=_r y & y <=_r x --> x=y) &
   15.40 +            (!x y z. x <=_r y & y <=_r z --> x <=_r z)"
   15.41 +
   15.42 + acc :: "'a ord => bool"
   15.43 +"acc r == wf{(y,x) . x <_r y}"
   15.44 +
   15.45 + top :: "'a ord => 'a => bool"
   15.46 +"top r T == !x. x <=_r T"
   15.47 +
   15.48 + closed :: "'a set => 'a binop => bool"
   15.49 +"closed A f == !x:A. !y:A. x +_f y : A"
   15.50 +
   15.51 + semilat :: "'a sl => bool"
   15.52 +"semilat == %(A,r,f). order r & closed A f &
   15.53 +                (!x:A. !y:A. x <=_r x +_f y)  &
   15.54 +                (!x:A. !y:A. y <=_r x +_f y)  &
   15.55 +                (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
   15.56 +
   15.57 + is_ub :: "('a*'a)set => 'a => 'a => 'a => bool"
   15.58 +"is_ub r x y u == (x,u):r & (y,u):r"
   15.59 +
   15.60 + is_lub :: "('a*'a)set => 'a => 'a => 'a => bool"
   15.61 +"is_lub r x y u == is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
   15.62 +
   15.63 + some_lub :: "('a*'a)set => 'a => 'a => 'a"
   15.64 +"some_lub r x y == SOME z. is_lub r x y z"
   15.65 +
   15.66 +
   15.67 +lemma order_refl [simp, intro]:
   15.68 +  "order r ==> x <=_r x";
   15.69 +  by (simp add: order_def)
   15.70 +
   15.71 +lemma order_antisym:
   15.72 +  "[| order r; x <=_r y; y <=_r x |] ==> x = y"
   15.73 +apply (unfold order_def)
   15.74 +apply (simp (no_asm_simp))  
   15.75 +done
   15.76 +
   15.77 +lemma order_trans:
   15.78 +   "[| order r; x <=_r y; y <=_r z |] ==> x <=_r z"
   15.79 +apply (unfold order_def)
   15.80 +apply blast
   15.81 +done 
   15.82 +
   15.83 +lemma order_less_irrefl [intro, simp]:
   15.84 +   "order r ==> ~ x <_r x"
   15.85 +apply (unfold order_def lesssub_def)
   15.86 +apply blast
   15.87 +done 
   15.88 +
   15.89 +lemma order_less_trans:
   15.90 +  "[| order r; x <_r y; y <_r z |] ==> x <_r z"
   15.91 +apply (unfold order_def lesssub_def)
   15.92 +apply blast
   15.93 +done 
   15.94 +
   15.95 +lemma topD [simp, intro]:
   15.96 +  "top r T ==> x <=_r T"
   15.97 +  by (simp add: top_def)
   15.98 +
   15.99 +lemma top_le_conv [simp]:
  15.100 +  "[| order r; top r T |] ==> (T <=_r x) = (x = T)"
  15.101 +  by (blast intro: order_antisym)
  15.102 +
  15.103 +lemma semilat_Def:
  15.104 +"semilat(A,r,f) == order r & closed A f & 
  15.105 +                 (!x:A. !y:A. x <=_r x +_f y) & 
  15.106 +                 (!x:A. !y:A. y <=_r x +_f y) & 
  15.107 +                 (!x:A. !y:A. !z:A. x <=_r z & y <=_r z --> x +_f y <=_r z)"
  15.108 +apply (unfold semilat_def Product_Type.split [THEN eq_reflection])
  15.109 +apply (rule refl [THEN eq_reflection])
  15.110 +done
  15.111 +
  15.112 +lemma semilatDorderI [simp, intro]:
  15.113 +  "semilat(A,r,f) ==> order r"
  15.114 +  by (simp add: semilat_Def)
  15.115 +
  15.116 +lemma semilatDclosedI [simp, intro]:
  15.117 +  "semilat(A,r,f) ==> closed A f"
  15.118 +apply (unfold semilat_Def)
  15.119 +apply simp
  15.120 +done
  15.121 +
  15.122 +lemma semilat_ub1 [simp]:
  15.123 +  "[| semilat(A,r,f); x:A; y:A |] ==> x <=_r x +_f y"
  15.124 +  by (unfold semilat_Def, simp)
  15.125 +
  15.126 +lemma semilat_ub2 [simp]:
  15.127 +  "[| semilat(A,r,f); x:A; y:A |] ==> y <=_r x +_f y"
  15.128 +  by (unfold semilat_Def, simp)
  15.129 +
  15.130 +lemma semilat_lub [simp]:
  15.131 + "[| x <=_r z; y <=_r z; semilat(A,r,f); x:A; y:A; z:A |] ==> x +_f y <=_r z";
  15.132 +  by (unfold semilat_Def, simp)
  15.133 +
  15.134 +
  15.135 +lemma plus_le_conv [simp]:
  15.136 +  "[| x:A; y:A; z:A; semilat(A,r,f) |] 
  15.137 +  ==> (x +_f y <=_r z) = (x <=_r z & y <=_r z)"
  15.138 +apply (unfold semilat_Def)
  15.139 +apply (blast intro: semilat_ub1 semilat_ub2 semilat_lub order_trans)
  15.140 +done
  15.141 +
  15.142 +lemma le_iff_plus_unchanged:
  15.143 +  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (x +_f y = y)"
  15.144 +apply (rule iffI)
  15.145 + apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub2, assumption+)
  15.146 +apply (erule subst)
  15.147 +apply simp
  15.148 +done 
  15.149 +
  15.150 +lemma le_iff_plus_unchanged2:
  15.151 +  "[| x:A; y:A; semilat(A,r,f) |] ==> (x <=_r y) = (y +_f x = y)"
  15.152 +apply (rule iffI)
  15.153 + apply (intro semilatDorderI order_antisym semilat_lub order_refl semilat_ub1, assumption+)
  15.154 +apply (erule subst)
  15.155 +apply simp
  15.156 +done 
  15.157 +
  15.158 +(*** closed ***)
  15.159 +
  15.160 +lemma closedD:
  15.161 +  "[| closed A f; x:A; y:A |] ==> x +_f y : A"
  15.162 +apply (unfold closed_def)
  15.163 +apply blast
  15.164 +done 
  15.165 +
  15.166 +lemma closed_UNIV [simp]: "closed UNIV f"
  15.167 +  by (simp add: closed_def)
  15.168 +
  15.169 +(*** lub ***)
  15.170 +
  15.171 +lemma is_lubD:
  15.172 +  "is_lub r x y u ==> is_ub r x y u & (!z. is_ub r x y z --> (u,z):r)"
  15.173 +  by (simp add: is_lub_def)
  15.174 +
  15.175 +lemma is_ubI:
  15.176 +  "[| (x,u) : r; (y,u) : r |] ==> is_ub r x y u"
  15.177 +  by (simp add: is_ub_def)
  15.178 +
  15.179 +lemma is_ubD:
  15.180 +  "is_ub r x y u ==> (x,u) : r & (y,u) : r"
  15.181 +  by (simp add: is_ub_def)
  15.182 +
  15.183 +
  15.184 +lemma is_lub_bigger1 [iff]:  
  15.185 +  "is_lub (r^* ) x y y = ((x,y):r^* )"
  15.186 +apply (unfold is_lub_def is_ub_def)
  15.187 +apply blast
  15.188 +done
  15.189 +
  15.190 +
  15.191 +lemma is_lub_bigger2 [iff]:
  15.192 +  "is_lub (r^* ) x y x = ((y,x):r^* )"
  15.193 +apply (unfold is_lub_def is_ub_def)
  15.194 +apply blast 
  15.195 +done 
  15.196 +
  15.197 +
  15.198 +lemma extend_lub:
  15.199 +  "[| univalent r; is_lub (r^* ) x y u; (x',x) : r |] 
  15.200 +  ==> EX v. is_lub (r^* ) x' y v"
  15.201 +apply (unfold is_lub_def is_ub_def)
  15.202 +apply (case_tac "(y,x) : r^*")
  15.203 + apply (case_tac "(y,x') : r^*")
  15.204 +  apply blast
  15.205 + apply (blast intro: r_into_rtrancl elim: converse_rtranclE
  15.206 +               dest: univalentD)
  15.207 +apply (rule exI)
  15.208 +apply (rule conjI)
  15.209 + apply (blast intro: rtrancl_into_rtrancl2 dest: univalentD)
  15.210 +apply (blast intro: rtrancl_into_rtrancl rtrancl_into_rtrancl2 
  15.211 +             elim: converse_rtranclE dest: univalentD)
  15.212 +done 
  15.213 +
  15.214 +lemma univalent_has_lubs [rule_format]:
  15.215 +  "[| univalent r; (x,u) : r^* |] ==> (!y. (y,u) : r^* --> 
  15.216 +  (EX z. is_lub (r^* ) x y z))"
  15.217 +apply (erule converse_rtrancl_induct)
  15.218 + apply clarify
  15.219 + apply (erule converse_rtrancl_induct)
  15.220 +  apply blast
  15.221 + apply (blast intro: rtrancl_into_rtrancl2)
  15.222 +apply (blast intro: extend_lub)
  15.223 +done
  15.224 +
  15.225 +lemma some_lub_conv:
  15.226 +  "[| acyclic r; is_lub (r^* ) x y u |] ==> some_lub (r^* ) x y = u"
  15.227 +apply (unfold some_lub_def is_lub_def)
  15.228 +apply (rule someI2)
  15.229 + apply assumption
  15.230 +apply (blast intro: antisymD dest!: acyclic_impl_antisym_rtrancl)
  15.231 +done 
  15.232 +
  15.233 +lemma is_lub_some_lub:
  15.234 +  "[| univalent r; acyclic r; (x,u):r^*; (y,u):r^* |] 
  15.235 +  ==> is_lub (r^* ) x y (some_lub (r^* ) x y)";
  15.236 +  by (fastsimp dest: univalent_has_lubs simp add: some_lub_conv)
  15.237 +
  15.238 +end
    16.1 --- a/src/HOL/MicroJava/BV/Step.thy	Sat Nov 18 19:48:34 2000 +0100
    16.2 +++ b/src/HOL/MicroJava/BV/Step.thy	Mon Nov 20 16:37:42 2000 +0100
    16.3 @@ -15,8 +15,8 @@
    16.4  step' :: "instr \<times> jvm_prog \<times> state_type => state_type"
    16.5  
    16.6  recdef step' "{}"
    16.7 -"step' (Load idx,  G, (ST, LT))          = (val (LT ! idx) # ST, LT)"
    16.8 -"step' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= Ok ts])"
    16.9 +"step' (Load idx,  G, (ST, LT))          = (ok_val (LT ! idx) # ST, LT)"
   16.10 +"step' (Store idx, G, (ts#ST, LT))       = (ST, LT[idx:= OK ts])"
   16.11  "step' (Bipush i, G, (ST, LT))           = (PrimT Integer # ST, LT)"
   16.12  "step' (Aconst_null, G, (ST, LT))        = (NT#ST,LT)"
   16.13  "step' (Getfield F C, G, (oT#ST, LT))    = (snd (the (field (G,C) F)) # ST, LT)"
   16.14 @@ -32,12 +32,11 @@
   16.15                                           = (PrimT Integer#ST,LT)"
   16.16  "step' (Ifcmpeq b, G, (ts1#ts2#ST,LT))   = (ST,LT)"
   16.17  "step' (Goto b, G, s)                    = s"
   16.18 -  (* Return has no successor instruction in the same method: *)
   16.19 -(* "step' (Return, G, (T#ST,LT))            = None" *)
   16.20 +  (* Return has no successor instruction in the same method *)
   16.21 +"step' (Return, G, s)                    = s" 
   16.22  "step' (Invoke C mn fpTs, G, (ST,LT))    = (let ST' = drop (length fpTs) ST 
   16.23    in  (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))" 
   16.24  
   16.25 -(* "step' (i,G,s)                           = None" *)
   16.26  
   16.27  constdefs
   16.28    step :: "instr => jvm_prog => state_type option => state_type option"
   16.29 @@ -113,7 +112,7 @@
   16.30  "succs IAdd pc               = [pc+1]"
   16.31  "succs (Ifcmpeq b) pc        = [pc+1, nat (int pc + b)]"
   16.32  "succs (Goto b) pc           = [nat (int pc + b)]"
   16.33 -"succs Return pc             = []"  
   16.34 +"succs Return pc             = [pc]"  
   16.35  "succs (Invoke C mn fpTs) pc = [pc+1]"
   16.36  
   16.37  
    17.1 --- a/src/HOL/MicroJava/BV/StepMono.thy	Sat Nov 18 19:48:34 2000 +0100
    17.2 +++ b/src/HOL/MicroJava/BV/StepMono.thy	Mon Nov 20 16:37:42 2000 +0100
    17.3 @@ -14,8 +14,8 @@
    17.4  
    17.5  
    17.6  lemma sup_loc_some [rule_format]:
    17.7 -"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = Ok t --> 
    17.8 -  (\<exists>t. b!n = Ok t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
    17.9 +"\<forall> y n. (G \<turnstile> b <=l y) --> n < length y --> y!n = OK t --> 
   17.10 +  (\<exists>t. b!n = OK t \<and> (G \<turnstile> (b!n) <=o (y!n)))" (is "?P b")
   17.11  proof (induct (open) ?P b)
   17.12    show "?P []" by simp
   17.13  
   17.14 @@ -25,12 +25,12 @@
   17.15      fix z zs n
   17.16      assume * : 
   17.17        "G \<turnstile> a <=o z" "list_all2 (sup_ty_opt G) list zs" 
   17.18 -      "n < Suc (length zs)" "(z # zs) ! n = Ok t"
   17.19 +      "n < Suc (length zs)" "(z # zs) ! n = OK t"
   17.20  
   17.21 -    show "(\<exists>t. (a # list) ! n = Ok t) \<and> G \<turnstile>(a # list) ! n <=o Ok t" 
   17.22 +    show "(\<exists>t. (a # list) ! n = OK t) \<and> G \<turnstile>(a # list) ! n <=o OK t" 
   17.23      proof (cases n) 
   17.24        case 0
   17.25 -      with * show ?thesis by (simp add: sup_ty_opt_Ok)
   17.26 +      with * show ?thesis by (simp add: sup_ty_opt_OK)
   17.27      next
   17.28        case Suc
   17.29        with Cons *
   17.30 @@ -42,7 +42,7 @@
   17.31  
   17.32  lemma all_widen_is_sup_loc:
   17.33  "\<forall>b. length a = length b --> 
   17.34 -     (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map Ok a) <=l (map Ok b))" 
   17.35 +     (\<forall>x\<in>set (zip a b). x \<in> widen G) = (G \<turnstile> (map OK a) <=l (map OK b))" 
   17.36   (is "\<forall>b. length a = length b --> ?Q a b" is "?P a")
   17.37  proof (induct "a")
   17.38    show "?P []" by simp
   17.39 @@ -273,14 +273,14 @@
   17.40          by - (rule widen_trans, auto)
   17.41      
   17.42        from G'
   17.43 -      have "G \<turnstile> map Ok apTs' <=l map Ok apTs"
   17.44 +      have "G \<turnstile> map OK apTs' <=l map OK apTs"
   17.45          by (simp add: sup_state_def)
   17.46        also
   17.47        from l w
   17.48 -      have "G \<turnstile> map Ok apTs <=l map Ok list" 
   17.49 +      have "G \<turnstile> map OK apTs <=l map OK list" 
   17.50          by (simp add: all_widen_is_sup_loc)
   17.51        finally
   17.52 -      have "G \<turnstile> map Ok apTs' <=l map Ok list" .
   17.53 +      have "G \<turnstile> map OK apTs' <=l map OK list" .
   17.54  
   17.55        with l'
   17.56        have w': "\<forall>x \<in> set (zip apTs' list). x \<in> widen G"
   17.57 @@ -302,12 +302,11 @@
   17.58  lemmas [simp] = step_def
   17.59  
   17.60  lemma step_mono_Some:
   17.61 -"[| succs i pc \<noteq> []; app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
   17.62 +"[| app i G rT (Some s2); G \<turnstile> s1 <=s s2 |] ==>
   17.63    G \<turnstile> the (step i G (Some s1)) <=s the (step i G (Some s2))"
   17.64  proof (cases s1, cases s2) 
   17.65    fix a1 b1 a2 b2
   17.66    assume s: "s1 = (a1,b1)" "s2 = (a2,b2)"
   17.67 -  assume succs: "succs i pc \<noteq> []"
   17.68    assume app2: "app i G rT (Some s2)"
   17.69    assume G: "G \<turnstile> s1 <=s s2"
   17.70  
   17.71 @@ -330,11 +329,11 @@
   17.72  
   17.73      with s app1
   17.74      obtain y where
   17.75 -       y:  "nat < length b1" "b1 ! nat = Ok y" by clarsimp
   17.76 +       y:  "nat < length b1" "b1 ! nat = OK y" by clarsimp
   17.77  
   17.78      from Load s app2
   17.79      obtain y' where
   17.80 -       y': "nat < length b2" "b2 ! nat = Ok y'" by clarsimp
   17.81 +       y': "nat < length b2" "b2 ! nat = OK y'" by clarsimp
   17.82  
   17.83      from G s 
   17.84      have "G \<turnstile> b1 <=l b2" by (simp add: sup_state_def)
   17.85 @@ -415,9 +414,10 @@
   17.86      show ?thesis 
   17.87        by (clarsimp simp add: sup_state_def)
   17.88    next
   17.89 -    case Return
   17.90 -    with succs have "False" by simp
   17.91 -    thus ?thesis by blast
   17.92 +    case Return 
   17.93 +    with G step
   17.94 +    show ?thesis
   17.95 +      by simp
   17.96    next
   17.97      case Pop
   17.98      with G s step app1 app2
   17.99 @@ -464,7 +464,7 @@
  17.100  qed
  17.101  
  17.102  lemma step_mono:
  17.103 -  "[| succs i pc \<noteq> []; app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
  17.104 +  "[| app i G rT s2; G \<turnstile> s1 <=' s2 |] ==>
  17.105    G \<turnstile> step i G s1 <=' step i G s2"
  17.106    by (cases s1, cases s2, auto dest: step_mono_Some)
  17.107