equal
deleted
inserted
replaced
531 *} |
531 *} |
532 fun rec_Minr :: "recf \<Rightarrow> recf" |
532 fun rec_Minr :: "recf \<Rightarrow> recf" |
533 where |
533 where |
534 "rec_Minr rf = |
534 "rec_Minr rf = |
535 (let vl = arity rf |
535 (let vl = arity rf |
536 in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl) |
536 in let rq = rec_all (id vl (vl - 1)) |
537 rec_not [Cn (Suc vl) rf |
537 (Cn (Suc vl) rec_not [Cn (Suc vl) rf |
538 (get_fstn_args (Suc vl) (vl - 1) @ |
538 (get_fstn_args (Suc vl) (vl - 1) @ [id (Suc vl) vl])]) |
539 [id (Suc vl) (vl)])]) |
|
540 in rec_sigma rq)" |
539 in rec_sigma rq)" |
541 |
540 |
542 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n" |
541 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n" |
543 by(induct n, auto simp: get_fstn_args.simps) |
542 by(induct n, auto simp: get_fstn_args.simps) |
544 |
543 |
764 fun rec_maxr :: "recf \<Rightarrow> recf" |
763 fun rec_maxr :: "recf \<Rightarrow> recf" |
765 where |
764 where |
766 "rec_maxr rr = (let vl = arity rr in |
765 "rec_maxr rr = (let vl = arity rr in |
767 let rt = id (Suc vl) (vl - 1) in |
766 let rt = id (Suc vl) (vl - 1) in |
768 let rf1 = Cn (Suc (Suc vl)) rec_le |
767 let rf1 = Cn (Suc (Suc vl)) rec_le |
769 [id (Suc (Suc vl)) |
768 [id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in |
770 ((Suc vl)), id (Suc (Suc vl)) (vl)] in |
|
771 let rf2 = Cn (Suc (Suc vl)) rec_not |
769 let rf2 = Cn (Suc (Suc vl)) rec_not |
772 [Cn (Suc (Suc vl)) |
770 [Cn (Suc (Suc vl)) |
773 rr (get_fstn_args (Suc (Suc vl)) |
771 rr (get_fstn_args (Suc (Suc vl)) |
774 (vl - 1) @ |
772 (vl - 1) @ |
775 [id (Suc (Suc vl)) ((Suc vl))])] in |
773 [id (Suc (Suc vl)) (Suc vl)])] in |
776 let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in |
774 let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in |
777 let Qf = Cn (Suc vl) rec_not [rec_all rt rf] |
775 let Qf = Cn (Suc vl) rec_not [rec_all rt rf] |
778 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ |
776 in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @ |
779 [id vl (vl - 1)]))" |
777 [id vl (vl - 1)]))" |
780 |
778 |
1946 *} |
1944 *} |
1947 definition rec_lg :: "recf" |
1945 definition rec_lg :: "recf" |
1948 where |
1946 where |
1949 "rec_lg = |
1947 "rec_lg = |
1950 (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in |
1948 (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in |
1951 let conR1 = Cn 2 rec_conj [Cn 2 rec_less |
1949 let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0], |
1952 [Cn 2 (constn 1) [id 2 0], id 2 0], |
1950 Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in |
1953 Cn 2 rec_less [Cn 2 (constn 1) |
|
1954 [id 2 0], id 2 1]] in |
|
1955 let conR2 = Cn 2 rec_not [conR1] in |
1951 let conR2 = Cn 2 rec_not [conR1] in |
1956 Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR) |
1952 Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR) |
1957 [id 2 0, id 2 1, id 2 0]], |
1953 [id 2 0, id 2 1, id 2 0]], |
1958 Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])" |
1954 Cn 2 rec_mult [conR2, Cn 2 (constn 0) [id 2 0]]])" |
1959 |
1955 |