# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1369496448 -3600
# Node ID b1b47d28c2956e725ec6d65d9f55d87bee85969a
# Parent  fa3c214559b0dabd7d71057f234586e968d61850
polished Recs theory

diff -r fa3c214559b0 -r b1b47d28c295 thys2/Recs.thy
--- a/thys2/Recs.thy	Sat May 25 11:46:25 2013 +0100
+++ b/thys2/Recs.thy	Sat May 25 16:40:48 2013 +0100
@@ -178,6 +178,8 @@
 | "arity (Pr n f g) = Suc n"
 | "arity (Mn n f) = n"
 
+text {* Abbreviations for calculating the arity of the constructors *}
+
 abbreviation
   "CN f gs \<equiv> Cn (arity (hd gs)) f gs"
 
@@ -187,6 +189,8 @@
 abbreviation
   "MN f \<equiv> Mn (arity f - 1) f"
 
+text {* the evaluation function and termination relation *}
+
 fun rec_eval :: "recf \<Rightarrow> nat list \<Rightarrow> nat"
   where
   "rec_eval Z xs = 0" 
@@ -215,7 +219,7 @@
               \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
 
 
-section {* Recursive Function Definitions *}
+section {* Arithmetic Functions *}
 
 text {*
   @{text "constn n"} is the recursive function which computes 
@@ -247,6 +251,40 @@
 definition 
   "rec_minus = rec_swap (PR (Id 1 0) (CN rec_pred [Id 3 1]))"
 
+lemma constn_lemma [simp]: 
+  "rec_eval (constn n) xs = n"
+by (induct n) (simp_all)
+
+lemma swap_lemma [simp]:
+  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
+by (simp add: rec_swap_def)
+
+lemma add_lemma [simp]: 
+  "rec_eval rec_add [x, y] =  x + y"
+by (induct x) (simp_all add: rec_add_def)
+
+lemma mult_lemma [simp]: 
+  "rec_eval rec_mult [x, y] = x * y"
+by (induct x) (simp_all add: rec_mult_def)
+
+lemma power_lemma [simp]: 
+  "rec_eval rec_power [x, y] = x ^ y"
+by (induct y) (simp_all add: rec_power_def)
+
+lemma fact_lemma [simp]: 
+  "rec_eval rec_fact [x] = fact x"
+by (induct x) (simp_all add: rec_fact_def)
+
+lemma pred_lemma [simp]: 
+  "rec_eval rec_pred [x] =  x - 1"
+by (induct x) (simp_all add: rec_pred_def)
+
+lemma minus_lemma [simp]: 
+  "rec_eval rec_minus [x, y] = x - y"
+by (induct y) (simp_all add: rec_minus_def)
+
+
+section {* Logical functions *}
 
 text {* 
   The @{text "sign"} function returns 1 when the input argument 
@@ -286,127 +324,6 @@
 definition 
   "rec_if = CN rec_ifz [CN rec_not [Id 3 0], Id 3 1, Id 3 2]"
 
-text {*
-  @{text "rec_less"} compares two arguments and returns @{text "1"} if
-  the first is less than the second; otherwise returns @{text "0"}. *}
-
-definition 
-  "rec_less = CN rec_sign [rec_swap rec_minus]"
-
-definition 
-  "rec_le = CN rec_disj [rec_less, rec_eq]"
-
-text {* Sigma and Accum for function with one and two arguments *}
-
-definition 
-  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
-
-definition 
-  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-definition 
-  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
-
-definition 
-  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
-
-definition 
-  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
-                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
-
-
-text {* Bounded quantifiers for one and two arguments *}
-
-definition
-  "rec_all1 f = CN rec_sign [rec_accum1 f]"
-
-definition
-  "rec_all2 f = CN rec_sign [rec_accum2 f]"
-
-definition
-  "rec_all3 f = CN rec_sign [rec_accum3 f]"
-
-definition
-  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
-                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
-
-definition
-  "rec_all2_less f = (let f' = CN rec_disj [CN rec_eq [Id 4 0, Id 4 1], CN f [Id 4 0, Id 4 2, Id 4 3]] 
-                      in CN (rec_all3 f') [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
-
-definition
-  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
-
-definition
-  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
-
-text {* Dvd, Quotient, Modulo *}
-
-(* FIXME: probably all not needed *)
-definition 
-  "rec_dvd = 
-     rec_swap (CN (rec_ex2 (CN rec_eq [Id 3 2, CN rec_mult [Id 3 1, Id 3 0]])) [Id 2 0, Id 2 1, Id 2 0])"  
-
-definition
-  "rec_quo = (let lhs = CN S [Id 3 0] in
-              let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
-              let cond = CN rec_eq [lhs, rhs] in
-              let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
-              in PR Z if_stmt)"
-
-definition
-  "rec_mod = CN rec_minus [Id 2 0, CN rec_mult [Id 2 1, rec_quo]]"
-
-text {* Iteration *}
-
-definition
-   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
-
-fun Iter where
-  "Iter f 0 = id"
-| "Iter f (Suc n) = f \<circ> (Iter f n)"
-
-lemma Iter_comm:
-  "(Iter f n) (f x) = f ((Iter f n) x)"
-by (induct n) (simp_all)
-
-lemma iter_lemma [simp]:
-  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
-by (induct n) (simp_all add: rec_iter_def)
-
-section {* Correctness of Recursive Functions *}
-
-lemma constn_lemma [simp]: 
-  "rec_eval (constn n) xs = n"
-by (induct n) (simp_all)
-
-lemma swap_lemma [simp]:
-  "rec_eval (rec_swap f) [x, y] = rec_eval f [y, x]"
-by (simp add: rec_swap_def)
-
-lemma add_lemma [simp]: 
-  "rec_eval rec_add [x, y] =  x + y"
-by (induct x) (simp_all add: rec_add_def)
-
-lemma mult_lemma [simp]: 
-  "rec_eval rec_mult [x, y] = x * y"
-by (induct x) (simp_all add: rec_mult_def)
-
-lemma power_lemma [simp]: 
-  "rec_eval rec_power [x, y] = x ^ y"
-by (induct y) (simp_all add: rec_power_def)
-
-lemma fact_lemma [simp]: 
-  "rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all add: rec_fact_def)
-
-lemma pred_lemma [simp]: 
-  "rec_eval rec_pred [x] =  x - 1"
-by (induct x) (simp_all add: rec_pred_def)
-
-lemma minus_lemma [simp]: 
-  "rec_eval rec_minus [x, y] = x - y"
-by (induct y) (simp_all add: rec_minus_def)
 
 lemma sign_lemma [simp]: 
   "rec_eval rec_sign [x] = (if x = 0 then 0 else 1)"
@@ -436,6 +353,26 @@
   "rec_eval rec_imp [x, y] = (if 0 < x \<and> y = 0 then 0 else 1)"
 by (simp add: rec_imp_def)
 
+lemma ifz_lemma [simp]:
+  "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
+by (case_tac z) (simp_all add: rec_ifz_def)
+
+lemma if_lemma [simp]:
+  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
+by (simp add: rec_if_def)
+
+section {* Less and Le Relations *}
+
+text {*
+  @{text "rec_less"} compares two arguments and returns @{text "1"} if
+  the first is less than the second; otherwise returns @{text "0"}. *}
+
+definition 
+  "rec_less = CN rec_sign [rec_swap rec_minus]"
+
+definition 
+  "rec_le = CN rec_disj [rec_less, rec_eq]"
+
 lemma less_lemma [simp]: 
   "rec_eval rec_less [x, y] = (if x < y then 1 else 0)"
 by (simp add: rec_less_def)
@@ -444,13 +381,25 @@
   "rec_eval rec_le [x, y] = (if (x \<le> y) then 1 else 0)"
 by(simp add: rec_le_def)
 
-lemma ifz_lemma [simp]:
-  "rec_eval rec_ifz [z, x, y] = (if z = 0 then x else y)" 
-by (case_tac z) (simp_all add: rec_ifz_def)
+
+section {* Summation and Product Functions *}
+
+definition 
+  "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
+
+definition 
+  "rec_sigma2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_add [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
 
-lemma if_lemma [simp]:
-  "rec_eval rec_if [z, x, y] = (if 0 < z then x else y)" 
-by (simp add: rec_if_def)
+definition 
+  "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
+
+definition 
+  "rec_accum2 f = PR (CN f [Z, Id 2 0, Id 2 1]) (CN rec_mult [Id 4 1, CN f [S, Id 4 2, Id 4 3]])"
+
+definition 
+  "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
+                     (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
+
 
 lemma sigma1_lemma [simp]: 
   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
@@ -472,6 +421,34 @@
   shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
 by (induct x) (simp_all add: rec_accum3_def)
 
+
+section {* Bounded Quantifiers *}
+
+definition
+  "rec_all1 f = CN rec_sign [rec_accum1 f]"
+
+definition
+  "rec_all2 f = CN rec_sign [rec_accum2 f]"
+
+definition
+  "rec_all3 f = CN rec_sign [rec_accum3 f]"
+
+definition
+  "rec_all1_less f = (let f' = CN rec_disj [CN rec_eq [Id 3 0, Id 3 1], CN f [Id 3 0, Id 3 2]] 
+                      in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
+
+definition
+  "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
+                      let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in 
+                      CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
+
+definition
+  "rec_ex1 f = CN rec_sign [rec_sigma1 f]"
+
+definition
+  "rec_ex2 f = CN rec_sign [rec_sigma2 f]"
+
+
 lemma ex1_lemma [simp]:
  "rec_eval (rec_ex1 f) [x, y] = (if (\<exists>z \<le> x. 0 < rec_eval f [z, y]) then 1 else 0)"
 by (simp add: rec_ex1_def)
@@ -504,19 +481,14 @@
 apply(metis nat_less_le)+
 done
 
+section {* Quotients *}
 
-lemma dvd_alt_def:
-  fixes x y k:: nat
-  shows "(x dvd y) = (\<exists> k \<le> y. y = x * k)"
-apply(auto simp add: dvd_def)
-apply(case_tac x)
-apply(auto)
-done
-
-lemma dvd_lemma [simp]:
-  "rec_eval rec_dvd [x, y] = (if x dvd y then 1 else 0)"
-unfolding dvd_alt_def
-by (auto simp add: rec_dvd_def)
+definition
+  "rec_quo = (let lhs = CN S [Id 3 0] in
+              let rhs = CN rec_mult [Id 3 2, CN S [Id 3 1]] in
+              let cond = CN rec_eq [lhs, rhs] in
+              let if_stmt = CN rec_if [cond, CN S [Id 3 1], Id 3 1]
+              in PR Z if_stmt)"
 
 fun Quo where
   "Quo x 0 = 0"
@@ -524,9 +496,7 @@
 
 lemma Quo0:
   shows "Quo 0 y = 0"
-apply(induct y)
-apply(auto)
-done
+by (induct y) (auto)
 
 lemma Quo1:
   "x * (Quo x y) \<le> y"
@@ -566,9 +536,23 @@
   shows "rec_eval rec_quo [y, x] = y div x"
 by (simp add: Quo_div Quo_rec_quo)
 
-lemma rem_lemma [simp]:
-  shows "rec_eval rec_mod [y, x] = y mod x"
-by (simp add: rec_mod_def mod_div_equality' nat_mult_commute)
+
+section {* Iteration *}
+
+definition
+   "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
+
+fun Iter where
+  "Iter f 0 = id"
+| "Iter f (Suc n) = f \<circ> (Iter f n)"
+
+lemma Iter_comm:
+  "(Iter f n) (f x) = f ((Iter f n) x)"
+by (induct n) (simp_all)
+
+lemma iter_lemma [simp]:
+  "rec_eval (rec_iter f) [n, x] =  Iter (\<lambda>x. rec_eval f [x]) n x"
+by (induct n) (simp_all add: rec_iter_def)
 
 
 section {* Bounded Maximisation *}
@@ -577,8 +561,10 @@
   "BMax_rec R 0 = 0"
 | "BMax_rec R (Suc n) = (if R (Suc n) then (Suc n) else BMax_rec R n)"
 
-definition BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
-  where "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
+definition 
+  BMax_set :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat"
+where 
+  "BMax_set R x = Max ({z. z \<le> x \<and> R z} \<union> {0})"
 
 lemma BMax_rec_eq1:
  "BMax_rec R x = (GREATEST z. (R z \<and> z \<le> x) \<or> z = 0)"
@@ -612,6 +598,7 @@
   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
 by (induct x) (simp_all add: rec_max2_def)
 
+
 section {* Encodings using Cantor's pairing function *}
 
 text {*
@@ -697,22 +684,27 @@
 apply(simp)
 done
 
+
 definition 
   "rec_triangle = CN rec_quo [CN rec_mult [Id 1 0, S], constn 2]"
 
+definition
+  "rec_max_triangle = 
+       (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
+        CN (rec_max1 cond) [Id 1 0, Id 1 0])"
+
+
 lemma triangle_lemma [simp]:
   "rec_eval rec_triangle [x] = triangle x"
 by (simp add: rec_triangle_def triangle_def)
  
-definition
-  "rec_max_triangle = 
-       (let cond = CN rec_not [CN rec_le [CN rec_triangle [Id 2 0], Id 2 1]] in
-        CN (rec_max1 cond) [Id 1 0, Id 1 0])"
-
 lemma max_triangle_lemma [simp]:
   "rec_eval rec_max_triangle [x] = Max_triangle x"
 by (simp add: Max_triangle_greatest rec_max_triangle_def Let_def BMax_rec_eq1) 
 
+
+text {* Encodings for Products *}
+
 definition
   "rec_penc = CN rec_add [CN rec_triangle [CN rec_add [Id 2 0, Id 2 1]], Id 2 0]"
 
@@ -734,7 +726,8 @@
   "rec_eval rec_penc [m, n] = penc m n"
 by (simp add: rec_penc_def prod_encode_def)
 
-text {* encoding and decoding of lists of natural numbers *}
+
+text {* Encodings of Lists *}
 
 fun 
   lenc :: "nat list \<Rightarrow> nat" 
@@ -762,11 +755,13 @@
 by (induct xs arbitrary: n rule: lenc.induct) 
    (auto simp add: ldec_zero nth_Cons split: nat.splits)
 
-
 lemma lenc_length_le:
   "length xs \<le> lenc xs"  
 by (induct xs) (simp_all add: prod_encode_def)
 
+
+text {* Membership for the List Encoding *}
+
 fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
   "within z 0 = (0 < z)"
 | "within z (Suc n) = within (pdec2 z) n"
@@ -787,6 +782,8 @@
 apply(simp_all)
 done
 
+text {* Length of Encoded Lists *}
+
 lemma enclen_length [simp]:
   "enclen (lenc xs) = length xs"
 unfolding enclen_def
@@ -803,6 +800,9 @@
   "enclen 0 = 0"
 by (simp add: enclen_def)
 
+
+text {* Recursive De3finitions for List Encodings *}
+
 fun 
   rec_lenc :: "recf list \<Rightarrow> recf" 
 where
@@ -819,11 +819,11 @@
   "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_pred [Id 2 0]]])) [Id 1 0, Id 1 0]"
 
 lemma ldec_iter:
-  "ldec z n = pdec1 ((Iter pdec2 n) z) - 1"
+  "ldec z n = pdec1 (Iter pdec2 n z) - 1"
 by (induct n arbitrary: z) (simp | subst Iter_comm)+
 
 lemma within_iter:
-  "within z n = (0 < (Iter pdec2 n) z)"
+  "within z n = (0 < Iter pdec2 n z)"
 by (induct n arbitrary: z) (simp | subst Iter_comm)+
 
 lemma lenc_lemma [simp]:
diff -r fa3c214559b0 -r b1b47d28c295 thys2/UF_Rec.thy
--- a/thys2/UF_Rec.thy	Sat May 25 11:46:25 2013 +0100
+++ b/thys2/UF_Rec.thy	Sat May 25 16:40:48 2013 +0100
@@ -291,9 +291,9 @@
   "Std cf = (left_std (Left cf) \<and> right_std (Right cf))"
 
 text{* 
-  @{text "Nostop m cf k"} means that afer @{text k} steps of 
+  @{text "Stop m cf k"} means that afer @{text k} steps of 
   execution the TM coded by @{text m} and started in configuration
-  @{text cf} is not at a stardard final configuration. *}
+  @{text cf} is in a stardard final configuration. *}
 
 fun Final :: "nat \<Rightarrow> bool"
   where