22 "get_paras_num (Pr n f g) = Suc n" | |
20 "get_paras_num (Pr n f g) = Suc n" | |
23 "get_paras_num (Mn n f) = n" |
21 "get_paras_num (Mn n f) = n" |
24 |
22 |
25 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
23 fun addition :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
26 where |
24 where |
27 "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, |
25 "addition m n p = [Dec m 4, Inc n, Inc p, Goto 0, Dec p 7, Inc m, Goto 4]" |
28 Inc m, Goto 4]" |
|
29 |
26 |
30 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
27 fun mv_box :: "nat \<Rightarrow> nat \<Rightarrow> abc_prog" |
31 where |
28 where |
32 "mv_box m n = [Dec m 3, Inc n, Goto 0]" |
29 "mv_box m n = [Dec m 3, Inc n, Goto 0]" |
33 |
30 |
45 abc_inst list" (infixl "[+]" 60) |
42 abc_inst list" (infixl "[+]" 60) |
46 where |
43 where |
47 "abc_append al bl = (let al_len = length al in |
44 "abc_append al bl = (let al_len = length al in |
48 al @ abc_shift bl al_len)" |
45 al @ abc_shift bl al_len)" |
49 |
46 |
50 text {* |
47 text {* The compilation of @{text "z"}-operator. *} |
51 The compilation of @{text "z"}-operator. |
|
52 *} |
|
53 definition rec_ci_z :: "abc_inst list" |
48 definition rec_ci_z :: "abc_inst list" |
54 where |
49 where |
55 "rec_ci_z \<equiv> [Goto 1]" |
50 "rec_ci_z \<equiv> [Goto 1]" |
56 |
51 |
57 text {* |
52 text {* The compilation of @{text "s"}-operator. *} |
58 The compilation of @{text "s"}-operator. |
|
59 *} |
|
60 definition rec_ci_s :: "abc_inst list" |
53 definition rec_ci_s :: "abc_inst list" |
61 where |
54 where |
62 "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])" |
55 "rec_ci_s \<equiv> (addition 0 1 2 [+] [Inc 1])" |
63 |
56 |
64 |
57 |
65 text {* |
58 text {* The compilation of @{text "id i j"}-operator *} |
66 The compilation of @{text "id i j"}-operator |
|
67 *} |
|
68 |
|
69 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
59 fun rec_ci_id :: "nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
70 where |
60 where |
71 "rec_ci_id i j = addition j i (i + 1)" |
61 "rec_ci_id i j = addition j i (i + 1)" |
72 |
62 |
73 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
63 fun mv_boxes :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> abc_inst list" |
74 where |
64 where |
75 "mv_boxes ab bb 0 = []" | |
65 "mv_boxes ab bb 0 = []" | |
76 "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) |
66 "mv_boxes ab bb (Suc n) = mv_boxes ab bb n [+] mv_box (ab + n) (bb + n)" |
77 (bb + n)" |
|
78 |
67 |
79 fun empty_boxes :: "nat \<Rightarrow> abc_inst list" |
68 fun empty_boxes :: "nat \<Rightarrow> abc_inst list" |
80 where |
69 where |
81 "empty_boxes 0 = []" | |
70 "empty_boxes 0 = []" | |
82 "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" |
71 "empty_boxes (Suc n) = empty_boxes n [+] [Dec n 2, Goto 0]" |
92 |
81 |
93 text {* |
82 text {* |
94 The compiler of recursive functions, where @{text "rec_ci recf"} return |
83 The compiler of recursive functions, where @{text "rec_ci recf"} return |
95 @{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the |
84 @{text "(ap, arity, fp)"}, where @{text "ap"} is the Abacus program, @{text "arity"} is the |
96 arity of the recursive function @{text "recf"}, |
85 arity of the recursive function @{text "recf"}, |
97 @{text "fp"} is the amount of memory which is going to be |
86 @{text "fp"} is the amount of memory which is going to be |
98 used by @{text "ap"} for its execution. |
87 used by @{text "ap"} for its execution. |
99 *} |
88 *} |
100 |
89 |
101 function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat" |
90 function rec_ci :: "recf \<Rightarrow> abc_inst list \<times> nat \<times> nat" |
102 where |
91 where |
125 Suc n, p + 1))" | |
114 Suc n, p + 1))" | |
126 "rec_ci (Mn n f) = |
115 "rec_ci (Mn n f) = |
127 (let (fprog, fpara, fn) = rec_ci f in |
116 (let (fprog, fpara, fn) = rec_ci f in |
128 let len = length (fprog) in |
117 let len = length (fprog) in |
129 (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
118 (fprog @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3), |
130 Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn) )" |
119 Goto (len + 1), Inc n, Goto 0], n, max (Suc n) fn))" |
131 by pat_completeness auto |
120 by pat_completeness auto |
132 termination |
121 termination |
133 proof |
122 proof |
134 term size |
|
135 show "wf (measure size)" by auto |
123 show "wf (measure size)" by auto |
136 next |
124 next |
137 fix n f gs x |
125 fix n f gs x |
138 assume "(x::recf) \<in> set (f # gs)" |
126 assume "(x::recf) \<in> set (f # gs)" |
139 thus "(x, Cn n f gs) \<in> measure size" |
127 thus "(x, Cn n f gs) \<in> measure size" |
152 declare rec_ci.simps [simp del] rec_ci_s_def[simp del] |
140 declare rec_ci.simps [simp del] rec_ci_s_def[simp del] |
153 rec_ci_z_def[simp del] rec_ci_id.simps[simp del] |
141 rec_ci_z_def[simp del] rec_ci_id.simps[simp del] |
154 mv_boxes.simps[simp del] abc_append.simps[simp del] |
142 mv_boxes.simps[simp del] abc_append.simps[simp del] |
155 mv_box.simps[simp del] addition.simps[simp del] |
143 mv_box.simps[simp del] addition.simps[simp del] |
156 |
144 |
157 thm rec_calc_rel.induct |
|
158 |
|
159 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] |
145 declare abc_steps_l.simps[simp del] abc_fetch.simps[simp del] |
160 abc_step_l.simps[simp del] |
146 abc_step_l.simps[simp del] |
161 |
147 |
162 lemma abc_steps_add: |
148 lemma abc_steps_add: |
163 "abc_steps_l (as, lm) ap (m + n) = |
149 "abc_steps_l (as, lm) ap (m + n) = |
794 apply(simp add: rec_ci.simps) |
780 apply(simp add: rec_ci.simps) |
795 apply(case_tac "rec_ci f", simp) |
781 apply(case_tac "rec_ci f", simp) |
796 apply(case_tac "rec_ci g", simp) |
782 apply(case_tac "rec_ci g", simp) |
797 apply(arith) |
783 apply(arith) |
798 done |
784 done |
799 |
|
800 (* |
|
801 lemma pr_para_ge_suc0: "rec_calc_rel (Pr n f g) lm xs \<Longrightarrow> 0 < n" |
|
802 apply(erule calc_pr_reverse, simp, simp) |
|
803 done |
|
804 *) |
|
805 |
785 |
806 lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) |
786 lemma ci_pr_para_eq: "rec_ci (Pr n f g) = (aprog, rs_pos, a_md) |
807 \<Longrightarrow> rs_pos = Suc n" |
787 \<Longrightarrow> rs_pos = Suc n" |
808 apply(simp add: rec_ci.simps) |
788 apply(simp add: rec_ci.simps) |
809 apply(case_tac "rec_ci g", case_tac "rec_ci f", simp) |
789 apply(case_tac "rec_ci g", case_tac "rec_ci f", simp) |
1441 lemma mv_box_inv_halt: |
1421 lemma mv_box_inv_halt: |
1442 "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1422 "\<lbrakk>length initlm > max m n; m \<noteq> n\<rbrakk> \<Longrightarrow> |
1443 \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> |
1423 \<exists> stp. (\<lambda> (as, lm). as = 3 \<and> |
1444 mv_box_inv (as, lm) m n initlm) |
1424 mv_box_inv (as, lm) m n initlm) |
1445 (abc_steps_l (0::nat, initlm) (mv_box m n) stp)" |
1425 (abc_steps_l (0::nat, initlm) (mv_box m n) stp)" |
1446 thm halt_lemma2 |
|
1447 apply(insert halt_lemma2[of mv_box_LE |
1426 apply(insert halt_lemma2[of mv_box_LE |
1448 "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm" |
1427 "\<lambda> ((as, lm), m). mv_box_inv (as, lm) m n initlm" |
1449 "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)" |
1428 "\<lambda> stp. (abc_steps_l (0, initlm) (Recursive.mv_box m n) stp, m)" |
1450 "\<lambda> ((as, lm), m). as = (3::nat)" |
1429 "\<lambda> ((as, lm), m). as = (3::nat)" |
1451 ]) |
1430 ]) |
1537 "max (Suc (Suc (Suc n))) (max bc ba) - n < |
1516 "max (Suc (Suc (Suc n))) (max bc ba) - n < |
1538 Suc (max (Suc (Suc (Suc n))) (max bc ba)) - n" |
1517 Suc (max (Suc (Suc (Suc n))) (max bc ba)) - n" |
1539 apply(arith) |
1518 apply(arith) |
1540 done |
1519 done |
1541 |
1520 |
1542 thm nth_replicate |
|
1543 (* |
|
1544 lemma exp_nth[simp]: "n < m \<Longrightarrow> a\<up>m ! n = a" |
|
1545 apply(sim) |
|
1546 done |
|
1547 *) |
|
1548 lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow> |
1521 lemma [simp]: "length lm = n \<and> rs_pos = n \<and> 0 < n \<Longrightarrow> |
1549 lm[n - Suc 0 := 0::nat] = butlast lm @ [0]" |
1522 lm[n - Suc 0 := 0::nat] = butlast lm @ [0]" |
1550 apply(auto) |
1523 apply(auto) |
1551 apply(insert list_update_append[of "butlast lm" "[last lm]" |
1524 apply(insert list_update_append[of "butlast lm" "[last lm]" |
1552 "length lm - Suc 0" "0"], simp) |
1525 "length lm - Suc 0" "0"], simp) |
1936 apply(rule_tac x = "stp + stpa" in exI) |
1909 apply(rule_tac x = "stp + stpa" in exI) |
1937 apply(simp add: abc_steps_add) |
1910 apply(simp add: abc_steps_add) |
1938 done |
1911 done |
1939 qed |
1912 qed |
1940 |
1913 |
1941 thm rec_calc_rel.induct |
|
1942 |
|
1943 lemma eq_switch: "x = y \<Longrightarrow> y = x" |
1914 lemma eq_switch: "x = y \<Longrightarrow> y = x" |
1944 by simp |
1915 by simp |
1945 |
1916 |
1946 lemma [simp]: |
1917 lemma [simp]: |
1947 "\<lbrakk>rec_ci f = (a, aa, ba); |
1918 "\<lbrakk>rec_ci f = (a, aa, ba); |
1954 |
1925 |
1955 lemma ci_mn_para_eq[simp]: |
1926 lemma ci_mn_para_eq[simp]: |
1956 "rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n" |
1927 "rec_ci (Mn n f) = (aprog, rs_pos, a_md) \<Longrightarrow> rs_pos = n" |
1957 apply(case_tac "rec_ci f", simp add: rec_ci.simps) |
1928 apply(case_tac "rec_ci f", simp add: rec_ci.simps) |
1958 done |
1929 done |
1959 (* |
1930 |
1960 lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> aa = Suc rs_pos" |
|
1961 apply(rule_tac calc_mn_reverse, simp) |
|
1962 apply(insert para_pattern [of f a aa ba "lm @ [rs]" 0], simp) |
|
1963 apply(subgoal_tac "rs_pos = length lm", simp) |
|
1964 apply(drule_tac ci_mn_para_eq, simp) |
|
1965 done |
|
1966 *) |
|
1967 lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba" |
1931 lemma [simp]: "rec_ci f = (a, aa, ba) \<Longrightarrow> aa < ba" |
1968 apply(simp add: ci_ad_ge_paras) |
1932 apply(simp add: ci_ad_ge_paras) |
1969 done |
1933 done |
1970 |
1934 |
1971 lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); |
1935 lemma [simp]: "\<lbrakk>rec_ci f = (a, aa, ba); |
2055 |
2019 |
2056 definition mn_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> |
2020 definition mn_LE :: "(((nat \<times> nat list) \<times> nat \<times> nat) \<times> |
2057 ((nat \<times> nat list) \<times> nat \<times> nat)) set" |
2021 ((nat \<times> nat list) \<times> nat \<times> nat)) set" |
2058 where "mn_LE \<equiv> (inv_image lex_triple mn_measure)" |
2022 where "mn_LE \<equiv> (inv_image lex_triple mn_measure)" |
2059 |
2023 |
2060 thm halt_lemma2 |
|
2061 lemma wf_mn_le[intro]: "wf mn_LE" |
2024 lemma wf_mn_le[intro]: "wf mn_LE" |
2062 by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def) |
2025 by(auto intro:wf_inv_image wf_lex_triple simp: mn_LE_def) |
2063 |
2026 |
2064 declare mn_ind_inv.simps[simp del] |
2027 declare mn_ind_inv.simps[simp del] |
2065 |
2028 |
2076 (length a, n)" |
2039 (length a, n)" |
2077 apply(simp add: abc_steps_zero) |
2040 apply(simp add: abc_steps_zero) |
2078 apply(erule_tac rec_ci_not_null) |
2041 apply(erule_tac rec_ci_not_null) |
2079 done |
2042 done |
2080 |
2043 |
2081 thm rec_ci.simps |
|
2082 lemma [simp]: |
2044 lemma [simp]: |
2083 "\<lbrakk>rec_ci f = (a, aa, ba); |
2045 "\<lbrakk>rec_ci f = (a, aa, ba); |
2084 rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk> |
2046 rec_ci (Mn n f) = (aprog, rs_pos, a_md)\<rbrakk> |
2085 \<Longrightarrow> abc_fetch (length a) aprog = |
2047 \<Longrightarrow> abc_fetch (length a) aprog = |
2086 Some (Dec (Suc n) (length a + 5))" |
2048 Some (Dec (Suc n) (length a + 5))" |
2187 |
2149 |
2188 lemma [simp]: "Suc rs_pos < a_md \<Longrightarrow> |
2150 lemma [simp]: "Suc rs_pos < a_md \<Longrightarrow> |
2189 Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos" |
2151 Suc (a_md - Suc (Suc rs_pos)) = a_md - Suc rs_pos" |
2190 by arith |
2152 by arith |
2191 |
2153 |
2192 term rec_ci |
|
2193 (* |
|
2194 lemma [simp]: "\<lbrakk>rec_ci (Mn n f) = (aprog, rs_pos, a_md); rec_calc_rel (Mn n f) lm rs\<rbrakk> \<Longrightarrow> Suc rs_pos < a_md" |
|
2195 apply(case_tac "rec_ci f") |
|
2196 apply(subgoal_tac "c > b \<and> b = Suc rs_pos \<and> a_md \<ge> c") |
|
2197 apply(arith, auto) |
|
2198 done |
|
2199 *) |
|
2200 lemma mn_ind_step: |
2154 lemma mn_ind_step: |
2201 assumes ind: |
2155 assumes ind: |
2202 "\<And>aprog a_md rs_pos rs suf_lm lm. |
2156 "\<And>aprog a_md rs_pos rs suf_lm lm. |
2203 \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); |
2157 \<lbrakk>rec_ci f = (aprog, rs_pos, a_md); |
2204 rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> |
2158 rec_calc_rel f lm rs\<rbrakk> \<Longrightarrow> |
2210 "rsx > 0" |
2164 "rsx > 0" |
2211 "Suc rs_pos < a_md" |
2165 "Suc rs_pos < a_md" |
2212 "aa = Suc rs_pos" |
2166 "aa = Suc rs_pos" |
2213 shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
2167 shows "\<exists>stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
2214 aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2168 aprog stp = (0, lm @ Suc x # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2215 thm abc_add_exc1 |
|
2216 proof - |
2169 proof - |
2217 have k1: |
2170 have k1: |
2218 "\<exists> stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc (rs_pos)) @ suf_lm) |
2171 "\<exists> stp. abc_steps_l (0, lm @ x # 0\<up>(a_md - Suc (rs_pos)) @ suf_lm) |
2219 aprog stp = |
2172 aprog stp = |
2220 (length a, lm @ x # rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ suf_lm)" |
2173 (length a, lm @ x # rsx # 0\<up>(a_md - Suc (Suc rs_pos)) @ suf_lm)" |
2347 aprog stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2300 aprog stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2348 proof - |
2301 proof - |
2349 from h and ind have k1: |
2302 from h and ind have k1: |
2350 "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
2303 "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
2351 aprog stp = (length a, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2304 aprog stp = (length a, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2352 thm mn_calc_f |
|
2353 apply(insert mn_calc_f[of f a aa ba n aprog |
2305 apply(insert mn_calc_f[of f a aa ba n aprog |
2354 rs_pos a_md lm rs 0 suf_lm], simp) |
2306 rs_pos a_md lm rs 0 suf_lm], simp) |
2355 apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff) |
2307 apply(subgoal_tac "aa = Suc n", simp add: exponent_cons_iff) |
2356 apply(subgoal_tac "rs_pos = n", simp, simp) |
2308 apply(subgoal_tac "rs_pos = n", simp, simp) |
2357 done |
2309 done |
2395 "\<forall>x<rs. \<exists>v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v" |
2347 "\<forall>x<rs. \<exists>v. rec_calc_rel f (lm @ [x]) v \<and> 0 < v" |
2396 "n = length lm" |
2348 "n = length lm" |
2397 hence k1: |
2349 hence k1: |
2398 "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog |
2350 "\<exists>stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog |
2399 stp = (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2351 stp = (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2400 thm mn_ind_steps |
|
2401 apply(auto intro: mn_ind_steps ind) |
2352 apply(auto intro: mn_ind_steps ind) |
2402 done |
2353 done |
2403 from h have k2: |
2354 from h have k2: |
2404 "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog |
2355 "\<exists>stp. abc_steps_l (0, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog |
2405 stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2356 stp = (length aprog, lm @ rs # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
2499 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> |
2450 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow> |
2500 addition_inv (0, lm) m n p lm" |
2451 addition_inv (0, lm) m n p lm" |
2501 apply(simp add: addition_inv.simps) |
2452 apply(simp add: addition_inv.simps) |
2502 apply(rule_tac x = "lm ! m" in exI, simp) |
2453 apply(rule_tac x = "lm ! m" in exI, simp) |
2503 done |
2454 done |
2504 |
|
2505 thm addition.simps |
|
2506 |
2455 |
2507 lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)" |
2456 lemma [simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)" |
2508 by(simp add: abc_fetch.simps addition.simps) |
2457 by(simp add: abc_fetch.simps addition.simps) |
2509 |
2458 |
2510 lemma [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)" |
2459 lemma [simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)" |
2843 (cn_merge_gs (map rec_ci list @ [rec_ci a]) pstr) stp = |
2792 (cn_merge_gs (map rec_ci list @ [rec_ci a]) pstr) stp = |
2844 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) + |
2793 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) list) + |
2845 (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list), |
2794 (\<lambda>(ap, pos, n). length ap) (rec_ci a) + (3 + 3 * length list), |
2846 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2795 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md - Suc (pstr + length list)) @ suf_lm)" |
2847 apply(simp add: cn_merge_gs_tl_app) |
2796 apply(simp add: cn_merge_gs_tl_app) |
2848 thm abc_append_exc2 |
|
2849 apply(rule_tac as = |
2797 apply(rule_tac as = |
2850 "(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list" |
2798 "(\<Sum>(ap, pos, n)\<leftarrow>map rec_ci list. length ap) + 3 * length list" |
2851 and bm = "lm @ 0\<up>(pstr - n) @ butlast ys @ |
2799 and bm = "lm @ 0\<up>(pstr - n) @ butlast ys @ |
2852 0\<up>(a_md - (pstr + length list)) @ suf_lm" |
2800 0\<up>(a_md - (pstr + length list)) @ suf_lm" |
2853 and bs = "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3" |
2801 and bs = "(\<lambda>(ap, pos, n). length ap) (rec_ci a) + 3" |
3034 = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)" |
2982 = (3, lm1 @ 0 # 0\<up>n @ lm3 @ lm2 @ lm4)" |
3035 apply(insert mv_box_ex[of "aa + n" "ba + n" |
2983 apply(insert mv_box_ex[of "aa + n" "ba + n" |
3036 "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp) |
2984 "lm1 @ 0\<up>n @ last lm2 # lm3 @ butlast lm2 @ 0 # lm4"], simp) |
3037 done |
2985 done |
3038 qed |
2986 qed |
3039 (* |
|
3040 lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; |
|
3041 ba < aa; |
|
3042 length lm2 = aa - Suc (ba + n)\<rbrakk> |
|
3043 \<Longrightarrow> ((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba) |
|
3044 = last lm3" |
|
3045 proof - |
|
3046 assume h: "Suc n \<le> aa - ba" |
|
3047 and g: " ba < aa" "length lm2 = aa - Suc (ba + n)" |
|
3048 from h and g have k: "aa - ba = Suc (length lm2 + n)" |
|
3049 by arith |
|
3050 thus "((0::nat) # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa - ba) = last lm3" |
|
3051 apply(simp, simp add: nth_append) |
|
3052 done |
|
3053 qed |
|
3054 *) |
|
3055 |
2987 |
3056 lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; |
2988 lemma [simp]: "\<lbrakk>Suc n \<le> aa - ba; ba < aa; length lm1 = ba; |
3057 length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk> |
2989 length lm2 = aa - Suc (ba + n); length lm3 = Suc n\<rbrakk> |
3058 \<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa + n) = last lm3" |
2990 \<Longrightarrow> (lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n @ last lm3 # lm4) ! (aa + n) = last lm3" |
3059 using nth_append[of "lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n" "last lm3 # lm4" "aa + n"] |
2991 using nth_append[of "lm1 @ butlast lm3 @ 0 # lm2 @ 0\<up>n" "last lm3 # lm4" "aa + n"] |
3150 "\<lbrakk>length lm = n; pstr > n; a_md > pstr + length ys + n\<rbrakk> |
3082 "\<lbrakk>length lm = n; pstr > n; a_md > pstr + length ys + n\<rbrakk> |
3151 \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ ys @ |
3083 \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(pstr - n) @ ys @ |
3152 0\<up>(a_md - pstr - length ys) @ suf_lm) |
3084 0\<up>(a_md - pstr - length ys) @ suf_lm) |
3153 (mv_boxes 0 (pstr + Suc (length ys)) n) stp |
3085 (mv_boxes 0 (pstr + Suc (length ys)) n) stp |
3154 = (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3086 = (3 * n, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3155 thm mv_boxes_ex |
|
3156 apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm" |
3087 apply(insert mv_boxes_ex[of n "pstr + Suc (length ys)" 0 "[]" "lm" |
3157 "0\<up>(pstr - n) @ ys @ [0]" "0\<up>(a_md - pstr - length ys - n - Suc 0) @ suf_lm"], simp) |
3088 "0\<up>(pstr - n) @ ys @ [0]" "0\<up>(a_md - pstr - length ys - n - Suc 0) @ suf_lm"], simp) |
3158 apply(erule_tac exE, rule_tac x = stp in exI, |
3089 apply(erule_tac exE, rule_tac x = stp in exI, |
3159 simp add: exponent_add_iff) |
3090 simp add: exponent_add_iff) |
3160 apply(simp only: exponent_cons_iff, simp) |
3091 apply(simp only: exponent_cons_iff, simp) |
3359 a_md \<ge> pstr + length ys + n; |
3290 a_md \<ge> pstr + length ys + n; |
3360 pstr > length ys\<rbrakk> \<Longrightarrow> |
3291 pstr > length ys\<rbrakk> \<Longrightarrow> |
3361 \<exists>stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ |
3292 \<exists>stp. abc_steps_l (0, 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ |
3362 suf_lm) (mv_boxes pstr 0 (length ys)) stp = |
3293 suf_lm) (mv_boxes pstr 0 (length ys)) stp = |
3363 (3 * length ys, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3294 (3 * length ys, ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3364 thm mv_boxes_ex2 |
|
3365 apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]" |
3295 apply(insert mv_boxes_ex2[of "length ys" "pstr" 0 "[]" |
3366 "0\<up>(pstr - length ys)" "ys" |
3296 "0\<up>(pstr - length ys)" "ys" |
3367 "0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"], |
3297 "0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm"], |
3368 simp add: exponent_add_iff) |
3298 simp add: exponent_add_iff) |
3369 done |
3299 done |
3429 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3359 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3430 "length ys = length gs" "length lm = n" |
3360 "length ys = length gs" "length lm = n" |
3431 "rec_ci f = (a, aa, ba)" |
3361 "rec_ci f = (a, aa, ba)" |
3432 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3362 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3433 (map rec_ci (f # gs))))" |
3363 (map rec_ci (f # gs))))" |
3434 thm rec_ci.simps |
|
3435 from h and g have k1: |
3364 from h and g have k1: |
3436 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = |
3365 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = |
3437 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3366 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3438 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)" |
3367 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)" |
3439 by(drule_tac reset_new_paras_prog_ex, auto) |
3368 by(drule_tac reset_new_paras_prog_ex, auto) |
3470 using h |
3399 using h |
3471 apply(simp) |
3400 apply(simp) |
3472 done |
3401 done |
3473 qed |
3402 qed |
3474 qed |
3403 qed |
3475 |
|
3476 thm rec_ci.simps |
|
3477 |
3404 |
3478 lemma calc_f_prog_ex: |
3405 lemma calc_f_prog_ex: |
3479 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3406 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3480 rec_ci f = (a, aa, ba); |
3407 rec_ci f = (a, aa, ba); |
3481 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3408 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3645 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3572 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3646 + 3 * n + length a + 3, |
3573 + 3 * n + length a + 3, |
3647 ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys @ lm @ |
3574 ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys @ lm @ |
3648 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3575 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3649 proof - |
3576 proof - |
3650 thm rec_ci.simps |
|
3651 from h and pdef have k1: |
3577 from h and pdef have k1: |
3652 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3578 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3653 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3579 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3654 6 *length gs + 3 * n + length a \<and> bp = mv_box (length ys) pstr " |
3580 6 *length gs + 3 * n + length a \<and> bp = mv_box (length ys) pstr " |
3655 apply(subgoal_tac "length ys = aa") |
3581 apply(subgoal_tac "length ys = aa") |
3925 8 * length gs + 3 * n + length a + 6" |
3851 8 * length gs + 3 * n + length a + 6" |
3926 shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @ |
3852 shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @ |
3927 lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3853 lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3928 aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)" |
3854 aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)" |
3929 proof - |
3855 proof - |
3930 thm rec_ci.simps |
|
3931 from h and pdef and starts have k1: |
3856 from h and pdef and starts have k1: |
3932 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3857 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3933 bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n" |
3858 bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n" |
3934 by(drule_tac restore_paras_prog_ex, auto) |
3859 by(drule_tac restore_paras_prog_ex, auto) |
3935 from k1 show "?thesis" |
3860 from k1 show "?thesis" |
3994 (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @ |
3919 (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @ |
3995 0\<up>(a_md - ?pstr - length ys) @ suf_lm)" |
3920 0\<up>(a_md - ?pstr - length ys) @ suf_lm)" |
3996 apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs) |
3921 apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs) |
3997 apply(rule_tac ind, auto) |
3922 apply(rule_tac ind, auto) |
3998 done |
3923 done |
3999 thm rec_ci.simps |
|
4000 from g have k2: |
3924 from g have k2: |
4001 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @ |
3925 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @ |
4002 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = |
3926 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = |
4003 (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ |
3927 (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ |
4004 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
3928 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
4005 thm save_paras |
|
4006 apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq) |
3929 apply(erule_tac ba = c in save_paras, auto intro: ci_cn_para_eq) |
4007 done |
3930 done |
4008 from g have k3: |
3931 from g have k3: |
4009 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs + 3 * n, |
3932 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs + 3 * n, |
4010 0\<up>?pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
3933 0\<up>?pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
4020 ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
3943 ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
4021 (?gs_len + 6 * length gs + 3 * n + length a, |
3944 (?gs_len + 6 * length gs + 3 * n + length a, |
4022 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
3945 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
4023 apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto) |
3946 apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto) |
4024 done |
3947 done |
4025 thm rec_ci.simps |
|
4026 from g h have k5: |
3948 from g h have k5: |
4027 "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a, |
3949 "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a, |
4028 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) |
3950 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) |
4029 aprog stp = |
3951 aprog stp = |
4030 (?gs_len + 6 * length gs + 3 * n + length a + 3, |
3952 (?gs_len + 6 * length gs + 3 * n + length a + 3, |
4205 "bp \<noteq> []" |
4127 "bp \<noteq> []" |
4206 "\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp)" |
4128 "\<forall> stp. (\<lambda> (ss, e). ss < length bp) (abc_steps_l (0, lm) bp stp)" |
4207 "p = ap [+] bp [+] cp" |
4129 "p = ap [+] bp [+] cp" |
4208 have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)" |
4130 have "\<exists> stp. (abc_steps_l (0, am) p stp) = (length ap, lm)" |
4209 using h |
4131 using h |
4210 thm abc_add_exc1 |
|
4211 apply(simp add: abc_append.simps) |
4132 apply(simp add: abc_append.simps) |
4212 apply(rule_tac abc_add_exc1, auto) |
4133 apply(rule_tac abc_add_exc1, auto) |
4213 done |
4134 done |
4214 from this obtain stpa where g1: |
4135 from this obtain stpa where g1: |
4215 "(abc_steps_l (0, am) p stpa) = (length ap, lm)" .. |
4136 "(abc_steps_l (0, am) p stpa) = (length ap, lm)" .. |
4265 fix stp |
4186 fix stp |
4266 assume h: "rf = Mn n f" |
4187 assume h: "rf = Mn n f" |
4267 "rec_ci rf = (aprog, rs_pos, a_md)" |
4188 "rec_ci rf = (aprog, rs_pos, a_md)" |
4268 "rec_ci f = (aprog', rs_pos', a_md')" |
4189 "rec_ci f = (aprog', rs_pos', a_md')" |
4269 "\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n" |
4190 "\<forall>y. \<exists>rs. rec_calc_rel f (lm @ [y]) rs \<and> rs \<noteq> 0" "length lm = n" |
4270 thm mn_ind_step |
|
4271 have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog stpa |
4191 have "\<exists>stpa \<ge> stp. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) aprog stpa |
4272 = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
4192 = (0, lm @ stp # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
4273 proof(induct stp, auto) |
4193 proof(induct stp, auto) |
4274 show "\<exists>stpa. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
4194 show "\<exists>stpa. abc_steps_l (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm) |
4275 aprog stpa = (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
4195 aprog stpa = (0, lm @ 0 # 0\<up>(a_md - Suc rs_pos) @ suf_lm)" |
4439 apply(subgoal_tac "aa \<in> set gs", simp) |
4359 apply(subgoal_tac "aa \<in> set gs", simp) |
4440 using h2 |
4360 using h2 |
4441 apply(rule_tac A = "set (take i gs)" in subsetD, |
4361 apply(rule_tac A = "set (take i gs)" in subsetD, |
4442 simp add: set_take_subset, simp) |
4362 simp add: set_take_subset, simp) |
4443 done |
4363 done |
4444 thm cn_merge_gs.simps |
|
4445 from this obtain stpa where g2: |
4364 from this obtain stpa where g2: |
4446 "abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) |
4365 "abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) |
4447 (cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa = |
4366 (cn_merge_gs (map rec_ci ?ggs) ?pstr) stpa = |
4448 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) + |
4367 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) + |
4449 3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @ |
4368 3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @ |
4508 apply(auto) |
4427 apply(auto) |
4509 apply(rule_tac min_max.le_supI2) |
4428 apply(rule_tac min_max.le_supI2) |
4510 apply(rule_tac Max_ge, simp, simp) |
4429 apply(rule_tac Max_ge, simp, simp) |
4511 apply(rule_tac disjI2) |
4430 apply(rule_tac disjI2) |
4512 using h2 |
4431 using h2 |
4513 thm rev_image_eqI |
|
4514 apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp) |
4432 apply(rule_tac x = "gs!i" in rev_image_eqI, simp, simp) |
4515 done |
4433 done |
4516 next |
4434 next |
4517 show "aprog = cn_merge_gs (map rec_ci (take i gs)) |
4435 show "aprog = cn_merge_gs (map rec_ci (take i gs)) |
4518 ?pstr [+] ga [+] cp" |
4436 ?pstr [+] ga [+] cp" |
4768 proof - |
4686 proof - |
4769 fix stp lm' m |
4687 fix stp lm' m |
4770 assume h: "rec_calc_rel recf args r" |
4688 assume h: "rec_calc_rel recf args r" |
4771 "abc_steps_l (0, args) ap stp = (length ap, lm')" |
4689 "abc_steps_l (0, args) ap stp = (length ap, lm')" |
4772 "abc_list_crsp lm' (args @ r # 0\<up>m)" |
4690 "abc_list_crsp lm' (args @ r # 0\<up>m)" |
4773 thm abc_append_exc2 |
|
4774 thm abc_lm_s.simps |
|
4775 have "\<exists>stp. abc_steps_l (0, args) (ap [+] |
4691 have "\<exists>stp. abc_steps_l (0, args) (ap [+] |
4776 (dummy_abc (length args))) stp = (length ap + 3, |
4692 (dummy_abc (length args))) stp = (length ap + 3, |
4777 abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))" |
4693 abc_lm_s lm' (length args) (abc_lm_v lm' (length args)))" |
4778 using h |
4694 using h |
4779 apply(rule_tac bm = lm' in abc_append_exc2, |
4695 apply(rule_tac bm = lm' in abc_append_exc2, |