--- 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