--- a/thys2/Recs.thy Thu Jun 06 17:27:45 2013 +0100
+++ b/thys2/Recs.thy Wed Jun 26 14:35:43 2013 +0100
@@ -213,7 +213,7 @@
| termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
terminates f xs;
length xs = n\<rbrakk>
- \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
+ \<Longrightarrow> terminates (Pr n f g) (x # xs)"
| termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs);
rec_eval f (r # xs) = 0;
\<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
@@ -242,8 +242,11 @@
definition
"rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
+definition
+ "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+
definition
- "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
+ "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
definition
"rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
@@ -271,9 +274,13 @@
"rec_eval rec_power [x, y] = x ^ y"
by (induct y) (simp_all add: rec_power_def)
+lemma fact_aux_lemma [simp]:
+ "rec_eval rec_fact_aux [x, y] = fact x"
+by (induct x) (simp_all add: rec_fact_aux_def)
+
lemma fact_lemma [simp]:
"rec_eval rec_fact [x] = fact x"
-by (induct x) (simp_all add: rec_fact_def)
+by (simp add: rec_fact_def)
lemma pred_lemma [simp]:
"rec_eval rec_pred [x] = x - 1"
@@ -300,7 +307,7 @@
@{text "rec_eq"} compares two arguments: returns @{text "1"}
if they are equal; @{text "0"} otherwise. *}
definition
- "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
+ "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]"
definition
"rec_noteq = CN rec_not [rec_eq]"
@@ -385,36 +392,40 @@
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]])"
+ "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0])
+ (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], 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]])"
+ "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1])
+ (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], 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]])"
+ "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0])
+ (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], 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]])"
+ "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1])
+ (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], 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]])"
+ "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2])
+ (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], 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])"
+ shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
by (induct x) (simp_all add: rec_sigma1_def)
lemma sigma2_lemma [simp]:
- shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f) [z, y1, y2])"
+ shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f [z, y1, y2])"
by (induct x) (simp_all add: rec_sigma2_def)
lemma accum1_lemma [simp]:
- shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f) [z, y])"
+ shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f [z, y])"
by (induct x) (simp_all add: rec_accum1_def)
lemma accum2_lemma [simp]:
- shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f) [z, y1, y2])"
+ shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f [z, y1, y2])"
by (induct x) (simp_all add: rec_accum2_def)
lemma accum3_lemma [simp]:
@@ -434,8 +445,9 @@
"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])"
+ "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in
+ let cond2 = CN f [Id 3 0, Id 3 2]
+ in CN (rec_all2 (CN rec_disj [cond1, cond2])) [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
@@ -540,7 +552,7 @@
section {* Iteration *}
definition
- "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
+ "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])"
fun Iter where
"Iter f 0 = id"
@@ -585,14 +597,14 @@
by (simp add: BMax_rec_eq2 Set.filter_def)
definition
- "rec_max1 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 4 0], Id 4 1])"
+ "rec_max1 f = PR Z (CN rec_ifz [CN f [CN S [Id 3 0], Id 3 2], CN S [Id 3 0], Id 3 1])"
lemma max1_lemma [simp]:
"rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
by (induct x) (simp_all add: rec_max1_def)
definition
- "rec_max2 f = PR (constn 0) (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
+ "rec_max2 f = PR Z (CN rec_ifz [CN f [CN S [Id 4 0], Id 4 2, Id 4 3], CN S [Id 4 0], Id 4 1])"
lemma max2_lemma [simp]:
"rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
@@ -801,7 +813,7 @@
by (simp add: enclen_def)
-text {* Recursive De3finitions for List Encodings *}
+text {* Recursive Definitions for List Encodings *}
fun
rec_lenc :: "recf list \<Rightarrow> recf"