File WellType.ML

open WellType;

Goalw [invmode_def] "invmode False (Acc (LVar e)) = IntVir";
b y Simp_tac 1;
qed "invmode_nonstatic";
Addsimps[invmode_nonstatic];

Goalw [invmode_def] "(invmode m e = Static) = m";
b y Simp_tac 1;
qed "invmode_Static_eq";
Addsimps[invmode_Static_eq];

Goalw [invmode_def] "(invmode m e = IntVir) = (¬m \<and> e\<noteq>Super)";
b y Simp_tac 1;
qed "invmode_IntVir_eq";

Goal "a'=Null \<longrightarrow> m \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null";
b y clarsimp_tac (claset(),simpset() addsimps [invmode_IntVir_eq]) 1;
qed "Null_staticD";

Delsimps[not_None_eq,split_paired_All,split_paired_Ex];
Delsplits[split_if,split_if_asm];
simpset_ref() := simpset() delloop "split_all_tac";
val wt_stmt_cases = wt.mk_cases "E,dt\<Turnstile>c\<Colon>\<surd>";
val wt_elim_cases = map wt.mk_cases [
	"E,dt\<Turnstile>In2  (LVar vn)               \<Colon>T",
	"E,dt\<Turnstile>In2  ({fd,s}e..fn)           \<Colon>T",
	"E,dt\<Turnstile>In2  (e.[i])                 \<Colon>T",
	"E,dt\<Turnstile>In1l (NewC C)                \<Colon>T",
	"E,dt\<Turnstile>In1l (New T'[i])             \<Colon>T",
	"E,dt\<Turnstile>In1l (Cast T' e)             \<Colon>T",
	"E,dt\<Turnstile>In1l (e InstOf T')           \<Colon>T",
	"E,dt\<Turnstile>In1l (Lit x)                 \<Colon>T",
	"E,dt\<Turnstile>In1l (Super)                 \<Colon>T",
	"E,dt\<Turnstile>In1l (Acc va)                \<Colon>T",
	"E,dt\<Turnstile>In1l (Ass va v)              \<Colon>T",
	"E,dt\<Turnstile>In1l (e0 ? e1 : e2)          \<Colon>T ",
	"E,dt\<Turnstile>In1l ({t,md,mode}e..mn({pT'}p))\<Colon>T ",
	"E,dt\<Turnstile>In1l (Methd C sig)           \<Colon>T ",
	"E,dt\<Turnstile>In1l (Body D blk res)        \<Colon>T ",
	"E,dt\<Turnstile>In3  ([])                    \<Colon>Ts",
	"E,dt\<Turnstile>In3  (e#es)                  \<Colon>Ts",
	"E,dt\<Turnstile>In1r  Skip                   \<Colon>x",
	"E,dt\<Turnstile>In1r (Expr e)                \<Colon>x",
	"E,dt\<Turnstile>In1r (c1;; c2)               \<Colon>x",  
	"E,dt\<Turnstile>In1r (If(e) c1 Else c2)      \<Colon>x",  
	"E,dt\<Turnstile>In1r (While(e) c)            \<Colon>x",
	"E,dt\<Turnstile>In1r (Throw e)               \<Colon>x",
	"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x",
	"E,dt\<Turnstile>In1r (c1 Finally c2)         \<Colon>x",
	"E,dt\<Turnstile>In1r (init C)                \<Colon>x"];
Addsplits[split_if,split_if_asm];
Addsimps[not_None_eq,split_paired_All,split_paired_Ex];
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac);

Goal "(G,L)\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd G C sig";
b y eresolve_tac wt_elim_cases 1;
b y Clarsimp_tac 1;
b y eatac is_methdI 1 1;
qed "wt_Methd_is_methd";

Goal "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT t; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; \
\      max_spec (prg E) t (mn, pTs) = {((md,(m,pns,rT)),pTs')}; \
\      mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{t,md,mode}e..mn({pTs'}ps)\<Colon>-rT";
b y rotate_tac ~1 1;
b y etac ssubst 1;
b y eatac wt.Call 2 1;
qed "wt_Call";

qed_goal "wt_init" thy "E,dt\<Turnstile>init C\<Colon>\<surd> = is_class (prg E) C" (K [
 auto_tac (claset() addEs wt_elim_cases addIs[wt.Init],simpset())]);
AddIffs [wt.Skip,wt_init];

Goal "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of In1 ec \<Rightarrow> (case ec of Inl e \<Rightarrow> \<exists>T. U=Inl T \
\                                          |      Inr s \<Rightarrow> U=Inl (PrimT Void)) \
\  | In2 e \<Rightarrow> (\<exists>T. U=Inl T) | In3 e \<Rightarrow> (\<exists>T. U=Inr T)";
b y split_all_tac 1;
b y etac wt.induct 1;
b y Auto_tac;
qed "wt_Inj_elim";

fun wt_fun name inj rhs =
let
  val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
  val () = qed_goal name thy (lhs ^ " = (" ^ rhs ^ ")") 
	(K [Auto_tac, ALLGOALS (ftac wt_Inj_elim) THEN Auto_tac])
  fun is_Inj (Const (inj,_) $ _) = true
    | is_Inj _                   = false
  fun pred (t as (_ $ (Const ("Pair",_) $
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
       x))) $ _ )) = is_Inj x
in
  make_simproc name lhs pred (thm name)
end;

val wt_expr_proc  = wt_fun "wt_expr_eq"  "In1l" "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>-T";
val wt_var_proc   = wt_fun "wt_var_eq"   "In2"  "\<exists>T.  U=Inl T  \<and> E,dt\<Turnstile>t\<Colon>=T";
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3"  "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts";
val wt_stmt_proc  = wt_fun "wt_stmt_eq"  "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>";
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc];

Goal "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))";
b y Auto_tac;
qed "Inj_eq_lemma";
Addsimps [Inj_eq_lemma];

(* unused *)
Goal "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> \
\ G = fst E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T  = T')";
b y EVERY'[pair_tac "E", pair_tac "x", etac wt.induct] 1;
b y ALLGOALS (EVERY'[rtac impI, REPEAT o mp_tac]);
b y safe_tac (claset() delrules [disjE]);
b y ALLGOALS (full_simp_tac (simpset() delsplits [split_if_asm]));
b y TRYALL Clarify_tac;
(* 17 subgoals *)
b y  ALLGOALS (fn i => if i = 9 then 
     EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", 
	   thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i (* Cond *)
	else thin_All_tac i);
b y ALLGOALS (eresolve_tac wt_elim_cases);
b y ALLGOALS (full_simp_tac (simpset() delsplits [split_if_asm]));
b y TRYALL (fast_tac (claset() delrules [equalityCE] 
	addD2 ("sym_trans", (sym RS trans))));
qed_spec_mp "univalent_tys_lemma";

(* unused *)
Goalw [univalent_def] 
"ws_prog (fst E) \<Longrightarrow> univalent {(t,T). E,dt\<Turnstile>t\<Colon>T}";
b y Clarsimp_tac 1;
b y rtac univalent_tys_lemma 1;
b y auto_tac (claset() addSIs [widen_antisym], simpset());
qed "univalent_tys";

Goal "typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T";
b y rtac val_.induct 1;
b y    	Auto_tac;
qed_spec_mp "typeof_empty_is_type";

(* unused *)
Goal "(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)";
b y rtac val_.induct 1;
b y     Fast_tac 5;
b y    ALLGOALS Simp_tac;
qed_spec_mp "typeof_is_type";

(**)
section "max_spec";

qed_goalw "max_spec2appl_meths" thy [max_spec_def] 
	"\<And>X. x \<in> max_spec G T sig \<Longrightarrow> x \<in> appl_methds G T sig" 
	(K [Fast_tac 1]);

qed_goalw "appl_methsD" thy [appl_methds_def] 
"\<And>X. (mh,pTs')\<in>appl_methds G T (mn, pTs) \<Longrightarrow> \
\  mh \<in> mheads G T (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
	(K [Fast_tac 1]);

bind_thm ("max_spec2mheads", insertI1 RSN (2,(equalityD2 RS subsetD)) RS 
                      max_spec2appl_meths RS appl_methsD);