diff -r 002b07ea0a57 -r fa40fd8abb54 thys2/Recs.thy --- 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: "\\ y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs)); terminates f xs; length xs = n\ - \ terminates (Pr n f g) (xs @ [x])" + \ terminates (Pr n f g) (x # xs)" | termi_mn: "\length xs = n; terminates f (r # xs); rec_eval f (r # xs) = 0; \ i < r. terminates f (i # xs) \ rec_eval f (i # xs) > 0\ \ 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] = (\ z \ x. (rec_eval f) [z, y])" + shows "rec_eval (rec_sigma1 f) [x, y] = (\ z \ 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] = (\ z \ x. (rec_eval f) [z, y1, y2])" + shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\ z \ 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] = (\ z \ x. (rec_eval f) [z, y])" + shows "rec_eval (rec_accum1 f) [x, y] = (\ z \ 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] = (\ z \ x. (rec_eval f) [z, y1, y2])" + shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\ z \ 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 (\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 (\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 \ recf"