2 imports Recs Hoare_tm2

     2 imports Recs Hoare_tm3

     8 fun actnum :: "taction \<Rightarrow> nat"

     8 fun actenc :: "action \<Rightarrow> nat"

     9   where

     9   where

    10   "actnum W0 = 0"

    10   "actenc W0 = 0"

    11 | "actnum W1 = 1"

    11 | "actenc W1 = 1"

    12 | "actnum L  = 2"

    12 | "actenc L  = 2"

    13 | "actnum R  = 3"

    13 | "actenc R  = 3"

    14 

    14 

    15 fun cellnum :: "Block \<Rightarrow> nat" where

    15 fun cellenc :: "Block \<Rightarrow> nat" where

    16   "cellnum Bk = 0"

    16   "cellenc Bk = 0"

    17 | "cellnum Oc = 1"

    17 | "cellenc Oc = 1"

    18 

    19 

    20 (* coding programs *)

    21 

    22 thm finfun_comp_def

    23 term finfun_rec

    24 

    25 definition code_finfun :: "(nat \<Rightarrow>f tm_inst option) \<Rightarrow> (nat \<times> tm_inst option) list"

    26   where

    27   "code_finfun f = ([(x, f $ x). x \<leftarrow> finfun_to_list f])"

    28 

    29 fun lookup where

    30   "lookup [] c = None"

    31 | "lookup ((a, b)#xs) c = (if a = c then b else lookup xs c)"

    32 

    33 lemma

    34   "f $ n = lookup (code_finfun f) n"

    35 apply(induct f rule: finfun_weak_induct)

    36 apply(simp add: code_finfun_def)

    37 apply(simp add: finfun_to_list_const)

    38 thm finfun_rec_const

    39 apply(finfun_rec_const)

    40 apply(simp add: finfun_rec_def)

    41 apply(auto)

    42 thm finfun_rec_unique

    43 apply(rule finfun_rec_unique)

    48 fun code_tp :: "() \<Rightarrow> nat list"

    22 definition 

    49   where

    23   "intenc i \<equiv> (if (0 \<le> i) then penc 0 (nat i) else penc 1 (nat (-i)))" 

    50   "code_tp [] = []"

    24 

    51 | "code_tp (c # tp) = (cellnum c) # code_tp tp"

    25 definition

    52 

    26   "intdec n \<equiv> (if (0 = pdec1 n) then (int (pdec2 n)) else -(int (pdec2 n)))"

    53 fun Code_tp where

    27 

    54   "Code_tp tp = lenc (code_tp tp)"

    28 definition 

    55 

    29   tapeenc :: "(int f\<rightharpoonup> Block) \<Rightarrow> nat"

    56 lemma code_tp_append [simp]:

    30 where

    57   "code_tp (tp1 @ tp2) = code_tp tp1 @ code_tp tp2"

    31   "tapeenc tp = lenc (map (\<lambda>(x, y). penc (intenc x) (cellenc y)) (fmap_to_alist tp))"

    58 by(induct tp1) (simp_all)

    32 

    59 

    33 fun 

    60 lemma code_tp_length [simp]:

    34   instenc :: "tm_inst \<Rightarrow> nat"

    61   "length (code_tp tp) = length tp"

    35 where

    62 by (induct tp) (simp_all)

    36   "instenc ((a1, s1), (a2, s2)) = lenc [actenc a1, s1, actenc a2, s2]"

    63 

    37 

    64 lemma code_tp_nth [simp]:

    38 definition 

    65   "n < length tp \<Longrightarrow> (code_tp tp) ! n = cellnum (tp ! n)"

    39   progenc :: "(nat f\<rightharpoonup> tm_inst) \<Rightarrow> nat"

    66 apply(induct n arbitrary: tp) 

    40 where

    67 apply(simp_all)

    41   "progenc p = lenc (map (\<lambda>(x, y). penc x (instenc y)) (fmap_to_alist p))"

    68 apply(case_tac [!] tp)

    42 

    69 apply(simp_all)

    43 text {* Coding Configurations of TMs *}

    70 done

    44 

    71 

    45 fun confenc where

    72 lemma code_tp_replicate [simp]:

    46   "confenc (faults, prog, s, pos, tp) = lenc [faults, progenc prog, s, intenc pos, tapeenc tp]"

    73   "code_tp (c \<up> n) = (cellnum c) \<up> n"

    47 

    74 by(induct n) (simp_all)

    48 section {* A Universal Function in HOL *}

    75 

    49 

    76 text {* Coding Configurations and TMs *}

    50 fun Step :: "nat \<Rightarrow> nat"

    77 

    51   where

    78 fun Code_conf where

    52   "Step cf = Conf (Newstate m (State cf) (Read (Right cf)), 

    79   "Code_conf (s, l, r) = (s, Code_tp l, Code_tp r)"

    53                      Newleft (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))),

    80 

    54                      Newright (Left cf) (Right cf) (Action m (State cf) (Read (Right cf))))"

    81 fun code_instr :: "instr \<Rightarrow> nat" where

    55 

    82   "code_instr i = penc (actnum (fst i)) (snd i)"

    56 

    83   

    57 text {* Reading and Writing the Encoded Tape *}

    84 fun Code_instr :: "instr \<times> instr \<Rightarrow> nat" where

    85   "Code_instr i = penc (code_instr (fst i)) (code_instr (snd i))"

    86 

    87 fun code_tprog :: "tprog \<Rightarrow> nat list"

    88   where

    89   "code_tprog [] =  []"

    90 | "code_tprog (i # tm) = Code_instr i # code_tprog tm"

    91 

    92 lemma code_tprog_length [simp]:

    93   "length (code_tprog tp) = length tp"

    94 by (induct tp) (simp_all)

    95 

    96 lemma code_tprog_nth [simp]:

    97   "n < length tp \<Longrightarrow> (code_tprog tp) ! n = Code_instr (tp ! n)"

    98 by (induct tp arbitrary: n) (simp_all add: nth_Cons')

    99 

   100 fun Code_tprog :: "tprog \<Rightarrow> nat"

   101   where 

   102   "Code_tprog tm = lenc (code_tprog tm)"

   103 

   104 

   105 section {* An Universal Function in HOL *}

   106 

   107 text {* Reading and writing the encoded tape *}