# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1395933153 0
# Node ID e6e412406a2dcea41214d83e8c2f4c90747a09fc
# Parent  457240e429724fbc82c38f1668a15e7ad6ba3eb1
added some comments

diff -r 457240e42972 -r e6e412406a2d thys/Hoare_gen.thy
--- a/thys/Hoare_gen.thy	Thu Mar 27 13:06:27 2014 +0000
+++ b/thys/Hoare_gen.thy	Thu Mar 27 15:12:33 2014 +0000
@@ -203,6 +203,8 @@
   shows "((EXS x. P(x)) \<and>* r) s"
   by (metis assms pred_ex_def sep_globalise)
 
+
+(* Interpreted Hoare triples *)
 definition
   IHoare :: "('b::sep_algebra \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool)  \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 
              ("(1_).(\<lbrace>(1_)\<rbrace>/ (_)/ \<lbrace>(1_)\<rbrace>)" 50)
diff -r 457240e42972 -r e6e412406a2d thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Thu Mar 27 13:06:27 2014 +0000
+++ b/thys/Hoare_tm.thy	Thu Mar 27 15:12:33 2014 +0000
@@ -49,10 +49,17 @@
 
 type_synonym tstate = nat
 
+datatype Block = Oc | Bk
+
+(* the successor state when tape symbol is Bk or Oc, respectively*)
 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
 
-datatype Block = Oc | Bk
-
+(* - number of faults
+   - TM program
+   - current state
+   - position of head
+   - tape
+*)
 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
 
 fun 
@@ -93,11 +100,11 @@
   by (cases s) (auto split: option.splits Block.splits)
 
 datatype tresource = 
-    TM int Block
-  | TC nat tm_inst
-  | TAt nat
-  | TPos int
-  | TFaults nat
+    TM int Block      (* at the position int of the tape is a Bl or Oc *)
+  | TC nat tm_inst    (* at the address nat is a certain instruction *)
+  | TAt nat           (* TM is at state nat*)
+  | TPos int          (* head of TM is at position int *)
+  | TFaults nat       (* there are nat faults *)
 
 definition "tprog_set prog = {TC i inst | i inst. prog i = Some inst}"
 definition "tpc_set pc = {TAt pc}"