diff -r 6013ca0e6e22 -r eccd79a974ae thys/Abacus.thy
--- a/thys/Abacus.thy	Wed Feb 13 20:08:14 2013 +0000
+++ b/thys/Abacus.thy	Thu Feb 14 09:31:19 2013 +0000
@@ -1082,11 +1082,11 @@
   where "inv_stop (as, lm) (s, l, r) ires= 
               (\<exists> rn. l = Bk # Bk # ires \<and> r = <lm> @  Bk\<up>rn)"
 
-
 lemma halt_lemma2': 
   "\<lbrakk>wf LE;  \<forall> n. ((\<not> P (f n) \<and> Q (f n)) \<longrightarrow> 
     (Q (f (Suc n)) \<and> (f (Suc n), (f n)) \<in> LE)); Q (f 0)\<rbrakk> 
       \<Longrightarrow> \<exists> n. P (f n)"
+
 apply(intro exCI, simp)
 apply(subgoal_tac "\<forall> n. Q (f n)", simp)
 apply(drule_tac f = f in wf_inv_image)
@@ -1162,7 +1162,7 @@
    "findnth_LE \<equiv> (inv_image lex_pair findnth_measure)"
 
 lemma wf_findnth_LE: "wf findnth_LE"
-by(auto intro:wf_inv_image simp: findnth_LE_def lex_pair_def)
+by(auto simp: findnth_LE_def lex_pair_def)
 
 declare findnth_inv.simps[simp del]
 
@@ -1318,20 +1318,6 @@
 apply(case_tac mr, simp_all, auto)
 done
 
-(*
-lemma zero_and_nil[intro]: "(Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup> @ Bk # <lm::nat list> @ 
-                             Bk\<^bsup>rn \<^esup>) \<or> (lm2 = [] \<and> Bk # Bk\<^bsup>n\<^esup> = Oc\<^bsup>mr\<^esup>)
-       \<Longrightarrow> mr = 0 \<and> lm = []"
-apply(rule context_conjI)
-apply(case_tac mr, auto simp:exponent_def)
-apply(insert BkCons_nil[of "replicate (n - 1) Bk" lm rn])
-apply(case_tac n, auto simp: exponent_def Bk_def  tape_of_nl_nil_eq)
-done
-
-lemma tape_of_nat_def: "<[m::nat]> =  Oc # Oc\<^bsup>m\<^esup>"
-apply(simp add: tape_of_nl_abv tape_of_nat_list.simps)
-done
-*)
 lemma [simp]:  "<[x::nat]> = Oc\<up>(Suc x)"
 apply(simp add: tape_of_nat_abv tape_of_nl_abv)
 done
@@ -4454,20 +4440,20 @@
            else if s = 2*n + 4 then 2
            else 0)"
 
-fun abc_mopup_measure :: "(config \<times> nat) \<Rightarrow> (nat \<times> nat \<times> nat)"
-  where
-  "abc_mopup_measure (c, n) = 
-    (abc_mopup_stage1 c n, abc_mopup_stage2 c n, 
-                                       abc_mopup_stage3 c n)"
-
-definition abc_mopup_LE ::
-   "(((nat \<times> cell list \<times> cell list) \<times> nat) \<times> 
-    ((nat \<times> cell list \<times> cell list) \<times> nat)) set"
-  where
-  "abc_mopup_LE \<equiv> (inv_image lex_triple abc_mopup_measure)"
-
-lemma wf_abc_mopup_le[intro]: "wf abc_mopup_LE"
-by(auto intro:wf_inv_image simp:abc_mopup_LE_def lex_triple_def lex_pair_def)
+definition
+  "abc_mopup_measure = measures [\<lambda>(c, n). abc_mopup_stage1 c n, 
+                                 \<lambda>(c, n). abc_mopup_stage2 c n, 
+                                 \<lambda>(c, n). abc_mopup_stage3 c n]"
+
+lemma wf_abc_mopup_measure:
+  shows "wf abc_mopup_measure" 
+unfolding abc_mopup_measure_def 
+by auto
+
+lemma abc_mopup_measure_induct [case_names Step]: 
+  "\<lbrakk>\<And>n. \<not> P (f n) \<Longrightarrow> (f (Suc n), (f n)) \<in> abc_mopup_measure\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
+using wf_abc_mopup_measure
+by (metis wf_iff_no_infinite_down_chain)
 
 lemma [simp]: "mopup_bef_erase_a (a, aa, []) lm n ires = False"
 apply(auto simp: mopup_bef_erase_a.simps)
@@ -4494,12 +4480,6 @@
 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"
@@ -4507,39 +4487,35 @@
   and f: "f = (\<lambda> stp. (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) stp, n))"
   and P: "P = (\<lambda> (c, n). is_final c)"
   shows "\<exists> stp. P (f stp)"
-proof(rule_tac LE = abc_mopup_LE in halt_lemma)
-  show "wf abc_mopup_LE" by(auto)
-next
-  show "\<forall>n. \<not> P (f n) \<longrightarrow> (f (Suc n), f n) \<in> abc_mopup_LE"
-  proof(rule_tac allI, rule_tac impI)
-    fix na
-    assume h: "\<not> P (f na)"
-    show "(f (Suc na), f na) \<in> abc_mopup_LE"
-    proof(simp add: f)
-      obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"
-        apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
-        done
-      then have "mopup_inv (a, b, c) lm n ires"
-        using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
-        apply(simp)
-        done
-      moreover have "a > 0"
-        using h g
-        apply(simp add: f P)
-        done
-      ultimately have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_LE"
-        apply(case_tac c, case_tac [2] aa)
-        apply(auto split:if_splits simp add:step.simps mopup_inv.simps)
-        apply(simp_all add: mopupfetchs abc_mopup_LE_def lex_triple_def lex_pair_def )
-        done
-      thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) 
-        (mopup_a n @ shift mopup_b (2 * n), 0), n),
-        steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
-        \<in> abc_mopup_LE"
-        using g by simp
-    qed
+proof (induct rule: abc_mopup_measure_induct) 
+  case (Step na)
+  have h: "\<not> P (f na)" by fact
+  show "(f (Suc na), f na) \<in> abc_mopup_measure"
+  proof(simp add: f)
+    obtain a b c where g:"steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na = (a, b, c)"
+      apply(case_tac "steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na", auto)
+      done
+    then have "mopup_inv (a, b, c) lm n ires"
+      using inv less mopup_inv_steps[of n lm "Suc 0" l r ires na]
+      apply(simp)
+      done
+    moreover have "a > 0"
+      using h g
+      apply(simp add: f P)
+      done
+    ultimately 
+    have "((step (a, b, c) (mopup_a n @ shift mopup_b (2 * n), 0), n), (a, b, c), n) \<in> abc_mopup_measure"
+      apply(case_tac c, case_tac [2] aa)
+      apply(auto split:if_splits simp add:step.simps mopup_inv.simps)
+      apply(simp_all add: mopupfetchs abc_mopup_measure_def lex_triple_def lex_pair_def )
+      done
+    thus "((step (steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na) 
+      (mopup_a n @ shift mopup_b (2 * n), 0), n),
+      steps (Suc 0, l, r) (mopup_a n @ shift mopup_b (2 * n), 0) na, n)
+      \<in> abc_mopup_measure"
+      using g by simp
   qed
-qed     
+qed
 
 lemma mopup_inv_start: 
   "n < length am \<Longrightarrow> mopup_inv (Suc 0, Bk # Bk # ires, <am> @ Bk \<up> k) am n ires"
@@ -4689,44 +4665,45 @@
 lemma compile_correct_unhalt: 
   assumes layout: "ly = layout_of ap"
   and compile: "tp = tm_of ap"
-  and crsp: "crsp ly (0, lm) (Suc 0, l, r) ires"
+  and crsp: "crsp ly (0, lm) (1, l, r) ires"
   and off: "off = length tp div 2"
   and abc_unhalt: "\<forall> stp. (\<lambda> (as, am). as < length ap) (abc_steps_l (0, lm) ap stp)"
-  shows "\<forall> stp.\<not> is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)"
+  shows "\<forall> stp.\<not> is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)"
 using assms
 proof(rule_tac allI, rule_tac notI)
   fix stp
-  assume h: "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp)"
+  assume h: "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stp)"
   obtain as am where a: "abc_steps_l (0, lm) ap stp = (as, am)"
     by(case_tac "abc_steps_l (0, lm) ap stp", auto)
   then have b: "as < length ap"
     using abc_unhalt
     by(erule_tac x = stp in allE, simp)
-  have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires "
+  have "\<exists> stpa\<ge>stp. crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires "
     using assms b a
-    apply(rule_tac crsp_steps2, simp_all)
+    apply(simp add: numeral)
+    apply(rule_tac crsp_steps2)
+    apply(simp_all)
     done
-  then obtain stpa where
-    "stpa\<ge>stp \<and> crsp ly (as, am) (steps (Suc 0, l, r) (tp, 0) stpa) ires" ..
-  then obtain s' l' r' where b: "(steps (Suc 0, l, r) (tp, 0) stpa) = (s', l', r') \<and> 
+  then obtain stpa where 
+    "stpa\<ge>stp \<and> crsp ly (as, am) (steps (1, l, r) (tp, 0) stpa) ires" ..
+  then obtain s' l' r' where b: "(steps (1, l, r) (tp, 0) stpa) = (s', l', r') \<and> 
        stpa\<ge>stp \<and> crsp ly (as, am) (s', l', r') ires"
-    by(case_tac "steps (Suc 0, l, r) (tp, 0) stpa", auto)
+    by(case_tac "steps (1, l, r) (tp, 0) stpa", auto)
   hence c:
-    "(steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')"
+    "(steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa) = (s', l', r')"
     by(rule_tac tm_append_first_steps_eq, simp_all add: crsp.simps)
   from b have d: "s' > 0 \<and> stpa \<ge> stp"
     by(simp add: crsp.simps)
   then obtain diff where e: "stpa = stp + diff"   by (metis le_iff_add)
   obtain s'' l'' r'' where f:
-    "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
+    "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp = (s'', l'', r'') \<and> is_final (s'', l'', r'')"
     using h
-    by(case_tac "steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stp", auto)
+    by(case_tac "steps (1, l, r) (tp @ shift (mopup n) off, 0) stp", auto)
 
   then have "is_final (steps (s'', l'', r'') (tp @ shift (mopup n) off, 0) diff)"
     by(auto intro: after_is_final)
-  then have "is_final (steps (Suc 0, l, r) (tp @ shift (mopup n) off, 0) stpa)"
-    using e
-    by(simp add: steps_add f)
+  then have "is_final (steps (1, l, r) (tp @ shift (mopup n) off, 0) stpa)"
+    using e f by simp
   from this and c d show "False" by simp
 qed