Up to index of Isabelle/HOL/Jinja
theory Equivalence = BigStep + SmallStep + WWellForm:(* Title: Jinja/J/Equivalence.thy
ID: $Id: Equivalence.html 1910 2004-05-19 04:46:04Z kleing $
Author: Tobias Nipkow
Copyright 2003 Technische Universitaet Muenchen
*)
header {* \isaheader{Equivalence of Big Step and Small Step Semantics} *}
theory Equivalence = BigStep + SmallStep + WWellForm:
section{*Small steps simulate big step*}
subsubsection "Cast"
lemma CastReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨Cast C e,s⟩ ->* ⟨Cast C e',s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CastRed)
done
(*>*)
lemma CastRedsNull:
"P \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P \<turnstile> ⟨Cast C e,s⟩ ->* ⟨null,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CastReds)
apply(rule RedCastNull)
done
(*>*)
lemma CastRedsAddr:
"[| P \<turnstile> ⟨e,s⟩ ->* ⟨addr a,s'⟩; hp s' a = Some(D,fs); P \<turnstile> D \<preceq>* C |] ==>
P \<turnstile> ⟨Cast C e,s⟩ ->* ⟨addr a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CastReds)
apply(erule (1) RedCast)
done
(*>*)
lemma CastRedsFail:
"[| P \<turnstile> ⟨e,s⟩ ->* ⟨addr a,s'⟩; hp s' a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |] ==>
P \<turnstile> ⟨Cast C e,s⟩ ->* ⟨THROW ClassCast,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CastReds)
apply(erule (1) RedCastFail)
done
(*>*)
lemma CastRedsThrow:
"[| P \<turnstile> ⟨e,s⟩ ->* ⟨throw a,s'⟩ |] ==> P \<turnstile> ⟨Cast C e,s⟩ ->* ⟨throw a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CastReds)
apply(rule red_reds.CastThrow)
done
(*>*)
subsubsection "LAss"
lemma LAssReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨ V:=e,s⟩ ->* ⟨ V:=e',s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule LAssRed)
done
(*>*)
lemma LAssRedsVal:
"[| P \<turnstile> ⟨e,s⟩ ->* ⟨Val v,(h',l')⟩ |] ==> P \<turnstile> ⟨ V:=e,s⟩ ->* ⟨unit,(h',l'(V\<mapsto>v))⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule LAssReds)
apply(rule RedLAss)
done
(*>*)
lemma LAssRedsThrow:
"[| P \<turnstile> ⟨e,s⟩ ->* ⟨throw a,s'⟩ |] ==> P \<turnstile> ⟨ V:=e,s⟩ ->* ⟨throw a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule LAssReds)
apply(rule red_reds.LAssThrow)
done
(*>*)
subsubsection "BinOp"
lemma BinOp1Reds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨ e «bop» e2, s⟩ ->* ⟨e' «bop» e2, s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule BinOpRed1)
done
(*>*)
lemma BinOp2Reds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨(Val v) «bop» e, s⟩ ->* ⟨(Val v) «bop» e', s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule BinOpRed2)
done
(*>*)
lemma BinOpRedsVal:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v2,s2⟩; binop(bop,v1,v2) = Some v |]
==> P \<turnstile> ⟨e1 «bop» e2, s0⟩ ->* ⟨Val v,s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
apply(erule BinOp2Reds)
apply(rule RedBinOp)
apply simp
done
(*>*)
lemma BinOpRedsThrow1:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw e',s'⟩ ==> P \<turnstile> ⟨e «bop» e2, s⟩ ->* ⟨throw e', s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule BinOp1Reds)
apply(rule red_reds.BinOpThrow1)
done
(*>*)
lemma BinOpRedsThrow2:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨throw e,s2⟩|]
==> P \<turnstile> ⟨e1 «bop» e2, s0⟩ ->* ⟨throw e,s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule BinOp1Reds)
apply(rule rtrancl_into_rtrancl)
apply(erule BinOp2Reds)
apply(rule red_reds.BinOpThrow2)
done
(*>*)
subsubsection "FAcc"
lemma FAccReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨e\<bullet>F{D}, s⟩ ->* ⟨e'\<bullet>F{D}, s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAccRed)
done
(*>*)
lemma FAccRedsVal:
"[|P \<turnstile> ⟨e,s⟩ ->* ⟨addr a,s'⟩; hp s' a = Some(C,fs); fs(F,D) = Some v |]
==> P \<turnstile> ⟨e\<bullet>F{D},s⟩ ->* ⟨Val v,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule FAccReds)
apply(erule (1) RedFAcc)
done
(*>*)
lemma FAccRedsNull:
"P \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P \<turnstile> ⟨e\<bullet>F{D},s⟩ ->* ⟨THROW NullPointer,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule FAccReds)
apply(rule RedFAccNull)
done
(*>*)
lemma FAccRedsThrow:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw a,s'⟩ ==> P \<turnstile> ⟨e\<bullet>F{D},s⟩ ->* ⟨throw a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule FAccReds)
apply(rule red_reds.FAccThrow)
done
(*>*)
subsubsection "FAss"
lemma FAssReds1:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨e\<bullet>F{D}:=e2, s⟩ ->* ⟨e'\<bullet>F{D}:=e2, s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAssRed1)
done
(*>*)
lemma FAssReds2:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨Val v\<bullet>F{D}:=e, s⟩ ->* ⟨Val v\<bullet>F{D}:=e', s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule FAssRed2)
done
(*>*)
lemma FAssRedsVal:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨addr a,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v,(h2,l2)⟩; Some(C,fs) = h2 a |] ==>
P \<turnstile> ⟨e1\<bullet>F{D}:=e2, s0⟩ ->* ⟨unit, (h2(a\<mapsto>(C,fs((F,D)\<mapsto>v))),l2)⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
apply(erule FAssReds2)
apply(rule RedFAss)
apply simp
done
(*>*)
lemma FAssRedsNull:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨null,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨Val v,s2⟩ |] ==>
P \<turnstile> ⟨e1\<bullet>F{D}:=e2, s0⟩ ->* ⟨THROW NullPointer, s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
apply(erule FAssReds2)
apply(rule RedFAssNull)
done
(*>*)
lemma FAssRedsThrow1:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw e',s'⟩ ==> P \<turnstile> ⟨e\<bullet>F{D}:=e2, s⟩ ->* ⟨throw e', s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule FAssReds1)
apply(rule red_reds.FAssThrow1)
done
(*>*)
lemma FAssRedsThrow2:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨throw e,s2⟩ |]
==> P \<turnstile> ⟨e1\<bullet>F{D}:=e2,s0⟩ ->* ⟨throw e,s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule FAssReds1)
apply(rule rtrancl_into_rtrancl)
apply(erule FAssReds2)
apply(rule red_reds.FAssThrow2)
done
(*>*)
subsubsection";;"
lemma SeqReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨e;;e2, s⟩ ->* ⟨e';;e2, s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule SeqRed)
done
(*>*)
lemma SeqRedsThrow:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw e',s'⟩ ==> P \<turnstile> ⟨e;;e2, s⟩ ->* ⟨throw e', s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule SeqReds)
apply(rule red_reds.SeqThrow)
done
(*>*)
lemma SeqReds2:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨Val v1,s1⟩; P \<turnstile> ⟨e2,s1⟩ ->* ⟨e2',s2⟩ |] ==> P \<turnstile> ⟨e1;;e2, s0⟩ ->* ⟨e2',s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule SeqReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedSeq)
apply assumption
done
(*>*)
subsubsection"If"
lemma CondReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨if (e) e1 else e2,s⟩ ->* ⟨if (e') e1 else e2,s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CondRed)
done
(*>*)
lemma CondRedsThrow:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw a,s'⟩ ==> P \<turnstile> ⟨if (e) e1 else e2, s⟩ ->* ⟨throw a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CondReds)
apply(rule red_reds.CondThrow)
done
(*>*)
lemma CondReds2T:
"[|P \<turnstile> ⟨e,s0⟩ ->* ⟨true,s1⟩; P \<turnstile> ⟨e1, s1⟩ ->* ⟨e',s2⟩ |] ==> P \<turnstile> ⟨if (e) e1 else e2, s0⟩ ->* ⟨e',s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedCondT)
apply assumption
done
(*>*)
lemma CondReds2F:
"[|P \<turnstile> ⟨e,s0⟩ ->* ⟨false,s1⟩; P \<turnstile> ⟨e2, s1⟩ ->* ⟨e',s2⟩ |] ==> P \<turnstile> ⟨if (e) e1 else e2, s0⟩ ->* ⟨e',s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedCondF)
apply assumption
done
(*>*)
subsubsection "While"
lemma WhileFReds:
"P \<turnstile> ⟨b,s⟩ ->* ⟨false,s'⟩ ==> P \<turnstile> ⟨while (b) c,s⟩ ->* ⟨unit,s'⟩"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedWhile)
apply(rule rtrancl_into_rtrancl)
apply(erule CondReds)
apply(rule RedCondF)
done
(*>*)
lemma WhileRedsThrow:
"P \<turnstile> ⟨b,s⟩ ->* ⟨throw e,s'⟩ ==> P \<turnstile> ⟨while (b) c,s⟩ ->* ⟨throw e,s'⟩"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedWhile)
apply(rule rtrancl_into_rtrancl)
apply(erule CondReds)
apply(rule red_reds.CondThrow)
done
(*>*)
lemma WhileTReds:
"[| P \<turnstile> ⟨b,s0⟩ ->* ⟨true,s1⟩; P \<turnstile> ⟨c,s1⟩ ->* ⟨Val v1,s2⟩; P \<turnstile> ⟨while (b) c,s2⟩ ->* ⟨e,s3⟩ |]
==> P \<turnstile> ⟨while (b) c,s0⟩ ->* ⟨e,s3⟩"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedWhile)
apply(rule rtrancl_trans)
apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedCondT)
apply(rule rtrancl_trans)
apply(erule SeqReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedSeq)
apply assumption
done
(*>*)
lemma WhileTRedsThrow:
"[| P \<turnstile> ⟨b,s0⟩ ->* ⟨true,s1⟩; P \<turnstile> ⟨c,s1⟩ ->* ⟨throw e,s2⟩ |]
==> P \<turnstile> ⟨while (b) c,s0⟩ ->* ⟨throw e,s2⟩"
(*<*)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedWhile)
apply(rule rtrancl_trans)
apply(erule CondReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedCondT)
apply(rule rtrancl_into_rtrancl)
apply(erule SeqReds)
apply(rule red_reds.SeqThrow)
done
(*>*)
subsubsection"Throw"
lemma ThrowReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨throw e,s⟩ ->* ⟨throw e',s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ThrowRed)
done
(*>*)
lemma ThrowRedsNull:
"P \<turnstile> ⟨e,s⟩ ->* ⟨null,s'⟩ ==> P \<turnstile> ⟨throw e,s⟩ ->* ⟨THROW NullPointer,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule ThrowReds)
apply(rule RedThrowNull)
done
(*>*)
lemma ThrowRedsThrow:
"P \<turnstile> ⟨e,s⟩ ->* ⟨throw a,s'⟩ ==> P \<turnstile> ⟨throw e,s⟩ ->* ⟨throw a,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule ThrowReds)
apply(rule red_reds.ThrowThrow)
done
(*>*)
subsubsection "InitBlock"
lemma InitBlockReds_aux:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==>
∀h l h' l' v. s = (h,l(V\<mapsto>v)) --> s' = (h',l') -->
P \<turnstile> ⟨{V:T := Val v; e},(h,l)⟩ ->* ⟨{V:T := Val(the(l' V)); e'},(h',l'(V:=(l V)))⟩"
(*<*)
apply(erule converse_rtrancl_induct2)
apply(fastsimp simp: fun_upd_same simp del:fun_upd_apply)
apply clarify
apply(rename_tac e0 X Y e1 h1 l1 h0 l0 h2 l2 v0)
apply(subgoal_tac "V ∈ dom l1")
prefer 2
apply(drule red_lcl_incr)
apply simp
apply clarsimp
apply(rename_tac v1)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule InitBlockRed)
apply assumption
apply simp
apply(erule_tac x = "l1(V := l0 V)" in allE)
apply(erule_tac x = v1 in allE)
apply(erule impE)
apply(rule ext)
apply(simp add:fun_upd_def)
apply(simp add:fun_upd_def)
done
(*>*)
lemma InitBlockReds:
"P \<turnstile> ⟨e, (h,l(V\<mapsto>v))⟩ ->* ⟨e', (h',l')⟩ ==>
P \<turnstile> ⟨{V:T := Val v; e}, (h,l)⟩ ->* ⟨{V:T := Val(the(l' V)); e'}, (h',l'(V:=(l V)))⟩"
(*<*)by(blast dest:InitBlockReds_aux)(*>*)
lemma InitBlockRedsFinal:
"[| P \<turnstile> ⟨e,(h,l(V\<mapsto>v))⟩ ->* ⟨e',(h',l')⟩; final e' |] ==>
P \<turnstile> ⟨{V:T := Val v; e},(h,l)⟩ ->* ⟨e',(h', l'(V := l V))⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule InitBlockReds)
apply(fast elim!:finalE intro:RedInitBlock InitBlockThrow)
done
(*>*)
subsubsection "Block"
lemma BlockRedsFinal:
assumes reds: "P \<turnstile> ⟨e0,s0⟩ ->* ⟨e2,(h2,l2)⟩" and fin: "final e2"
shows "!!h0 l0. s0 = (h0,l0(V:=None)) ==> P \<turnstile> ⟨{V:T; e0},(h0,l0)⟩ ->* ⟨e2,(h2,l2(V:=l0 V))⟩"
(*<*)
using reds
proof (induct rule:converse_rtrancl_induct2)
case refl thus ?case
by(fastsimp intro:finalE[OF fin] RedBlock BlockThrow
simp del:fun_upd_apply)
next
case (step e0 s0 e1 s1)
have red: "P \<turnstile> ⟨e0,s0⟩ -> ⟨e1,s1⟩"
and reds: "P \<turnstile> ⟨e1,s1⟩ ->* ⟨e2,(h2,l2)⟩"
and IH: "!!h l. s1 = (h,l(V := None))
==> P \<turnstile> ⟨{V:T; e1},(h,l)⟩ ->* ⟨e2,(h2, l2(V := l V))⟩"
and s0: "s0 = (h0, l0(V := None))" .
obtain h1 l1 where s1: "s1 = (h1,l1)" by fastsimp
show ?case
proof cases
assume "assigned V e0"
then obtain v e where e0: "e0 = V := Val v;; e"
by (unfold assigned_def)blast
from red e0 s0 have e1: "e1 = unit;;e" and s1: "s1 = (h0, l0(V \<mapsto> v))"
by auto
from e1 fin have "e1 ≠ e2" by (auto simp:final_def)
then obtain e' s' where red1: "P \<turnstile> ⟨e1,s1⟩ -> ⟨e',s'⟩"
and reds': "P \<turnstile> ⟨e',s'⟩ ->* ⟨e2,(h2,l2)⟩"
using converse_rtranclE2[OF reds] by blast
from red1 e1 have es': "e' = e" "s' = s1" by auto
show ?case using e0 s1 es' reds'
by(fastsimp intro!: InitBlockRedsFinal[OF _ fin] simp del:fun_upd_apply)
next
assume unass: "¬ assigned V e0"
show ?thesis
proof (cases "l1 V")
assume None: "l1 V = None"
hence "P \<turnstile> ⟨{V:T; e0},(h0,l0)⟩ -> ⟨{V:T; e1},(h1, l1(V := l0 V))⟩"
using s0 s1 red by(simp add: BlockRedNone[OF _ _ unass])
moreover
have "P \<turnstile> ⟨{V:T; e1},(h1, l1(V := l0 V))⟩ ->* ⟨e2,(h2, l2(V := l0 V))⟩"
using IH[of _ "l1(V := l0 V)"] s1 None by(simp add:fun_upd_idem)
ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
next
fix v assume Some: "l1 V = Some v"
hence "P \<turnstile> ⟨{V:T;e0},(h0,l0)⟩ -> ⟨{V:T := Val v; e1},(h1,l1(V := l0 V))⟩"
using s0 s1 red by(simp add: BlockRedSome[OF _ _ unass])
moreover
have "P \<turnstile> ⟨{V:T := Val v; e1},(h1,l1(V:= l0 V))⟩ ->*
⟨e2,(h2,l2(V:=l0 V))⟩"
using InitBlockRedsFinal[OF _ fin,of _ _ "l1(V:=l0 V)" V]
Some reds s1 by(simp add:fun_upd_idem)
ultimately show ?case by(rule converse_rtrancl_into_rtrancl)
qed
qed
qed
(*>*)
subsubsection "try-catch"
lemma TryReds:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨try e catch(C V) e2,s⟩ ->* ⟨try e' catch(C V) e2,s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule TryRed)
done
(*>*)
lemma TryRedsVal:
"P \<turnstile> ⟨e,s⟩ ->* ⟨Val v,s'⟩ ==> P \<turnstile> ⟨try e catch(C V) e2,s⟩ ->* ⟨Val v,s'⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule TryReds)
apply(rule RedTry)
done
(*>*)
lemma TryCatchRedsFinal:
"[| P \<turnstile> ⟨e1,s0⟩ ->* ⟨Throw a,(h1,l1)⟩; h1 a = Some(D,fs); P \<turnstile> D \<preceq>* C;
P \<turnstile> ⟨e2, (h1, l1(V \<mapsto> Addr a))⟩ ->* ⟨e2', (h2,l2)⟩; final e2' |]
==> P \<turnstile> ⟨try e1 catch(C V) e2, s0⟩ ->* ⟨e2', (h2, l2(V := l1 V))⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule TryReds)
apply(rule converse_rtrancl_into_rtrancl)
apply(rule RedTryCatch)
apply fastsimp
apply assumption
apply(rule InitBlockRedsFinal)
apply assumption
apply(simp)
done
(*>*)
lemma TryRedsFail:
"[| P \<turnstile> ⟨e1,s⟩ ->* ⟨Throw a,(h,l)⟩; h a = Some(D,fs); ¬ P \<turnstile> D \<preceq>* C |]
==> P \<turnstile> ⟨try e1 catch(C V) e2,s⟩ ->* ⟨Throw a,(h,l)⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule TryReds)
apply(fastsimp intro!: RedTryFail)
done
(*>*)
subsubsection "List"
lemma ListReds1:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨e#es,s⟩ [->]* ⟨e' # es,s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ListRed1)
done
(*>*)
lemma ListReds2:
"P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> P \<turnstile> ⟨Val v # es,s⟩ [->]* ⟨Val v # es',s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule ListRed2)
done
(*>*)
lemma ListRedsVal:
"[| P \<turnstile> ⟨e,s0⟩ ->* ⟨Val v,s1⟩; P \<turnstile> ⟨es,s1⟩ [->]* ⟨es',s2⟩ |]
==> P \<turnstile> ⟨e#es,s0⟩ [->]* ⟨Val v # es',s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule ListReds1)
apply(erule ListReds2)
done
(*>*)
subsubsection"Call"
text{* First a few lemmas on what happens to free variables during redction. *}
lemma assumes wf: "wwf_J_prog P"
shows Red_fv: "P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> fv e' ⊆ fv e"
and "P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> fvs es' ⊆ fvs es"
(*<*)
proof (induct rule:red_reds_induct)
case (RedCall C D M T Ts a body fs pns h l vs)
hence "fv body ⊆ {this} ∪ set pns"
using prems by(fastsimp dest!:sees_wf_mdecl simp:wf_mdecl_def)
with prems show ?case by fastsimp
qed auto
(*>*)
lemma Red_dom_lcl:
"P \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fv e" and
"P \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> dom l' ⊆ dom l ∪ fvs es"
(*<*)
proof (induct rule:red_reds_induct)
case RedLAss thus ?case by(force split:if_splits)
next
case CallParams thus ?case by(force split:if_splits)
next
case BlockRedNone thus ?case by clarsimp (fastsimp split:if_splits)
next
case BlockRedSome thus ?case by clarsimp (fastsimp split:if_splits)
next
case InitBlockRed thus ?case by clarsimp (fastsimp split:if_splits)
qed (simp_all, blast+)
(*>*)
lemma Reds_dom_lcl:
"[| wwf_J_prog P; P \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩ |] ==> dom l' ⊆ dom l ∪ fv e"
(*<*)
apply(erule converse_rtrancl_induct_red)
apply blast
apply(blast dest: Red_fv Red_dom_lcl)
done
(*>*)
text{* Now a few lemmas on the behaviour of blocks during reduction. *}
(* If you want to avoid the premise "distinct" further down …
consts upd_vals :: "locals => vname list => val list => val list"
primrec
"upd_vals l [] vs = []"
"upd_vals l (V#Vs) vs = (if V ∈ set Vs then hd vs else the(l V)) #
upd_vals l Vs (tl vs)"
lemma [simp]: "!!vs. length(upd_vals l Vs vs) = length Vs"
by(induct Vs, auto)
*)
lemma overwrite_upd_lemma:
"(f(g(a\<mapsto>b) | A))(a := g a) = f(g|insert a A)"
(*<*)
apply(rule ext)
apply(simp add:overwrite_def)
done
declare fun_upd_apply[simp del] map_upds_twist[simp del]
(*>*)
lemma blocksReds:
"!!l. [| length Vs = length Ts; length vs = length Ts; distinct Vs;
P \<turnstile> ⟨e, (h,l(Vs [\<mapsto>] vs))⟩ ->* ⟨e', (h',l')⟩ |]
==> P \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ ->* ⟨blocks(Vs,Ts,map (the ˆ l') Vs,e'), (h',l'(l|set Vs))⟩"
(*<*)
proof(induct Vs Ts vs e rule:blocks.induct)
case (5 V Vs T Ts v vs e) show ?case
using InitBlockReds[OF "5.hyps"[of "l(V\<mapsto>v)"]] "5.prems"
by(auto simp:overwrite_upd_lemma)
qed auto
(*>*)
lemma blocksFinal:
"!!l. [| length Vs = length Ts; length vs = length Ts; final e |] ==>
P \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ ->* ⟨e, (h,l)⟩"
(*<*)
proof(induct Vs Ts vs e rule:blocks.induct)
case 5
show ?case using "5.prems" InitBlockReds[OF "5.hyps"]
by(fastsimp elim!:finalE elim: rtrancl_into_rtrancl[OF _ RedInitBlock]
rtrancl_into_rtrancl[OF _ InitBlockThrow])
qed auto
(*>*)
lemma blocksRedsFinal:
assumes wf: "length Vs = length Ts" "length vs = length Ts" "distinct Vs"
and reds: "P \<turnstile> ⟨e, (h,l(Vs [\<mapsto>] vs))⟩ ->* ⟨e', (h',l')⟩"
and fin: "final e'" and l'': "l'' = l'(l|set Vs)"
shows "P \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ ->* ⟨e', (h',l'')⟩"
(*<*)
proof -
let ?bv = "blocks(Vs,Ts,map (the o l') Vs,e')"
have "P \<turnstile> ⟨blocks(Vs,Ts,vs,e), (h,l)⟩ ->* ⟨?bv, (h',l'')⟩"
using l'' by simp (rule blocksReds[OF wf reds])
also have "P \<turnstile> ⟨?bv, (h',l'')⟩ ->* ⟨e', (h',l'')⟩"
using wf by(fastsimp intro:blocksFinal fin)
finally show ?thesis .
qed
(*>*)
text{* An now the actual method call reduction lemmas. *}
lemma CallRedsObj:
"P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> P \<turnstile> ⟨e\<bullet>M(es),s⟩ ->* ⟨e'\<bullet>M(es),s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CallObj)
done
(*>*)
lemma CallRedsParams:
"P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> P \<turnstile> ⟨(Val v)\<bullet>M(es),s⟩ ->* ⟨(Val v)\<bullet>M(es'),s'⟩"
(*<*)
apply(erule rtrancl_induct2)
apply blast
apply(erule rtrancl_into_rtrancl)
apply(erule CallParams)
done
(*>*)
lemma CallRedsFinal:
assumes wwf: "wwf_J_prog P"
and "P \<turnstile> ⟨e,s0⟩ ->* ⟨addr a,s1⟩"
"P \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
"h2 a = Some(C,fs)" "P \<turnstile> C sees M:Ts->T = (pns,body) in D"
"size vs = size pns"
and l2': "l2' = [this \<mapsto> Addr a, pns[\<mapsto>]vs]"
and body: "P \<turnstile> ⟨body,(h2,l2')⟩ ->* ⟨ef,(h3,l3)⟩"
and "final ef"
shows "P \<turnstile> ⟨e\<bullet>M(es), s0⟩ ->* ⟨ef,(h3,l2)⟩"
(*<*)
proof -
have wf: "size Ts = size pns ∧ distinct pns ∧ this ∉ set pns"
and wt: "fv body ⊆ {this} ∪ set pns"
using prems by(fastsimp dest!:sees_wf_mdecl simp:wf_mdecl_def)+
from body[THEN Red_lcl_add, of l2]
have body': "P \<turnstile> ⟨body,(h2,l2(this\<mapsto> Addr a, pns[\<mapsto>]vs))⟩ ->* ⟨ef,(h3,l2++l3)⟩"
by (simp add:l2')
have "dom l3 ⊆ {this} ∪ set pns"
using Reds_dom_lcl[OF wwf body] wt l2' set_take_subset by force
hence eql2: "(l2++l3)(l2|{this} ∪ set pns) = l2"
by(fastsimp simp add:map_add_def overwrite_def expand_fun_eq)
have "P \<turnstile> ⟨e\<bullet>M(es),s0⟩ ->* ⟨(addr a)\<bullet>M(es),s1⟩" by(rule CallRedsObj)
also have "P \<turnstile> ⟨(addr a)\<bullet>M(es),s1⟩ ->*
⟨(addr a)\<bullet>M(map Val vs),(h2,l2)⟩"
by(rule CallRedsParams)
also have "P \<turnstile> ⟨(addr a)\<bullet>M(map Val vs), (h2,l2)⟩ ->
⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2)⟩"
by(rule RedCall)(auto simp: prems wf)
also have "P \<turnstile> ⟨blocks(this#pns, Class D#Ts, Addr a#vs, body), (h2,l2)⟩
->* ⟨ef,(h3,(l2++l3)(l2|{this} ∪ set pns))⟩"
by(rule blocksRedsFinal, insert prems wf body', simp_all)
finally show ?thesis using eql2 by simp
qed
(*>*)
lemma CallRedsThrowParams:
"[| P \<turnstile> ⟨e,s0⟩ ->* ⟨Val v,s1⟩; P \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs1 @ throw a # es2,s2⟩ |]
==> P \<turnstile> ⟨e\<bullet>M(es),s0⟩ ->* ⟨throw a,s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
apply(erule CallRedsParams)
apply(rule CallThrowParams)
apply simp
done
(*>*)
lemma CallRedsThrowObj:
"P \<turnstile> ⟨e,s0⟩ ->* ⟨throw a,s1⟩ ==> P \<turnstile> ⟨e\<bullet>M(es),s0⟩ ->* ⟨throw a,s1⟩"
(*<*)
apply(rule rtrancl_into_rtrancl)
apply(erule CallRedsObj)
apply(rule CallThrowObj)
done
(*>*)
lemma CallRedsNull:
"[| P \<turnstile> ⟨e,s0⟩ ->* ⟨null,s1⟩; P \<turnstile> ⟨es,s1⟩ [->]* ⟨map Val vs,s2⟩ |]
==> P \<turnstile> ⟨e\<bullet>M(es),s0⟩ ->* ⟨THROW NullPointer,s2⟩"
(*<*)
apply(rule rtrancl_trans)
apply(erule CallRedsObj)
apply(rule rtrancl_into_rtrancl)
apply(erule CallRedsParams)
apply(rule RedCallNull)
done
(*>*)
subsubsection "The main Theorem"
lemma assumes wwf: "wwf_J_prog P"
shows big_by_small: "P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩ ==> P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
and bigs_by_smalls: "P \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩ ==> P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩"
(*<*)
proof (induct rule: eval_evals.induct)
case New thus ?case by (auto simp:RedNew)
next
case NewFail thus ?case by (auto simp:RedNewFail)
next
case Cast thus ?case by(fastsimp intro:CastRedsAddr)
next
case CastNull thus ?case by(simp add:CastRedsNull)
next
case CastFail thus ?case by(fastsimp intro!:CastRedsFail)
next
case CastThrow thus ?case by(auto dest!:eval_final simp:CastRedsThrow)
next
case Val thus ?case by simp
next
case BinOp thus ?case by(auto simp:BinOpRedsVal)
next
case BinOpThrow1 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow1)
next
case BinOpThrow2 thus ?case by(auto dest!:eval_final simp: BinOpRedsThrow2)
next
case Var thus ?case by (auto simp:RedVar)
next
case LAss thus ?case by(auto simp: LAssRedsVal)
next
case LAssThrow thus ?case by(auto dest!:eval_final simp: LAssRedsThrow)
next
case FAcc thus ?case by(auto intro:FAccRedsVal)
next
case FAccNull thus ?case by(simp add:FAccRedsNull)
next
case FAccThrow thus ?case by(auto dest!:eval_final simp:FAccRedsThrow)
next
case FAss thus ?case by(auto simp:FAssRedsVal)
next
case FAssNull thus ?case by(auto simp:FAssRedsNull)
next
case FAssThrow1 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow1)
next
case FAssThrow2 thus ?case by(auto dest!:eval_final simp:FAssRedsThrow2)
next
case CallObjThrow thus ?case by(auto dest!:eval_final simp:CallRedsThrowObj)
next
case CallNull thus ?case by(simp add:CallRedsNull)
next
case CallParamsThrow thus ?case
by(auto dest!:evals_final simp:CallRedsThrowParams)
next
case (Call C D M T Ts a body e e' fs h2 h3 l2 l2' l3 pns ps s0 s1 vs)
have IHe: "P \<turnstile> ⟨e,s0⟩ ->* ⟨addr a,s1⟩"
and IHes: "P \<turnstile> ⟨ps,s1⟩ [->]* ⟨map Val vs,(h2,l2)⟩"
and h2a: "h2 a = Some(C,fs)"
and method: "P \<turnstile> C sees M:Ts->T = (pns,body) in D"
and same_length: "length vs = length pns"
and l2': "l2' = [this \<mapsto> Addr a, pns[\<mapsto>]vs]"
and eval_body: "P \<turnstile> ⟨body,(h2, l2')⟩ => ⟨e',(h3, l3)⟩"
and IHbody: "P \<turnstile> ⟨body,(h2,l2')⟩ ->* ⟨e',(h3,l3)⟩".
show "P \<turnstile> ⟨e\<bullet>M(ps),s0⟩ ->* ⟨e',(h3, l2)⟩"
using method same_length l2' h2a IHbody eval_final[OF eval_body]
by(fastsimp intro:CallRedsFinal[OF wwf IHe IHes])
next
case Block thus ?case by(auto simp: BlockRedsFinal dest:eval_final)
next
case Seq thus ?case by(auto simp:SeqReds2)
next
case SeqThrow thus ?case by(auto dest!:eval_final simp: SeqRedsThrow)
next
case CondT thus ?case by(auto simp:CondReds2T)
next
case CondF thus ?case by(auto simp:CondReds2F)
next
case CondThrow thus ?case by(auto dest!:eval_final simp:CondRedsThrow)
next
case WhileF thus ?case by(auto simp:WhileFReds)
next
case WhileT thus ?case by(auto simp: WhileTReds)
next
case WhileCondThrow thus ?case by(auto dest!:eval_final simp: WhileRedsThrow)
next
case WhileBodyThrow thus ?case by(auto dest!:eval_final simp: WhileTRedsThrow)
next
case Throw thus ?case by(auto simp:ThrowReds)
next
case ThrowNull thus ?case by(auto simp:ThrowRedsNull)
next
case ThrowThrow thus ?case by(auto dest!:eval_final simp:ThrowRedsThrow)
next
case Try thus ?case by(simp add:TryRedsVal)
next
case TryCatch thus ?case by(fast intro!: TryCatchRedsFinal dest!:eval_final)
next
case TryThrow thus ?case by(fastsimp intro!:TryRedsFail)
next
case Nil thus ?case by simp
next
case Cons thus ?case
by(fastsimp intro!:Cons_eq_appendI[OF refl refl] ListRedsVal)
next
case ConsThrow thus ?case by(fastsimp elim: ListReds1)
qed
(*>*)
subsection{*Big steps simulates small step*}
text{* This direction was carried out by Norbert Schirmer and Daniel
Wasserrab. *}
text {* The big step equivalent of @{text RedWhile}: *}
lemma unfold_while:
"P \<turnstile> ⟨while(b) c,s⟩ => ⟨e',s'⟩ = P \<turnstile> ⟨if(b) (c;;while(b) c) else (unit),s⟩ => ⟨e',s'⟩"
(*<*)
proof
assume "P \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
thus "P \<turnstile> ⟨if (b) (c;; while (b) c) else unit,s⟩ => ⟨e',s'⟩"
by cases (fastsimp intro: eval_evals.intros)+
next
assume "P \<turnstile> ⟨if (b) (c;; while (b) c) else unit,s⟩ => ⟨e',s'⟩"
thus "P \<turnstile> ⟨while (b) c,s⟩ => ⟨e',s'⟩"
proof (cases)
fix a
assume e': "e' = throw a"
assume "P \<turnstile> ⟨b,s⟩ => ⟨throw a,s'⟩"
hence "P \<turnstile> ⟨while(b) c,s⟩ => ⟨throw a,s'⟩" by (rule WhileCondThrow)
with e' show ?thesis by simp
next
fix s1
assume eval_false: "P \<turnstile> ⟨b,s⟩ => ⟨false,s1⟩"
and eval_unit: "P \<turnstile> ⟨unit,s1⟩ => ⟨e',s'⟩"
with eval_unit have "s' = s1" "e' = unit" by (auto elim: eval_cases)
moreover from eval_false have "P \<turnstile> ⟨while (b) c,s⟩ => ⟨unit,s1⟩"
by - (rule WhileF, simp)
ultimately show ?thesis by simp
next
fix s1
assume eval_true: "P \<turnstile> ⟨b,s⟩ => ⟨true,s1⟩"
and eval_rest: "P \<turnstile> ⟨c;; while (b) c,s1⟩=>⟨e',s'⟩"
from eval_rest show ?thesis
proof (cases)
fix s2 v1
assume "P \<turnstile> ⟨c,s1⟩ => ⟨Val v1,s2⟩" "P \<turnstile> ⟨while (b) c,s2⟩ => ⟨e',s'⟩"
with eval_true show "P \<turnstile> ⟨while(b) c,s⟩ => ⟨e',s'⟩" by (rule WhileT)
next
fix a
assume "P \<turnstile> ⟨c,s1⟩ => ⟨throw a,s'⟩" "e' = throw a"
with eval_true show "P \<turnstile> ⟨while(b) c,s⟩ => ⟨e',s'⟩"
by (rules intro: WhileBodyThrow)
qed
qed
qed
(*>*)
lemma blocksEval:
"!!Ts vs l l'. [|size ps = size Ts; size ps = size vs; P \<turnstile> ⟨blocks(ps,Ts,vs,e),(h,l)⟩ => ⟨e',(h',l')⟩ |]
==> ∃ l''. P \<turnstile> ⟨e,(h,l(ps[\<mapsto>]vs))⟩ => ⟨e',(h',l'')⟩"
(*<*)
proof (induct ps)
case Nil then show ?case by fastsimp
next
case (Cons p ps')
have length_eqs: "length (p # ps') = length Ts"
"length (p # ps') = length vs" .
then obtain T Ts' where Ts: "Ts = T#Ts'" by (cases "Ts") simp
obtain v vs' where vs: "vs = v#vs'" using length_eqs by (cases "vs") simp
have "P \<turnstile> ⟨blocks (p # ps', Ts, vs, e),(h,l)⟩ => ⟨e',(h', l')⟩".
with Ts vs
have "P \<turnstile> ⟨{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l)⟩ => ⟨e',(h', l')⟩"
by simp
then obtain l''' where
eval_ps': "P \<turnstile> ⟨blocks (ps', Ts', vs', e),(h, l(p\<mapsto>v))⟩ => ⟨e',(h', l''')⟩"
and l''': "l'=l'''(p:=l p)"
by (auto elim!: eval_cases)
then obtain l'' where
hyp: "P \<turnstile> ⟨e,(h, l(p\<mapsto>v)(ps'[\<mapsto>]vs'))⟩ => ⟨e',(h', l'')⟩"
using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto
from hyp
show "∃l''. P \<turnstile> ⟨e,(h, l(p # ps'[\<mapsto>]vs))⟩ => ⟨e',(h', l'')⟩"
using Ts vs by auto
qed
(*>*)
(* FIXME exercise: show precise relationship between l' and l'':
lemma blocksEval:
"!! Ts vs l l'. [|length ps = length Ts; length ps = length vs;
P\<turnstile> ⟨blocks(ps,Ts,vs,e),(h,l)⟩ => ⟨e',(h',l')⟩ |]
==> ∃ l''. P \<turnstile> ⟨e,(h,l(ps[\<mapsto>]vs))⟩ => ⟨e',(h',l'')⟩ ∧ l'=l''(l|set ps)"
proof (induct ps)
case Nil then show ?case by simp
next
case (Cons p ps')
have length_eqs: "length (p # ps') = length Ts"
"length (p # ps') = length vs" .
then obtain T Ts' where Ts: "Ts=T#Ts'" by (cases "Ts") simp
obtain v vs' where vs: "vs=v#vs'" using length_eqs by (cases "vs") simp
have "P \<turnstile> ⟨blocks (p # ps', Ts, vs, e),(h,l)⟩ => ⟨e',(h', l')⟩".
with Ts vs
have "P \<turnstile> ⟨{p:T := Val v; blocks (ps', Ts', vs', e)},(h,l)⟩ => ⟨e',(h', l')⟩"
by simp
then obtain l''' where
eval_ps': "P \<turnstile> ⟨blocks (ps', Ts', vs', e),(h, l(p\<mapsto>v))⟩ => ⟨e',(h', l''')⟩"
and l''': "l'=l'''(p:=l p)"
by (cases) (auto elim: eval_cases)
then obtain l'' where
hyp: "P \<turnstile> ⟨e,(h, l(p\<mapsto>v)(ps'[\<mapsto>]vs'))⟩ => ⟨e',(h', l'')⟩" and
l'': "l''' = l''(l(p\<mapsto>v)|set ps')"
using length_eqs Ts vs Cons.hyps [OF _ _ eval_ps'] by auto
have "l' = l''(l|set (p # ps'))"
proof -
have "(l''(l(p\<mapsto>v)|set ps'))(p := l p) = l''(l|insert p (set ps'))"
by (induct ps') (auto intro: ext simp add: fun_upd_def overwrite_def)
with l''' l'' show ?thesis by simp
qed
with hyp
show "∃l''. P \<turnstile> ⟨e,(h, l(p # ps'[\<mapsto>]vs))⟩ => ⟨e',(h', l'')⟩ ∧
l' = l''(l|set (p # ps'))"
using Ts vs by auto
qed
*)
lemma
assumes wf: "wwf_J_prog P"
shows eval_restrict_lcl:
"P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> (!!W. fv e ⊆ W ==> P \<turnstile> ⟨e,(h,l⌊W)⟩ => ⟨e',(h',l'⌊W)⟩)"
and "P \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> (!!W. fvs es ⊆ W ==> P \<turnstile> ⟨es,(h,l⌊W)⟩ [=>] ⟨es',(h',l'⌊W)⟩)"
(*<*)
proof(induct rule:eval_evals_induct)
case (Block T V e0 e1 h0 h1 l0 l1)
have IH: "!!W. fv e0 ⊆ W ==> P \<turnstile> ⟨e0,(h0,l0(V:=None)⌊W)⟩ => ⟨e1,(h1,l1⌊W)⟩".
have "fv({V:T; e0}) ⊆ W".
hence "fv e0 - {V} ⊆ W" by (simp_all add:Un_subset_iff)
hence "fv e0 ⊆ insert V W" by fast
from IH[OF this]
have "P \<turnstile> ⟨e0,(h0, (l0⌊W)(V := None))⟩ => ⟨e1,(h1, l1⌊insert V W)⟩"
by fastsimp
from eval_evals.Block[OF this] show ?case by fastsimp
next
case Seq thus ?case by simp (blast intro:eval_evals.Seq)
next
case New thus ?case by(simp add:eval_evals.intros)
next
case NewFail thus ?case by(simp add:eval_evals.intros)
next
case Cast thus ?case by simp (blast intro:eval_evals.Cast)
next
case CastNull thus ?case by simp (blast intro:eval_evals.CastNull)
next
case CastFail thus ?case by simp (blast intro:eval_evals.CastFail)
next
case CastThrow thus ?case by(simp add:eval_evals.intros)
next
case Val thus ?case by(simp add:eval_evals.intros)
next
case BinOp thus ?case by simp (blast intro:eval_evals.BinOp)
next
case BinOpThrow1 thus ?case by simp (blast intro:eval_evals.BinOpThrow1)
next
case BinOpThrow2 thus ?case by simp (blast intro:eval_evals.BinOpThrow2)
next
case Var thus ?case by(simp add:eval_evals.intros)
next
case (LAss V e h l l' h0 l0 v)
have IH: "!!W. fv e ⊆ W ==> P \<turnstile> ⟨e,(h0,l0⌊W)⟩ => ⟨Val v,(h,l⌊W)⟩"
and [simp]: "l' = l(V \<mapsto> v)".
have "fv (V:=e) ⊆ W".
hence fv: "fv e ⊆ W" and VinW: "V ∈ W" by auto
from eval_evals.LAss[OF IH[OF fv] refl, of V] VinW
show ?case by simp
next
case LAssThrow thus ?case by(fastsimp intro: eval_evals.LAssThrow)
next
case FAcc thus ?case by simp (blast intro: eval_evals.FAcc)
next
case FAccNull thus ?case by(fastsimp intro: eval_evals.FAccNull)
next
case FAccThrow thus ?case by(fastsimp intro: eval_evals.FAccThrow)
next
case FAss thus ?case by simp (blast intro: eval_evals.FAss)
next
case FAssNull thus ?case by simp (blast intro: eval_evals.FAssNull)
next
case FAssThrow1 thus ?case by simp (blast intro: eval_evals.FAssThrow1)
next
case FAssThrow2 thus ?case by simp (blast intro: eval_evals.FAssThrow2)
next
case CallObjThrow thus ?case by simp (blast intro: eval_evals.intros)
next
case CallNull thus ?case by simp (blast intro: eval_evals.CallNull)
next
case CallParamsThrow thus ?case
by simp (blast intro: eval_evals.CallParamsThrow)
next
case (Call C D M T Ts a body e e' fs h2 h3 l2 l2' l3 pns
ps h0 l0 h1 l1 vs)
have IHe: "!!W. fv e ⊆ W ==> P \<turnstile> ⟨e,(h0,l0⌊W)⟩ => ⟨addr a,(h1,l1⌊W)⟩"
and IHps: "!!W. fvs ps ⊆ W ==> P \<turnstile> ⟨ps,(h1,l1⌊W)⟩ [=>] ⟨map Val vs,(h2,l2⌊W)⟩"
and IHbd: "!!W. fv body ⊆ W ==> P \<turnstile> ⟨body,(h2,l2'⌊W)⟩ => ⟨e',(h3,l3⌊W)⟩"
and h2a: "h2 a = Some (C, fs)"
and method: "P \<turnstile> C sees M: Ts->T = (pns, body) in D"
and same_len: "size vs = size pns"
and l2': "l2' = [this \<mapsto> Addr a, pns [\<mapsto>] vs]".
have "fv (e\<bullet>M(ps)) ⊆ W".
hence fve: "fv e ⊆ W" and fvps: "fvs(ps) ⊆ W" by auto
have wfmethod: "size Ts = size pns ∧ this ∉ set pns" and
fvbd: "fv body ⊆ {this} ∪ set pns"
using method wf by(fastsimp dest!:sees_wf_mdecl simp:wf_mdecl_def)+
show ?case
using IHbd[OF fvbd] l2' same_len wfmethod h2a
eval_evals.Call[OF IHe[OF fve] IHps[OF fvps] _ method same_len l2']
by (simp add:subset_insertI)
next
case SeqThrow thus ?case by simp (blast intro: eval_evals.SeqThrow)
next
case CondT thus ?case by simp (blast intro: eval_evals.CondT)
next
case CondF thus ?case by simp (blast intro: eval_evals.CondF)
next
case CondThrow thus ?case by simp (blast intro: eval_evals.CondThrow)
next
case WhileF thus ?case by simp (blast intro: eval_evals.WhileF)
next
case WhileT thus ?case by simp (blast intro: eval_evals.WhileT)
next
case WhileCondThrow thus ?case by simp (blast intro: eval_evals.WhileCondThrow)
next
case WhileBodyThrow thus ?case by simp (blast intro: eval_evals.WhileBodyThrow)
next
case Throw thus ?case by simp (blast intro: eval_evals.Throw)
next
case ThrowNull thus ?case by simp (blast intro: eval_evals.ThrowNull)
next
case ThrowThrow thus ?case by simp (blast intro: eval_evals.ThrowThrow)
next
case Try thus ?case by simp (blast intro: eval_evals.Try)
next
case (TryCatch C D V a e1 e2 e2' fs h1 h2 l1 l2 h0 l0)
have IH1: "!!W. fv e1 ⊆ W ==> P \<turnstile> ⟨e1,(h0,l0⌊W)⟩ => ⟨Throw a,(h1,l1⌊W)⟩"
and IH2: "!!W. fv e2 ⊆ W ==> P \<turnstile> ⟨e2,(h1,l1(V\<mapsto>Addr a)⌊W)⟩ => ⟨e2',(h2,l2⌊W)⟩"
and lookup: "h1 a = Some(D, fs)" and subtype: "P \<turnstile> D \<preceq>* C".
have "fv (try e1 catch(C V) e2) ⊆ W".
hence fv1: "fv e1 ⊆ W" and fv2: "fv e2 ⊆ insert V W" by auto
have IH2': "P \<turnstile> ⟨e2,(h1,(l1⌊W)(V \<mapsto> Addr a))⟩ => ⟨e2',(h2,l2⌊insert V W)⟩"
using IH2[OF fv2] fun_upd_restrict[of l1 W] (*FIXME just l|W instead of l|(W-V) in simp rule??*) by simp
with eval_evals.TryCatch[OF IH1[OF fv1] _ subtype IH2'] lookup
show ?case by fastsimp
next
case TryThrow thus ?case by simp (blast intro: eval_evals.TryThrow)
next
case Nil thus ?case by (simp add: eval_evals.Nil)
next
case Cons thus ?case by simp (blast intro: eval_evals.Cons)
next
case ConsThrow thus ?case by simp (blast intro: eval_evals.ConsThrow)
qed
(*>*)
lemma eval_notfree_unchanged:
"P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> (!!V. V ∉ fv e ==> l' V = l V)"
and "P \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> (!!V. V ∉ fvs es ==> l' V = l V)"
(*<*)
proof(induct rule:eval_evals_induct)
case LAss thus ?case by(simp add:fun_upd_apply)
next
case Block thus ?case
by (simp only:fun_upd_apply split:if_splits) fastsimp
next
case TryCatch thus ?case
by (simp only:fun_upd_apply split:if_splits) fastsimp
qed simp_all
(*>*)
lemma eval_closed_lcl_unchanged:
"[| P \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩; fv e = {} |] ==> l' = l"
(*<*)by(fastsimp dest:eval_notfree_unchanged simp add:expand_fun_eq)(*>*)
lemma list_eval_Throw:
assumes eval_e: "P \<turnstile> ⟨throw x,s⟩ => ⟨e',s'⟩"
shows "P \<turnstile> ⟨map Val vs @ throw x # es',s⟩ [=>] ⟨map Val vs @ e' # es',s'⟩"
(*<*)
proof -
from eval_e
obtain a where e': "e' = Throw a"
by (cases) (auto dest!: eval_final)
{
fix es
have "!!vs. es = map Val vs @ throw x # es'
==> P \<turnstile> ⟨es,s⟩[=>]⟨map Val vs @ e' # es',s'⟩"
proof (induct es type: list)
case Nil thus ?case by simp
next
case (Cons e es vs)
have e_es: "e # es = map Val vs @ throw x # es'".
show "P \<turnstile> ⟨e # es,s⟩ [=>] ⟨map Val vs @ e' # es',s'⟩"
proof (cases vs)
case Nil
with e_es obtain "e=throw x" "es=es'" by simp
moreover from eval_e e'
have "P \<turnstile> ⟨throw x # es,s⟩ [=>] ⟨Throw a # es,s'⟩"
by (rules intro: ConsThrow)
ultimately show ?thesis using Nil e' by simp
next
case (Cons v vs')
have vs: "vs = v # vs'".
with e_es obtain
e: "e=Val v" and es:"es= map Val vs' @ throw x # es'"
by simp
from e
have "P \<turnstile> ⟨e,s⟩ => ⟨Val v,s⟩"
by (rules intro: eval_evals.Val)
moreover from es
have "P \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs' @ e' # es',s'⟩"
by (rule Cons.hyps)
ultimately show
"P \<turnstile> ⟨e#es,s⟩ [=>] ⟨map Val vs @ e' # es',s'⟩"
using vs by (auto intro: eval_evals.Cons)
qed
qed
}
thus ?thesis
by simp
qed
(*>*)
(* Hiermit kann man die ganze pair-Splitterei in den automatischen Taktiken
abschalten. Wieder anschalten siehe nach dem Beweis. *)
(*<*)
declare split_paired_All [simp del] split_paired_Ex [simp del]
ML_setup {*
simpset_ref() := simpset() delloop "split_all_tac";
claset_ref () := claset () delSWrapper "split_all_tac"
*}
(*>*)
(* FIXME
exercise 1: define a big step semantics where the body of a procedure can
access not juts this and pns but all of the enclosing l. What exactly is fed
in? What exactly is returned at the end? Notion: "dynamic binding"
excercise 2: the semantics of exercise 1 is closer to the small step
semantics. Reformulate equivalence proof by modifying call lemmas.
*)
text {* The key lemma: *}
lemma
assumes wf: "wwf_J_prog P"
shows extend_1_eval:
"P \<turnstile> ⟨e,s⟩ -> ⟨e'',s''⟩ ==> (!!s' e'. P \<turnstile> ⟨e'',s''⟩ => ⟨e',s'⟩ ==> P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩)"
and extend_1_evals:
"P \<turnstile> ⟨es,t⟩ [->] ⟨es'',t''⟩ ==> (!!t' es'. P \<turnstile> ⟨es'',t''⟩ [=>] ⟨es',t'⟩ ==> P \<turnstile> ⟨es,t⟩ [=>] ⟨es',t'⟩)"
(*<*)
proof (induct rule: red_reds.induct)
case (RedCall C D M T Ts a body fs pns s vs s' e')
have "P \<turnstile> ⟨addr a,s⟩ => ⟨addr a,s⟩" by (rule eval_evals.intros)
moreover
have finals: "finals(map Val vs)" by simp
obtain h2 l2 where s: "s = (h2,l2)" by (cases s) simp
with finals have "P \<turnstile> ⟨map Val vs,s⟩ [=>] ⟨map Val vs,(h2,l2)⟩"
by (rules intro: eval_finalsId)
moreover from s have "h2 a = Some (C, fs)" using RedCall by simp
moreover have method: "P \<turnstile> C sees M: Ts->T = (pns, body) in D".
moreover have same_len1: "length Ts = length pns"
and this_distinct: "this ∉ set pns" and fv: "fv body ⊆ {this} ∪ set pns"
using method wf by (fastsimp dest!:sees_wf_mdecl simp:wf_mdecl_def)+
have same_len: "length vs = length pns".
moreover
obtain l2' where l2': "l2' = [this\<mapsto>Addr a,pns[\<mapsto>]vs]" by simp
moreover
obtain h3 l3 where s': "s' = (h3,l3)" by (cases s') simp
have eval_blocks:
"P \<turnstile> ⟨blocks (this # pns, Class D # Ts, Addr a # vs, body),s⟩ => ⟨e',s'⟩".
hence id: "l3 = l2" using fv s s' same_len1 same_len
by(fastsimp elim: eval_closed_lcl_unchanged)
from eval_blocks obtain l3' where "P \<turnstile> ⟨body,(h2,l2')⟩ => ⟨e',(h3,l3')⟩"
proof -
from same_len1 have "length(this#pns) = length(Class D#Ts)" by simp
moreover from same_len1 same_len
have "length (this#pns) = length (Addr a#vs)" by simp
moreover from eval_blocks
have "P \<turnstile> ⟨blocks (this#pns,Class D#Ts,Addr a#vs,body),(h2,l2)⟩
=>⟨e',(h3,l3)⟩" using s s' by simp
ultimately obtain l''
where "P \<turnstile> ⟨body,(h2,l2(this # pns[\<mapsto>]Addr a # vs))⟩=>⟨e',(h3, l'')⟩"
by (blast dest:blocksEval)
from eval_restrict_lcl[OF wf this fv] this_distinct same_len1 same_len
have "P \<turnstile> ⟨body,(h2,[this # pns[\<mapsto>]Addr a # vs])⟩ =>
⟨e',(h3, l''⌊(set(this#pns)))⟩"
by(simp add:subset_insert_iff insert_Diff_if)
thus ?thesis by(fastsimp intro!:that simp add: l2')
qed
ultimately
have "P \<turnstile> ⟨(addr a)\<bullet>M(map Val vs),s⟩ => ⟨e',(h3,l2)⟩" by (rule Call)
with s' id show ?case by simp
next
case RedNew
thus ?case
by (rules elim: eval_cases intro: eval_evals.intros)
next
case RedNewFail
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case (CastRed C e e'' s s'' s' e')
thus ?case
by -(erule eval_cases,auto intro: eval_evals.intros)
next
case RedCastNull
thus ?case
by (rules elim: eval_cases intro: eval_evals.intros)
next
case (RedCast C D a fs s s'' e'')
thus ?case
by (cases s) (auto elim: eval_cases intro: eval_evals.intros)
next
case (RedCastFail C D a fs s s'' e'')
thus ?case
by (cases s) (auto elim!: eval_cases intro: eval_evals.intros)
next
case BinOpRed1
thus ?case
by -(erule eval_cases,auto intro: eval_evals.intros)
next
case (BinOpRed2 bop e2 e2' s s'' v1 s' e')
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
case RedBinOp
thus ?case
by (rules elim: eval_cases intro: eval_evals.intros)
next
case (RedVar V s v s' e')
thus ?case
by (cases s)(fastsimp elim: eval_cases intro: eval_evals.intros)
next
case LAssRed
thus ?case
by -(erule eval_cases,auto intro: eval_evals.intros)
next
case (RedLAss V h l v s' e')
thus ?case
by (cases s)(fastsimp elim: eval_cases intro: eval_evals.intros)
next
case FAccRed
thus ?case
by -(erule eval_cases,auto intro: eval_evals.intros)
next
case (RedFAcc C D F a fs s v s' e')
thus ?case
by (cases s)(fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedFAccNull
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros)
next
case (FAssRed1 D F e1 e1' e2 s s'' s' e')
thus ?case
by (cases s)(erule eval_cases, auto intro: eval_evals.intros)
next
case (FAssRed2 D F a e2 e2' s s'' s' e')
thus ?case
by (cases s)
(fastsimp elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
case (RedFAss C D F a fm h l v s' e')
thus ?case
by (cases s)(fastsimp elim!: eval_cases intro: eval_evals.intros)
next
case RedFAssNull
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros)
next
case CallObj
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros)
next
case CallParams
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros eval_finalId)
next
case RedCallNull
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros eval_finalsId)
next
case InitBlockRed
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros eval_finalId
simp add: map_upd_triv fun_upd_same)
next
case (RedInitBlock T V s u v s' e')
have "P \<turnstile> ⟨Val u,s⟩ => ⟨e',s'⟩".
then obtain s': "s'=s" and e': "e'=Val u" by cases simp
obtain h l where s: "s=(h,l)" by (cases s) simp
have "P \<turnstile> ⟨{V:T :=Val v; Val u},(h,l)⟩ => ⟨Val u,(h, (l(V\<mapsto>v))(V:=l V))⟩"
by (fastsimp intro!: eval_evals.intros)
thus "P \<turnstile> ⟨{V:T := Val v; Val u},s⟩ => ⟨e',s'⟩"
using s s' e' by simp
next
case BlockRedNone
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros
simp add: fun_upd_same fun_upd_idem)
next
case BlockRedSome
thus ?case
by (fastsimp elim!: eval_cases intro: eval_evals.intros
simp add: fun_upd_same fun_upd_idem)
next
case (RedBlock T V s v s' e')
have "P \<turnstile> ⟨Val v,s⟩ => ⟨e',s'⟩".
then obtain s': "s'=s" and e': "e'=Val v"
by cases simp
obtain h l where s: "s=(h,l)" by (cases s) simp
have "P \<turnstile> ⟨Val v,(h,l(V:=None))⟩ => ⟨Val v,(h,l(V:=None))⟩"
by (rule eval_evals.intros)
hence "P \<turnstile> ⟨{V:T;Val v},(h,l)⟩ => ⟨Val v,(h,(l(V:=None))(V:=l V))⟩"
by (rule eval_evals.Block)
thus "P \<turnstile> ⟨{V:T; Val v},s⟩ => ⟨e',s'⟩"
using s s' e'
by simp
next
case SeqRed
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedSeq
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case CondRed
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedCondT
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedCondF
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedWhile
thus ?case
by (auto simp add: unfold_while intro:eval_evals.intros elim:eval_cases)
next
case ThrowRed
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedThrowNull
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case TryRed
thus ?case
by (auto elim!: eval_cases intro: eval_evals.intros)
next
case RedTry
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case RedTryCatch
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case (RedTryFail C D V a e2 fs s s' e')
thus ?case
by (cases s)(auto elim!: eval_cases intro: eval_evals.intros)
next
case ListRed1
thus ?case
by (fastsimp elim: evals_cases intro: eval_evals.intros)
next
case ListRed2
thus ?case
by (fastsimp elim!: evals_cases eval_cases
intro: eval_evals.intros eval_finalId)
next
case CastThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case BinOpThrow1
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case BinOpThrow2
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case LAssThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case FAccThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case FAssThrow1
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case FAssThrow2
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case (CallThrowObj M a es s s' e')
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case (CallThrowParams M e es es' s v vs s' e')
have "P \<turnstile> ⟨Val v,s⟩ => ⟨Val v,s⟩" by (rule eval_evals.intros)
moreover
have es: "es = map Val vs @ throw e # es'" .
have eval_e: "P \<turnstile> ⟨throw e,s⟩ => ⟨e',s'⟩".
then obtain xa where e': "e' = Throw xa" by (cases) (auto dest!: eval_final)
with list_eval_Throw [OF eval_e] es
have "P \<turnstile> ⟨es,s⟩ [=>] ⟨map Val vs @ Throw xa # es',s'⟩" by simp
ultimately have "P \<turnstile> ⟨Val v\<bullet>M(es),s⟩ => ⟨Throw xa,s'⟩"
by (rule eval_evals.CallParamsThrow)
thus ?case using e' by simp
next
case (InitBlockThrow T V a s v s' e')
have "P \<turnstile> ⟨Throw a,s⟩ => ⟨e',s'⟩".
then obtain s': "s' = s" and e': "e' = Throw a"
by cases (auto elim!:eval_cases)
obtain h l where s: "s = (h,l)" by (cases s) simp
have "P \<turnstile> ⟨{V:T :=Val v; Throw a},(h,l)⟩ => ⟨Throw a, (h, (l(V\<mapsto>v))(V:=l V))⟩"
by(fastsimp intro:eval_evals.intros)
thus "P \<turnstile> ⟨{V:T := Val v; Throw a},s⟩ => ⟨e',s'⟩" using s s' e' by simp
next
case (BlockThrow T V a s s' e')
have "P \<turnstile> ⟨Throw a, s⟩ => ⟨e',s'⟩".
then obtain s': "s' = s" and e': "e' = Throw a"
by cases (auto elim!:eval_cases)
obtain h l where s: "s=(h,l)" by (cases s) simp
have "P \<turnstile> ⟨Throw a, (h,l(V:=None))⟩ => ⟨Throw a, (h,l(V:=None))⟩"
by (simp add:eval_evals.intros eval_finalId)
hence "P\<turnstile>⟨{V:T;Throw a},(h,l)⟩=>⟨Throw a, (h,(l(V:=None))(V:=l V))⟩"
by (rule eval_evals.Block)
thus "P \<turnstile> ⟨{V:T; Throw a},s⟩ => ⟨e',s'⟩" using s s' e' by simp
next
case SeqThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case CondThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
next
case ThrowThrow
thus ?case
by (fastsimp elim: eval_cases intro: eval_evals.intros)
qed
(*>*)
(*<*)
(* ... und wieder anschalten: *)
declare split_paired_All [simp] split_paired_Ex [simp]
ML_setup {*
claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac);
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
*}
(*>*)
text {* Its extension to @{text"->*"}: *}
lemma extend_eval:
assumes wf: "wwf_J_prog P"
and reds: "P \<turnstile> ⟨e,s⟩ ->* ⟨e'',s''⟩" and eval_rest: "P \<turnstile> ⟨e'',s''⟩ => ⟨e',s'⟩"
shows "P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩"
(*<*)
using reds eval_rest
apply (induct rule: converse_rtrancl_induct)
apply simp
apply (case_tac y)
apply (case_tac z)
apply simp
by (rule extend_1_eval)
(*>*)
lemma extend_evals:
assumes wf: "wwf_J_prog P"
and reds: "P \<turnstile> ⟨es,s⟩ [->]* ⟨es'',s''⟩" and eval_rest: "P \<turnstile> ⟨es'',s''⟩ [=>] ⟨es',s'⟩"
shows "P \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩"
(*<*)
using reds eval_rest
apply (induct rule: converse_rtrancl_induct)
apply simp
apply (case_tac y)
apply (case_tac z)
apply simp
by (rule extend_1_evals)
(*>*)
text {* Finally, small step semantics can be simulated by big step semantics:
*}
theorem
assumes wf: "wwf_J_prog P"
shows small_by_big: "[|P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩; final e'|] ==> P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩"
and "[|P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩; finals es'|] ==> P \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩"
(*<*)
proof -
note wf
moreover assume "P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
moreover assume "final e'"
then have "P \<turnstile> ⟨e',s'⟩ => ⟨e',s'⟩"
by (rule eval_finalId)
ultimately show "P \<turnstile> ⟨e,s⟩=>⟨e',s'⟩"
by (rule extend_eval)
next
note wf
moreover assume "P \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩"
moreover assume "finals es'"
then have "P \<turnstile> ⟨es',s'⟩ [=>] ⟨es',s'⟩"
by (rule eval_finalsId)
ultimately show "P \<turnstile> ⟨es,s⟩ [=>] ⟨es',s'⟩"
by (rule extend_evals)
qed
(*>*)
subsection "Equivalence"
text{* And now, the crowning achievement: *}
corollary big_iff_small:
"wwf_J_prog P ==>
P \<turnstile> ⟨e,s⟩ => ⟨e',s'⟩ = (P \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ∧ final e')"
(*<*)by(blast dest: big_by_small eval_final small_by_big)(*>*)
end
lemma CastReds:
Step P e s e' s' ==> Step P (Cast C e) s (Cast C e') s'
lemma CastRedsNull:
Step P e s null s' ==> Step P (Cast C e) s null s'
lemma CastRedsAddr:
[| Step P e s (addr a) s'; hp s' a = ⌊(D, fs)⌋; subcls P D C |] ==> Step P (Cast C e) s (addr a) s'
lemma CastRedsFail:
[| Step P e s (addr a) s'; hp s' a = ⌊(D, fs)⌋; ¬ subcls P D C |] ==> Step P (Cast C e) s (THROW ClassCast) s'
lemma CastRedsThrow:
Step P e s (throw a) s' ==> Step P (Cast C e) s (throw a) s'
lemma LAssReds:
Step P e s e' s' ==> Step P (V:=e) s (V:=e') s'
lemma LAssRedsVal:
Step P e s (Val v) (h', l') ==> Step P (V:=e) s unit (h', l'(V |-> v))
lemma LAssRedsThrow:
Step P e s (throw a) s' ==> Step P (V:=e) s (throw a) s'
lemma BinOp1Reds:
Step P e s e' s' ==> Step P (e «bop» e2) s (e' «bop» e2) s'
lemma BinOp2Reds:
Step P e s e' s' ==> Step P (Val v «bop» e) s (Val v «bop» e') s'
lemma BinOpRedsVal:
[| Step P e1 s0 (Val v1) s1; Step P e2 s1 (Val v2) s2; binop (bop, v1, v2) = ⌊v⌋ |] ==> Step P (e1 «bop» e2) s0 (Val v) s2
lemma BinOpRedsThrow1:
Step P e s (throw e') s' ==> Step P (e «bop» e2) s (throw e') s'
lemma BinOpRedsThrow2:
[| Step P e1 s0 (Val v1) s1; Step P e2 s1 (throw e) s2 |] ==> Step P (e1 «bop» e2) s0 (throw e) s2
lemma FAccReds:
Step P e s e' s' ==> Step P (e\<bullet>F{D}) s (e'\<bullet>F{D}) s'
lemma FAccRedsVal:
[| Step P e s (addr a) s'; hp s' a = ⌊(C, fs)⌋; fs (F, D) = ⌊v⌋ |] ==> Step P (e\<bullet>F{D}) s (Val v) s'
lemma FAccRedsNull:
Step P e s null s' ==> Step P (e\<bullet>F{D}) s (THROW NullPointer) s'
lemma FAccRedsThrow:
Step P e s (throw a) s' ==> Step P (e\<bullet>F{D}) s (throw a) s'
lemma FAssReds1:
Step P e s e' s' ==> Step P (e\<bullet>F{D} := e2) s (e'\<bullet>F{D} := e2) s'
lemma FAssReds2:
Step P e s e' s' ==> Step P (Val v\<bullet>F{D} := e) s (Val v\<bullet>F{D} := e') s'
lemma FAssRedsVal:
[| Step P e1 s0 (addr a) s1; Step P e2 s1 (Val v) (h2, l2); ⌊(C, fs)⌋ = h2 a |] ==> Step P (e1\<bullet>F{D} := e2) s0 unit (h2(a |-> (C, fs((F, D) |-> v))), l2)
lemma FAssRedsNull:
[| Step P e1 s0 null s1; Step P e2 s1 (Val v) s2 |] ==> Step P (e1\<bullet>F{D} := e2) s0 (THROW NullPointer) s2
lemma FAssRedsThrow1:
Step P e s (throw e') s' ==> Step P (e\<bullet>F{D} := e2) s (throw e') s'
lemma FAssRedsThrow2:
[| Step P e1 s0 (Val v) s1; Step P e2 s1 (throw e) s2 |] ==> Step P (e1\<bullet>F{D} := e2) s0 (throw e) s2
lemma SeqReds:
Step P e s e' s' ==> Step P (e;; e2) s (e';; e2) s'
lemma SeqRedsThrow:
Step P e s (throw e') s' ==> Step P (e;; e2) s (throw e') s'
lemma SeqReds2:
[| Step P e1 s0 (Val v1) s1; Step P e2 s1 e2' s2 |] ==> Step P (e1;; e2) s0 e2' s2
lemma CondReds:
Step P e s e' s' ==> Step P (if (e) e1 else e2) s (if (e') e1 else e2) s'
lemma CondRedsThrow:
Step P e s (throw a) s' ==> Step P (if (e) e1 else e2) s (throw a) s'
lemma CondReds2T:
[| Step P e s0 true s1; Step P e1 s1 e' s2 |] ==> Step P (if (e) e1 else e2) s0 e' s2
lemma CondReds2F:
[| Step P e s0 false s1; Step P e2 s1 e' s2 |] ==> Step P (if (e) e1 else e2) s0 e' s2
lemma WhileFReds:
Step P b s false s' ==> Step P (while (b) c) s unit s'
lemma WhileRedsThrow:
Step P b s (throw e) s' ==> Step P (while (b) c) s (throw e) s'
lemma WhileTReds:
[| Step P b s0 true s1; Step P c s1 (Val v1) s2; Step P (while (b) c) s2 e s3 |] ==> Step P (while (b) c) s0 e s3
lemma WhileTRedsThrow:
[| Step P b s0 true s1; Step P c s1 (throw e) s2 |] ==> Step P (while (b) c) s0 (throw e) s2
lemma ThrowReds:
Step P e s e' s' ==> Step P (throw e) s (throw e') s'
lemma ThrowRedsNull:
Step P e s null s' ==> Step P (throw e) s (THROW NullPointer) s'
lemma ThrowRedsThrow:
Step P e s (throw a) s' ==> Step P (throw e) s (throw a) s'
lemma InitBlockReds_aux:
Step P e s e' s' ==> ALL h l h' l' v. s = (h, l(V |-> v)) --> s' = (h', l') --> Step P {V:T; V:=Val v;; e} (h, l) {V:T; V:=Val (the (l' V));; e'} (h', l'(V := l V))
lemma InitBlockReds:
Step P e (h, l(V |-> v)) e' (h', l') ==> Step P {V:T; V:=Val v;; e} (h, l) {V:T; V:=Val (the (l' V));; e'} (h', l'(V := l V))
lemma InitBlockRedsFinal:
[| Step P e (h, l(V |-> v)) e' (h', l'); final e' |] ==> Step P {V:T; V:=Val v;; e} (h, l) e' (h', l'(V := l V))
lemma
[| Step P e0 s0 e2 (h2, l2); final e2; s0 = (h0, l0(V := None)) |] ==> Step P {V:T; e0} (h0, l0) e2 (h2, l2(V := l0 V))
lemma TryReds:
Step P e s e' s' ==> Step P (try e catch(C V) e2) s (try e' catch(C V) e2) s'
lemma TryRedsVal:
Step P e s (Val v) s' ==> Step P (try e catch(C V) e2) s (Val v) s'
lemma TryCatchRedsFinal:
[| Step P e1 s0 (Throw a) (h1, l1); h1 a = ⌊(D, fs)⌋; subcls P D C; Step P e2 (h1, l1(V |-> Addr a)) e2' (h2, l2); final e2' |] ==> Step P (try e1 catch(C V) e2) s0 e2' (h2, l2(V := l1 V))
lemma TryRedsFail:
[| Step P e1 s (Throw a) (h, l); h a = ⌊(D, fs)⌋; ¬ subcls P D C |] ==> Step P (try e1 catch(C V) e2) s (Throw a) (h, l)
lemma ListReds1:
Step P e s e' s' ==> Steps P (e # es) s (e' # es) s'
lemma ListReds2:
Steps P es s es' s' ==> Steps P (Val v # es) s (Val v # es') s'
lemma ListRedsVal:
[| Step P e s0 (Val v) s1; Steps P es s1 es' s2 |] ==> Steps P (e # es) s0 (Val v # es') s2
lemma Red_fv:
[| wwf_J_prog P; red P e (h, l) e' (h', l') |] ==> fv e' <= fv e
and
[| wwf_J_prog P; reds P es (h, l) es' (h', l') |] ==> fvs es' <= fvs es
lemma Red_dom_lcl:
red P e (h, l) e' (h', l') ==> dom l' <= dom l Un fv e
and
reds P es (h, l) es' (h', l') ==> dom l' <= dom l Un fvs es
lemma Reds_dom_lcl:
[| wwf_J_prog P; Step P e (h, l) e' (h', l') |] ==> dom l' <= dom l Un fv e
lemma overwrite_upd_lemma:
(f(g(a |-> b)|A))(a := g a) = f(g|insert a A)
lemma blocksReds:
[| length Vs = length Ts; length vs = length Ts; distinct Vs; Step P e (h, l(Vs [|->] vs)) e' (h', l') |] ==> Step P (blocks (Vs, Ts, vs, e)) (h, l) (blocks (Vs, Ts, map (the o l') Vs, e')) (h', l'(l|set Vs))
lemma blocksFinal:
[| length Vs = length Ts; length vs = length Ts; final e |] ==> Step P (blocks (Vs, Ts, vs, e)) (h, l) e (h, l)
lemma
[| length Vs = length Ts; length vs = length Ts; distinct Vs; Step P e (h, l(Vs [|->] vs)) e' (h', l'); final e'; l'' = l'(l|set Vs) |] ==> Step P (blocks (Vs, Ts, vs, e)) (h, l) e' (h', l'')
lemma CallRedsObj:
Step P e s e' s' ==> Step P (e\<bullet>M(es)) s (e'\<bullet>M(es)) s'
lemma CallRedsParams:
Steps P es s es' s' ==> Step P (Val v\<bullet>M(es)) s (Val v\<bullet>M(es')) s'
lemma
[| wwf_J_prog P; Step P e s0 (addr a) s1; Steps P es s1 (map Val vs) (h2, l2); h2 a = ⌊(C, fs)⌋; P \<turnstile> C sees M: Ts->T = (pns, body) in D; length vs = length pns; l2' = [this |-> Addr a, pns [|->] vs]; Step P body (h2, l2') ef (h3, l3); final ef |] ==> Step P (e\<bullet>M(es)) s0 ef (h3, l2)
lemma CallRedsThrowParams:
[| Step P e s0 (Val v) s1; Steps P es s1 (map Val vs1 @ throw a # es2) s2 |] ==> Step P (e\<bullet>M(es)) s0 (throw a) s2
lemma CallRedsThrowObj:
Step P e s0 (throw a) s1 ==> Step P (e\<bullet>M(es)) s0 (throw a) s1
lemma CallRedsNull:
[| Step P e s0 null s1; Steps P es s1 (map Val vs) s2 |] ==> Step P (e\<bullet>M(es)) s0 (THROW NullPointer) s2
lemma big_by_small:
[| wwf_J_prog P; eval P e s e' s' |] ==> Step P e s e' s'
and bigs_by_smalls:
[| wwf_J_prog P; evals P es s es' s' |] ==> Steps P es s es' s'
lemma unfold_while:
eval P (while (b) c) s e' s' = eval P (if (b) (c;; while (b) c) else unit) s e' s'
lemma blocksEval:
[| length ps = length Ts; length ps = length vs; eval P (blocks (ps, Ts, vs, e)) (h, l) e' (h', l') |] ==> EX l''. eval P e (h, l(ps [|->] vs)) e' (h', l'')
lemma eval_restrict_lcl:
[| wwf_J_prog P; eval P e (h, l) e' (h', l'); fv e <= W |] ==> eval P e (h, l|_W) e' (h', l'|_W)
and
[| wwf_J_prog P; evals P es (h, l) es' (h', l'); fvs es <= W |] ==> evals P es (h, l|_W) es' (h', l'|_W)
lemma eval_notfree_unchanged:
[| eval P e (h, l) e' (h', l'); V ~: fv e |] ==> l' V = l V
and
[| evals P es (h, l) es' (h', l'); V ~: fvs es |] ==> l' V = l V
lemma eval_closed_lcl_unchanged:
[| eval P e (h, l) e' (h', l'); fv e = {} |] ==> l' = l
lemma
eval P (throw x) s e' s' ==> evals P (map Val vs @ throw x # es') s (map Val vs @ e' # es') s'
lemma extend_1_eval:
[| wwf_J_prog P; red P e s e'' s''; eval P e'' s'' e' s' |] ==> eval P e s e' s'
and extend_1_evals:
[| wwf_J_prog P; reds P es t es'' t''; evals P es'' t'' es' t' |] ==> evals P es t es' t'
lemma
[| wwf_J_prog P; Step P e s e'' s''; eval P e'' s'' e' s' |] ==> eval P e s e' s'
lemma
[| wwf_J_prog P; Steps P es s es'' s''; evals P es'' s'' es' s' |] ==> evals P es s es' s'
theorem small_by_big:
[| wwf_J_prog P; Step P e s e' s'; final e' |] ==> eval P e s e' s'
and
[| wwf_J_prog P; Steps P es s es' s'; finals es' |] ==> evals P es s es' s'
corollary big_iff_small:
wwf_J_prog P ==> eval P e s e' s' = (Step P e s e' s' & final e')