Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
theories
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 30 Jan 2013 09:33:06 +0000
changeset 101 06db15939b7c
parent 100 dfe852aacae6
child 102 cdef5b1072fe
theories
ROOT.ML file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions
thys/UF.thy file | annotate | diff | comparison | revisions
thys/abacus.thy file | annotate | diff | comparison | revisions 
--- a/ROOT.ML	Wed Jan 30 03:46:22 2013 +0000
+++ b/ROOT.ML	Wed Jan 30 09:33:06 2013 +0000
@@ -14,8 +14,8 @@
 no_document 
 use_thys ["thys/turing_basic",
           "thys/turing_hoare", 
-	  "thys/uncomputable"(*, 
+	  "thys/uncomputable", 
 	  "thys/abacus", 
 	  "thys/rec_def", 
 	  "thys/recursive",
-          "thys/UF"*)]
+          "thys/UF"]
Binary file paper.pdf has changed
--- a/thys/UF.thy	Wed Jan 30 03:46:22 2013 +0000
+++ b/thys/UF.thy	Wed Jan 30 09:33:06 2013 +0000
@@ -4473,9 +4473,9 @@
 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_nl_abv 
+apply(case_tac "ys = []", simp add: tape_of_nl_abv tape_of_nat_abv
                                     tape_of_nat_list.simps)
-apply(simp add: tape_of_nl_cons)
+apply(simp add: tape_of_nl_cons tape_of_nat_abv)
 done
 
 lemma listsum2_append:
@@ -4518,7 +4518,7 @@
     Suc (listsum2 (map Suc xs @ [Suc x]) (length xs) + x + length xs)"
     apply(case_tac "xs = []")
     apply(simp add: tape_of_nl_abv listsum2.simps 
-      tape_of_nat_list.simps)
+      tape_of_nat_list.simps tape_of_nat_abv)
     apply(simp add: tape_of_nat_list_butlast_last)
     using listsum2_append[of "length xs" "map Suc xs" "[Suc x]"]
     apply(simp)
--- a/thys/abacus.thy	Wed Jan 30 03:46:22 2013 +0000
+++ b/thys/abacus.thy	Wed Jan 30 09:33:06 2013 +0000
@@ -1330,7 +1330,7 @@
 
 lemma tape_of_nl_cons: "<m # lm> = (if lm = [] then Oc\<up>(Suc m)
                     else Oc\<up>(Suc m) @ Bk # <lm>)"
-apply(case_tac lm, simp_all add: tape_of_nl_abv  split: if_splits)
+apply(case_tac lm, simp_all add: tape_of_nl_abv  tape_of_nat_abv split: if_splits)
 done
 
 
@@ -1952,7 +1952,7 @@
 apply(auto simp: inv_on_left_moving_in_middle_B.simps 
                  inv_check_left_moving_on_leftmost.simps split: if_splits)
 apply(case_tac [!] "rev lm1", simp_all)
-apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] lista, simp_all add: tape_of_nl_abv tape_of_nat_abv tape_of_nat_list.simps)
 done
 
 lemma [simp]:
@@ -2020,11 +2020,11 @@
 apply(erule_tac exE)+
 apply(rule_tac x = "rev (tl (rev lm1))" in exI, 
       rule_tac x = "[hd (rev lm1)] @ lm2" in exI, auto)
-apply(case_tac [!] "rev lm1",simp_all add: tape_of_nl_abv tape_of_nat_list.simps)
+apply(case_tac [!] "rev lm1",simp_all add: tape_of_nat_abv tape_of_nl_abv tape_of_nat_list.simps)
 apply(case_tac [!] a, simp_all)
-apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps, auto)
-apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps, auto)
-apply(case_tac [!] lista, simp_all add: tape_of_nat_list.simps)
+apply(case_tac [1] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [3] lm2, simp_all add: tape_of_nat_list.simps tape_of_nat_abv, auto)
+apply(case_tac [!] lista, simp_all add: tape_of_nat_abv tape_of_nat_list.simps)
 done
 
 lemma [simp]: 
@@ -4295,8 +4295,8 @@
 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
 apply(subgoal_tac "length list = Suc q", auto)
 apply(subgoal_tac "drop q list = [list ! q]")
-apply(simp add: tape_of_nl_abv)
-by (metis append_Nil2 append_eq_conv_conj lessI nth_drop')
+apply(simp add: tape_of_nl_abv tape_of_nat_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI)
 
 lemma erase2jumpover2:
   "\<lbrakk>q < length list; \<forall>rn. <drop q list> @ Bk # Bk \<up> n \<noteq>
@@ -4307,9 +4307,8 @@
 apply(erule_tac notE)
 apply(rule_tac drop_tape_of_cons, simp_all add: abc_lm_v.simps)
 apply(subgoal_tac "length list = Suc q", auto)
-apply(erule_tac x = "n" in allE, simp)
-by (metis append_Nil2 append_eq_conv_conj lessI nth_drop'
-  replicate_Suc tape_of_nat_list.simps(2) tape_of_nl_abv) 
+apply(erule_tac x = "n" in allE, simp add: tape_of_nl_abv)
+by (metis append_Nil2 append_eq_conv_conj drop_Suc_conv_tl lessI replicate_Suc tape_of_nl_abv tape_of_nl_cons)
 
 lemma mopup_bef_erase_a_2_jump_over[simp]: 
  "\<lbrakk>n < length lm; 0 < s; s mod 2 = Suc 0;  s \<le> 2 * n;
@@ -4725,6 +4724,12 @@
 apply(rule mopup_a_nth, auto)
 done
 
+(* FIXME: is also in uncomputable *)
+lemma halt_lemma: 
+  "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+by (metis wf_iff_no_infinite_down_chain)
+
+
 lemma mopup_halt:
   assumes 
   less: "n < length lm"
tm