--- a/thys/Uncomputable.thy Fri Dec 21 12:31:36 2018 +0100
+++ b/thys/Uncomputable.thy Fri Dec 21 15:30:24 2018 +0100
@@ -77,7 +77,7 @@
if s = 4 then inv_begin4 n tp
else False)"
-lemma [elim]: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
+lemma inv_begin_step_E: "\<lbrakk>0 < i; 0 < j\<rbrakk> \<Longrightarrow>
\<exists>ia>0. ia + j - Suc 0 = i + j \<and> Oc # Oc \<up> i = Oc \<up> ia"
by (rule_tac x = "Suc i" in exI, simp)
@@ -88,7 +88,7 @@
using assms
unfolding tcopy_begin_def
apply(cases cf)
-apply(auto simp: numeral split: if_splits)
+apply(auto simp: numeral split: if_splits elim:inv_begin_step_E)
apply(case_tac "hd c")
apply(auto)
apply(case_tac c)
@@ -239,75 +239,52 @@
inv_loop4.simps[simp del] inv_loop5.simps[simp del]
inv_loop6.simps[simp del]
-lemma [elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
+lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc \<up> t \<Longrightarrow> RR"
by (case_tac t, auto)
-lemma [simp]: "inv_loop1 x (b, []) = False"
-by (simp add: inv_loop1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+lemma inv_loop3_Bk_empty_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop2.simps inv_loop3.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
+lemma inv_loop3_Bk_empty[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, [])"
by (auto simp: inv_loop3.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
+lemma inv_loop5_Oc_empty_via_4[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, [])\<rbrakk> \<Longrightarrow> inv_loop5 x (b, [Oc])"
apply(auto simp: inv_loop4.simps inv_loop5.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = "Suc j" in exI, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], [])\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, []); b \<noteq> []\<rbrakk> \<Longrightarrow> RR"
-by (auto simp: inv_loop4.simps inv_loop5.simps)
-
-lemma [elim]: "inv_loop6 x ([], []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "inv_loop6 x (b, []) \<Longrightarrow> RR"
-by (auto simp: inv_loop6.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+lemma inv_loop1_Bk[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
by (auto simp: inv_loop1.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> list = Oc # Bk \<up> x @ Oc \<up> x"
-by (auto simp: inv_loop1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+lemma inv_loop3_Bk_via_2[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop2.simps inv_loop3.simps)
apply(rule_tac [!] x = i in exI, rule_tac [!] x = j in exI, simp_all)
done
-lemma [elim]: "Bk # list = Oc \<up> j \<Longrightarrow> RR"
-by (case_tac j, simp_all)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
+lemma inv_loop3_Bk_move[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop3 x (Bk # b, list)"
apply(auto simp: inv_loop3.simps)
apply(rule_tac [!] x = i in exI,
rule_tac [!] x = j in exI, simp_all)
apply(case_tac [!] t, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
+lemma inv_loop5_Oc_via_4_Bk[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_loop5 x (b, Oc # list)"
by (auto simp: inv_loop4.simps inv_loop5.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+lemma inv_loop6_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
by (auto simp: inv_loop6.simps inv_loop5.simps)
-lemma [simp]: "inv_loop5_loop x (b, Bk # list) = False"
+lemma inv_loop5_loop_no_Bk[simp]: "inv_loop5_loop x (b, Bk # list) = False"
by (auto simp: inv_loop5.simps)
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
+lemma inv_loop6_exit_no_Bk[simp]: "inv_loop6_exit x (b, Bk # list) = False"
by (auto simp: inv_loop6.simps)
declare inv_loop5_loop.simps[simp del] inv_loop5_exit.simps[simp del]
inv_loop6_loop.simps[simp del] inv_loop6_exit.simps[simp del]
-lemma [elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop6_loopBk_via_5[elim]:"\<lbrakk>0 < x; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_loop.simps )
apply(erule_tac exE)+
@@ -319,10 +296,10 @@
apply(case_tac [!] nat, simp_all)
done
-lemma [simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
+lemma inv_loop6_loop_no_Oc_Bk[simp]: "inv_loop6_loop x (b, Oc # Bk # list) = False"
by (auto simp: inv_loop6_loop.simps)
-lemma [elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
+lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "\<lbrakk>x > 0; inv_loop5_exit x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop5_exit.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
@@ -331,24 +308,12 @@
apply(case_tac [!] nat, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail_via_5[elim]: "\<lbrakk>0 < x; inv_loop5 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop5.simps inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [simp]: "inv_loop6 x ([], Bk # xs) = False"
-apply(simp add: inv_loop6.simps inv_loop6_loop.simps
- inv_loop6_exit.simps)
-apply(auto)
-done
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
-by (simp)
-
-lemma [simp]: "inv_loop6_exit x (b, Bk # list) = False"
-by (simp add: inv_loop6_exit.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop6_loop_Bk_Bk_drop[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop6_loop x (tl b, Bk # Bk # list)"
apply(simp only: inv_loop6_loop.simps)
apply(erule_tac exE)+
@@ -357,7 +322,7 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
+lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "\<lbrakk>0 < x; inv_loop6_loop x (b, Bk # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop6_exit x (tl b, Oc # Bk # list)"
apply(simp only: inv_loop6_loop.simps inv_loop6_exit.simps)
apply(erule_tac exE)+
@@ -365,20 +330,20 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
+lemma inv_loop6_Bk_tail[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop6 x (tl b, hd b # Bk # list)"
apply(simp add: inv_loop6.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
+lemma inv_loop2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_loop1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (Oc # b, list)"
apply(auto simp: inv_loop1.simps inv_loop2.simps)
apply(rule_tac x = "Suc i" in exI, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
+lemma inv_loop2_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_loop2 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop2 x (b, Bk # list)"
by (auto simp: inv_loop2.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+lemma inv_loop4_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_loop3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop3.simps inv_loop4.simps)
apply(rule_tac [!] x = i in exI, auto)
apply(rule_tac [!] x = "Suc 0" in exI, rule_tac [!] x = "j - 1" in exI, auto)
@@ -386,20 +351,17 @@
apply(case_tac [!] j, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
+lemma inv_loop4_Oc_move[elim]: "\<lbrakk>0 < x; inv_loop4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_loop4 x (Oc # b, list)"
apply(auto simp: inv_loop4.simps)
apply(rule_tac [!] x = "i" in exI, auto)
apply(rule_tac [!] x = "Suc k" in exI, rule_tac [!] x = "t - 1" in exI, auto)
apply(case_tac [!] t, simp_all)
done
-lemma [simp]: "inv_loop5 x ([], list) = False"
-by (auto simp: inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps)
-
-lemma [simp]: "inv_loop5_exit x (b, Oc # list) = False"
+lemma inv_loop5_exit_no_Oc[simp]: "inv_loop5_exit x (b, Oc # list) = False"
by (auto simp: inv_loop5_exit.simps)
-lemma [elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
+lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " \<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk>
\<Longrightarrow> inv_loop5_exit x (tl b, Bk # Oc # list)"
apply(simp only: inv_loop5_loop.simps inv_loop5_exit.simps)
apply(erule_tac exE)+
@@ -407,7 +369,7 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
+lemma inv_loop5_loop_Oc_Oc_drop[elim]: "\<lbrakk>inv_loop5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk>
\<Longrightarrow> inv_loop5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_loop5_loop.simps)
apply(erule_tac exE)+
@@ -416,21 +378,43 @@
apply(case_tac [!] k, auto)
done
-lemma [elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
+lemma inv_loop5_Oc_tl[elim]: "\<lbrakk>inv_loop5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow> inv_loop5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_loop5.simps)
apply(case_tac "hd b", simp_all, auto)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
+lemma inv_loop1_Bk_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_loop1 x ([], Bk # Oc # list)"
+apply(auto simp: inv_loop6.simps inv_loop1.simps
+ inv_loop6_loop.simps inv_loop6_exit.simps)
+done
+
+lemma inv_loop1_Oc_via_6[elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
+ \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_loop6.simps inv_loop1.simps
inv_loop6_loop.simps inv_loop6_exit.simps)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_loop6 x (b, Oc # list); b \<noteq> []\<rbrakk>
- \<Longrightarrow> inv_loop1 x (tl b, hd b # Oc # list)"
-apply(auto simp: inv_loop6.simps inv_loop1.simps
- inv_loop6_loop.simps inv_loop6_exit.simps)
-done
+
+lemma inv_loop_nonempty[simp]:
+ "inv_loop1 x (b, []) = False"
+ "inv_loop2 x ([], b) = False"
+ "inv_loop2 x (l', []) = False"
+ "inv_loop3 x (b, []) = False"
+ "inv_loop4 x ([], b) = False"
+ "inv_loop5 x ([], list) = False"
+ "inv_loop6 x ([], Bk # xs) = False"
+ by (auto simp: inv_loop1.simps inv_loop2.simps inv_loop3.simps inv_loop4.simps
+ inv_loop5.simps inv_loop6.simps inv_loop5_exit.simps inv_loop5_loop.simps
+ inv_loop6_loop.simps)
+
+lemma inv_loop_nonemptyE[elim]:
+ "\<lbrakk>inv_loop5 x (b, [])\<rbrakk> \<Longrightarrow> RR" "inv_loop6 x (b, []) \<Longrightarrow> RR"
+ "\<lbrakk>inv_loop1 x (b, Bk # list)\<rbrakk> \<Longrightarrow> b = []"
+ by (auto simp: inv_loop4.simps inv_loop5.simps inv_loop5_exit.simps inv_loop5_loop.simps
+ inv_loop6.simps inv_loop6_exit.simps inv_loop6_loop.simps inv_loop1.simps)
+
+lemma inv_loop6_Bk_Bk_drop[elim]: "\<lbrakk>inv_loop6 x ([], Bk # list)\<rbrakk> \<Longrightarrow> inv_loop6 x ([], Bk # Bk # list)"
+ by (simp)
lemma inv_loop_step:
"\<lbrakk>inv_loop x cf; x > 0\<rbrakk> \<Longrightarrow> inv_loop x (step cf (tcopy_loop, 0))"
@@ -476,39 +460,19 @@
using wf_measure_loop
by (metis wf_iff_no_infinite_down_chain)
-
-
-lemma [simp]: "inv_loop2 x ([], b) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop2 x (l', []) = False"
-by (auto simp: inv_loop2.simps)
-
-lemma [simp]: "inv_loop3 x (b, []) = False"
-by (auto simp: inv_loop3.simps)
-
-lemma [simp]: "inv_loop4 x ([], b) = False"
-by (auto simp: inv_loop4.simps)
-
-
-lemma [elim]:
- "\<lbrakk>inv_loop4 x (l', []); l' \<noteq> []; x > 0;
+lemma inv_loop4_not_just_Oc[elim]:
+ "\<lbrakk>inv_loop4 x (l', []);
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l'))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\<lambda>a. a = Oc) (rev l'))"
+ \<Longrightarrow> RR"
+ "\<lbrakk>inv_loop4 x (l', Bk # list);
+ length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
+ length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop4.simps)
apply(case_tac [!] j, simp_all add: List.takeWhile_tail)
done
-
-lemma [elim]:
- "\<lbrakk>inv_loop4 x (l', Bk # list); l' \<noteq> []; 0 < x;
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) \<noteq>
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
-by (auto simp: inv_loop4.simps)
-
lemma takeWhile_replicate_append:
"P a \<Longrightarrow> takeWhile P (a\<up>x @ ys) = a\<up>x @ takeWhile P ys"
by (induct x, auto)
@@ -517,12 +481,11 @@
"P a \<Longrightarrow> takeWhile P (a\<up>x) = a\<up>x"
by (induct x, auto)
-lemma [elim]:
- "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_Bk_E[elim]:
+ "\<lbrakk>inv_loop5 x (l', Bk # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop5.simps inv_loop5_exit.simps)
apply(case_tac [!] j, simp_all)
apply(case_tac [!] "nat", simp_all)
@@ -531,21 +494,20 @@
apply(case_tac nata, simp_all add: List.takeWhile_tail)
done
-lemma [elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
+lemma inv_loop1_hd_Oc[elim]: "\<lbrakk>inv_loop1 x (l', Oc # list)\<rbrakk> \<Longrightarrow> hd list = Oc"
by (auto simp: inv_loop1.simps)
-lemma [elim]:
- "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_not_just_Bk[elim]:
+ "\<lbrakk>inv_loop6 x (l', Bk # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop6.simps)
apply(case_tac l', simp_all)
done
-lemma [elim]:
- "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []; 0 < x\<rbrakk> \<Longrightarrow>
+lemma inv_loop2_OcE[elim]:
+ "\<lbrakk>inv_loop2 x (l', Oc # list); l' \<noteq> []\<rbrakk> \<Longrightarrow>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Bk # list)) <
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
apply(auto simp: inv_loop2.simps)
@@ -553,22 +515,20 @@
takeWhile_replicate)
done
-lemma [elim]:
- "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop5_OcE[elim]:
+ "\<lbrakk>inv_loop5 x (l', Oc # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \<noteq>
length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+ \<Longrightarrow> RR"
apply(auto simp: inv_loop5.simps)
apply(case_tac l', auto)
done
-lemma[elim]:
- "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> []; 0 < x;
+lemma inv_loop6_OcE[elim]:
+ "\<lbrakk>inv_loop6 x (l', Oc # list); l' \<noteq> [];
length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list))
\<noteq> length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))\<rbrakk>
- \<Longrightarrow> length (takeWhile (\<lambda>a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) <
- length (takeWhile (\<lambda>a. a = Oc) (rev l' @ Oc # list))"
+ \<Longrightarrow> RR"
apply(case_tac l')
apply(auto simp: inv_loop6.simps)
done
@@ -668,29 +628,21 @@
inv_end3.simps[simp del] inv_end4.simps[simp del]
inv_end5.simps[simp del]
-lemma [simp]: "inv_end1 x (b, []) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [simp]: "inv_end2 x (b, []) = False"
-by (auto simp: inv_end2.simps)
-
-lemma [simp]: "inv_end3 x (b, []) = False"
-by (auto simp: inv_end3.simps)
+lemma inv_end_nonempty[simp]:
+ "inv_end1 x (b, []) = False"
+ "inv_end1 x ([], list) = False"
+ "inv_end2 x (b, []) = False"
+ "inv_end3 x (b, []) = False"
+ "inv_end4 x (b, []) = False"
+ "inv_end5 x (b, []) = False"
+ "inv_end5 x ([], Oc # list) = False"
+by (auto simp: inv_end1.simps inv_end2.simps inv_end3.simps inv_end4.simps inv_end5.simps)
-lemma [simp]: "inv_end4 x (b, []) = False"
-by (auto simp: inv_end4.simps)
-
-lemma [simp]: "inv_end5 x (b, []) = False"
-by (auto simp: inv_end5.simps)
-
-lemma [simp]: "inv_end1 x ([], list) = False"
-by (auto simp: inv_end1.simps)
-
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
+lemma inv_end0_Bk_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Bk # list); b \<noteq> []\<rbrakk>
\<Longrightarrow> inv_end0 x (tl b, hd b # Bk # list)"
by (auto simp: inv_end1.simps inv_end0.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
+lemma inv_end3_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Bk # list)\<rbrakk>
\<Longrightarrow> inv_end3 x (b, Oc # list)"
apply(auto simp: inv_end2.simps inv_end3.simps)
apply(rule_tac x = "j - 1" in exI)
@@ -698,65 +650,65 @@
apply(case_tac x, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
+lemma inv_end2_Bk_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Bk # b, list)"
by (auto simp: inv_end2.simps inv_end3.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Bk_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x ([], Bk # list)\<rbrakk> \<Longrightarrow>
inv_end5 x ([], Bk # Bk # list)"
by (auto simp: inv_end4.simps inv_end5.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Bk_tail_via_4[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Bk # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Bk # list)"
apply(auto simp: inv_end4.simps inv_end5.simps)
apply(rule_tac x = 1 in exI, simp)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
+lemma inv_end0_Bk_via_5[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Bk # list)\<rbrakk> \<Longrightarrow> inv_end0 x (Bk # b, list)"
apply(auto simp: inv_end5.simps inv_end0.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_1[elim]: "\<lbrakk>0 < x; inv_end1 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
by (auto simp: inv_end1.simps inv_end2.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Bk_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x ([], Oc # list)\<rbrakk> \<Longrightarrow>
inv_end4 x ([], Bk # Oc # list)"
by (auto simp: inv_end2.simps inv_end4.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end4_Oc_via_2[elim]: "\<lbrakk>0 < x; inv_end2 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end4 x (tl b, hd b # Oc # list)"
apply(auto simp: inv_end2.simps inv_end4.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
+lemma inv_end2_Oc_via_3[elim]: "\<lbrakk>0 < x; inv_end3 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end2 x (Oc # b, list)"
by (auto simp: inv_end2.simps inv_end3.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
+lemma inv_end4_Bk_via_Oc[elim]: "\<lbrakk>0 < x; inv_end4 x (b, Oc # list)\<rbrakk> \<Longrightarrow> inv_end4 x (b, Bk # list)"
by (auto simp: inv_end2.simps inv_end4.simps)
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
+lemma inv_end5_Bk_drop_Oc[elim]: "\<lbrakk>0 < x; inv_end5 x ([], Oc # list)\<rbrakk> \<Longrightarrow> inv_end5 x ([], Bk # Oc # list)"
by (auto simp: inv_end2.simps inv_end5.simps)
declare inv_end5_loop.simps[simp del]
inv_end5_exit.simps[simp del]
-lemma [simp]: "inv_end5_exit x (b, Oc # list) = False"
+lemma inv_end5_exit_no_Oc[simp]: "inv_end5_exit x (b, Oc # list) = False"
by (auto simp: inv_end5_exit.simps)
-lemma [simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
+lemma inv_end5_loop_no_Bk_Oc[simp]: "inv_end5_loop x (tl b, Bk # Oc # list) = False"
apply(auto simp: inv_end5_loop.simps)
apply(case_tac [!] j, simp_all)
done
-lemma [elim]:
+lemma inv_end5_exit_Bk_Oc_via_loop[elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Bk\<rbrakk> \<Longrightarrow>
inv_end5_exit x (tl b, Bk # Oc # list)"
apply(auto simp: inv_end5_loop.simps inv_end5_exit.simps)
apply(case_tac [!] i, simp_all)
done
-lemma [elim]:
+lemma inv_end5_loop_Oc_Oc_drop[elim]:
"\<lbrakk>0 < x; inv_end5_loop x (b, Oc # list); b \<noteq> []; hd b = Oc\<rbrakk> \<Longrightarrow>
inv_end5_loop x (tl b, Oc # Oc # list)"
apply(simp only: inv_end5_loop.simps inv_end5_exit.simps)
@@ -766,7 +718,7 @@
apply(case_tac [!] i, simp_all)
done
-lemma [elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
+lemma inv_end5_Oc_tail[elim]: "\<lbrakk>0 < x; inv_end5 x (b, Oc # list); b \<noteq> []\<rbrakk> \<Longrightarrow>
inv_end5 x (tl b, hd b # Oc # list)"
apply(simp add: inv_end2.simps inv_end5.simps)
apply(case_tac "hd b", simp_all, auto)
@@ -816,9 +768,6 @@
unfolding end_LE_def
by (auto)
-lemma [simp]: "inv_end5 x ([], Oc # list) = False"
-by (auto simp: inv_end5.simps inv_end5_loop.simps)
-
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)
@@ -878,14 +827,11 @@
(* tcopy *)
-lemma [intro]: "tm_wf (tcopy_begin, 0)"
-by (auto simp: tm_wf.simps tcopy_begin_def)
-
-lemma [intro]: "tm_wf (tcopy_loop, 0)"
-by (auto simp: tm_wf.simps tcopy_loop_def)
-
-lemma [intro]: "tm_wf (tcopy_end, 0)"
-by (auto simp: tm_wf.simps tcopy_end_def)
+lemma tm_wf_tcopy[intro]:
+ "tm_wf (tcopy_begin, 0)"
+ "tm_wf (tcopy_loop, 0)"
+ "tm_wf (tcopy_end, 0)"
+by (auto simp: tm_wf.simps tcopy_end_def tcopy_loop_def tcopy_begin_def)
lemma tcopy_correct1:
assumes "0 < x"
@@ -999,10 +945,10 @@
where
"halts p ns \<equiv> {(\<lambda>tp. tp = ([], <ns>))} p {(\<lambda>tp. (\<exists>k n l. tp = (Bk \<up> k, <n::nat> @ Bk \<up> l)))}"
-lemma [intro, simp]: "tm_wf0 tcopy"
+lemma tm_wf0_tcopy[intro, simp]: "tm_wf0 tcopy"
by (auto simp: tcopy_def)
-lemma [intro, simp]: "tm_wf0 dither"
+lemma tm_wf0_dither[intro, simp]: "tm_wf0 dither"
by (auto simp: tm_wf.simps dither_def)
text {*