# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1362657128 0
# Node ID 38ed0ed6de3dba3361fb7044309535e77f3c5bd0
# Parent  12f278bd67aaf7a5223d6d8393ea478edd5d0f27
added definition of termination for rec_exec

diff -r 12f278bd67aa -r 38ed0ed6de3d Tests/Rec_Def.thy
--- a/Tests/Rec_Def.thy	Wed Mar 06 07:08:51 2013 +0000
+++ b/Tests/Rec_Def.thy	Thu Mar 07 11:52:08 2013 +0000
@@ -16,6 +16,7 @@
 "hd0 [] = 0" |
 "hd0 (m # ms) = m"
 
+(*
 fun
   primerec :: "recf \<Rightarrow> nat \<Rightarrow> bool"
 where
@@ -49,17 +50,7 @@
 apply(auto intro: eval.domintros)
 ????
 
-
-
-
-
-
-
-
-
-
-
-  
+*)
 
 partial_function (option) 
   eval :: "recf \<Rightarrow> nat option \<Rightarrow> (nat list) option => nat list \<Rightarrow> nat option"
@@ -86,36 +77,40 @@
 abbreviation
   "eval0 f ns \<equiv> eval f None None ns"
 
-abbreviation
-  "eval1 f ns \<equiv> if (\<exists>x. eval0 f ns = Some x) then the (eval0 f ns) else undefined"
-
-lemma "eval1 Zero [n] = 0"
-apply(subst (1 2) eval.simps)
+lemma "eval0 Zero [n] = Some 0"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 Succ [n] = n + 1"
-apply(subst (1 2) eval.simps)
+lemma "eval0 Succ [n] = Some (n + 1)"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "j < i \<Longrightarrow> eval1 (Id i j) ns = ns ! j"
-apply(subst (1 2) eval.simps)
+lemma "j < i \<Longrightarrow> eval0 (Id i j) ns = Some (ns ! j)"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 (Pr n f g) (0 # ns) = eval1 f ns"
-apply(subst (1 2) eval.simps)
+lemma "eval0 (Pr n f g) (0 # ns) = eval0 f ns"
+apply(subst eval.simps)
 apply(simp)
 done
 
-lemma "eval1 (Pr n f g) (Suc k # ns) = eval1 g ((eval1 (Pr n f g) (k # ns)) # k # ns)" 
-apply(subst (1 2) eval.simps)
+lemma "eval0 (Pr n f g) (Suc k # ns) = 
+  do { r \<leftarrow> eval0 (Pr n f g) (k # ns); eval0 g (r # k # ns) }"
+apply(subst eval.simps)
 apply(simp)
-apply(auto)
 done
 
 
 
+lemma 
+  "eval0 (Mn n f) ns = Some (LEAST r. eval0 f (r # ns) = Some 0)"
+apply(subst eval.simps)
+apply(simp)
+apply(subst eval.simps)
+apply(simp)
+done
 
 end
\ No newline at end of file
diff -r 12f278bd67aa -r 38ed0ed6de3d Tests/Rec_def2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Tests/Rec_def2.thy	Thu Mar 07 11:52:08 2013 +0000
@@ -0,0 +1,47 @@
+theory Rec_def2
+imports Main
+begin
+
+datatype recf =  z
+              |  s
+              |  id nat nat
+              |  Cn nat recf "recf list"
+              |  Pr nat recf recf
+              |  Mn nat recf 
+
+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 = 
+             (let ys = (map (\<lambda> a. rec_exec a xs) gs) in 
+                                  rec_exec f ys)" | 
+  "rec_exec (Pr n f g) xs = 
+     (if hd xs = 0 then 
+                  rec_exec f (tl xs)
+      else rec_exec g ((hd xs - 1) # tl xs @ [rec_exec (Pr n f g) ((hd xs - 1) # tl xs)]))" |
+  "rec_exec (Mn n f) xs = (LEAST x. rec_exec f (x # xs) = 0)"
+by pat_completeness auto
+
+termination
+apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). hd xs)]")
+apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
+done
+
+
+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_0: "\<lbrakk>terminate f xs; length xs = n\<rbrakk> \<Longrightarrow> terminate (Pr n f g) (0 # xs)"
+| termi_pr_suc: "\<lbrakk>terminate (Pr n f gs) (x # xs);
+                  terminate g (x # rec_exec (Pr n f gs) (x # xs) # xs)\<rbrakk> 
+                  \<Longrightarrow> terminate (Pr n f gs) (Suc x # xs)"
+| termi_mn: "\<lbrakk>length xs = n; rec_exec f (r # xs) = 0;
+              \<forall> i < r. terminate f (i # xs) \<and> rec_exec f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminate (Mn n f) xs"
+
+end
\ No newline at end of file