# HG changeset patch
# User Sebastiaan Joosten <sebastiaan.joosten@uibk.ac.at>
# Date 1545234430 -3600
# Node ID 4e50ff17734836e7b67578ebb1aef26060267bed
# Parent  a9003e6d046325e4eb27c9360e7a9af9975aa1e6
Cleanup in UF

diff -r a9003e6d0463 -r 4e50ff177348 thys/UF.thy
--- 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