File Evaln.ML

open Evaln;

Goal "\<And>s ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws";
b y split_all_tac 1;
b y etac evaln.induct 1;
(* 27 subgoals *)
b y Simp_tac 12; (* Ass *)
b y ALLGOALS 
    (asm_full_simp_tac (HOL_basic_ss addsplits [split_if_asm] 
                                 addsimprocs [split_beta_proc])); (* for Call*)
b y ALLGOALS (resolve_tac eval.intrs THEN_ALL_NEW TRY o atac);
b y ALLGOALS (force_tac (claset(),HOL_ss delsplits [split_if]));
qed "evaln_eval";

Goal "\<lbrakk>Suc n <= m'; (\<And>m. n <= m \<Longrightarrow> P (Suc m)) \<rbrakk> \<Longrightarrow> P m'";
b y cut_facts_tac (premises()) 1;
b y ftac Suc_le_D 1;
b y Clarify_tac 1;
b y eresolve_tac (premises()) 1;
qed "Suc_le_D_lemma";

Goal "\<And>s ws. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> ws";
b y split_all_tac 1;
b y etac evaln.induct 1;
(* 27 subgoals *)
b y Simp_tac 12; (* Ass *)
b y ALLGOALS 
    (asm_full_simp_tac (HOL_basic_ss addsplits [split_if_asm] 
                                 addsimprocs [split_beta_proc])); (* for Call*)
b y ALLGOALS (EVERY'[strip_tac, TRY o etac Suc_le_D_lemma, REPEAT o smp_tac 1]);
b y ALLGOALS (resolve_tac evaln.intrs THEN_ALL_NEW TRY o atac);
b y ALLGOALS (force_tac (claset(),HOL_ss delsplits [split_if]));
qed_spec_mp "evaln_nonstrict";

AddEs [evaln_nonstrict];
val evaln_nonstrict_Suc = (le_refl RS le_SucI) RSN (2, evaln_nonstrict);

Goal "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2\<rbrakk> \<Longrightarrow> G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max n1 n2\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max n1 n2\<rightarrow> ws2";
b y fast_tac (claset() addSIs [le_maxI1,le_maxI2]) 1;
qed "evaln_max2";

Goal "\<lbrakk>G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>n1\<rightarrow> ws1; G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>n2\<rightarrow> ws2; G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>n3\<rightarrow> ws3\<rbrakk> \<Longrightarrow> G\<turnstile>s1 \<midarrow>t1\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws1 \<and> G\<turnstile>s2 \<midarrow>t2\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws2 \<and> G\<turnstile>s3 \<midarrow>t3\<succ>\<midarrow>max (max n1 n2) n3\<rightarrow> ws3";
b y EVERY'[datac evaln_max2 1, etac thin_rl] 1;
b y fast_tac (claset() addSIs [le_maxI1,le_maxI2]) 1;
qed "evaln_max3";

Goal "\<And>s ws. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<exists>n. G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> ws)";
b y split_all_tac 1;
b y etac eval.induct 1;
(* 27 subgoals *)
b y Simp_tac 12; (* for Ass *)
b y ALLGOALS (asm_full_simp_tac (HOL_basic_ss addsplits [split_if_asm]
                              addsimprocs [split_beta_proc])); (* for Call*)
b y ALLGOALS (EVERY'[REPEAT o eresolve_tac [exE, conjE], rtac exI,
                     TRY o datac evaln_max3 2, 
           resolve_tac evaln.intrs THEN_ALL_NEW force_tac (HOL_cs, HOL_ss)]);
qed "eval_evaln";





Delsplits[split_if,split_if_asm,option.split,option.split_asm];
val evaln_cases = evaln.mk_cases "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> vs'";

val cases1 = [
	"G\<turnstile>(Some xc, s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow>  vs'",
	"G\<turnstile>Norm s \<midarrow>In1r Skip                      \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In3  ([])                      \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In3  (e#es)                    \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Lit w)                   \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In2  (LVar vn)                 \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Cast T e)                \<succ>\<midarrow>n\<rightarrow> vs'"];
val cases2 = [
	"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T)              \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Super)                   \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Acc va)                  \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Expr e)                  \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2)                 \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig)             \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Body D c e)              \<succ>\<midarrow>n\<rightarrow> xs'"];
val cases3 = [
	"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2)            \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2)        \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (While(e) c)              \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2)           \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Throw e)                 \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In1l (NewC C)                  \<succ>\<midarrow>n\<rightarrow> vs'"];
val cases4 = [
	"G\<turnstile>Norm s \<midarrow>In1l (New T[e])                \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l (Ass va e)                \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2)  \<succ>\<midarrow>n\<rightarrow> xs'",
	"G\<turnstile>Norm s \<midarrow>In2  ({C,stat}e..fn)           \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In2  (e1.[e2])                 \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1l ({t,cT,mode}e..mn({pT}p)) \<succ>\<midarrow>n\<rightarrow> vs'",
	"G\<turnstile>Norm s \<midarrow>In1r (init C)                  \<succ>\<midarrow>n\<rightarrow> xs'"];
val evaln_elim_cases = map evaln.mk_cases (cases1@cases2@cases3@cases4);
Addsplits[split_if,split_if_asm,option.split,option.split_asm];

Goal "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w,s') \<Longrightarrow> case t of In1 ec \<Rightarrow> \
\ (case ec of Inl e \<Rightarrow> (\<exists>v. w = In1 v) | Inr c \<Rightarrow> w = In1 Unit) \
\ | In2 e \<Rightarrow> (\<exists>v. w = In2 v) | In3 e \<Rightarrow> (\<exists>v. w = In3 v)";
b y etac evaln_cases 1 THEN Auto_tac;
b y induct_tac "t" 1;
b y   induct_tac "a" 1;
b y Auto_tac;
qed "evaln_Inj_elim";

fun enf nam inj rhs =
let
  val name = "evaln_" ^ nam ^ "_eq"
  val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<midarrow>n\<rightarrow> (w, s')"
  val () = qed_goal name thy (lhs ^ " = (" ^ rhs ^ ")") 
	(K [Auto_tac, ALLGOALS (ftac evaln_Inj_elim) THEN Auto_tac])
  fun is_Inj (Const (inj,_) $ _) = true
    | is_Inj _                   = false
  fun pred (_ $ (Const ("Pair",_) $ _ $ (Const ("Pair", _) $ _ $ 
    (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ )))) $ _ ) = is_Inj x
in
  make_simproc name lhs pred (thm name)
end;

val evaln_expr_proc = enf "expr" "In1l" "\<exists>v.  w=In1 v   \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<midarrow>n\<rightarrow> s'";
val evaln_var_proc  = enf "var"  "In2"  "\<exists>vf. w=In2 vf  \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<midarrow>n\<rightarrow> s'";
val evaln_exprs_proc= enf "exprs""In3"  "\<exists>vs. w=In3 vs  \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s'";
val evaln_stmt_proc = enf "stmt" "In1r" "     w=In1 Unit\<and> G\<turnstile>s \<midarrow>t     \<midarrow>n\<rightarrow> s'";
Addsimprocs [evaln_expr_proc,evaln_var_proc,evaln_exprs_proc,evaln_stmt_proc];

val evaln_XcptIs = sum3_instantiate evaln.Xcpt;
AddSIs evaln_XcptIs;


fun split_solve_tac s = EVERY' [pair_tac s, case_tac "x = None" THEN_ALL_NEW 
 (force_tac (claset() addSEs evaln_elim_cases addSIs evaln.intrs, simpset()))];
fun split_prover n s = qed_goal n thy s (fn prems => 
	[cut_facts_tac prems 1, split_solve_tac "s" 1]);
split_prover "evaln_LitI" "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<midarrow>n\<rightarrow> s";
split_prover "CondI" "\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<midarrow>n\<rightarrow> s2";
split_prover "evaln_SkipI" "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s";
split_prover "evaln_ExprI" "G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<midarrow>n\<rightarrow> s'";
split_prover "evaln_CompI" "\<lbrakk>G\<turnstile>s \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2";
split_prover "evaln_IfI" "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<midarrow>n\<rightarrow> s2";
AddSIs[evaln_SkipI];

qed_goal "evaln_SkipD" thy "\<And>X. G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' \<Longrightarrow> s' = s" 
	(K [etac evaln_cases 1 THEN Auto_tac]);
AddSDs [evaln_SkipD];
Goal "G\<turnstile>s \<midarrow>Skip\<midarrow>n\<rightarrow> s' = (s = s')";
b y Auto_tac;
qed "evaln_Skip_eq";
Addsimps[evaln_Skip_eq];

Goal "G\<turnstile>s \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (v,s') \<Longrightarrow> fst s = Some xc \<longrightarrow> s' = s \<and> v = arbitrary3 e";
b y etac evaln_cases 1 THEN Auto_tac;
qed "evaln_xcpt_lemma";

Goal         "\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s') = (s' = (Some xc,s) \<and> \
\ w=arbitrary3 e \<and> G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (arbitrary3 e,(Some xc,s)))";
b y Auto_tac;
b y ALLGOALS (ftac evaln_xcpt_lemma) THEN Auto_tac;
qed "evaln_xcpt";

local
  fun is_Some (Const ("Pair",_) $ (Const ("Option.option.Some",_) $ _)$ _) =true
    | is_Some _ = false
  fun pred (_ $ (Const ("Pair",_) $
     _ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
       (Const ("Pair", _) $ _ $ x)))) $ _ ) = is_Some x
in
  val evaln_xcpt_proc = 
  make_simproc "evaln_xcpt" "G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<midarrow>n\<rightarrow> (w,s')"pred evaln_xcpt
end;
Addsimprocs [evaln_xcpt_proc];