--- a/thys/UF.thy Wed Dec 19 16:10:58 2018 +0100
+++ b/thys/UF.thy Wed Dec 19 16:47:10 2018 +0100
@@ -20,28 +20,28 @@
subsection {* The construction of component functions *}
text {*
- The recursive function used to do arithmatic addition.
+ The recursive function used to do arithmetic addition.
*}
definition rec_add :: "recf"
where
"rec_add \<equiv> Pr 1 (id 1 0) (Cn 3 s [id 3 2])"
text {*
- The recursive function used to do arithmatic multiplication.
+ The recursive function used to do arithmetic multiplication.
*}
definition rec_mult :: "recf"
where
"rec_mult = Pr 1 z (Cn 3 rec_add [id 3 0, id 3 2])"
text {*
- The recursive function used to do arithmatic precede.
+ The recursive function used to do arithmetic precede.
*}
definition rec_pred :: "recf"
where
"rec_pred = Cn 1 (Pr 1 z (id 3 1)) [id 1 0, id 1 0]"
text {*
- The recursive function used to do arithmatic subtraction.
+ The recursive function used to do arithmetic subtraction.
*}
definition rec_minus :: "recf"
where
@@ -289,29 +289,12 @@
arity.simps[simp del] Sigma.simps[simp del]
rec_sigma.simps[simp del]
-lemma rec_pr_0_simp_rewrite: "
- rec_exec (Pr n f g) (xs @ [0]) = rec_exec f xs"
-by(simp add: rec_exec.simps)
-
-lemma rec_pr_0_simp_rewrite_single_param: "
- rec_exec (Pr n f g) [0] = rec_exec f []"
-by(simp add: rec_exec.simps)
-
lemma rec_pr_Suc_simp_rewrite:
"rec_exec (Pr n f g) (xs @ [Suc x]) =
rec_exec g (xs @ [x] @
[rec_exec (Pr n f g) (xs @ [x])])"
by(simp add: rec_exec.simps)
-lemma rec_pr_Suc_simp_rewrite_single_param:
- "rec_exec (Pr n f g) ([Suc x]) =
- rec_exec g ([x] @ [rec_exec (Pr n f g) ([x])])"
-by(simp add: rec_exec.simps)
-
-lemma Sigma_0_simp_rewrite_single_param:
- "Sigma f [0] = f [0]"
-by(simp add: Sigma.simps)
-
lemma Sigma_0_simp_rewrite:
"Sigma f (xs @ [0]) = f (xs @ [0])"
by(simp add: Sigma.simps)
@@ -320,11 +303,7 @@
"Sigma f (xs @ [Suc x]) = Sigma f (xs @ [x]) + f (xs @ [Suc x])"
by(simp add: Sigma.simps)
-lemma Sigma_Suc_simp_rewrite_single:
- "Sigma f ([Suc x]) = Sigma f ([x]) + f ([Suc x])"
-by(simp add: Sigma.simps)
-
-lemma [simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1"
+lemma append_access_1[simp]: "(xs @ ys) ! (Suc (length xs)) = ys ! 1"
by(simp add: nth_append)
lemma get_fstn_args_take: "\<lbrakk>length xs = m; n \<le> m\<rbrakk> \<Longrightarrow>
@@ -602,9 +581,6 @@
apply(erule_tac x = n in allE, simp add: nth_append primerec_accum)
done
-lemma min_Suc_Suc[simp]: "min (Suc (Suc x)) x = x"
- by auto
-
declare numeral_3_eq_3[simp]
lemma primerec_rec_pred_1[intro]: "primerec rec_pred (Suc 0)"
@@ -660,10 +636,6 @@
apply(auto, simp add: nth_append, auto)
done
-lemma min_P0[simp]: "Rr (xs @ [0]) \<Longrightarrow>
- Min {x. x = (0::nat) \<and> Rr (xs @ [x])} = 0"
-by(rule_tac Min_eqI, simp, simp, simp)
-
lemma primerec_rec_not_1[intro]: "primerec rec_not (Suc 0)"
apply(simp add: rec_not_def)
apply(rule prime_cn, auto)
@@ -815,8 +787,6 @@
declare rec_maxr.simps[simp del] Maxr.simps[simp del]
declare le_lemma[simp]
-lemma min_with_suc3[simp]: "(min (Suc (Suc (Suc (x)))) (x)) = x"
-by simp
declare numeral_2_eq_2[simp]
@@ -846,24 +816,6 @@
apply(case_tac i, auto)
done
-lemma take_butlast_list_plus_two[simp]:
- "length ys = Suc n \<Longrightarrow> (take n ys @ [ys ! n, ys ! n]) =
- ys @ [ys ! n]"
-apply(simp)
-apply(subgoal_tac "\<exists> xs y. ys = xs @ [y]", auto)
-apply(rule_tac x = "butlast ys" in exI, rule_tac x = "last ys" in exI)
-apply(case_tac "ys = []", simp_all)
-done
-
-lemma Maxr_Suc_simp:
- "Maxr Rr xs (Suc w) =(if Rr (xs @ [Suc w]) then Suc w
- else Maxr Rr xs w)"
-apply(auto simp: Maxr.simps expand_conj_in_set)
-apply(rule_tac Max_eqI, auto)
-done
-
-lemma min_Suc_1[simp]: "min (Suc n) n = n" by simp
-
lemma Sigma_0: "\<forall> i \<le> n. (f (xs @ [i]) = 0) \<Longrightarrow>
Sigma f (xs @ [n]) = 0"
apply(induct n, simp add: Sigma.simps)
@@ -1583,17 +1535,6 @@
"fac 0 = 1" |
"fac (Suc x) = (Suc x) * fac x"
-lemma rec_exec_rec_dummyfac_0: "rec_exec rec_dummyfac [0, 0] = Suc 0"
-by(simp add: rec_dummyfac_def rec_exec.simps)
-
-lemma rec_cn_simp: "rec_exec (Cn n f gs) xs =
- (let rgs = map (\<lambda> g. rec_exec g xs) gs in
- rec_exec f rgs)"
-by(simp add: rec_exec.simps)
-
-lemma rec_id_simp: "rec_exec (id m n) xs = xs ! n"
- by(simp add: rec_exec.simps)
-
lemma fac_dummy: "rec_exec rec_dummyfac [x, y] = y !"
apply(induct y)
apply(auto simp: rec_dummyfac_def rec_exec.simps)
@@ -1804,7 +1745,7 @@
text {*
@{text "Lo"} specifies the @{text "lo"} function given on page 79 of
- Boolos's book. It is one of the two notions of integeral logarithmatic
+ Boolos's book. It is one of the two notions of integeral logarithmetic
operation on that page. The other is @{text "lg"}.
*}
fun lo :: " nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -1814,10 +1755,6 @@
declare lo.simps[simp del]
-lemma primerec_then_ge_0[elim]: "primerec rf n \<Longrightarrow> n > 0"
-apply(induct rule: primerec.induct, auto)
-done
-
lemma primerec_sigma[intro!]:
"\<lbrakk>n > Suc 0; primerec rf n\<rbrakk> \<Longrightarrow>
primerec (rec_sigma rf) n"
@@ -1885,27 +1822,13 @@
done
qed
-lemma MaxloR0[simp]: "Max {ya. ya = 0 \<and> loR [0, y, ya]} = 0"
-apply(rule_tac Max_eqI, auto simp: loR.simps)
-done
-
-lemma two_less_square[simp]: "Suc 0 < y \<Longrightarrow> Suc (Suc 0) < y * y"
- by(induct y, auto)
-
-lemma less_mult: "\<lbrakk>x > 0; y > Suc 0\<rbrakk> \<Longrightarrow> x < y * x"
-apply(case_tac y, simp, simp)
-done
-
lemma x_less_exp: "\<lbrakk>y > Suc 0\<rbrakk> \<Longrightarrow> x < y^x"
apply(induct x, simp, simp)
apply(case_tac x, simp, auto)
apply(rule_tac y = "y* y^nat" in le_less_trans, simp)
-apply(rule_tac less_mult, auto)
+apply(rule_tac n_less_m_mult_n, auto)
done
-lemma le_mult: "y \<noteq> (0::nat) \<Longrightarrow> x \<le> x * y"
- by(induct y, simp, simp)
-
lemma uplimit_loR:
assumes "Suc 0 < x" "Suc 0 < y" "loR [x, y, xa]"
shows "xa \<le> x"
@@ -1955,7 +1878,7 @@
text {*
@{text "lg"} specifies the @{text "lg"} function given on page 79 of
- Boolos's book. It is one of the two notions of integeral logarithmatic
+ Boolos's book. It is one of the two notions of integeral logarithmetic
operation on that page. The other is @{text "lo"}.
*}
fun lg :: "nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -2838,20 +2761,6 @@
declare nonstop.simps[simp del]
-lemma primerec_not0: "primerec f n \<Longrightarrow> n > 0"
-by(induct f n rule: primerec.induct, auto)
-
-lemma primerec_not0E[elim]: "primerec f 0 \<Longrightarrow> RR"
-apply(drule_tac primerec_not0, simp)
-done
-
-lemma length_butlast[simp]: "length xs = Suc n \<Longrightarrow> length (butlast xs) = n"
-apply(subgoal_tac "\<exists> y ys. xs = ys @ [y]",force)
-apply(rule_tac x = "last xs" in exI)
-apply(rule_tac x = "butlast xs" in exI)
-apply(case_tac "xs = []", auto)
-done
-
text {*
The lemma relates the interpreter of primitive functions with
the calculation relation of general recursive functions.
@@ -2890,50 +2799,20 @@
;(simp add:primerec_rec_pi_helpers primrec_dummyfac)?)+
by fastforce+
-lemma primerec_rec_trpl[intro]: "primerec rec_trpl (Suc (Suc (Suc 0)))"
-apply(simp add: rec_trpl_def)
-apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma primerec_rec_listsum2[intro!]: "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_listsum2 vl n) vl"
-apply(induct n)
-apply(simp_all add: rec_strt'.simps Let_def rec_listsum2.simps)
-apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)+
-done
-
-lemma primerec_rec_strt': "\<lbrakk>0 < vl; n \<le> vl\<rbrakk> \<Longrightarrow> primerec (rec_strt' vl n) vl"
-apply(induct n)
-apply(simp_all add: rec_strt'.simps Let_def)
-apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}, auto+)
-done
-
-lemma primerec_rec_strt: "vl > 0 \<Longrightarrow> primerec (rec_strt vl) vl"
-apply(simp add: rec_strt.simps rec_strt'.simps)
-by(tactic {* resolve_tac @{context} [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}; force elim:primerec_rec_strt')
-
-lemma primerec_map_vl:
- "i < vl \<Longrightarrow> primerec ((map (\<lambda>i. recf.id (Suc vl) (i))
- [Suc 0..<vl] @ [recf.id (Suc vl) (vl)]) ! i) (Suc vl)"
-apply(induct i, auto simp: nth_append)
-done
-
lemma primerec_recs[intro]:
+ "primerec rec_trpl (Suc (Suc (Suc 0)))"
"primerec rec_newleft0 (Suc (Suc 0))"
"primerec rec_newleft1 (Suc (Suc 0))"
-"primerec rec_newleft2 (Suc (Suc 0))"
-"primerec rec_newleft3 ((Suc (Suc 0)))"
-"primerec rec_newleft (Suc (Suc (Suc 0)))"
-"primerec rec_left (Suc 0)"
-"primerec rec_actn (Suc (Suc (Suc 0)))"
-"primerec rec_stat (Suc 0)"
-"primerec rec_newstat (Suc (Suc (Suc 0)))"
+ "primerec rec_newleft2 (Suc (Suc 0))"
+ "primerec rec_newleft3 (Suc (Suc 0))"
+ "primerec rec_newleft (Suc (Suc (Suc 0)))"
+ "primerec rec_left (Suc 0)"
+ "primerec rec_actn (Suc (Suc (Suc 0)))"
+ "primerec rec_stat (Suc 0)"
+ "primerec rec_newstat (Suc (Suc (Suc 0)))"
apply(simp_all add: rec_newleft_def rec_embranch.simps rec_left_def rec_lo_def rec_entry_def
rec_actn_def Let_def arity.simps rec_newleft0_def rec_stat_def rec_newstat_def
- rec_newleft1_def rec_newleft2_def rec_newleft3_def)
+ rec_newleft1_def rec_newleft2_def rec_newleft3_def rec_trpl_def)
apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
@{thm prime_id}, @{thm prime_pr}] 1*};force)+
done
@@ -2951,12 +2830,6 @@
by(tactic {* resolve_tac @{context} [@{thm prime_cn},
@{thm prime_id}, @{thm prime_pr}] 1*};force)
-lemma primerec_rec_inpt[intro]: "0 < vl \<Longrightarrow> primerec (rec_inpt (Suc vl)) (Suc vl)"
-apply(simp add: rec_inpt_def)
-apply(tactic {* resolve_tac @{context} [@{thm prime_cn},
- @{thm prime_id}, @{thm prime_pr}] 1*}; fastforce elim:primerec_rec_strt primerec_map_vl)
-done
-
lemma primerec_rec_conf[intro]: "primerec rec_conf (Suc (Suc (Suc 0)))"
apply(simp add: rec_conf_def)
by(tactic {* resolve_tac @{context} [@{thm prime_cn},
@@ -3061,20 +2934,6 @@
"rec_F = Cn (Suc (Suc 0)) rec_valu [Cn (Suc (Suc 0)) rec_right [Cn (Suc (Suc 0))
rec_conf ([id (Suc (Suc 0)) 0, id (Suc (Suc 0)) (Suc 0), rec_halt])]]"
-lemma get_fstn_args_nth[simp]:
- "k < n \<Longrightarrow> (get_fstn_args m n ! k) = id m (k)"
-apply(induct n, simp)
-apply(case_tac "k = n", simp_all add: get_fstn_args.simps
- nth_append)
-done
-
-lemma get_fstn_args_is_id[simp]:
- "\<lbrakk>ys \<noteq> [];
- k < length ys\<rbrakk> \<Longrightarrow>
- (get_fstn_args (length ys) (length ys) ! k) =
- id (length ys) (k)"
-by(erule_tac get_fstn_args_nth)
-
lemma terminate_halt_lemma:
"\<lbrakk>rec_exec rec_nonstop ([m, r] @ [t]) = 0;
\<forall>i<t. 0 < rec_exec rec_nonstop ([m, r] @ [i])\<rbrakk> \<Longrightarrow> terminate rec_halt [m, r]"
@@ -3610,13 +3469,7 @@
next
show "l \<in> ?setx" by simp
qed
-qed
-
-lemma conf_decode2:
- "\<lbrakk>m \<noteq> n; m \<noteq> k; n \<noteq> k;
- \<not> Suc 0 < Pi m ^ l * Pi n ^ st * Pi k ^ r\<rbrakk> \<Longrightarrow> l = 0"
-apply(case_tac "Pi m ^ l * Pi n ^ st * Pi k ^ r", auto)
-done
+qed
lemma left_trpl_fst[simp]: "left (trpl l st r) = l"
apply(simp add: left.simps trpl.simps lo.simps loR.simps mod_dvd_simp)
@@ -3808,8 +3661,6 @@
lemma fetch_zero_zero[simp]: "fetch tp 0 b = (nact, ns) \<Longrightarrow> ns = 0"
by(simp add: fetch.simps)
-lemma Five_Suc: "5 = Suc 4" by simp
-
lemma modify_tprog_fetch_state:
"\<lbrakk>st \<le> length tp div 2; st > 0; b = 1 \<or> b = 0\<rbrakk> \<Longrightarrow>
modify_tprog tp ! Suc (4 * (st - Suc 0) + 2 * b) =
@@ -3900,9 +3751,6 @@
"\<lbrakk>a = a'; b = b'; c = c'\<rbrakk> \<Longrightarrow> trpl a b c = trpl a' b' c'"
by simp
-lemma bl2wc_Bk[simp]: "bl2wc [Bk] = 0"
-by(simp add: bl2wc.simps bl2nat.simps)
-
lemma bl2nat_double: "bl2nat xs (Suc n) = 2 * bl2nat xs n"
proof(induct xs arbitrary: n)
case Nil thus "?case"
@@ -4021,84 +3869,6 @@
done
qed
-lemma bl2nat_exp: "n \<noteq> 0 \<Longrightarrow> bl2nat bl n = 2^n * bl2nat bl 0"
-apply(induct bl)
-apply(auto simp: bl2nat.simps)
-apply(case_tac a, auto simp: bl2nat.simps bl2nat_double)
-done
-
-lemma nat_minus_eq: "\<lbrakk>a = b; c = d\<rbrakk> \<Longrightarrow> a - c = b - d"
-by auto
-
-lemma tape_of_nat_list_butlast_last:
- "ys \<noteq> [] \<Longrightarrow> <ys @ [y]> = <ys> @ Bk # Oc\<up>Suc y"
-apply(induct ys, simp, simp)
-apply(case_tac "ys = []", simp add: tape_of_list_def tape_of_nat_def)
-apply(simp add: tape_of_nl_cons tape_of_nat_def)
-done
-
-lemma listsum2_append:
- "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> listsum2 (xs @ ys) n = listsum2 xs n"
-apply(induct n)
-apply(auto simp: listsum2.simps nth_append)
-done
-
-lemma strt'_append:
- "\<lbrakk>n \<le> length xs\<rbrakk> \<Longrightarrow> strt' xs n = strt' (xs @ ys) n"
-proof(induct n arbitrary: xs ys)
- fix xs ys
- show "strt' xs 0 = strt' (xs @ ys) 0" by(simp add: strt'.simps)
-next
- fix n xs ys
- assume ind:
- "\<And> xs ys. n \<le> length xs \<Longrightarrow> strt' xs n = strt' (xs @ ys) n"
- and h: "Suc n \<le> length (xs::nat list)"
- show "strt' xs (Suc n) = strt' (xs @ ys) (Suc n)"
- using ind[of xs ys] h
- apply(simp add: strt'.simps nth_append listsum2_append)
- done
-qed
-
-lemma length_listsum2_eq:
- "\<lbrakk>length (ys::nat list) = k\<rbrakk>
- \<Longrightarrow> length (<ys>) = listsum2 (map Suc ys) k + k - 1"
-apply(induct k arbitrary: ys, simp_all add: listsum2.simps)
-apply(subgoal_tac "\<exists> xs x. ys = xs @ [x]", auto)
-proof -
- fix xs x
- assume ind: "\<And>ys. length ys = length xs \<Longrightarrow> length (<ys>)
- = listsum2 (map Suc ys) (length xs) +
- length (xs::nat list) - Suc 0"
- have "length (<xs>)
- = listsum2 (map Suc xs) (length xs) + length xs - Suc 0"
- apply(rule_tac ind, simp)
- done
- thus "length (<xs @ [x]>) =
- Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
- apply(case_tac "xs = []")
- apply(simp add: tape_of_list_def listsum2.simps
- tape_of_nat_list.simps tape_of_nat_def)
- apply(simp add: tape_of_nat_list_butlast_last)
- using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
- apply(simp)
- done
-next
- fix k ys
- assume "length ys = Suc k"
- thus "\<exists>xs x. ys = xs @ [x]"
- apply(rule_tac x = "butlast ys" in exI,
- rule_tac x = "last ys" in exI)
- apply(case_tac ys, auto)
- done
-qed
-
-lemma tape_of_nat_list_length:
- "length (<(ys::nat list)>) =
- listsum2 (map Suc ys) (length ys) + length ys - 1"
- using length_listsum2_eq[of ys "length ys"]
- apply(simp)
- done
-
lemma trpl_code_simp[simp]:
"trpl_code (steps0 (Suc 0, Bk\<up>l, <lm>) tp 0) =
rec_exec rec_conf [code tp, bl2wc (<lm>), 0]"
@@ -4451,7 +4221,6 @@
"\<lbrakk>steps0 (Suc 0, Bk\<up>l, <lm>) tp stp = (0, Bk\<up>m, Oc\<up>rs@Bk\<up>n);
tm_wf (tp,0); 0<rs\<rbrakk>
\<Longrightarrow> rec_exec rec_F [code tp, (bl2wc (<lm>))] = (rs - Suc 0)"
-thm halt_least_step nonstop_t_eq nonstop_lemma rec_t_eq_steps conf_lemma
apply(frule_tac halt_least_step, auto)
apply(frule_tac nonstop_t_eq, auto simp: nonstop_lemma)
using rec_t_eq_steps[of tp l lm stp]
@@ -4485,4 +4254,6 @@
qed
qed
+unused_thms
+
end
\ No newline at end of file