# HG changeset patch
# User kleing
# Date 976626528 -3600
# Node ID bb3a81a005f75d6da247ba95b23fccaee7eeabff
# Parent  114999ff8d1986906a399365d3033ec4bced9d8d
completeness (unfinished)

diff -r 114999ff8d19 -r bb3a81a005f7 src/HOL/MicroJava/BV/JVM.thy
--- a/src/HOL/MicroJava/BV/JVM.thy	Tue Dec 12 14:08:26 2000 +0100
+++ b/src/HOL/MicroJava/BV/JVM.thy	Tue Dec 12 14:08:48 2000 +0100
@@ -386,6 +386,107 @@
   thus ?thesis by blast
 qed
 
+
+(* there's still two nontrivial (but provable) "sorry"s in here  *)
+theorem wt_kil_complete:
+  "[| wt_method G C pTs rT maxs mxl bs phi; wf_prog wf_mb G; 
+      length phi = length bs; is_class G C; \<forall>x \<in> set pTs. is_type G x |]
+  ==> wt_kil G C pTs rT maxs mxl bs"
+proof -
+  assume wf:      "wf_prog wf_mb G"  
+  assume isclass: "is_class G C"
+  assume istype:  "\<forall>x \<in> set pTs. is_type G x"
+  assume length:  "length phi = length bs"
+
+  assume "wt_method G C pTs rT maxs mxl bs phi"
+  then obtain
+    instrs:   "0 < length bs" and
+    wt_start: "wt_start G C pTs mxl phi" and
+    wt_ins:   "\<forall>pc. pc < length bs \<longrightarrow> 
+                    wt_instr (bs ! pc) G rT phi maxs (length bs) pc"
+    by (unfold wt_method_def) simp
+
+  let ?succs = "\<lambda>pc. succs (bs!pc) pc"
+  let ?step  = "\<lambda>pc. step (bs!pc) G"
+  let ?app   = "\<lambda>pc. app (bs!pc) G maxs rT"
+
+  from wt_ins
+  have bounded: "bounded ?succs (size bs)"
+    by (unfold wt_instr_def bounded_def) blast
+
+  from wt_ins
+  have "static_wt (sup_state_opt G) ?app ?step ?succs phi"
+    apply (unfold static_wt_def wt_instr_def lesub_def)
+    apply (simp (no_asm) only: length)
+    apply blast
+    done
+
+  with bounded
+  have "dynamic_wt (sup_state_opt G) (err_step ?app ?step) ?succs (map OK phi)"
+    by - (erule static_imp_dynamic, simp add: length)
+
+  hence dynamic:
+    "dynamic_wt (sup_state_opt G) (exec G maxs rT bs) ?succs (map OK phi)"
+    by (unfold exec_def)
+ 
+  let ?maxr = "1+size pTs+mxl"
+
+  from wf bounded
+  have is_bcv: 
+    "is_bcv (JVM.le G maxs ?maxr) Err (exec G maxs rT bs) ?succs 
+            (size bs) (states G maxs ?maxr) (kiljvm G maxs ?maxr rT bs)"
+    by (rule is_bcv_kiljvm)
+
+  let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)))
+                #(replicate (size bs-1) (OK None))"
+
+  { fix l x
+    have "set (replicate l x) \<subseteq> {x}"
+      by (cases "0 < l") simp+
+  } note subset_replicate = this
+
+  from istype
+  have "set pTs \<subseteq> types G"
+    by auto
+
+  hence "OK `` set pTs \<subseteq> err (types G)"
+    by auto
+
+  with instrs isclass 
+  have start:
+    "?start \<in> list (length bs) (states G maxs ?maxr)"
+    apply (unfold list_def JVM_states_unfold)
+    apply simp
+    apply (rule conjI)
+     apply (simp add: Un_subset_iff)
+     apply (rule_tac B = "{Err}" in subset_trans)
+      apply (simp add: subset_replicate)
+     apply simp
+    apply (rule_tac B = "{OK None}" in subset_trans)
+     apply (simp add: subset_replicate)
+    apply simp
+    done
+
+  let ?phi = "map OK phi"
+
+  have 1: "?phi \<in> list (length bs) (states G maxs ?maxr)" sorry
+
+  from wt_start
+  have 2: "?start <=[le G maxs ?maxr] ?phi" sorry
+
+  from dynamic
+  have "welltyping (le G maxs ?maxr) Err (exec G maxs rT bs) ?succs ?phi"
+    by (simp add: dynamic_wt_def JVM_le_Err_conv)
+  
+  with start 1 2 is_bcv
+  have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?maxr rT bs ?start ! p \<noteq> Err"
+    by (unfold is_bcv_def) blast
+
+  with bounded instrs
+  show "wt_kil G C pTs rT maxs mxl bs"
+    by (unfold wt_kil_def) simp
+qed
+
 lemma is_type_pTs:
   "[| wf_prog wf_mb G; (C,S,fs,mdecls) \<in> set G; (sig,rT,code) \<in> set mdecls; 
       t \<in> set (snd sig) |]