Mercurial Mercurial > hg > tm / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys2/Recs.thy
changeset 269 fa40fd8abb54
parent 266 b1b47d28c295
child 281 00ac265b251b
equal deleted inserted replaced
268:002b07ea0a57 269:fa40fd8abb54 
   211 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
   211 | termi_cn: "\<lbrakk>terminates f (map (\<lambda>g. rec_eval g xs) gs); 
   212               \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
 
   212               \<forall>g \<in> set gs. terminates g xs; length xs = n\<rbrakk> \<Longrightarrow> terminates (Cn n f gs) xs"
 
   213 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
 
   213 | termi_pr: "\<lbrakk>\<forall> y < x. terminates g (y # (rec_eval (Pr n f g) (y # xs) # xs));
 
   214               terminates f xs;
 
   214               terminates f xs;
 
   215               length xs = n\<rbrakk> 
   215               length xs = n\<rbrakk> 
   216               \<Longrightarrow> terminates (Pr n f g) (xs @ [x])"
 
   216               \<Longrightarrow> terminates (Pr n f g) (x # xs)"
 
   217 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
   217 | termi_mn: "\<lbrakk>length xs = n; terminates f (r # xs); 
   218               rec_eval f (r # xs) = 0;
 
   218               rec_eval f (r # xs) = 0;
 
   219               \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
 
   219               \<forall> i < r. terminates f (i # xs) \<and> rec_eval f (i # xs) > 0\<rbrakk> \<Longrightarrow> terminates (Mn n f) xs"
 
   220 
   220 
   221 
   221 
   240   "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
 
   240   "rec_mult = PR Z (CN rec_add [Id 3 1, Id 3 2])"
 
   241 
   241 
   242 definition 
   242 definition 
   243   "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
 
   243   "rec_power = rec_swap (PR (constn 1) (CN rec_mult [Id 3 1, Id 3 2]))"
 
   244 
   244 
   245 definition
 
   245 definition 
   246   "rec_fact = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
 
   246   "rec_fact_aux = PR (constn 1) (CN rec_mult [CN S [Id 3 0], Id 3 1])"
 
       
   247 
       
   248 definition
 
       
   249   "rec_fact = CN rec_fact_aux [Id 1 0, Id 1 0]"
 
   247 
   250 
   248 definition 
   251 definition 
   249   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
   252   "rec_pred = CN (PR Z (Id 3 0)) [Id 1 0, Id 1 0]"
 
   250 
   253 
   251 definition 
   254 definition 
   269 
   272 
   270 lemma power_lemma [simp]: 
   273 lemma power_lemma [simp]: 
   271   "rec_eval rec_power [x, y] = x ^ y"
 
   274   "rec_eval rec_power [x, y] = x ^ y"
 
   272 by (induct y) (simp_all add: rec_power_def)
 
   275 by (induct y) (simp_all add: rec_power_def)
 
   273 
   276 
       
   277 lemma fact_aux_lemma [simp]: 
       
   278   "rec_eval rec_fact_aux [x, y] = fact x"
 
       
   279 by (induct x) (simp_all add: rec_fact_aux_def)
 
       
   280 
   274 lemma fact_lemma [simp]: 
   281 lemma fact_lemma [simp]: 
   275   "rec_eval rec_fact [x] = fact x"
 
   282   "rec_eval rec_fact [x] = fact x"
 
   276 by (induct x) (simp_all add: rec_fact_def)
 
   283 by (simp add: rec_fact_def)
 
   277 
   284 
   278 lemma pred_lemma [simp]: 
   285 lemma pred_lemma [simp]: 
   279   "rec_eval rec_pred [x] =  x - 1"
 
   286   "rec_eval rec_pred [x] =  x - 1"
 
   280 by (induct x) (simp_all add: rec_pred_def)
 
   287 by (induct x) (simp_all add: rec_pred_def)
 
   281 
   288 
   298 
   305 
   299 text {*
 
   306 text {*
 
   300   @{text "rec_eq"} compares two arguments: returns @{text "1"}
 
   307   @{text "rec_eq"} compares two arguments: returns @{text "1"}
 
   301   if they are equal; @{text "0"} otherwise. *}
 
   308   if they are equal; @{text "0"} otherwise. *}
 
   302 definition 
   309 definition 
   303   "rec_eq = CN rec_minus [constn 1, CN rec_add [rec_minus, rec_swap rec_minus]]"
 
   310   "rec_eq = CN rec_minus [CN (constn 1) [Id 2 0], CN rec_add [rec_minus, rec_swap rec_minus]]"
 
   304 
   311 
   305 definition 
   312 definition 
   306   "rec_noteq = CN rec_not [rec_eq]"
 
   313   "rec_noteq = CN rec_not [rec_eq]"
 
   307 
   314 
   308 definition 
   315 definition 
   383 
   390 
   384 
   391 
   385 section {* Summation and Product Functions *}
 
   392 section {* Summation and Product Functions *}
 
   386 
   393 
   387 definition 
   394 definition 
   388   "rec_sigma1 f = PR (CN f [Z, Id 1 0]) (CN rec_add [Id 3 1, CN f [S, Id 3 2]])"
 
   395   "rec_sigma1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
   389 
   396                      (CN rec_add [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
   390 definition 
   397 
   391   "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]])"
 
   398 definition 
   392 
   399   "rec_sigma2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
   393 definition 
   400                      (CN rec_add [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
   394   "rec_accum1 f = PR (CN f [Z, Id 1 0]) (CN rec_mult [Id 3 1, CN f [S, Id 3 2]])"
 
   401 
   395 
   402 definition 
   396 definition 
   403   "rec_accum1 f = PR (CN f [CN Z [Id 1 0], Id 1 0]) 
   397   "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]])"
 
   404                      (CN rec_mult [Id 3 1, CN f [CN S [Id 3 0], Id 3 2]])"
 
   398 
   405 
   399 definition 
   406 definition 
   400   "rec_accum3 f = PR (CN f [Z, Id 3 0, Id 3 1, Id 3 2]) 
   407   "rec_accum2 f = PR (CN f [CN Z [Id 2 0], Id 2 0, Id 2 1]) 
   401                      (CN rec_mult [Id 5 1, CN f [S, Id 5 2, Id 5 3, Id 5 4]])"
 
   408                      (CN rec_mult [Id 4 1, CN f [CN S [Id 4 0], Id 4 2, Id 4 3]])"
 
       
   409 
       
   410 definition 
       
   411   "rec_accum3 f = PR (CN f [CN Z [Id 3 0], Id 3 0, Id 3 1, Id 3 2]) 
       
   412                      (CN rec_mult [Id 5 1, CN f [CN S [Id 5 0], Id 5 2, Id 5 3, Id 5 4]])"
 
   402 
   413 
   403 
   414 
   404 lemma sigma1_lemma [simp]: 
   415 lemma sigma1_lemma [simp]: 
   405   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. (rec_eval f)  [z, y])"
 
   416   shows "rec_eval (rec_sigma1 f) [x, y] = (\<Sum> z \<le> x. rec_eval f [z, y])"
 
   406 by (induct x) (simp_all add: rec_sigma1_def)
 
   417 by (induct x) (simp_all add: rec_sigma1_def)
 
   407 
   418 
   408 lemma sigma2_lemma [simp]: 
   419 lemma sigma2_lemma [simp]: 
   409   shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. (rec_eval f)  [z, y1, y2])"
 
   420   shows "rec_eval (rec_sigma2 f) [x, y1, y2] = (\<Sum> z \<le> x. rec_eval f  [z, y1, y2])"
 
   410 by (induct x) (simp_all add: rec_sigma2_def)
 
   421 by (induct x) (simp_all add: rec_sigma2_def)
 
   411 
   422 
   412 lemma accum1_lemma [simp]: 
   423 lemma accum1_lemma [simp]: 
   413   shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. (rec_eval f)  [z, y])"
 
   424   shows "rec_eval (rec_accum1 f) [x, y] = (\<Prod> z \<le> x. rec_eval f  [z, y])"
 
   414 by (induct x) (simp_all add: rec_accum1_def)
 
   425 by (induct x) (simp_all add: rec_accum1_def)
 
   415 
   426 
   416 lemma accum2_lemma [simp]: 
   427 lemma accum2_lemma [simp]: 
   417   shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2])"
 
   428   shows "rec_eval (rec_accum2 f) [x, y1, y2] = (\<Prod> z \<le> x. rec_eval f  [z, y1, y2])"
 
   418 by (induct x) (simp_all add: rec_accum2_def)
 
   429 by (induct x) (simp_all add: rec_accum2_def)
 
   419 
   430 
   420 lemma accum3_lemma [simp]: 
   431 lemma accum3_lemma [simp]: 
   421   shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
 
   432   shows "rec_eval (rec_accum3 f) [x, y1, y2, y3] = (\<Prod> z \<le> x. (rec_eval f)  [z, y1, y2, y3])"
 
   422 by (induct x) (simp_all add: rec_accum3_def)
 
   433 by (induct x) (simp_all add: rec_accum3_def)
 
   432 
   443 
   433 definition
 
   444 definition
 
   434   "rec_all3 f = CN rec_sign [rec_accum3 f]"
 
   445   "rec_all3 f = CN rec_sign [rec_accum3 f]"
 
   435 
   446 
   436 definition
 
   447 definition
 
   437   "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]] 
   448   "rec_all1_less f = (let cond1 = CN rec_eq [Id 3 0, Id 3 1] in
 
   438                       in CN (rec_all2 f') [Id 2 0, Id 2 0, Id 2 1])"
 
   449                       let cond2 = CN f [Id 3 0, Id 3 2] 
       
   450                       in CN (rec_all2 (CN rec_disj [cond1, cond2])) [Id 2 0, Id 2 0, Id 2 1])"
 
   439 
   451 
   440 definition
 
   452 definition
 
   441   "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
   453   "rec_all2_less f = (let cond1 = CN rec_eq [Id 4 0, Id 4 1] in 
   442                       let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in 
   454                       let cond2 = CN f [Id 4 0, Id 4 2, Id 4 3] in 
   443                       CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
 
   455                       CN (rec_all3 (CN rec_disj [cond1, cond2])) [Id 3 0, Id 3 0, Id 3 1, Id 3 2])"
 
   538 
   550 
   539 
   551 
   540 section {* Iteration *}
 
   552 section {* Iteration *}
 
   541 
   553 
   542 definition
 
   554 definition
 
   543    "rec_iter f = PR (Id 2 0) (CN f [Id 3 1])"
 
   555    "rec_iter f = PR (Id 1 0) (CN f [Id 3 1])"
 
   544 
   556 
   545 fun Iter where
 
   557 fun Iter where
 
   546   "Iter f 0 = id"
 
   558   "Iter f 0 = id"
 
   547 | "Iter f (Suc n) = f \<circ> (Iter f n)"
 
   559 | "Iter f (Suc n) = f \<circ> (Iter f n)"
 
   548 
   560 
   583 lemma BMax_rec_eq3:
 
   595 lemma BMax_rec_eq3:
 
   584   "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
 
   596   "BMax_rec R x = Max (Set.filter (\<lambda>z. R z) {..x} \<union> {0})"
 
   585 by (simp add: BMax_rec_eq2 Set.filter_def)
 
   597 by (simp add: BMax_rec_eq2 Set.filter_def)
 
   586 
   598 
   587 definition 
   599 definition 
   588   "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])"
 
   600   "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])"
 
   589  
   601  
   590 lemma max1_lemma [simp]:
 
   602 lemma max1_lemma [simp]:
 
   591   "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
 
   603   "rec_eval (rec_max1 f) [x, y] = BMax_rec (\<lambda>u. rec_eval f [u, y] = 0) x"
 
   592 by (induct x) (simp_all add: rec_max1_def)
 
   604 by (induct x) (simp_all add: rec_max1_def)
 
   593 
   605 
   594 definition 
   606 definition 
   595   "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])"
 
   607   "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])"
 
   596  
   608  
   597 lemma max2_lemma [simp]:
 
   609 lemma max2_lemma [simp]:
 
   598   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
 
   610   "rec_eval (rec_max2 f) [x, y1, y2] = BMax_rec (\<lambda>u. rec_eval f [u, y1, y2] = 0) x"
 
   599 by (induct x) (simp_all add: rec_max2_def)
 
   611 by (induct x) (simp_all add: rec_max2_def)
 
   600 
   612 
   799 lemma enclen_zero [simp]:
 
   811 lemma enclen_zero [simp]:
 
   800   "enclen 0 = 0"
 
   812   "enclen 0 = 0"
 
   801 by (simp add: enclen_def)
 
   813 by (simp add: enclen_def)
 
   802 
   814 
   803 
   815 
   804 text {* Recursive De3finitions for List Encodings *}
 
   816 text {* Recursive Definitions for List Encodings *}
 
   805 
   817 
   806 fun 
   818 fun 
   807   rec_lenc :: "recf list \<Rightarrow> recf" 
   819   rec_lenc :: "recf list \<Rightarrow> recf" 
   808 where
 
   820 where
 
   809   "rec_lenc [] = Z"
 
   821   "rec_lenc [] = Z"
tm