Theory execute_Bigstep (Isabelle repository snapshot 408271602165 12-Mar-2013)

(*  Title:      Jinja/J/execute_Bigstep.thy
    Author:     Tobias Nipkow
    Copyright   2004 Technische Universitaet Muenchen
*)

header {* \isaheader{Code Generation For BigStep} *}

theory execute_Bigstep
imports
  BigStep Examples
  "~~/src/HOL/Library/Code_Target_Numeral"
begin

inductive map_val :: "expr list => val list => bool"
where
  Nil: "map_val [] []"
| Cons: "map_val xs ys ==> map_val (Val y # xs) (y # ys)"

inductive map_val2 :: "expr list => val list => expr list => bool"
where
  Nil: "map_val2 [] [] []"
| Cons: "map_val2 xs ys zs ==> map_val2 (Val y # xs) (y # ys) zs"
| Throw: "map_val2 (throw e # xs) [] (throw e # xs)"

theorem map_val_conv: "(xs = map Val ys) = map_val xs ys"
(*<*)
proof -
  have "!!ys. xs = map Val ys ==> map_val xs ys"
    apply (induct xs type:list)
    apply (case_tac ys)
    apply simp
    apply (rule map_val.Nil)
    apply simp
    apply (case_tac ys)
    apply simp
    apply simp
    apply (erule conjE)
    apply (rule map_val.Cons)
    apply simp
    done
  moreover have "map_val xs ys ==> xs = map Val ys"
    by (erule map_val.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)

theorem map_val2_conv:
 "(xs = map Val ys @ throw e # zs) = map_val2 xs ys (throw e # zs)"
(*<*)
proof -
  have "!!ys. xs = map Val ys @ throw e # zs ==> map_val2 xs ys (throw e # zs)"
    apply (induct xs type:list)
    apply (case_tac ys)
    apply simp
    apply simp
    apply simp
    apply (case_tac ys)
    apply simp
    apply (rule map_val2.Throw)
    apply simp
    apply (rule map_val2.Cons)
    apply simp
    done
  moreover have "map_val2 xs ys (throw e # zs) ==> xs = map Val ys @ throw e # zs"
    by (erule map_val2.induct) simp+
  ultimately show ?thesis ..
qed
(*>*)

lemma CallNull2:
  "[| P \<turnstile> ⟨e,s⇣₀⟩ => ⟨null,s⇣₁⟩;  P \<turnstile> ⟨ps,s⇣₁⟩ [=>] ⟨evs,s⇣₂⟩; map_val evs vs |]
  ==> P \<turnstile> ⟨e•M(ps),s⇣₀⟩ => ⟨THROW NullPointer,s⇣₂⟩"
apply(rule CallNull, assumption+)
apply(simp add: map_val_conv[symmetric])
done


lemma CallParamsThrow2:
  "[| P \<turnstile> ⟨e,s⇣₀⟩ => ⟨Val v,s⇣₁⟩; P \<turnstile> ⟨es,s⇣₁⟩ [=>] ⟨evs,s⇣₂⟩;
     map_val2 evs vs (throw ex # es'') |]
   ==> P \<turnstile> ⟨e•M(es),s⇣₀⟩ => ⟨throw ex,s⇣₂⟩"
apply(rule eval_evals.CallParamsThrow, assumption+)
apply(simp add: map_val2_conv[symmetric])
done

lemma Call2:
  "[| P \<turnstile> ⟨e,s⇣₀⟩ => ⟨addr a,s⇣₁⟩;  P \<turnstile> ⟨ps,s⇣₁⟩ [=>] ⟨evs,(h⇣₂,l⇣₂)⟩;
     map_val evs vs;
     h⇣₂ a = Some(C,fs);  P \<turnstile> C sees M:Ts->T = (pns,body) in D;
     length vs = length pns;  l⇣₂' = [this\<mapsto>Addr a, pns[\<mapsto>]vs];
     P \<turnstile> ⟨body,(h⇣₂,l⇣₂')⟩ => ⟨e',(h⇣₃,l⇣₃)⟩ |]
  ==> P \<turnstile> ⟨e•M(ps),s⇣₀⟩ => ⟨e',(h⇣₃,l⇣₂)⟩"
apply(rule Call, assumption+)
apply(simp add: map_val_conv[symmetric])
apply assumption+
done

code_pred 
  (modes: i => o => bool)
  map_val 
.

code_pred
  (modes: i => o => o => bool)
  map_val2
.

lemmas [code_pred_intro] =
 eval_evals.New eval_evals.NewFail
 eval_evals.Cast eval_evals.CastNull eval_evals.CastFail eval_evals.CastThrow
 eval_evals.Val eval_evals.Var
 eval_evals.BinOp eval_evals.BinOpThrow1 eval_evals.BinOpThrow2
 eval_evals.LAss eval_evals.LAssThrow
 eval_evals.FAcc eval_evals.FAccNull eval_evals.FAccThrow
 eval_evals.FAss eval_evals.FAssNull
 eval_evals.FAssThrow1 eval_evals.FAssThrow2
 eval_evals.CallObjThrow

declare CallNull2 [code_pred_intro CallNull2]
declare CallParamsThrow2 [code_pred_intro CallParamsThrow2]
declare Call2 [code_pred_intro Call2]

lemmas [code_pred_intro] =
 eval_evals.Block
 eval_evals.Seq eval_evals.SeqThrow
 eval_evals.CondT eval_evals.CondF eval_evals.CondThrow
 eval_evals.WhileF eval_evals.WhileT
 eval_evals.WhileCondThrow

declare eval_evals.WhileBodyThrow [code_pred_intro WhileBodyThrow2]

lemmas [code_pred_intro] =
 eval_evals.Throw eval_evals.ThrowNull
 eval_evals.ThrowThrow
 eval_evals.Try eval_evals.TryCatch eval_evals.TryThrow
 eval_evals.Nil eval_evals.Cons eval_evals.ConsThrow

code_pred
  (modes: i => i => i => o => o => bool as execute)
  eval
proof -
  case eval
  from eval.prems show thesis
  proof(cases (no_simp))
    case CallNull thus ?thesis
      by(rule CallNull2[OF refl])(simp add: map_val_conv[symmetric])
  next
    case CallParamsThrow thus ?thesis
      by(rule CallParamsThrow2[OF refl])(simp add: map_val2_conv[symmetric])
  next
    case Call thus ?thesis
      by -(rule Call2[OF refl], simp_all add: map_val_conv[symmetric])
  next
    case WhileBodyThrow thus ?thesis by(rule WhileBodyThrow2[OF refl])
  qed(assumption|erule (4) that[OF refl]|erule (3) that[OF refl])+
next
  case evals
  from evals.prems show thesis
    by(cases (no_simp))(assumption|erule (3) that[OF refl])+
qed

notation execute ("_ \<turnstile> ((1⟨_,/_⟩) =>/ ⟨'_, '_⟩)" [51,0,0] 81)

definition "test1 = [] \<turnstile> ⟨testExpr1,(empty,empty)⟩ => ⟨_,_⟩"
definition "test2 = [] \<turnstile> ⟨testExpr2,(empty,empty)⟩ => ⟨_,_⟩"
definition "test3 = [] \<turnstile> ⟨testExpr3,(empty,empty(''V''\<mapsto>Intg 77))⟩ => ⟨_,_⟩"
definition "test4 = [] \<turnstile> ⟨testExpr4,(empty,empty)⟩ => ⟨_,_⟩"
definition "test5 = [(''Object'',('''',[],[])),(''C'',(''Object'',[(''F'',Integer)],[]))] \<turnstile> ⟨testExpr5,(empty,empty)⟩ => ⟨_,_⟩"
definition "test6 = [(''Object'',('''',[],[])), classI] \<turnstile> ⟨testExpr6,(empty,empty)⟩ => ⟨_,_⟩"

definition "V = ''V''"
definition "C = ''C''"
definition "F = ''F''"

ML_val {*
  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 5)), _), _) = Predicate.yield @{code test1};
  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 11)), _), _) = Predicate.yield @{code test2};
  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 83)), _), _) = Predicate.yield @{code test3};

  val SOME ((_, (_, l)), _) = Predicate.yield @{code test4};
  val SOME (@{code Intg} (@{code int_of_integer} 6)) = l @{code V};

  val SOME ((_, (h, _)), _) = Predicate.yield @{code test5};
  val SOME (c, fs) = h (@{code nat_of_integer} 1);
  val SOME (obj, _) = h (@{code nat_of_integer} 0);
  val SOME (@{code Intg} i) = fs (@{code F}, @{code C});
  @{assert} (c = @{code C} andalso obj = @{code Object} andalso i = @{code int_of_integer} 42);

  val SOME ((@{code Val} (@{code Intg} (@{code int_of_integer} 160)), _), _) = Predicate.yield @{code test6};
*}

definition "test7 = [classObject, classL] \<turnstile> ⟨testExpr_BuildList, (empty,empty)⟩ => ⟨_,_⟩"

definition "L = ''L''"
definition "N = ''N''"

ML_val {*
  val SOME ((_, (h, _)), _) = Predicate.yield @{code test7};
  val SOME (_, fs1) = h (@{code nat_of_integer} 0);
  val SOME (_, fs2) = h (@{code nat_of_integer} 1);
  val SOME (_, fs3) = h (@{code nat_of_integer} 2);
  val SOME (_, fs4) = h (@{code nat_of_integer} 3);

  val F = @{code "F"};
  val L = @{code "L"};
  val N = @{code "N"};

  @{assert} (fs1 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 1)) andalso
     fs1 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 1)) andalso
     fs2 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 2)) andalso
     fs2 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 2)) andalso
     fs3 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 3)) andalso
     fs3 (N, L) = SOME (@{code Addr} (@{code nat_of_integer} 3)) andalso
     fs4 (F, L) = SOME (@{code Intg} (@{code int_of_integer} 4)) andalso
     fs4 (N, L) = SOME @{code Null});
*}

definition "test8 = [classObject, classA] \<turnstile> ⟨testExpr_ClassA, (empty,empty)⟩ => ⟨_,_⟩"
definition "i = ''int''"
definition "t = ''test''"
definition "A = ''A''"

ML_val {*
  val SOME ((_, (h, l)), _) = Predicate.yield @{code test8};
  val SOME (_, fs1) = h (@{code nat_of_integer} 0);
  val SOME (_, fs2) = h (@{code nat_of_integer} 1);

  val i = @{code "i"};
  val t = @{code "t"};
  val A = @{code "A"};

  @{assert} (fs1 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 10)) andalso 
     fs1 (t, A) = SOME @{code Null} andalso
     fs2 (i, A) = SOME (@{code Intg} (@{code int_of_integer} 50)) andalso 
     fs2 (t, A) = SOME @{code Null});
*}

end