--- a/src/HOL/IMP/Procs.thy Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs.thy Mon Feb 04 09:06:20 2013 +0100
@@ -18,12 +18,11 @@
definition "test_com =
{VAR ''x'';;
- ''x'' ::= N 0;
- {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');;
+ {PROC ''p'' = ''x'' ::= N 1;;
{PROC ''q'' = CALL ''p'';;
{VAR ''x'';;
- ''x'' ::= N 5;
- {PROC ''p'' = ''x'' ::= Plus (V ''x'') (N 1);;
+ ''x'' ::= N 2;
+ {PROC ''p'' = ''x'' ::= N 3;;
CALL ''q''; ''y'' ::= V ''x''}}}}}"
end
--- a/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Dyn_Vars_Dyn.thy Mon Feb 04 09:06:20 2013 +0100
@@ -31,9 +31,6 @@
code_pred big_step .
-values "{map t [''x'',''y'',''z''] |t.
- (\<lambda>p. SKIP) \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'',''y'',''z''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'',''y''] |t. (\<lambda>p. SKIP) \<turnstile> (test_com, <>) \<Rightarrow> t}"
end
--- a/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Dyn.thy Mon Feb 04 09:06:20 2013 +0100
@@ -33,9 +33,6 @@
code_pred big_step .
-values "{map t [''x'', ''y'', ''z''] |t.
- [] \<turnstile> (CALL ''p'', <''x'' := 42, ''y'' := 43>) \<Rightarrow> t}"
-
-values "{map t [''x'', ''y'', ''z''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
+values "{map t [''x'', ''y''] |t. [] \<turnstile> (test_com, <>) \<Rightarrow> t}"
end
--- a/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Sun Feb 03 17:31:33 2013 +0100
+++ b/src/HOL/IMP/Procs_Stat_Vars_Stat.thy Mon Feb 04 09:06:20 2013 +0100
@@ -32,7 +32,7 @@
e \<turnstile> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3" |
Var: "(pe,ve(x:=f),f+1) \<turnstile> (c,s) \<Rightarrow> t \<Longrightarrow>
- (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t(f := s f)" |
+ (pe,ve,f) \<turnstile> ({VAR x;; c}, s) \<Rightarrow> t" |
Call1: "((p,c,ve)#pe,ve,f) \<turnstile> (c, s) \<Rightarrow> t \<Longrightarrow>
((p,c,ve)#pe,ve',f) \<turnstile> (CALL p, s) \<Rightarrow> t" |
@@ -45,10 +45,8 @@
code_pred big_step .
-values "{map t [0,1] |t. ([], <>, 0) \<turnstile> (CALL ''p'', nth [42, 43]) \<Rightarrow> t}"
-
-values "{map t [0, 1, 2] |t.
- ([], <''x'' := 0, ''y'' := 1,''z'' := 2>, 0)
+values "{map t [10,11] |t.
+ ([], <''x'' := 10, ''y'' := 11>, 12)
\<turnstile> (test_com, <>) \<Rightarrow> t}"
end