(* Title: HOL/MicroJava/Comp/CorrCompTp.thy
Author: Martin Strecker
*)
theory CorrCompTp
imports LemmasComp TypeInf "../BV/JVM" "../BV/Altern"
begin
declare split_paired_All [simp del]
declare split_paired_Ex [simp del]
(**********************************************************************)
definition inited_LT :: "[cname, ty list, (vname \ ty) list] \ locvars_type" where
"inited_LT C pTs lvars == (OK (Class C))#((map OK pTs))@(map (Fun.comp OK snd) lvars)"
definition is_inited_LT :: "[cname, ty list, (vname \ ty) list, locvars_type] \ bool" where
"is_inited_LT C pTs lvars LT == (LT = (inited_LT C pTs lvars))"
definition local_env :: "[java_mb prog, cname, sig, vname list,(vname \ ty) list] \ java_mb env" where
"local_env G C S pns lvars ==
let (mn, pTs) = S in (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C))"
lemma local_env_fst [simp]: "fst (local_env G C S pns lvars) = G"
by (simp add: local_env_def split_beta)
lemma wt_class_expr_is_class:
"\ ws_prog G; E \ expr :: Class cname; E = local_env G C (mn, pTs) pns lvars\
\<Longrightarrow> is_class G cname "
apply (subgoal_tac "((fst E), (snd E)) \ expr :: Class cname")
apply (frule ty_expr_is_type)
apply simp
apply simp
apply (simp (no_asm_use))
done
(********************************************************************************)
subsection "index"
lemma local_env_snd:
"snd (local_env G C (mn, pTs) pns lvars) = map_of lvars(pns[\]pTs)(This\Class C)"
by (simp add: local_env_def)
lemma index_in_bounds:
"length pns = length pTs \
snd (local_env G C (mn, pTs) pns lvars) vname = Some T
\<Longrightarrow> index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)"
apply (simp add: local_env_snd index_def split_beta)
apply (case_tac "vname = This")
apply (simp add: inited_LT_def)
apply simp
apply (drule map_of_upds_SomeD)
apply (drule length_takeWhile)
apply (simp add: inited_LT_def)
done
lemma map_upds_append:
"length k1s = length x1s \ m(k1s[\]x1s)(k2s[\]x2s) = m ((k1s@k2s)[\](x1s@x2s))"
apply (induct k1s arbitrary: x1s m)
apply simp
apply (subgoal_tac "\x xr. x1s = x # xr")
apply clarsimp
(* subgoal *)
apply (case_tac x1s)
apply auto
done
lemma map_of_append:
"map_of ((rev xs) @ ys) = (map_of ys) ((map fst xs) [\] (map snd xs))"
apply (induct xs arbitrary: ys)
apply simp
apply (rename_tac a xs ys)
apply (drule_tac x="a # ys" in meta_spec)
apply (simp only: rev.simps append_assoc append_Cons append_Nil
list.map map_of.simps map_upds_Cons list.sel)
done
lemma map_of_as_map_upds: "map_of (rev xs) = Map.empty ((map fst xs) [\] (map snd xs))"
by (rule map_of_append [of _ "[]", simplified])
lemma map_of_rev: "unique xs \ map_of (rev xs) = map_of xs"
apply (induct xs)
apply simp
apply (simp add: unique_def map_of_append map_of_as_map_upds [symmetric]
Map.map_of_append[symmetric] del:Map.map_of_append)
done
lemma map_upds_rev:
"\ distinct ks; length ks = length xs \ \ m (rev ks [\] rev xs) = m (ks [\] xs)"
apply (induct ks arbitrary: xs)
apply simp
apply (subgoal_tac "\x xr. xs = x # xr")
apply clarify
apply (drule_tac x=xr in meta_spec)
apply (simp add: map_upds_append [symmetric])
apply (case_tac xs, auto)
done
lemma map_upds_takeWhile [rule_format]:
"\ks. (Map.empty(rev ks[\]rev xs)) k = Some x \ length ks = length xs \
xs ! length (takeWhile (\<lambda>z. z \<noteq> k) ks) = x"
apply (induct xs)
apply simp
apply (intro strip)
apply (subgoal_tac "\k' kr. ks = k' # kr")
apply (clarify)
apply (drule_tac x=kr in spec)
apply (simp only: rev.simps)
apply (subgoal_tac "(Map.empty(rev kr @ [k'][\]rev xs @ [a])) = Map.empty (rev kr[\]rev xs)([k'][\][a])")
apply (simp split:if_split_asm)
apply (simp add: map_upds_append [symmetric])
apply (case_tac ks)
apply auto
done
lemma local_env_inited_LT:
"\ snd (local_env G C (mn, pTs) pns lvars) vname = Some T;
length pns = length pTs; distinct pns; unique lvars \<rbrakk>
\<Longrightarrow> (inited_LT C pTs lvars ! index (pns, lvars, blk, res) vname) = OK T"
apply (simp add: local_env_snd index_def)
apply (case_tac "vname = This")
apply (simp add: inited_LT_def)
apply (simp add: inited_LT_def)
apply (simp (no_asm_simp) only: map_map [symmetric] map_append [symmetric] list.map [symmetric])
apply (subgoal_tac "length (takeWhile (\z. z \ vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars)")
apply (simp (no_asm_simp) only: List.nth_map ok_val.simps)
apply (subgoal_tac "map_of lvars = map_of (map (\ p. (fst p, snd p)) lvars)")
apply (simp only:)
apply (subgoal_tac "distinct (map fst lvars)")
apply (frule_tac g=snd in AuxLemmas.map_of_map_as_map_upd)
apply (simp only:)
apply (simp add: map_upds_append)
apply (frule map_upds_SomeD)
apply (rule map_upds_takeWhile)
apply (simp (no_asm_simp))
apply (simp add: map_upds_append [symmetric])
apply (simp add: map_upds_rev)
(* show length (pns @ map fst lvars) = length (pTs @ map snd lvars) *)
apply simp
(* show distinct (map fst lvars) *)
apply (simp only: unique_def Fun.comp_def)
(* show map_of lvars = map_of (map (\<lambda>p. (fst p, snd p)) lvars) *)
apply simp
(* show length (takeWhile (\<lambda>z. z \<noteq> vname) (pns @ map fst lvars)) < length (pTs @ map snd lvars) *)
apply (drule map_of_upds_SomeD)
apply (drule length_takeWhile)
apply simp
done
lemma inited_LT_at_index_no_err:
"i < length (inited_LT C pTs lvars) \ inited_LT C pTs lvars ! i \ Err"
apply (simp only: inited_LT_def)
apply (simp only: map_map [symmetric] map_append [symmetric] list.map [symmetric] length_map)
apply (simp only: nth_map)
apply simp
done
lemma sup_loc_update_index: "
\<lbrakk> G \<turnstile> T \<preceq> T'; is_type G T'; length pns = length pTs; distinct pns; unique lvars;
snd (local_env G C (mn, pTs) pns lvars) vname = Some T' \
\<Longrightarrow>
comp G \<turnstile> (inited_LT C pTs lvars) [index (pns, lvars, blk, res) vname := OK T] <=l
inited_LT C pTs lvars"
apply (subgoal_tac " index (pns, lvars, blk, res) vname < length (inited_LT C pTs lvars)")
apply (frule_tac blk=blk and res=res in local_env_inited_LT, assumption+)
apply (rule sup_loc_trans)
apply (rule_tac b="OK T'" in sup_loc_update)
apply (simp add: comp_widen)
apply assumption
apply (rule sup_loc_refl)
apply (simp add: list_update_same_conv [THEN iffD2])
(* subgoal *)
apply (rule index_in_bounds)
apply simp+
done
(********************************************************************************)
subsection "Preservation of ST and LT by compTpExpr / compTpStmt"
lemma sttp_of_comb_nil [simp]: "sttp_of (comb_nil sttp) = sttp"
by (simp add: comb_nil_def)
lemma mt_of_comb_nil [simp]: "mt_of (comb_nil sttp) = []"
by (simp add: comb_nil_def)
lemma sttp_of_comb [simp]: "sttp_of ((f1 \ f2) sttp) = sttp_of (f2 (sttp_of (f1 sttp)))"
apply (case_tac "f1 sttp")
apply (case_tac "(f2 (sttp_of (f1 sttp)))")
apply (simp add: comb_def)
done
lemma mt_of_comb: "(mt_of ((f1 \ f2) sttp)) =
(mt_of (f1 sttp)) @ (mt_of (f2 (sttp_of (f1 sttp))))"
by (simp add: comb_def split_beta)
lemma mt_of_comb_length [simp]: "\ n1 = length (mt_of (f1 sttp)); n1 \ n \
\<Longrightarrow> (mt_of ((f1 \<box> f2) sttp) ! n) = (mt_of (f2 (sttp_of (f1 sttp))) ! (n - n1))"
by (simp add: comb_def nth_append split_beta)
lemma compTpExpr_Exprs_LT_ST: "
\<lbrakk>jmb = (pns, lvars, blk, res);
wf_prog wf_java_mdecl G;
wf_java_mdecl G C ((mn, pTs), rT, jmb);
E = local_env G C (mn, pTs) pns lvars \<rbrakk>
\<Longrightarrow>
(\<forall> ST LT T.
E \<turnstile> ex :: T \<longrightarrow>
is_inited_LT C pTs lvars LT \<longrightarrow>
sttp_of (compTpExpr jmb G ex (ST, LT)) = (T # ST, LT))
\<and>
(\<forall> ST LT Ts.
E \<turnstile> exs [::] Ts \<longrightarrow>
is_inited_LT C pTs lvars LT \<longrightarrow>
sttp_of (compTpExprs jmb G exs (ST, LT)) = ((rev Ts) @ ST, LT))"
apply (rule compat_expr_expr_list.induct)
(* expresssions *)
(* NewC *)
apply (intro strip)
apply (drule NewC_invers)
apply (simp add: pushST_def)
(* Cast *)
apply (intro strip)
apply (drule Cast_invers, clarify)
apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
apply (simp add: replST_def split_beta)
(* Lit *)
apply (intro strip)
apply (drule Lit_invers)
apply (simp add: pushST_def)
(* BinOp *)
apply (intro strip)
apply (drule BinOp_invers, clarify)
apply (drule_tac x=ST in spec)
apply (drule_tac x="Ta # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
apply (rename_tac binop x2 x3 ST LT T Ta, case_tac binop)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: popST_def pushST_def)
apply (simp)
apply (simp (no_asm_simp) add: replST_def)
(* LAcc *)
apply (intro strip)
apply (drule LAcc_invers)
apply (simp add: pushST_def is_inited_LT_def)
apply (simp add: wf_prog_def)
apply (frule wf_java_mdecl_disjoint_varnames)
apply (simp add: disjoint_varnames_def)
apply (frule wf_java_mdecl_length_pTs_pns)
apply (erule conjE)+
apply (simp (no_asm_simp) add: local_env_inited_LT)
(* LAss *)
apply (intro strip)
apply (drule LAss_invers, clarify)
apply (drule LAcc_invers)
apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
apply (simp add: popST_def dupST_def)
(* FAcc *)
apply (intro strip)
apply (drule FAcc_invers, clarify)
apply ((drule_tac x=ST in spec), (drule spec)+, (drule mp, assumption)+)
apply (simp add: replST_def)
(* show snd (the (field (G, cname) vname)) = T *)
apply (subgoal_tac "is_class G Ca")
apply (rename_tac cname x2 vname ST LT T Ca, subgoal_tac "is_class G cname \ field (G, cname) vname = Some (cname, T)")
apply simp
(* show is_class G cname \<and> field (G, cname) vname = Some (cname, T) *)
apply (rule field_in_fd) apply assumption+
(* show is_class G Ca *)
apply (fast intro: wt_class_expr_is_class)
(* FAss *)
apply (intro strip)
apply (drule FAss_invers, clarify)
apply (drule FAcc_invers, clarify)
apply (drule_tac x=ST in spec)
apply (drule_tac x="Class Ca # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
apply (simp add: popST_def dup_x1ST_def)
(* Call *)
apply (intro strip)
apply (drule Call_invers, clarify)
apply (drule_tac x=ST in spec)
apply (rename_tac cname x2 x3 x4 x5 ST LT T pTsa md, drule_tac x="Class cname # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
apply (simp add: replST_def)
(* expression lists *)
(* nil *)
apply (intro strip)
apply (drule Nil_invers)
apply (simp add: comb_nil_def)
(* cons *)
apply (intro strip)
apply (drule Cons_invers, clarify)
apply (drule_tac x=ST in spec)
apply (drule_tac x="T # ST" in spec)
apply ((drule spec)+, (drule mp, assumption)+)
apply simp
done
lemmas compTpExpr_LT_ST [rule_format (no_asm)] =
compTpExpr_Exprs_LT_ST [THEN conjunct1]
lemmas compTpExprs_LT_ST [rule_format (no_asm)] =
compTpExpr_Exprs_LT_ST [THEN conjunct2]
lemma compTpStmt_LT_ST [rule_format (no_asm)]: "
\<lbrakk> jmb = (pns,lvars,blk,res);
wf_prog wf_java_mdecl G;
wf_java_mdecl G C ((mn, pTs), rT, jmb);
E = (local_env G C (mn, pTs) pns lvars)\<rbrakk>
\<Longrightarrow> (\<forall> ST LT.
E \<turnstile> s\<surd> \<longrightarrow>
(is_inited_LT C pTs lvars LT)
\<longrightarrow> sttp_of (compTpStmt jmb G s (ST, LT)) = (ST, LT))"
apply (rule stmt.induct)
(* Skip *)
apply (intro strip)
apply simp
(* Expr *)
apply (intro strip)
apply (drule Expr_invers, erule exE)
apply (simp (no_asm_simp) add: compTpExpr_LT_ST)
apply (frule_tac ST=ST in compTpExpr_LT_ST, assumption+)
apply (simp add: popST_def)
(* Comp *)
apply (intro strip)
apply (drule Comp_invers, clarify)
apply (simp (no_asm_use))
apply simp
(* Cond *)
apply (intro strip)
apply (drule Cond_invers)
apply (erule conjE)+
apply (drule_tac x=ST in spec)
apply (drule_tac x=ST in spec)
apply (drule spec)+ apply (drule mp, assumption)+
apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
apply (simp add: popST_def pushST_def nochangeST_def)
(* Loop *)
apply (intro strip)
apply (drule Loop_invers)
apply (erule conjE)+
apply (drule_tac x=ST in spec)
apply (drule spec)+ apply (drule mp, assumption)+
apply (drule_tac ST="PrimT Boolean # ST" in compTpExpr_LT_ST, assumption+)
apply (simp add: popST_def pushST_def nochangeST_def)
done
lemma compTpInit_LT_ST: "
sttp_of (compTpInit jmb (vn,ty) (ST, LT)) = (ST, LT[(index jmb vn):= OK ty])"
by (simp add: compTpInit_def storeST_def pushST_def)
lemma compTpInitLvars_LT_ST_aux [rule_format (no_asm)]:
"\ pre lvars_pre lvars0.
jmb = (pns,lvars0,blk,res) \<and>
lvars0 = (lvars_pre @ lvars) \<and>
(length pns) + (length lvars_pre) + 1 = length pre \<and>
disjoint_varnames pns (lvars_pre @ lvars)
\<longrightarrow>
sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err))
= (ST, pre @ map (Fun.comp OK snd) lvars)"
supply [[simproc del: defined_all]]
apply (induct lvars)
apply simp
apply (intro strip)
apply (subgoal_tac "\vn ty. a = (vn, ty)")
prefer 2
apply (simp (no_asm_simp))
apply ((erule exE)+, simp (no_asm_simp))
apply (drule_tac x="pre @ [OK ty]" in spec)
apply (drule_tac x="lvars_pre @ [a]" in spec)
apply (drule_tac x="lvars0" in spec)
apply (simp add: compTpInit_LT_ST index_of_var2)
done
lemma compTpInitLvars_LT_ST:
"\ jmb = (pns, lvars, blk, res); wf_java_mdecl G C ((mn, pTs), rT, jmb) \
\<Longrightarrow> sttp_of (compTpInitLvars jmb lvars (ST, start_LT C pTs (length lvars)))
= (ST, inited_LT C pTs lvars)"
apply (simp add: start_LT_def inited_LT_def)
apply (simp only: append_Cons [symmetric])
apply (rule compTpInitLvars_LT_ST_aux)
apply (auto dest: wf_java_mdecl_length_pTs_pns wf_java_mdecl_disjoint_varnames)
done
(********************************************************************************)
lemma max_of_list_elem: "x \ set xs \ x \ (max_of_list xs)"
by (induct xs, auto intro: max.cobounded1 simp: le_max_iff_disj max_of_list_def)
lemma max_of_list_sublist: "set xs \ set ys
\<Longrightarrow> (max_of_list xs) \<le> (max_of_list ys)"
by (induct xs, auto dest: max_of_list_elem simp: max_of_list_def)
lemma max_of_list_append [simp]:
"max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)"
apply (simp add: max_of_list_def)
apply (induct xs)
apply simp_all
done
lemma app_mono_mxs: "\ app i G mxs rT pc et s; mxs \ mxs' \
\<Longrightarrow> app i G mxs' rT pc et s"
apply (case_tac s)
apply (simp add: app_def)
apply (case_tac i, auto intro: less_trans)
done
lemma err_mono [simp]: "A \ B \ err A \ err B"
by (auto simp: err_def)
lemma opt_mono [simp]: "A \ B \ opt A \ opt B"
by (auto simp: opt_def)
lemma states_mono: "\ mxs \ mxs' \
\<Longrightarrow> states G mxs mxr \<subseteq> states G mxs' mxr"
apply (simp add: states_def JVMType.sl_def)
apply (simp add: Product.esl_def stk_esl_def reg_sl_def
upto_esl_def Listn.sl_def Err.sl_def JType.esl_def)
apply (simp add: Err.esl_def Err.le_def Listn.le_def)
apply (simp add: Product.le_def Product.sup_def Err.sup_def)
apply (simp add: Opt.esl_def Listn.sup_def)
apply (rule err_mono)
apply (rule opt_mono)
apply (rule Sigma_mono)
apply (rule Union_mono)
apply auto
done
lemma check_type_mono:
"\ check_type G mxs mxr s; mxs \ mxs' \ \ check_type G mxs' mxr s"
apply (simp add: check_type_def)
apply (frule_tac G=G and mxr=mxr in states_mono)
apply auto
done
(* wt is preserved when adding instructions/state-types at the end *)
lemma wt_instr_prefix: "
\<lbrakk> wt_instr_altern (bc ! pc) cG rT mt mxs mxr max_pc et pc;
bc' = bc @ bc_post; mt' = mt @ mt_post;
mxs \<le> mxs'; max_pc \<le> max_pc';
pc < length bc; pc < length mt;
max_pc = (length mt)\<rbrakk>
\<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' et pc"
apply (simp add: wt_instr_altern_def nth_append)
apply (auto intro: app_mono_mxs check_type_mono)
done
(************************************************************************)
lemma pc_succs_shift:
"pc'\set (succs i (pc'' + n)) \ ((pc' - n) \set (succs i pc''))"
apply (induct i, simp_all)
apply arith
done
lemma pc_succs_le:
"\ pc' \ set (succs i (pc'' + n));
\<forall>b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc'' + b)) \<rbrakk>
\<Longrightarrow> n \<le> pc'"
apply (induct i, simp_all)
apply arith
done
(**********************************************************************)
definition offset_xcentry :: "[nat, exception_entry] \ exception_entry" where
"offset_xcentry ==
\<lambda> n (start_pc, end_pc, handler_pc, catch_type).
(start_pc + n, end_pc + n, handler_pc + n, catch_type)"
definition offset_xctable :: "[nat, exception_table] \ exception_table" where
"offset_xctable n == (map (offset_xcentry n))"
lemma match_xcentry_offset [simp]: "
match_exception_entry G cn (pc + n) (offset_xcentry n ee) =
match_exception_entry G cn pc ee"
by (simp add: match_exception_entry_def offset_xcentry_def split_beta)
lemma match_xctable_offset: "
(match_exception_table G cn (pc + n) (offset_xctable n et)) =
(map_option (\<lambda> pc'. pc' + n) (match_exception_table G cn pc et))"
apply (induct et)
apply (simp add: offset_xctable_def)+
apply (case_tac "match_exception_entry G cn pc a")
apply (simp add: offset_xcentry_def split_beta)+
done
lemma match_offset [simp]: "
match G cn (pc + n) (offset_xctable n et) = match G cn pc et"
apply (induct et)
apply (simp add: offset_xctable_def)+
done
lemma match_any_offset [simp]: "
match_any G (pc + n) (offset_xctable n et) = match_any G pc et"
apply (induct et)
apply (simp add: offset_xctable_def offset_xcentry_def split_beta)+
done
lemma app_mono_pc: "\ app i G mxs rT pc et s; pc'= pc + n \
\<Longrightarrow> app i G mxs rT pc' (offset_xctable n et) s"
apply (case_tac s)
apply (simp add: app_def)
apply (case_tac i, auto)
done
(**********************************************************************)
(* Currently: empty exception_table *)
abbreviation (input)
empty_et :: exception_table
where "empty_et == []"
(* move into Effect.thy *)
lemma xcpt_names_Nil [simp]: "(xcpt_names (i, G, pc, [])) = []"
by (induct i, simp_all)
lemma xcpt_eff_Nil [simp]: "(xcpt_eff i G pc s []) = []"
by (simp add: xcpt_eff_def)
lemma app_jumps_lem: "\ app i cG mxs rT pc empty_et s; s=(Some st) \
\<Longrightarrow> \<forall> b. ((i = (Goto b) \<or> i=(Ifcmpeq b)) \<longrightarrow> 0 \<le> (int pc + b))"
by (induct i) auto
(* wt is preserved when adding instructions/state-types to the front *)
lemma wt_instr_offset: "
\<lbrakk> \<forall> pc'' < length mt.
wt_instr_altern ((bc@bc_post) ! pc'') cG rT (mt@mt_post) mxs mxr max_pc empty_et pc'';
bc' = bc_pre @ bc @ bc_post; mt' = mt_pre @ mt @ mt_post;
length bc_pre = length mt_pre; length bc = length mt;
length mt_pre \<le> pc; pc < length (mt_pre @ mt);
mxs \<le> mxs'; max_pc + length mt_pre \<le> max_pc' \<rbrakk>
\<Longrightarrow> wt_instr_altern (bc' ! pc) cG rT mt' mxs' mxr max_pc' empty_et pc"
apply (simp add: wt_instr_altern_def)
apply (subgoal_tac "\ pc''. pc = pc'' + length mt_pre", erule exE)
prefer 2
apply (rule_tac x="pc - length mt_pre" in exI, arith)
apply (drule_tac x=pc'' in spec)
apply (drule mp)
apply arith (* show pc'' < length mt *)
apply clarify
apply (rule conjI)
(* app *)
apply (simp add: nth_append)
apply (rule app_mono_mxs)
apply (frule app_mono_pc)
apply (rule HOL.refl)
apply (simp add: offset_xctable_def)
apply assumption+
(* check_type *)
apply (rule conjI)
apply (simp add: nth_append)
apply (rule check_type_mono)
apply assumption+
(* ..eff.. *)
apply (intro ballI)
apply (subgoal_tac "\ pc' s'. x = (pc', s')", (erule exE)+, simp)
apply (case_tac s')
(* s' = None *)
apply (simp add: eff_def nth_append norm_eff_def)
apply (frule_tac x="(pc', None)" and f=fst and b=pc' in rev_image_eqI)
apply (simp (no_asm_simp))
apply (simp add: image_comp Fun.comp_def)
apply (frule pc_succs_shift)
apply (drule bspec, assumption)
apply arith
(* s' = Some a *)
apply (drule_tac x="(pc' - length mt_pre, s')" in bspec)
(* show (pc' - length mt_pre, s') \<in> set (eff \<dots>) *)
apply (simp add: eff_def)
(* norm_eff *)
apply (clarsimp simp: nth_append pc_succs_shift)
(* show P x of bspec *)
apply simp
apply (subgoal_tac "length mt_pre \ pc'")
apply (simp add: nth_append)
apply arith
(* subgoals *)
apply (simp add: eff_def xcpt_eff_def)
apply (clarsimp)
apply (rule pc_succs_le, assumption+)
apply (subgoal_tac "\ st. mt ! pc'' = Some st", erule exE)
apply (rule_tac s="Some st" and st=st and cG=cG and mxs=mxs and rT=rT in app_jumps_lem)
apply (simp add: nth_append)+
(* subgoal \<exists> st. mt ! pc'' = Some st *)
apply (simp add: norm_eff_def map_option_case nth_append)
apply (case_tac "mt ! pc''")
apply simp+
done
(**********************************************************************)
definition start_sttp_resp_cons :: "[state_type \ method_type \ state_type] \ bool" where
"start_sttp_resp_cons f ==
(\<forall> sttp. let (mt', sttp') = (f sttp) in (\<exists>mt'_rest. mt' = Some sttp # mt'_rest))"
definition start_sttp_resp :: "[state_type \ method_type \ state_type] \ bool" where
"start_sttp_resp f == (f = comb_nil) \ (start_sttp_resp_cons f)"
lemma start_sttp_resp_comb_nil [simp]: "start_sttp_resp comb_nil"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_cons_comb_cons [simp]: "start_sttp_resp_cons f
\<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
apply (simp add: start_sttp_resp_cons_def comb_def split_beta)
apply (rule allI)
apply (drule_tac x=sttp in spec)
apply auto
done
lemma start_sttp_resp_cons_comb_cons_r: "\ start_sttp_resp f; start_sttp_resp_cons f'\
\<Longrightarrow> start_sttp_resp_cons (f \<box> f')"
by (auto simp: start_sttp_resp_def)
lemma start_sttp_resp_cons_comb [simp]: "start_sttp_resp_cons f
\<Longrightarrow> start_sttp_resp (f \<box> f')"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_comb: "\ start_sttp_resp f; start_sttp_resp f' \
\<Longrightarrow> start_sttp_resp (f \<box> f')"
by (auto simp: start_sttp_resp_def)
lemma start_sttp_resp_cons_nochangeST [simp]: "start_sttp_resp_cons nochangeST"
by (simp add: start_sttp_resp_cons_def nochangeST_def)
lemma start_sttp_resp_cons_pushST [simp]: "start_sttp_resp_cons (pushST Ts)"
by (simp add: start_sttp_resp_cons_def pushST_def split_beta)
lemma start_sttp_resp_cons_dupST [simp]: "start_sttp_resp_cons dupST"
by (simp add: start_sttp_resp_cons_def dupST_def split_beta)
lemma start_sttp_resp_cons_dup_x1ST [simp]: "start_sttp_resp_cons dup_x1ST"
by (simp add: start_sttp_resp_cons_def dup_x1ST_def split_beta)
lemma start_sttp_resp_cons_popST [simp]: "start_sttp_resp_cons (popST n)"
by (simp add: start_sttp_resp_cons_def popST_def split_beta)
lemma start_sttp_resp_cons_replST [simp]: "start_sttp_resp_cons (replST n tp)"
by (simp add: start_sttp_resp_cons_def replST_def split_beta)
lemma start_sttp_resp_cons_storeST [simp]: "start_sttp_resp_cons (storeST i tp)"
by (simp add: start_sttp_resp_cons_def storeST_def split_beta)
lemma start_sttp_resp_cons_compTpExpr [simp]: "start_sttp_resp_cons (compTpExpr jmb G ex)"
apply (induct ex)
apply simp+
apply (simp add: start_sttp_resp_cons_def comb_def pushST_def split_beta) (* LAcc *)
apply simp+
done
lemma start_sttp_resp_cons_compTpInit [simp]: "start_sttp_resp_cons (compTpInit jmb lv)"
by (simp add: compTpInit_def split_beta)
lemma start_sttp_resp_nochangeST [simp]: "start_sttp_resp nochangeST"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_pushST [simp]: "start_sttp_resp (pushST Ts)"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_dupST [simp]: "start_sttp_resp dupST"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_dup_x1ST [simp]: "start_sttp_resp dup_x1ST"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_popST [simp]: "start_sttp_resp (popST n)"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_replST [simp]: "start_sttp_resp (replST n tp)"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_storeST [simp]: "start_sttp_resp (storeST i tp)"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_compTpExpr [simp]: "start_sttp_resp (compTpExpr jmb G ex)"
by (simp add: start_sttp_resp_def)
lemma start_sttp_resp_compTpExprs [simp]: "start_sttp_resp (compTpExprs jmb G exs)"
by (induct exs, (simp add: start_sttp_resp_comb)+)
lemma start_sttp_resp_compTpStmt [simp]: "start_sttp_resp (compTpStmt jmb G s)"
by (induct s, (simp add: start_sttp_resp_comb)+)
lemma start_sttp_resp_compTpInitLvars [simp]: "start_sttp_resp (compTpInitLvars jmb lvars)"
by (induct lvars, simp+)
(* ********************************************************************** *)
subsection "length of compExpr/ compTpExprs"
(* ********************************************************************** *)
lemma length_comb [simp]: "length (mt_of ((f1 \ f2) sttp)) =
length (mt_of (f1 sttp)) + length (mt_of (f2 (sttp_of (f1 sttp))))"
by (simp add: comb_def split_beta)
lemma length_comb_nil [simp]: "length (mt_of (comb_nil sttp)) = 0"
by (simp add: comb_nil_def)
lemma length_nochangeST [simp]: "length (mt_of (nochangeST sttp)) = 1"
by (simp add: nochangeST_def)
lemma length_pushST [simp]: "length (mt_of (pushST Ts sttp)) = 1"
by (simp add: pushST_def split_beta)
lemma length_dupST [simp]: "length (mt_of (dupST sttp)) = 1"
by (simp add: dupST_def split_beta)
lemma length_dup_x1ST [simp]: "length (mt_of (dup_x1ST sttp)) = 1"
by (simp add: dup_x1ST_def split_beta)
lemma length_popST [simp]: "length (mt_of (popST n sttp)) = 1"
by (simp add: popST_def split_beta)
lemma length_replST [simp]: "length (mt_of (replST n tp sttp)) = 1"
by (simp add: replST_def split_beta)
lemma length_storeST [simp]: "length (mt_of (storeST i tp sttp)) = 1"
by (simp add: storeST_def split_beta)
lemma length_compTpExpr_Exprs [rule_format]: "
(\<forall>sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
\<and> (\<forall>sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
apply (rule compat_expr_expr_list.induct)
apply (simp_all)[3]
apply (rename_tac binop a b, case_tac binop)
apply (auto simp add: pushST_def split_beta)
done
lemma length_compTpExpr: "length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)"
by (rule length_compTpExpr_Exprs [THEN conjunct1 [THEN spec]])
lemma length_compTpExprs: "length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)"
by (rule length_compTpExpr_Exprs [THEN conjunct2 [THEN spec]])
lemma length_compTpStmt [rule_format]: "
(\<forall> sttp. (length (mt_of (compTpStmt jmb G s sttp)) = length (compStmt jmb s)))"
by (rule stmt.induct) (auto simp: length_compTpExpr)
lemma length_compTpInit: "length (mt_of (compTpInit jmb lv sttp)) = length (compInit jmb lv)"
by (simp add: compTpInit_def compInit_def split_beta)
lemma length_compTpInitLvars [rule_format]:
"\ sttp. length (mt_of (compTpInitLvars jmb lvars sttp)) = length (compInitLvars jmb lvars)"
by (induct lvars, (simp add: compInitLvars_def length_compTpInit split_beta)+)
(* ********************************************************************** *)
subsection "Correspondence bytecode - method types"
(* ********************************************************************** *)
abbreviation (input)
ST_of :: "state_type \ opstack_type"
where "ST_of == fst"
abbreviation (input)
LT_of :: "state_type \ locvars_type"
where "LT_of == snd"
lemma states_lower:
"\ OK (Some (ST, LT)) \ states cG mxs mxr; length ST \ mxs\
\<Longrightarrow> OK (Some (ST, LT)) \<in> states cG (length ST) mxr"
apply (simp add: states_def JVMType.sl_def)
apply (simp add: Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
JType.esl_def)
apply (simp add: Err.esl_def Err.le_def Listn.le_def)
apply (simp add: Product.le_def Product.sup_def Err.sup_def)
apply (simp add: Opt.esl_def Listn.sup_def)
apply clarify
apply auto
done
lemma check_type_lower:
"\ check_type cG mxs mxr (OK (Some (ST, LT))); length ST \ mxs\
\<Longrightarrow>check_type cG (length ST) mxr (OK (Some (ST, LT)))"
by (simp add: check_type_def states_lower)
(* ******************************************************************* *)
definition bc_mt_corresp :: "
[bytecode, state_type \<Rightarrow> method_type \<times> state_type, state_type, jvm_prog, ty, nat, p_count]
\<Rightarrow> bool" where
"bc_mt_corresp bc f sttp0 cG rT mxr idx ==
let (mt, sttp) = f sttp0 in
(length bc = length mt \<and>
((check_type cG (length (ST_of sttp0)) mxr (OK (Some sttp0))) \<longrightarrow>
(\<forall> mxs.
mxs = max_ssize (mt@[Some sttp]) \<longrightarrow>
(\<forall> pc. pc < idx \<longrightarrow>
wt_instr_altern (bc ! pc) cG rT (mt@[Some sttp]) mxs mxr (length mt + 1) empty_et pc)
\<and>
check_type cG mxs mxr (OK ((mt@[Some sttp]) ! idx)))))"
lemma bc_mt_corresp_comb: "
\<lbrakk> bc' = (bc1@bc2); l' = (length bc');
bc_mt_corresp bc1 f1 sttp0 cG rT mxr (length bc1);
bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
start_sttp_resp f2\<rbrakk>
\<Longrightarrow> bc_mt_corresp bc' (f1 \<box> f2) sttp0 cG rT mxr l'"
apply (subgoal_tac "\mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
apply (subgoal_tac "\mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
(* unfold start_sttp_resp and make case distinction *)
apply (simp only: start_sttp_resp_def)
apply (erule disjE)
(* case f2 = comb_nil *)
apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
apply (erule conjE)+
apply (intro strip)
apply simp
(* case start_sttp_resp_cons f2 *)
apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def del: all_simps)
apply (intro strip)
apply (erule conjE)+
apply (drule mp, assumption)
apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
apply (erule conjE)+
apply (drule mp, assumption)
apply (erule conjE)+
apply (rule conjI)
(* show wt_instr \<dots> *)
apply (drule_tac x=sttp1 in spec, simp)
apply (erule exE)
apply (intro strip)
apply (case_tac "pc < length mt1")
(* case pc < length mt1 *)
apply (drule spec, drule mp, simp)
apply simp
apply (rule_tac mt="mt1 @ [Some sttp1]" in wt_instr_prefix)
apply assumption+ apply (rule HOL.refl)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: max_ssize_def)
apply (simp add: max_of_list_def ac_simps)
apply arith
apply (simp (no_asm_simp))+
(* case pc \<ge> length mt1 *)
apply (rule_tac bc=bc2 and mt=mt2 and bc_post="[]" and mt_post="[Some sttp2]"
and mxr=mxr
in wt_instr_offset)
apply simp
apply (simp (no_asm_simp))+
apply simp
apply (simp add: max_ssize_def) apply (simp (no_asm_simp))
(* show check_type \<dots> *)
apply (subgoal_tac "((mt2 @ [Some sttp2]) ! length bc2) = Some sttp2")
apply (simp only:)
apply (rule check_type_mono) apply assumption
apply (simp (no_asm_simp) add: max_ssize_def ac_simps)
apply (simp add: nth_append)
apply (erule conjE)+
apply (case_tac sttp1)
apply (simp add: check_type_def)
apply (rule states_lower, assumption)
apply (simp (no_asm_simp) add: max_ssize_def)
apply (simp (no_asm_simp) add: max_of_list_def ssize_sto_def)
apply (simp (no_asm_simp))+
done
lemma bc_mt_corresp_zero [simp]:
"\ length (mt_of (f sttp)) = length bc; start_sttp_resp f\
\<Longrightarrow> bc_mt_corresp bc f sttp cG rT mxr 0"
apply (simp add: bc_mt_corresp_def start_sttp_resp_def split_beta)
apply (erule disjE)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
apply (intro strip)
apply (simp add: start_sttp_resp_cons_def split_beta)
apply (drule_tac x=sttp in spec, erule exE)
apply simp
apply (rule check_type_mono, assumption)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def split: prod.split)
done
(* ********************************************************************** *)
definition mt_sttp_flatten :: "method_type \ state_type \ method_type" where
"mt_sttp_flatten mt_sttp == (mt_of mt_sttp) @ [Some (sttp_of mt_sttp)]"
lemma mt_sttp_flatten_length [simp]: "n = (length (mt_of (f sttp)))
\<Longrightarrow> (mt_sttp_flatten (f sttp)) ! n = Some (sttp_of (f sttp))"
by (simp add: mt_sttp_flatten_def)
lemma mt_sttp_flatten_comb: "(mt_sttp_flatten ((f1 \ f2) sttp)) =
(mt_of (f1 sttp)) @ (mt_sttp_flatten (f2 (sttp_of (f1 sttp))))"
by (simp add: mt_sttp_flatten_def comb_def split_beta)
lemma mt_sttp_flatten_comb_length [simp]: "\ n1 = length (mt_of (f1 sttp)); n1 \ n \
\<Longrightarrow> (mt_sttp_flatten ((f1 \<box> f2) sttp) ! n) = (mt_sttp_flatten (f2 (sttp_of (f1 sttp))) ! (n - n1))"
by (simp add: mt_sttp_flatten_comb nth_append)
lemma mt_sttp_flatten_comb_zero [simp]:
"start_sttp_resp f \ (mt_sttp_flatten (f sttp)) ! 0 = Some sttp"
apply (simp only: start_sttp_resp_def)
apply (erule disjE)
apply (simp add: comb_nil_def mt_sttp_flatten_def)
apply (simp add: start_sttp_resp_cons_def mt_sttp_flatten_def split_beta)
apply (drule_tac x=sttp in spec)
apply (erule exE)
apply simp
done
(* move into prelude -- compare with nat_int_length *)
lemma int_outside_right: "0 \ (m::int) \ m + (int n) = int ((nat m) + n)"
by simp
lemma int_outside_left: "0 \ (m::int) \ (int n) + m = int (n + (nat m))"
by simp
(* ********************************************************************** *)
(* bc_mt_corresp for individual instructions *)
(* ---------------------------------------------------------------------- *)
lemma less_Suc [simp] : "n \ k \ (k < Suc n) = (k = n)"
by arith
lemmas check_type_simps = check_type_def states_def JVMType.sl_def
Product.esl_def stk_esl_def reg_sl_def upto_esl_def Listn.sl_def Err.sl_def
JType.esl_def Err.esl_def Err.le_def Listn.le_def Product.le_def Product.sup_def Err.sup_def
Opt.esl_def Listn.sup_def
lemma check_type_push:
"\ is_class cG cname; check_type cG (length ST) mxr (OK (Some (ST, LT))) \
\<Longrightarrow> check_type cG (Suc (length ST)) mxr (OK (Some (Class cname # ST, LT)))"
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
done
lemma bc_mt_corresp_New: "\is_class cG cname \
\<Longrightarrow> bc_mt_corresp [New cname] (pushST [Class cname]) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_push)
done
lemma bc_mt_corresp_Pop: "
bc_mt_corresp [Pop] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def ssize_sto_def max_of_list_def)
apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp
done
lemma bc_mt_corresp_Checkcast: "\ is_class cG cname; sttp = (ST, LT);
(\<exists>rT STo. ST = RefT rT # STo) \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Checkcast cname] (replST (Suc 0) (Class cname)) sttp cG rT mxr (Suc 0)"
apply (erule exE)+
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length STo)" in exI)
apply simp
done
lemma bc_mt_corresp_LitPush: "\ typeof (\v. None) val = Some T \
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T]) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def
max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp
apply (drule sym)
apply (case_tac val)
apply simp+
done
lemma bc_mt_corresp_LitPush_CT:
"\ typeof (\v. None) val = Some T \ cG \ T \ T'; is_type cG T' \
\<Longrightarrow> bc_mt_corresp [LitPush val] (pushST [T']) sttp cG rT mxr (Suc 0)"
apply (subgoal_tac "\ST LT. sttp= (ST, LT)", (erule exE)+)
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def max_ssize_def
max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_simps)
apply (simp add: sup_state_Cons)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp
apply simp
done
declare not_Err_eq [iff del]
lemma bc_mt_corresp_Load: "\ i < length LT; LT ! i \ Err; mxr = length LT \
\<Longrightarrow> bc_mt_corresp [Load i]
(\<lambda>(ST, LT). pushST [ok_val (LT ! i)] (ST, LT)) (ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def pushST_def wt_instr_altern_def max_ssize_def max_of_list_def
ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply (simp (no_asm_simp))
apply (simp only: err_def)
apply (frule listE_nth_in)
apply assumption
apply (subgoal_tac "LT ! i \ {x. \y\types cG. x = OK y}")
apply (drule CollectD)
apply (erule bexE)
apply (simp (no_asm_simp))
apply blast
apply blast
done
lemma bc_mt_corresp_Store_init:
"i < length LT \ bc_mt_corresp [Store i] (storeST i T) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def storeST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def)
apply (simp add: ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule conjI)
apply (rule_tac x="(length ST)" in exI)
apply simp+
done
lemma bc_mt_corresp_Store:
"\ i < length LT; cG \ LT[i := OK T] <=l LT \
\<Longrightarrow> bc_mt_corresp [Store i] (popST (Suc 0)) (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: sup_state_conv)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="(length ST)" in exI)
apply simp
done
lemma bc_mt_corresp_Dup: "
bc_mt_corresp [Dup] dupST (T # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dupST_def wt_instr_altern_def
max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (Suc (length ST))" in exI)
apply simp
done
lemma bc_mt_corresp_Dup_x1: "
bc_mt_corresp [Dup_x1] dup_x1ST (T1 # T2 # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def dup_x1ST_def wt_instr_altern_def
max_ssize_def max_of_list_def ssize_sto_def eff_def norm_eff_def max.absorb2)
apply (intro strip)
apply (rule conjI)
apply (rule check_type_mono, assumption, simp)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI)
apply simp+
done
lemma bc_mt_corresp_IAdd: "
bc_mt_corresp [IAdd] (replST 2 (PrimT Integer))
(PrimT Integer # PrimT Integer # ST, LT) cG rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp
done
lemma bc_mt_corresp_Getfield: "\ wf_prog wf_mb G;
field (G, C) vname = Some (cname, T); is_class G C \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Getfield vname cname]
(replST (Suc 0) (snd (the (field (G, cname) vname))))
(Class C # ST, LT) (comp G) rT mxr (Suc 0)"
apply (frule wf_prog_ws_prog [THEN wf_subcls1])
apply (frule field_in_fd, assumption+)
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def replST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
apply (simp only: comp_is_type)
apply (rule_tac C=cname in fields_is_type)
apply (simp add: TypeRel.field_def)
apply (drule JBasis.table_of_remap_SomeD)+
apply assumption+
apply (erule wf_prog_ws_prog)
apply assumption
done
lemma bc_mt_corresp_Putfield: "\ wf_prog wf_mb G;
field (G, C) vname = Some (cname, Ta); G \<turnstile> T \<preceq> Ta; is_class G C \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Putfield vname cname] (popST 2) (T # Class C # T # ST, LT)
(comp G) rT mxr (Suc 0)"
apply (frule wf_prog_ws_prog [THEN wf_subcls1])
apply (frule field_in_fd, assumption+)
apply (frule widen_field, assumption+)
apply (simp add: bc_mt_corresp_def popST_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: comp_field comp_subcls1 comp_widen comp_is_class)
apply (simp add: max_ssize_def max_of_list_def ssize_sto_def)
apply (intro strip)
apply (simp add: check_type_simps max.absorb1)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
done
lemma Call_app:
"\ wf_prog wf_mb G; is_class G cname;
STs = rev pTsa @ Class cname # ST;
max_spec G cname (mname, pTsa) = {((md, T), pTs')} \
\<Longrightarrow> app (Invoke cname mname pTs') (comp G) (length (T # ST)) rT 0 empty_et (Some (STs, LTs))"
apply (subgoal_tac "(\mD' rT' comp_b.
method (comp G, cname) (mname, pTs') = Some (mD', rT', comp_b))")
apply (simp add: comp_is_class)
apply (rule_tac x=pTsa in exI)
apply (rule_tac x="Class cname" in exI)
apply (simp add: max_spec_preserves_length comp_is_class)
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (simp add: split_paired_all comp_widen list_all2_iff)
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (rule exI)+
apply (simp add: wf_prog_ws_prog [THEN comp_method])
done
lemma bc_mt_corresp_Invoke:
"\ wf_prog wf_mb G;
max_spec G cname (mname, pTsa) = {((md, T), fpTs)};
is_class G cname \<rbrakk>
\<Longrightarrow> bc_mt_corresp [Invoke cname mname fpTs] (replST (Suc (length pTsa)) T)
(rev pTsa @ Class cname # ST, LT) (comp G) rT mxr (Suc 0)"
apply (simp add: bc_mt_corresp_def wt_instr_altern_def eff_def norm_eff_def)
apply (simp add: replST_def del: appInvoke)
apply (intro strip)
apply (rule conjI)
\<comment> \<open>app\<close>
apply (rule Call_app [THEN app_mono_mxs])
apply assumption+
apply (rule HOL.refl)
apply assumption
apply (simp add: max_ssize_def max_of_list_elem ssize_sto_def)
\<comment> \<open>\<open><=s\<close>\<close>
apply (frule max_spec2mheads, (erule exE)+, (erule conjE)+)
apply (simp add: wf_prog_ws_prog [THEN comp_method])
apply (simp add: max_spec_preserves_length [symmetric])
\<comment> \<open>\<open>check_type\<close>\<close>
apply (simp add: max_ssize_def ssize_sto_def)
apply (simp add: max_of_list_def)
apply (subgoal_tac "(max (length pTsa + length ST) (length ST)) = (length pTsa + length ST)")
apply simp
apply (simp add: check_type_simps)
apply clarify
apply (rule_tac x="Suc (length ST)" in exI)
apply simp+
apply (simp only: comp_is_type)
apply (frule method_wf_mdecl) apply assumption apply assumption
apply (simp add: wf_mdecl_def wf_mhead_def)
apply (simp)
done
lemma wt_instr_Ifcmpeq: "\Suc pc < max_pc;
0 \<le> (int pc + i); nat (int pc + i) < max_pc;
(mt_sttp_flatten f ! pc = Some (ts#ts'#ST,LT)) \
((\<exists>p. ts = PrimT p \<and> ts' = PrimT p) \<or> (\<exists>r r'. ts = RefT r \<and> ts' = RefT r'));
mt_sttp_flatten f ! Suc pc = Some (ST,LT);
mt_sttp_flatten f ! nat (int pc + i) = Some (ST,LT);
check_type (TranslComp.comp G) mxs mxr (OK (Some (ts # ts' # ST, LT))) \
\<Longrightarrow> wt_instr_altern (Ifcmpeq i) (comp G) rT (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
by (simp add: wt_instr_altern_def eff_def norm_eff_def)
lemma wt_instr_Goto: "\ 0 \ (int pc + i); nat (int pc + i) < max_pc;
mt_sttp_flatten f ! nat (int pc + i) = (mt_sttp_flatten f ! pc);
check_type (TranslComp.comp G) mxs mxr (OK (mt_sttp_flatten f ! pc)) \<rbrakk>
\<Longrightarrow> wt_instr_altern (Goto i) (comp G) rT (mt_sttp_flatten f) mxs mxr max_pc empty_et pc"
apply (case_tac "(mt_sttp_flatten f ! pc)")
apply (simp add: wt_instr_altern_def eff_def norm_eff_def app_def xcpt_app_def)+
done
(* ********************************************************************** *)
lemma bc_mt_corresp_comb_inside: "
\<lbrakk>
bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
bc' = (bc1@bc2@bc3); f'= (f1 \<box> f2 \<box> f3);
l1 = (length bc1); l12 = (length (bc1@bc2));
bc_mt_corresp bc2 f2 (sttp_of (f1 sttp0)) cG rT mxr (length bc2);
length bc1 = length (mt_of (f1 sttp0));
start_sttp_resp f2; start_sttp_resp f3\<rbrakk>
\<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr l12"
apply (subgoal_tac "\ mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
apply (subgoal_tac "\ mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
apply (subgoal_tac "\ mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
(* unfold start_sttp_resp and make case distinction *)
apply (simp only: start_sttp_resp_def)
apply (erule_tac Q="start_sttp_resp_cons f2" in disjE)
(* case f2 = comb_nil *)
apply (simp add: bc_mt_corresp_def comb_nil_def start_sttp_resp_cons_def)
(* case start_sttp_resp_cons f2 *)
apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def)
apply (drule_tac x=sttp1 in spec, simp, erule exE)
apply (intro strip, (erule conjE)+)
(* get rid of all check_type info *)
apply (subgoal_tac "check_type cG (length (fst sttp1)) mxr (OK (Some sttp1))")
apply (subgoal_tac "check_type cG (max_ssize (mt2 @ [Some sttp2])) mxr (OK (Some sttp2))")
apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
(OK ((mt2 @ mt3 @ [Some sttp3]) ! length mt2))")
apply simp
apply (intro strip, (erule conjE)+)
apply (case_tac "pc < length mt1")
(* case pc < length mt1 *)
apply (drule spec, drule mp, assumption)
apply assumption
(* case pc \<ge> length mt1 *)
(* case distinction on start_sttp_resp f3 *)
apply (erule_tac P="f3 = comb_nil" in disjE)
(* case f3 = comb_nil *)
apply (subgoal_tac "mt3 = [] \ sttp2 = sttp3") apply (erule conjE)+
apply (subgoal_tac "bc3=[]")
apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]"
and mxs="(max_ssize (mt2 @ [(Some sttp2)]))"
and max_pc="(Suc (length mt2))"
in wt_instr_offset)
apply simp
apply (rule HOL.refl)+
apply (simp (no_asm_simp))+
apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
apply (rule max_of_list_sublist)
apply (simp (no_asm_simp) only: set_append list.set list.map) apply blast
apply (simp (no_asm_simp))
apply simp (* subgoal bc3 = [] *)
apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
(* case start_sttp_resp_cons f3 *)
apply (subgoal_tac "\mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
apply (rule_tac bc_pre=bc1 and bc=bc2 and bc_post=bc3
and mt_pre=mt1 and mt=mt2 and mt_post="mt3@ [Some sttp3]"
and mxs="(max_ssize (mt2 @ [Some sttp2]))"
and max_pc="(Suc (length mt2))"
in wt_instr_offset)
apply (intro strip)
apply (rule_tac bc=bc2 and mt="(mt2 @ [Some sttp2])"
and mxs="(max_ssize (mt2 @ [Some sttp2]))"
and max_pc="(Suc (length mt2))"
in wt_instr_prefix)
(* preconditions of wt_instr_prefix *)
apply simp
apply (rule HOL.refl)
apply (simp (no_asm_simp))+
apply simp+
(* (some) preconditions of wt_instr_offset *)
apply (simp (no_asm_simp) add: max_ssize_def del: max_of_list_append)
apply (rule max_of_list_sublist)
apply (simp (no_asm_simp) only: set_append list.set list.map)
apply blast
apply (simp (no_asm_simp))
apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
(* subgoals check_type*)
(* \<dots> ! length mt2 *)
apply simp
apply (erule_tac P="f3 = comb_nil" in disjE)
(* -- case f3 = comb_nil *)
apply (subgoal_tac "mt3 = [] \ sttp2 = sttp3") apply (erule conjE)+
apply simp
apply (rule check_type_mono, assumption)
apply (simp only: max_ssize_def)
apply (rule max_of_list_sublist)
apply (simp (no_asm_simp))
apply blast
apply simp (* subgoal bc3 = [] *)
apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
(* -- case start_sttp_resp_cons f3 *)
apply (subgoal_tac "\mt3_rest. (mt3 = Some sttp2 # mt3_rest)", erule exE)
apply (simp (no_asm_simp) add: nth_append)
apply (erule conjE)+
apply (rule check_type_mono, assumption)
apply (simp only: max_ssize_def)
apply (rule max_of_list_sublist)
apply (simp (no_asm_simp))
apply blast
apply (drule_tac x=sttp2 in spec, simp) (* subgoal \<exists>mt3_rest. \<dots> *)
(* subgoal check_type \<dots> Some sttp2 *)
apply (simp add: nth_append)
(* subgoal check_type \<dots> Some sttp1 *)
apply (simp add: nth_append)
apply (erule conjE)+
apply (case_tac "sttp1", simp)
apply (rule check_type_lower, assumption)
apply (simp (no_asm_simp) add: max_ssize_def ssize_sto_def)
apply (simp (no_asm_simp) add: max_of_list_def)
(* subgoals \<exists> ... *)
apply (rule surj_pair)+
done
(* ******************** *)
definition contracting :: "(state_type \ method_type \ state_type) \ bool" where
"contracting f == (\ ST LT.
let (ST', LT') = sttp_of (f (ST, LT))
in (length ST' \ length ST \ set ST' \ set ST \
length LT' = length LT \ set LT' \ set LT))"
(* ### possibly move into HOL *)
lemma set_drop_Suc [rule_format]: "\xs. set (drop (Suc n) xs) \ set (drop n xs)"
apply (induct n)
apply simp
apply (intro strip)
apply (rule list.induct)
apply simp
apply simp
apply blast
apply (intro strip)
apply (rule_tac P="\ xs. set (drop (Suc (Suc n)) xs) \ set (drop (Suc n) xs)" in list.induct)
apply simp+
done
lemma set_drop_le [rule_format,simp]: "\n xs. n \ m \ set (drop m xs) \ set (drop n xs)"
apply (induct m)
apply simp
apply (intro strip)
apply (subgoal_tac "n \ m \ n = Suc m")
apply (erule disjE)
apply (frule_tac x=n in spec, drule_tac x=xs in spec, drule mp, assumption)
apply (rule set_drop_Suc [THEN subset_trans], assumption)
apply auto
done
declare set_drop_subset [simp]
lemma contracting_popST [simp]: "contracting (popST n)"
by (simp add: contracting_def popST_def)
lemma contracting_nochangeST [simp]: "contracting nochangeST"
by (simp add: contracting_def nochangeST_def)
lemma check_type_contracting: "\ check_type cG mxs mxr (OK (Some sttp)); contracting f\
\<Longrightarrow> check_type cG mxs mxr (OK (Some (sttp_of (f sttp))))"
apply (subgoal_tac "\ ST LT. sttp = (ST, LT)", (erule exE)+)
apply (simp add: check_type_simps contracting_def)
apply clarify
apply (drule_tac x=ST in spec, drule_tac x=LT in spec)
apply (case_tac "(sttp_of (f (ST, LT)))")
apply simp
apply (erule conjE)+
apply (drule listE_set)+
apply (rule conjI)
apply (rule_tac x="length a" in exI)
apply simp
apply (rule listI)
apply simp
apply blast
apply (rule listI)
apply simp
apply blast
apply auto
done
(* ******************** *)
lemma bc_mt_corresp_comb_wt_instr: "
\<lbrakk> bc_mt_corresp bc' f' sttp0 cG rT mxr l1;
bc' = (bc1@[inst]@bc3); f'= (f1 \<box> f2 \<box> f3);
l1 = (length bc1);
length bc1 = length (mt_of (f1 sttp0));
length (mt_of (f2 (sttp_of (f1 sttp0)))) = 1;
start_sttp_resp_cons f1; start_sttp_resp_cons f2; start_sttp_resp f3;
check_type cG (max_ssize (mt_sttp_flatten (f' sttp0))) mxr
(OK ((mt_sttp_flatten (f' sttp0)) ! (length bc1)))
\<longrightarrow>
wt_instr_altern inst cG rT
(mt_sttp_flatten (f' sttp0))
(max_ssize (mt_sttp_flatten (f' sttp0)))
mxr
(Suc (length bc'))
empty_et
(length bc1);
contracting f2
\<rbrakk>
\<Longrightarrow> bc_mt_corresp bc' f' sttp0 cG rT mxr (length (bc1@[inst]))"
apply (subgoal_tac "\ mt1 sttp1. (f1 sttp0) = (mt1, sttp1)", (erule exE)+)
apply (subgoal_tac "\ mt2 sttp2. (f2 sttp1) = (mt2, sttp2)", (erule exE)+)
apply (subgoal_tac "\ mt3 sttp3. (f3 sttp2) = (mt3, sttp3)", (erule exE)+)
apply (simp add: bc_mt_corresp_def comb_def start_sttp_resp_cons_def
mt_sttp_flatten_def)
apply (intro strip, (erule conjE)+)
apply (drule mp, assumption)+
apply (erule conjE)+
apply (drule mp, assumption)
apply (rule conjI)
(* wt_instr \<dots> *)
apply (intro strip)
apply (case_tac "pc < length mt1")
(* case pc < length mt1 *)
apply (drule spec, drule mp, assumption)
apply assumption
(* case pc \<ge> length mt1 *)
apply (subgoal_tac "pc = length mt1") prefer 2 apply arith
apply (simp only:)
apply (simp add: nth_append mt_sttp_flatten_def)
(* check_type \<dots> *)
apply (simp add: start_sttp_resp_def)
apply (drule_tac x="sttp0" in spec, simp, erule exE)
apply (drule_tac x="sttp1" in spec, simp, erule exE)
apply (subgoal_tac "check_type cG (max_ssize (mt1 @ mt2 @ mt3 @ [Some sttp3])) mxr
(OK (Some (sttp_of (f2 sttp1))))")
apply (simp only:)
apply (erule disjE)
(* case f3 = comb_nil *)
apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! Suc (length mt1)) = (Some (snd (f2 sttp1)))")
apply (subgoal_tac "mt3 = [] \ sttp2 = sttp3")
apply (erule conjE)+
apply (simp add: nth_append)
apply (simp add: comb_nil_def) (* subgoal mt3 = [] \<and> sttp2 = sttp3 *)
apply (simp add: nth_append comb_nil_def) (* subgoal \<dots> ! Suc (length mt1) *)
(* case start_sttp_resp_cons f3 *)
apply (simp add: start_sttp_resp_cons_def)
apply (drule_tac x="sttp2" in spec, simp, erule exE)
apply (simp add: nth_append)
(* subgoal check_type *)
apply (rule check_type_contracting)
apply (subgoal_tac "((mt1 @ mt2 @ mt3 @ [Some sttp3]) ! length mt1) = (Some sttp1)")
apply (simp add: nth_append)
apply (simp add: nth_append)
apply assumption
(* subgoals *)
apply (rule surj_pair)+
done
lemma compTpExpr_LT_ST_rewr [simp]:
"\ wf_java_prog G; wf_java_mdecl G C ((mn, pTs), rT, (pns, lvars, blk, res));
local_env G C (mn, pTs) pns lvars \<turnstile> ex :: T;
is_inited_LT C pTs lvars LT\<rbrakk>
\<Longrightarrow> sttp_of (compTpExpr (pns, lvars, blk, res) G ex (ST, LT)) = (T # ST, LT)"
by (rule compTpExpr_LT_ST) auto
lemma wt_method_compTpExpr_Exprs_corresp: "
\<lbrakk> jmb = (pns,lvars,blk,res);
wf_prog wf_java_mdecl G;
wf_java_mdecl G C ((mn, pTs), rT, jmb);
E = (local_env G C (mn, pTs) pns lvars)\<rbrakk>
\<Longrightarrow>
(\<forall> ST LT T bc' f'.
E \<turnstile> ex :: T \<longrightarrow>
(is_inited_LT C pTs lvars LT) \<longrightarrow>
bc' = (compExpr jmb ex) \
f' = (compTpExpr jmb G ex)
\<longrightarrow> bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) (length bc'))
\<and>
(\<forall> ST LT Ts.
E \<turnstile> exs [::] Ts \<longrightarrow>
(is_inited_LT C pTs lvars LT)
\<longrightarrow> bc_mt_corresp (compExprs jmb exs) (compTpExprs jmb G exs) (ST, LT) (comp G) rT (length LT) (length (compExprs jmb exs)))"
apply (rule compat_expr_expr_list.induct)
(* expresssions *)
(* NewC *)
apply (intro allI impI)
apply (simp only:)
apply (drule NewC_invers)
apply (simp (no_asm_use))
apply (rule bc_mt_corresp_New)
apply (simp add: comp_is_class)
(* Cast *)
apply (intro allI impI)
apply (simp only:)
apply (drule Cast_invers)
apply clarify
apply (simp (no_asm_use))
apply (rule bc_mt_corresp_comb)
apply (rule HOL.refl, simp (no_asm_simp), blast)
apply (simp (no_asm_simp), rule bc_mt_corresp_Checkcast)
apply (simp add: comp_is_class)
apply (simp only: compTpExpr_LT_ST)
apply (drule cast_RefT)
apply blast
apply (simp add: start_sttp_resp_def)
(* Lit *)
apply (intro allI impI)
apply (simp only:)
apply (drule Lit_invers)
apply simp
apply (rule bc_mt_corresp_LitPush)
apply assumption
(* BinOp *)
apply (intro allI impI)
apply (simp (no_asm_simp) only:)
apply (drule BinOp_invers, erule exE, (erule conjE)+)
apply (rename_tac binop expr1 expr2 ST LT T bc' f' Ta, case_tac binop)
apply (simp (no_asm_simp))
(* case Eq *)
apply (subgoal_tac "bc_mt_corresp bc' f' (ST, LT) (comp G) rT (length LT) 0")
prefer 2
apply (rule bc_mt_corresp_zero)
apply (simp add: length_compTpExpr)
apply (simp (no_asm_simp))
apply (drule_tac ?bc1.0="[]" and ?bc2.0 = "compExpr jmb expr1"
and ?f1.0=comb_nil and ?f2.0 = "compTpExpr jmb G expr1"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply blast
apply (simp (no_asm_simp) add: length_compTpExpr)+
apply (drule_tac ?bc2.0 = "compExpr jmb expr2" and ?f2.0 = "compTpExpr jmb G expr2"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply (simp only: compTpExpr_LT_ST)
apply (simp (no_asm_simp) add: length_compTpExpr)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2"
and inst = "Ifcmpeq 3" and ?bc3.0 = "[LitPush (Bool False),Goto 2, LitPush (Bool True)]"
and ?f1.0="compTpExpr jmb G expr1 \ compTpExpr jmb G expr2"
and ?f2.0="popST 2" and ?f3.0="pushST [PrimT Boolean] \ popST 1 \ pushST [PrimT Boolean]"
in bc_mt_corresp_comb_wt_instr)
apply (simp (no_asm_simp) add: length_compTpExpr)+
(* wt_instr *)
apply (intro strip)
apply (simp (no_asm_simp) add: wt_instr_altern_def length_compTpExpr eff_def)
apply (simp (no_asm_simp) add: norm_eff_def)
apply (simp (no_asm_simp) only: int_outside_left nat_int)
apply (simp (no_asm_simp) add: length_compTpExpr)
apply (simp only: compTpExpr_LT_ST)+
apply (simp add: eff_def norm_eff_def popST_def pushST_def mt_sttp_flatten_def)
apply (case_tac Ta)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp))
apply (rule contracting_popST) (* contracting (popST 2) *)
apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3]"
and ?bc2.0 = "[LitPush (Bool False)]"
and ?bc3.0 = "[Goto 2, LitPush (Bool True)]"
and ?f1.0 = "compTpExpr jmb G expr1 \ compTpExpr jmb G expr2 \ popST 2"
and ?f2.0 = "pushST [PrimT Boolean]"
and ?f3.0 = "popST (Suc 0) \ pushST [PrimT Boolean]"
in bc_mt_corresp_comb_inside)
apply (simp (no_asm_simp))+
apply simp
apply (rule_tac T="(PrimT Boolean)" in bc_mt_corresp_LitPush) apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: length_compTpExpr)
apply (simp (no_asm_simp))
apply (simp (no_asm_simp) add: start_sttp_resp_def)
apply (drule_tac ?bc1.0 = "compExpr jmb expr1 @ compExpr jmb expr2 @ [Ifcmpeq 3, LitPush (Bool False)]"
and inst = "Goto 2" and ?bc3.0 = "[LitPush (Bool True)]"
and ?f1.0="compTpExpr jmb G expr1 \ compTpExpr jmb G expr2 \ popST 2 \ pushST [PrimT Boolean]"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.56 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
