1 theory Test1

     2 imports Main

     3 begin

     4 

     5 ML {*

     6 fun timing_wrapper tac st =

     7 let

     8   val t_start = Timing.start ();

     9   val res = tac st;

    10   val t_end = Timing.result t_start;

    11 in

    12   (tracing (Timing.message t_end); res)

    13 end

    14 *}

    15 

    16 

    17 datatype abc_inst =

    18      Inc nat

    19    | Dec nat nat

    20    | Goto nat

    21   

    22 type_synonym abc_prog = "abc_inst list"

    23 

    24 datatype recf = 

    25   z 

    26 | s 

    27 | id nat nat              --"Projection"

    28 | Cn nat recf "recf list" --"Composition"

    29 | Pr nat recf recf        --"Primitive recursion"

    30 | Mn nat recf             --"Minimisation"

    31 

    32 

    33 

    34 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    35   where

    36   "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]"

    37 

    38 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog"

    39   where

    40   "mv_box m n = [Dec m 3, Inc n, Goto 0]"

    41 

    42 fun abc_inst_shift :: "abc_inst \<Rightarrow> nat \<Rightarrow> abc_inst"

    43   where

    44   "abc_inst_shift (Inc m) n = Inc m" |

    45   "abc_inst_shift (Dec m e) n = Dec m (e + n)" |

    46   "abc_inst_shift (Goto m) n = Goto (m + n)"

    47 

    48 fun abc_shift :: "abc_inst list \<Rightarrow> nat \<Rightarrow> abc_inst list" 

    49   where

    50   "abc_shift [] n = []"

    51 | "abc_shift (x#xs) n = (abc_inst_shift x n) # (abc_shift xs n)" 

    52 

    53 fun abc_append :: "abc_inst list \<Rightarrow> abc_inst list \<Rightarrow> abc_inst list" (infixl "[+]" 60)

    54   where

    55   "abc_append al bl = al @ abc_shift bl (length al)"

    56 

    57 lemma [simp]: 

    58   "length (pa [+] pb) = length pa + length pb"

    59 by (induct pb) (auto)

    60 

    61 

    62 text {* The compilation of @{text "z"}-operator. *}

    63 definition rec_ci_z :: "abc_inst list"

    64   where

    65    [simp]: "rec_ci_z = [Goto 1]"

    66 

    67 

    68 text {* The compilation of @{text "s"}-operator. *}

    69 definition rec_ci_s :: "abc_inst list"

    70   where

    71   "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])"

    72 

    73 lemma [simp]:

    74   "rec_ci_s = [Dec 0 4, Inc 1, Inc 2, Goto 0, Dec 2 7, Inc 0, Goto 4, Inc 1] "

    75 by (simp add: rec_ci_s_def)

    76 

    77 text {* The compilation of @{text "id i j"}-operator *}

    78 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    79   where

    80   "rec_ci_id i j = addition j i (i + 1)"

    81 

    82 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list"

    83   where

    84   "mv_boxes ab bb n = (case n of 

    85       0 => [] 

    86     | Suc n => mv_boxes ab bb n [+] mv_box (ab + n) (bb + n))"

    87 

    88 fun empty_boxes :: "nat \<Rightarrow> abc_inst list"

    89   where

    90   "empty_boxes n = (case n of

    91       0 => []

    92     | Suc n => empty_boxes n [+] [Dec n 2, Goto 0])"

    93 

    94 fun cn_merge_gs ::

    95   "(abc_inst list \<times> nat \<times> nat) list \<Rightarrow> nat \<Rightarrow> abc_inst list"

    96   where

    97   "cn_merge_gs [] p = []" |

    98   "cn_merge_gs (g # gs) p = 

    99       (let (gprog, gpara, gn) = g in 

   100          gprog [+] mv_box gpara p [+] cn_merge_gs gs (Suc p))"

   101 

   102 fun list_max :: "nat list \<Rightarrow> nat"

   103   where

   104   "list_max [] = 0"

   105 | "list_max (x#xs) = (let y = list_max xs in

   106                       if (y < x) then x else y)"

   107 

   108 fun rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat"

   109   where

   110   "rec_ci z = (rec_ci_z, 1, 2)" |

   111   "rec_ci s = (rec_ci_s, 1, 3)" |

   112   "rec_ci (id m n) = (rec_ci_id m n, m, m + 2)" |

   113   "rec_ci (Cn n f gs) = 

   114       (let cied_gs = map rec_ci gs in

   115        let (fprog, fpara, fn) = rec_ci f in 

   116        let pstr = list_max (Suc n # fn # (map (\<lambda> (aprog, p, n). n) cied_gs)) in

   117        let qstr = pstr + Suc (length gs) in 

   118        (cn_merge_gs cied_gs pstr [+] mv_boxes 0 qstr n [+] 

   119           mv_boxes pstr 0 (length gs) [+] fprog [+] 

   120             mv_box fpara pstr [+] empty_boxes (length gs) [+] 

   121              mv_box pstr n [+] mv_boxes qstr 0 n, n,  qstr + n))" | 

   122   "rec_ci (Pr n f g) = 

   123          (let (fprog, fpara, fn) = rec_ci f in 

   124           let (gprog, gpara, gn) = rec_ci g in 

   125           let p = list_max [n + 3, fn, gn] in 

   126           let e = length gprog + 7 in 

   127            (mv_box n p [+] fprog [+] mv_box n (Suc n) [+] 

   128                (([Dec p e] [+] gprog [+] 

   129                  [Inc n, Dec (Suc n) 3, Goto 1]) @

   130                      [Dec (Suc (Suc n)) 0, Inc (Suc n), Goto (length gprog + 4)]),

   131              Suc n, p + 1))" |

   132   "rec_ci (Mn n f) =

   133          (let (fprog, fpara, fn) = rec_ci f in 

   134           let len = length (fprog) in 

   135             (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),

   136              Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))"

   137 

   138 definition rec_add :: "recf"

   139   where

   140    [simp]: "rec_add \<equiv>  Pr 1 (id 1 0) (Cn 3 s [id 3 2])"

   141 

   142 fun constn :: "nat \<Rightarrow> recf" where

   143   "constn n = (case n of

   144       0 => z  |

   145       Suc n => Cn 1 s [constn n])"

   146 

   147 ML {*

   148 fun dest_suc_trm @{term "Suc 0"} = raise TERM ("Suc 0", [])

   149   | dest_suc_trm @{term "Suc (Suc 0)"} = 2

   150   | dest_suc_trm (@{term "Suc"} $ t) = 1 + dest_suc_trm t

   151   | dest_suc_trm t = snd (HOLogic.dest_number t)

   152 

   153 fun get_thm ctxt (t, n) =

   154 let

   155   val num = HOLogic.mk_number @{typ "nat"} n

   156   val goal = Logic.mk_equals (t, num)

   157   val num_ss = HOL_ss addsimps @{thms semiring_norm}

   158 in

   159   Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))

   160 end

   161 

   162 fun nat_number_simproc ss ctrm =

   163 let

   164   val trm = term_of ctrm

   165   val ctxt = Simplifier.the_context ss

   166 in

   167   SOME (get_thm ctxt (trm, dest_suc_trm trm))

   168   handle TERM _ => NONE

   169 end

   170 *}

   171 

   172 simproc_setup nat_number ("Suc n") = {* K nat_number_simproc*}

   173 

   174 declare Nat.One_nat_def[simp del]

   175 

   176 lemma [simp]: 

   177   shows "nat_case g f (1::nat) = f (0::nat)"

   178 by (metis One_nat_def nat_case_Suc)

   179 

   180 lemma 

   181   "rec_ci (constn 0) = XXX"

   182 apply(tactic {*

   183   timing_wrapper (asm_full_simp_tac @{simpset} 1)

   184 *})

   185 oops

   186 

   187 lemma 

   188   "rec_ci (constn 10) = XXX"

   189 apply(tactic {*

   190   timing_wrapper (asm_full_simp_tac @{simpset} 1)

   191 *})

   192 oops

   193 

   194 lemma 

   195   "rec_ci (constn 3) = XXX"

   196 apply(tactic {*

   197   timing_wrapper (asm_full_simp_tac @{simpset} 1)

   198 *})

   199 oops

   200 

   201 lemma 

   202   "rec_ci (rec_add) = XXX"

   203 apply(simp del: abc_append.simps)

   204 apply(simp)

   205 oops

   206 

   207 definition rec_mult :: "recf"

   208   where

   209   [simp]: "rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"

   210 

   211 lemma 

   212   "rec_ci (rec_mult) = XXX"

   213 apply(simp)

   214 oops

   215 

   216 end