thys/Hoare_tm.thy
changeset 14 23eeaac32d21
parent 13 e6e412406a2d
child 15 e3ecf558aef2
equal deleted inserted replaced
13:e6e412406a2d 14:23eeaac32d21
    29 
    29 
    30 method_setup prune = 
    30 method_setup prune = 
    31   {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
    31   {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
    32   "pruning parameters"
    32   "pruning parameters"
    33 
    33 
    34 lemma int_add_C :"x + (y::int) = y + x"
    34 lemma int_add_C: 
       
    35   "x + (y::int) = y + x"
    35   by simp
    36   by simp
    36 
    37 
    37 lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
    38 lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
    38   by simp
    39   by simp
    39 
    40 
    49 
    50 
    50 type_synonym tstate = nat
    51 type_synonym tstate = nat
    51 
    52 
    52 datatype Block = Oc | Bk
    53 datatype Block = Oc | Bk
    53 
    54 
    54 (* the successor state when tape symbol is Bk or Oc, respectively*)
    55 (* the successor state when tape symbol is Bk or Oc, respectively *)
    55 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
    56 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
    56 
    57 
    57 (* - number of faults
    58 (* - number of faults (nat)
    58    - TM program
    59    - TM program (nat \<rightharpoonup> tm_inst)
    59    - current state
    60    - current state (nat)
    60    - position of head
    61    - position of head (int)
    61    - tape
    62    - tape (int \<rightharpoonup> Block)
    62 *)
    63 *)
    63 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
    64 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
    64 
    65 
    65 fun 
    66 fun 
    66   next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"
    67   next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"