Theory Rec_Def

(* Title: thys/Rec_Def.thy
   Author: Jian Xu, Xingyuan Zhang, and Christian Urban
   Modifications: Sebastiaan Joosten
   Modifications: Franz Regensburger (FABR) 08/2022
     added LaTeX sections and some comments
 *)

chapter ‹Recursive Function and their compilation into Turing Machines›

theory Rec_Def
  imports Main
begin

section ‹Definition of a recursive datatype for Recursive Functions›

datatype recf =  z
  |  s
  |  id nat nat
  |  Cn nat recf "recf list"
  |  Pr nat recf recf
  |  Mn nat recf 

section ‹Definition of an interpreter for Recursive Functions›

definition pred_of_nl :: "nat list ⇒ nat list"
  where
    "pred_of_nl xs = butlast xs @ [last xs - 1]"

function rec_exec :: "recf ⇒ nat list ⇒ nat"
  where
    "rec_exec z xs = 0" |
    "rec_exec s xs = (Suc (xs ! 0))" |
    "rec_exec (id m n) xs = (xs ! n)" |
    "rec_exec (Cn n f gs) xs = 
     rec_exec f (map (λ a. rec_exec a xs) gs)" | 
    "rec_exec (Pr n f g) xs = 
     (if last xs = 0 then rec_exec f (butlast xs)
      else rec_exec g (butlast xs @ (last xs - 1) # [rec_exec (Pr n f g) (butlast xs @ [last xs - 1])]))" |
    "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (xs @ [x]) = 0)"
  by pat_completeness auto

termination
  apply(relation "measures [λ (r, xs). size r, (λ (r, xs). last xs)]")
        apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 size_list_estimation'[THEN trans_le_add1])
  done

inductive terminate :: "recf ⇒ nat list ⇒ bool"
  where
    termi_z: "terminate z [n]"
  | termi_s: "terminate s [n]"
  | termi_id: "⟦n < m; length xs = m⟧ ⟹ terminate (id m n) xs"
  | termi_cn: "⟦terminate f (map (λg. rec_exec g xs) gs); 
              ∀g ∈ set gs. terminate g xs; length xs = n⟧ ⟹ terminate (Cn n f gs) xs"
  | termi_pr: "⟦∀ y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
              terminate f xs;
              length xs = n⟧ 
              ⟹ terminate (Pr n f g) (xs @ [x])"
  | termi_mn: "⟦length xs = n; terminate f (xs @ [r]); 
              rec_exec f (xs @ [r]) = 0;
              ∀ i < r. terminate f (xs @ [i]) ∧ rec_exec f (xs @ [i]) > 0⟧ ⟹ terminate (Mn n f) xs"


end