--- a/thys/Hoare_tm.thy Mon Mar 24 11:39:39 2014 +0000
+++ b/thys/Hoare_tm.thy Mon Mar 24 12:15:55 2014 +0000
@@ -12,21 +12,6 @@
Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt) trms))
*}
-lemma int_add_C :"x + (y::int) = y + x"
- by simp
-
-lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
- by simp
-
-lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)"
- by simp
-
-lemmas int_add_ac = int_add_A int_add_C int_add_LC
-
-method_setup prune =
- {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *}
- "pruning parameters"
-
ML {*
structure StepRules = Named_Thms
(val name = @{binding "step"}
@@ -43,6 +28,22 @@
setup {* FwdRules.setup *}
+method_setup prune =
+ {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *}
+ "pruning parameters"
+
+lemma int_add_C :"x + (y::int) = y + x"
+ by simp
+
+lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
+ by simp
+
+lemma int_add_LC: "x + (y + (z::int)) = y + (x + z)"
+ by simp
+
+lemmas int_add_ac = int_add_A int_add_C int_add_LC
+
+
section {* Operational Semantics of TM *}
datatype taction = W0 | W1 | L | R
@@ -55,11 +56,13 @@
type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
-fun next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))"
-where "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" |
- "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" |
- "next_tape L (pos, m) = (pos - 1, m)" |
- "next_tape R (pos, m) = (pos + 1, m)"
+fun
+ next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))"
+where
+ "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" |
+ "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" |
+ "next_tape L (pos, m) = (pos - 1, m)" |
+ "next_tape R (pos, m) = (pos + 1, m)"
fun tstep :: "tconf \<Rightarrow> tconf"
where "tstep (faults, prog, pc, pos, m) =
@@ -88,7 +91,7 @@
s = (faults, prog, pc, pos, m) \<longrightarrow>
prog pc = None \<longrightarrow> P (faults + 1, prog, pc, pos, m))
)"
- by (case_tac s, auto split:option.splits Block.splits)
+ by (cases s) (auto split: option.splits Block.splits)
datatype tresource =
TM int Block
@@ -111,6 +114,8 @@
interpretation tm: sep_exec tstep trset_of .
+
+
section {* Assembly language for TMs and its program logic *}
subsection {* The assembly language *}
@@ -520,18 +525,24 @@
show ?thesis by auto
qed
+
subsection {* Basic assertions for TM *}
+(* ones between tape position i and j *)
function ones :: "int \<Rightarrow> int \<Rightarrow> tassert" where
- "ones i j = (if j < i then <(i = j + 1)> else
- (one i) ** ones (i + 1) j)"
+ "ones i j = (if j < i then <(i = j + 1)>
+ else (one i) \<and>* ones (i + 1) j)"
by auto
-termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
-
-lemma ones_base_simp: "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"
+
+termination
+ by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
+
+lemma ones_base_simp:
+ "j < i \<Longrightarrow> ones i j = <(i = j + 1)>"
by simp
-lemma ones_step_simp: "\<not> j < i \<Longrightarrow> ones i j = ((one i) ** ones (i + 1) j)"
+lemma ones_step_simp:
+ "\<not> j < i \<Longrightarrow> ones i j = ((one i) \<and>* ones (i + 1) j)"
by simp
lemmas ones_simps = ones_base_simp ones_step_simp
@@ -539,9 +550,8 @@
declare ones.simps [simp del] ones_simps [simp]
lemma ones_induct [case_names Base Step]:
- fixes P i j
assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
- and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) ** ones (i + 1) j)"
+ and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (ones (i + 1) j)\<rbrakk> \<Longrightarrow> P i j ((one i) \<and>* ones (i + 1) j)"
shows "P i j (ones i j)"
proof(induct i j rule:ones.induct)
fix i j
@@ -560,8 +570,8 @@
qed
function ones' :: "int \<Rightarrow> int \<Rightarrow> tassert" where
- "ones' i j = (if j < i then <(i = j + 1)> else
- ones' i (j - 1) ** one j)"
+ "ones' i j = (if j < i then <(i = j + 1)>
+ else ones' i (j - 1) \<and>* one j)"
by auto
termination by (relation "measure(\<lambda> (i::int, j). nat (j - i + 1))") auto
@@ -584,7 +594,6 @@
qed
lemma ones_rev_induct [case_names Base Step]:
- fixes P i j
assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (ones i (j - 1))\<rbrakk> \<Longrightarrow> P i j ((ones i (j - 1)) ** one j)"
shows "P i j (ones i j)"
@@ -622,7 +631,6 @@
lemmas zeros_simps [simp] = zeros_base_simp zeros_step_simp
lemma zeros_induct [case_names Base Step]:
- fixes P i j
assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
and h2: "\<And> i j. \<lbrakk>\<not> j < i; P (i + 1) j (zeros (i + 1) j)\<rbrakk> \<Longrightarrow>
P i j ((zero i) ** zeros (i + 1) j)"
@@ -643,7 +651,7 @@
qed
qed
-lemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) ** zero j)"
+lemma zeros_rev: "\<not> j < i \<Longrightarrow> (zeros i j) = ((zeros i (j - 1)) \<and>* zero j)"
proof(induct i j rule:zeros_induct)
case (Base i j)
thus ?case by auto
@@ -660,7 +668,6 @@
qed
lemma zeros_rev_induct [case_names Base Step]:
- fixes P i j
assumes h1: "\<And> i j. j < i \<Longrightarrow> P i j (<(i = j + (1::int))>)"
and h2: "\<And> i j. \<lbrakk>\<not> j < i; P i (j - 1) (zeros i (j - 1))\<rbrakk> \<Longrightarrow>
P i j ((zeros i (j - 1)) ** zero j)"
@@ -682,7 +689,7 @@
qed
qed
-definition "rep i j k = ((ones i (i + (int k))) ** <(j = i + int k)>)"
+definition "rep i j k = ((ones i (i + (int k))) \<and>* <(j = i + int k)>)"
fun reps :: "int \<Rightarrow> int \<Rightarrow> nat list\<Rightarrow> tassert"
where
@@ -892,6 +899,7 @@
qed
qed
+
subsection {* A theory of list extension *}
definition "list_ext n xs = xs @ replicate ((Suc n) - length xs) 0"
@@ -925,6 +933,7 @@
lemma nth_app: "length xs \<le> a \<Longrightarrow> (xs @ ys)!a = ys!(a - length xs)"
by (metis not_less nth_append)
+(* FIXME in Hoare_gen? *)
lemma pred_exI:
assumes "(P(x) \<and>* r) s"
shows "((EXS x. P(x)) \<and>* r) s"