1 theory rec_def

     2 imports Main

     3 begin

     4 

     5 section {*

     6   Recursive functions

     7 *}

     8 

     9 text {*

    10   Datatype of recursive operators.

    11 *}

    12 

    13 datatype recf = 

    14  -- {* The zero function, which always resturns @{text "0"} as result. *}

    15   z | 

    16  -- {* The successor function, which increments its arguments. *}

    17   s | 

    18  -- {*

    19   The projection function, where @{text "id i j"} returns the @{text "j"}-th

    20   argment out of the @{text "i"} arguments.

    21   *}

    22   id nat nat | 

    23  -- {*

    24   The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"} 

    25   computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> , 

    26   gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}.

    27   *}

    28   Cn nat recf "recf list" | 

    29 -- {*

    30   The primitive resursive operator, where @{text "Pr n f g"} computes:

    31   @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"} 

    32   and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k, 

    33                                                   Pr n f g (x1, \<dots>, xn-1, k))"}.

    34   *}

    35   Pr nat recf recf | 

    36 -- {*

    37   The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"} 

    38   computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all

    39   @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}.

    40   *}

    41   Mn nat recf 

    42 

    43 text {* 

    44   The semantis of recursive operators is given by an inductively defined

    45   relation as follows, where  

    46   @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of 

    47   @{text "R"} over input arguments @{text "[x1, x2, \<dots>, xn"} terminates

    48   and gives rise to a result @{text "r"}

    49 *}

    50 

    51 inductive rec_calc_rel :: "recf \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"

    52 where

    53   calc_z: "rec_calc_rel z [n] 0" |

    54   calc_s: "rec_calc_rel s [n] (Suc n)" |

    55   calc_id: "\<lbrakk>length args = i; j < i; args!j = r\<rbrakk> \<Longrightarrow> rec_calc_rel (id i j) args r" |

    56   calc_cn: "\<lbrakk>length args = n;

    57              \<forall> k < length gs. rec_calc_rel (gs ! k) args (rs ! k);

    58              length rs = length gs; 

    59              rec_calc_rel f rs r\<rbrakk> 

    60             \<Longrightarrow> rec_calc_rel (Cn n f gs) args r" |

    61   calc_pr_zero: 

    62            "\<lbrakk>length args = n;

    63              rec_calc_rel f args r0 \<rbrakk> 

    64             \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [0]) r0" |

    65   calc_pr_ind: "

    66            \<lbrakk> length args = n;

    67              rec_calc_rel (Pr n f g) (args @ [k]) rk; 

    68              rec_calc_rel g (args @ [k] @ [rk]) rk'\<rbrakk>

    69             \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [Suc k]) rk'"  |

    70   calc_mn: "\<lbrakk>length args = n; 

    71              rec_calc_rel f (args@[r]) 0; 

    72              \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk> 

    73             \<Longrightarrow> rec_calc_rel (Mn n f) args r" 

    74 

    75 inductive_cases calc_pr_reverse:

    76               "rec_calc_rel (Pr n f g) (lm) rSucy"

    77 

    78 inductive_cases calc_z_reverse: "rec_calc_rel z lm x"

    79 

    80 inductive_cases calc_s_reverse: "rec_calc_rel s lm x"

    81 

    82 inductive_cases calc_id_reverse: "rec_calc_rel (id m n) lm x"

    83 

    84 inductive_cases calc_cn_reverse: "rec_calc_rel (Cn n f gs) lm x"

    85 

    86 inductive_cases calc_mn_reverse:"rec_calc_rel (Mn n f) lm x"

    87 end