--- a/thys/Rec_Def.thy Thu Mar 14 20:43:43 2013 +0000
+++ b/thys/Rec_Def.thy Wed Mar 27 09:47:02 2013 +0000
@@ -1,95 +1,50 @@
-(* Title: thys/Rec_Def.thy
- Author: Jian Xu, Xingyuan Zhang, and Christian Urban
-*)
-
-header {* Definition of Recursive Functions *}
-
-
theory Rec_Def
imports Main
begin
-section {* Recursive functions *}
+datatype recf = z
+ | s
+ | id nat nat
+ | Cn nat recf "recf list"
+ | Pr nat recf recf
+ | Mn nat recf
-datatype recf =
- z | s |
- -- {* The projection function, where @{text "id i j"} returns the @{text "j"}-th
- argment out of the @{text "i"} arguments. *}
- id nat nat |
- -- {* The compostion operator, where "@{text "Cn n f [g1; g2; \<dots> ;gm]"}
- computes @{text "f (g1(x1, x2, \<dots>, xn), g2(x1, x2, \<dots>, xn), \<dots> ,
- gm(x1, x2, \<dots> , xn))"} for input argments @{text "x1, \<dots>, xn"}. *}
- Cn nat recf "recf list" |
- -- {* The primitive resursive operator, where @{text "Pr n f g"} computes:
- @{text "Pr n f g (x1, x2, \<dots>, xn-1, 0) = f(x1, \<dots>, xn-1)"}
- and @{text "Pr n f g (x1, x2, \<dots>, xn-1, k') = g(x1, x2, \<dots>, xn-1, k,
- Pr n f g (x1, \<dots>, xn-1, k))"}.
- *}
- Pr nat recf recf |
- -- {* The minimization operator, where @{text "Mn n f (x1, x2, \<dots> , xn)"}
- computes the first i such that @{text "f (x1, \<dots>, xn, i) = 0"} and for all
- @{text "j"}, @{text "f (x1, x2, \<dots>, xn, j) > 0"}. *}
- Mn nat recf
-
-(*
-partial_function (tailrec)
- rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
-where
- "rec_exec f ns = (case (f, ns) of
- (z, xs) => 0
- | (s, xs) => Suc (xs ! 0)
- | (id m n, xs) => (xs ! n)
- | (Cn n f gs, xs) =>
- (let ys = (map (\<lambda> a. rec_exec a xs) gs) in
- rec_exec f ys)
- | (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])]))
- | (Mn n f, xs) => (LEAST x. rec_exec f (xs @ [x]) = 0))"
-*)
+definition pred_of_nl :: "nat list \<Rightarrow> nat list"
+ where
+ "pred_of_nl xs = butlast xs @ [last xs - 1]"
-text {*
- The semantis of recursive operators is given by an inductively defined
- relation as follows, where
- @{text "rec_calc_rel R [x1, x2, \<dots>, xn] r"} means the computation of
- @{text "R"} over input arguments @{text "[x1, x2, \<dots>, xn"} terminates
- and gives rise to a result @{text "r"}
-*}
+function rec_exec :: "recf \<Rightarrow> nat list \<Rightarrow> 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 (\<lambda> 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 [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
+apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
+done
-inductive rec_calc_rel :: "recf \<Rightarrow> nat list \<Rightarrow> nat \<Rightarrow> bool"
-where
- calc_z: "rec_calc_rel z [n] 0" |
- calc_s: "rec_calc_rel s [n] (Suc n)" |
- calc_id: "\<lbrakk>length args = i; j < i; args!j = r\<rbrakk> \<Longrightarrow> rec_calc_rel (id i j) args r" |
- calc_cn: "\<lbrakk>length args = n;
- \<forall> k < length gs. rec_calc_rel (gs ! k) args (rs ! k);
- length rs = length gs;
- rec_calc_rel f rs r\<rbrakk>
- \<Longrightarrow> rec_calc_rel (Cn n f gs) args r" |
- calc_pr_zero:
- "\<lbrakk>length args = n;
- rec_calc_rel f args r0 \<rbrakk>
- \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [0]) r0" |
- calc_pr_ind: "
- \<lbrakk> length args = n;
- rec_calc_rel (Pr n f g) (args @ [k]) rk;
- rec_calc_rel g (args @ [k] @ [rk]) rk'\<rbrakk>
- \<Longrightarrow> rec_calc_rel (Pr n f g) (args @ [Suc k]) rk'" |
- calc_mn: "\<lbrakk>length args = n;
- rec_calc_rel f (args@[r]) 0;
- \<forall> i < r. (\<exists> ri. rec_calc_rel f (args@[i]) ri \<and> ri \<noteq> 0)\<rbrakk>
- \<Longrightarrow> rec_calc_rel (Mn n f) args r"
+inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"
+ where
+ termi_z: "terminate z [n]"
+| termi_s: "terminate s [n]"
+| termi_id: "\<lbrakk>n < m; length xs = m\<rbrakk> \<Longrightarrow> terminate (id m n) xs"
+| termi_cn: "\<lbrakk>terminate f (map (\<lambda>g. rec_exec g xs) gs);
+ \<forall>g \<in> set gs. terminate g xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Cn n f gs) xs"
+| termi_pr: "\<lbrakk>\<forall> y < x. terminate g (xs @ y # [rec_exec (Pr n f g) (xs @ [y])]);
+ terminate f xs;
+ length xs = n\<rbrakk>
+ \<Longrightarrow> terminate (Pr n f g) (xs @ [x])"
+| termi_mn: "\<lbrakk>length xs = n; terminate f (xs @ [r]);
+ rec_exec f (xs @ [r]) = 0;
+ \<forall> i < r. terminate f (xs @ [i]) \<and> rec_exec f (xs @ [i]) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
-inductive_cases calc_pr_reverse: "rec_calc_rel (Pr n f g) (lm) rSucy"
-inductive_cases calc_z_reverse: "rec_calc_rel z lm x"
-
-inductive_cases calc_s_reverse: "rec_calc_rel s lm x"
-
-inductive_cases calc_id_reverse: "rec_calc_rel (id m n) lm x"
-
-inductive_cases calc_cn_reverse: "rec_calc_rel (Cn n f gs) lm x"
-
-inductive_cases calc_mn_reverse:"rec_calc_rel (Mn n f) lm x"
end
\ No newline at end of file