diff -r 6e1c03614d36 -r 93db7414931d thys/Uncomputable.thy --- 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]: "\0 < i; 0 < j\ \ +lemma inv_begin_step_E: "\0 < i; 0 < j\ \ \ia>0. ia + j - Suc 0 = i + j \ Oc # Oc \ i = Oc \ 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 \ t \ RR" +lemma Bk_no_Oc_repeatE[elim]: "Bk # list = Oc \ t \ RR" by (case_tac t, auto) -lemma [simp]: "inv_loop1 x (b, []) = False" -by (simp add: inv_loop1.simps) - -lemma [elim]: "\0 < x; inv_loop2 x (b, [])\ \ inv_loop3 x (Bk # b, [])" +lemma inv_loop3_Bk_empty_via_2[elim]: "\0 < x; inv_loop2 x (b, [])\ \ inv_loop3 x (Bk # b, [])" by (auto simp: inv_loop2.simps inv_loop3.simps) - -lemma [elim]: "\0 < x; inv_loop3 x (b, [])\ \ inv_loop3 x (Bk # b, [])" +lemma inv_loop3_Bk_empty[elim]: "\0 < x; inv_loop3 x (b, [])\ \ inv_loop3 x (Bk # b, [])" by (auto simp: inv_loop3.simps) - -lemma [elim]: "\0 < x; inv_loop4 x (b, [])\ \ inv_loop5 x (b, [Oc])" +lemma inv_loop5_Oc_empty_via_4[elim]: "\0 < x; inv_loop4 x (b, [])\ \ 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]: "\0 < x; inv_loop5 x ([], [])\ \ RR" -by (auto simp: inv_loop4.simps inv_loop5.simps) - -lemma [elim]: "\0 < x; inv_loop5 x (b, []); b \ []\ \ RR" -by (auto simp: inv_loop4.simps inv_loop5.simps) - -lemma [elim]: "inv_loop6 x ([], []) \ RR" -by (auto simp: inv_loop6.simps) - -lemma [elim]: "inv_loop6 x (b, []) \ RR" -by (auto simp: inv_loop6.simps) - -lemma [elim]: "\0 < x; inv_loop1 x (b, Bk # list)\ \ b = []" +lemma inv_loop1_Bk[elim]: "\0 < x; inv_loop1 x (b, Bk # list)\ \ list = Oc # Bk \ x @ Oc \ x" by (auto simp: inv_loop1.simps) -lemma [elim]: "\0 < x; inv_loop1 x (b, Bk # list)\ \ list = Oc # Bk \ x @ Oc \ x" -by (auto simp: inv_loop1.simps) - -lemma [elim]: "\0 < x; inv_loop2 x (b, Bk # list)\ \ inv_loop3 x (Bk # b, list)" +lemma inv_loop3_Bk_via_2[elim]: "\0 < x; inv_loop2 x (b, Bk # list)\ \ 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 \ j \ RR" -by (case_tac j, simp_all) - -lemma [elim]: "\0 < x; inv_loop3 x (b, Bk # list)\ \ inv_loop3 x (Bk # b, list)" +lemma inv_loop3_Bk_move[elim]: "\0 < x; inv_loop3 x (b, Bk # list)\ \ 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]: "\0 < x; inv_loop4 x (b, Bk # list)\ \ inv_loop5 x (b, Oc # list)" +lemma inv_loop5_Oc_via_4_Bk[elim]: "\0 < x; inv_loop4 x (b, Bk # list)\ \ inv_loop5 x (b, Oc # list)" by (auto simp: inv_loop4.simps inv_loop5.simps) -lemma [elim]: "\0 < x; inv_loop5 x ([], Bk # list)\ \ inv_loop6 x ([], Bk # Bk # list)" +lemma inv_loop6_Bk_via_5[elim]: "\0 < x; inv_loop5 x ([], Bk # list)\ \ 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]:"\0 < x; inv_loop5_exit x (b, Bk # list); b \ []; hd b = Bk\ +lemma inv_loop6_loopBk_via_5[elim]:"\0 < x; inv_loop5_exit x (b, Bk # list); b \ []; hd b = Bk\ \ 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]: "\x > 0; inv_loop5_exit x (b, Bk # list); b \ []; hd b = Oc\ \ +lemma inv_loop6_exit_Oc_Bk_via_5[elim]: "\x > 0; inv_loop5_exit x (b, Bk # list); b \ []; hd b = Oc\ \ 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]: "\0 < x; inv_loop5 x (b, Bk # list); b \ []\ \ inv_loop6 x (tl b, hd b # Bk # list)" +lemma inv_loop6_Bk_tail_via_5[elim]: "\0 < x; inv_loop5 x (b, Bk # list); b \ []\ \ 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]: "\0 < x; inv_loop6 x ([], Bk # list)\ \ 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]: "\0 < x; inv_loop6_loop x (b, Bk # list); b \ []; hd b = Bk\ +lemma inv_loop6_loop_Bk_Bk_drop[elim]: "\0 < x; inv_loop6_loop x (b, Bk # list); b \ []; hd b = Bk\ \ 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]: "\0 < x; inv_loop6_loop x (b, Bk # list); b \ []; hd b = Oc\ +lemma inv_loop6_exit_Oc_Bk_via_loop6[elim]: "\0 < x; inv_loop6_loop x (b, Bk # list); b \ []; hd b = Oc\ \ 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]: "\0 < x; inv_loop6 x (b, Bk # list); b \ []\ \ inv_loop6 x (tl b, hd b # Bk # list)" +lemma inv_loop6_Bk_tail[elim]: "\0 < x; inv_loop6 x (b, Bk # list); b \ []\ \ 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]: "\0 < x; inv_loop1 x (b, Oc # list)\ \ inv_loop2 x (Oc # b, list)" +lemma inv_loop2_Oc_via_1[elim]: "\0 < x; inv_loop1 x (b, Oc # list)\ \ 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]: "\0 < x; inv_loop2 x (b, Oc # list)\ \ inv_loop2 x (b, Bk # list)" +lemma inv_loop2_Bk_via_Oc[elim]: "\0 < x; inv_loop2 x (b, Oc # list)\ \ inv_loop2 x (b, Bk # list)" by (auto simp: inv_loop2.simps) -lemma [elim]: "\0 < x; inv_loop3 x (b, Oc # list)\ \ inv_loop4 x (Oc # b, list)" +lemma inv_loop4_Oc_via_3[elim]: "\0 < x; inv_loop3 x (b, Oc # list)\ \ 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]: "\0 < x; inv_loop4 x (b, Oc # list)\ \ inv_loop4 x (Oc # b, list)" +lemma inv_loop4_Oc_move[elim]: "\0 < x; inv_loop4 x (b, Oc # list)\ \ 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]: " \inv_loop5_loop x (b, Oc # list); b \ []; hd b = Bk\ +lemma inv_loop5_exit_Bk_Oc_via_loop[elim]: " \inv_loop5_loop x (b, Oc # list); b \ []; hd b = Bk\ \ 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]: "\inv_loop5_loop x (b, Oc # list); b \ []; hd b = Oc\ +lemma inv_loop5_loop_Oc_Oc_drop[elim]: "\inv_loop5_loop x (b, Oc # list); b \ []; hd b = Oc\ \ 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]: "\inv_loop5 x (b, Oc # list); b \ []\ \ inv_loop5 x (tl b, hd b # Oc # list)" +lemma inv_loop5_Oc_tl[elim]: "\inv_loop5 x (b, Oc # list); b \ []\ \ 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]: "\0 < x; inv_loop6 x ([], Oc # list)\ \ inv_loop1 x ([], Bk # Oc # list)" +lemma inv_loop1_Bk_Oc_via_6[elim]: "\0 < x; inv_loop6 x ([], Oc # list)\ \ 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]: "\0 < x; inv_loop6 x (b, Oc # list); b \ []\ + \ 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]: "\0 < x; inv_loop6 x (b, Oc # list); b \ []\ - \ 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]: + "\inv_loop5 x (b, [])\ \ RR" "inv_loop6 x (b, []) \ RR" + "\inv_loop1 x (b, Bk # list)\ \ 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]: "\inv_loop6 x ([], Bk # list)\ \ inv_loop6 x ([], Bk # Bk # list)" + by (simp) lemma inv_loop_step: "\inv_loop x cf; x > 0\ \ 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]: - "\inv_loop4 x (l', []); l' \ []; x > 0; +lemma inv_loop4_not_just_Oc[elim]: + "\inv_loop4 x (l', []); length (takeWhile (\a. a = Oc) (rev l' @ [Oc])) \ length (takeWhile (\a. a = Oc) (rev l'))\ - \ length (takeWhile (\a. a = Oc) (rev l' @ [Oc])) < length (takeWhile (\a. a = Oc) (rev l'))" + \ RR" + "\inv_loop4 x (l', Bk # list); + length (takeWhile (\a. a = Oc) (rev l' @ Oc # list)) \ + length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))\ + \ RR" apply(auto simp: inv_loop4.simps) apply(case_tac [!] j, simp_all add: List.takeWhile_tail) done - -lemma [elim]: - "\inv_loop4 x (l', Bk # list); l' \ []; 0 < x; - length (takeWhile (\a. a = Oc) (rev l' @ Oc # list)) \ - length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))\ - \ length (takeWhile (\a. a = Oc) (rev l' @ Oc # list)) < - length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))" -by (auto simp: inv_loop4.simps) - lemma takeWhile_replicate_append: "P a \ takeWhile P (a\x @ ys) = a\x @ takeWhile P ys" by (induct x, auto) @@ -517,12 +481,11 @@ "P a \ takeWhile P (a\x) = a\x" by (induct x, auto) -lemma [elim]: - "\inv_loop5 x (l', Bk # list); l' \ []; 0 < x; +lemma inv_loop5_Bk_E[elim]: + "\inv_loop5 x (l', Bk # list); l' \ []; length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \ length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))\ - \ length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < - length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))" + \ 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]: "\inv_loop1 x (l', Oc # list)\ \ hd list = Oc" +lemma inv_loop1_hd_Oc[elim]: "\inv_loop1 x (l', Oc # list)\ \ hd list = Oc" by (auto simp: inv_loop1.simps) -lemma [elim]: - "\inv_loop6 x (l', Bk # list); l' \ []; 0 < x; +lemma inv_loop6_not_just_Bk[elim]: + "\inv_loop6 x (l', Bk # list); l' \ []; length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) \ length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))\ - \ length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Bk # list)) < - length (takeWhile (\a. a = Oc) (rev l' @ Bk # list))" + \ RR" apply(auto simp: inv_loop6.simps) apply(case_tac l', simp_all) done -lemma [elim]: - "\inv_loop2 x (l', Oc # list); l' \ []; 0 < x\ \ +lemma inv_loop2_OcE[elim]: + "\inv_loop2 x (l', Oc # list); l' \ []\ \ length (takeWhile (\a. a = Oc) (rev l' @ Bk # list)) < length (takeWhile (\a. a = Oc) (rev l' @ Oc # list))" apply(auto simp: inv_loop2.simps) @@ -553,22 +515,20 @@ takeWhile_replicate) done -lemma [elim]: - "\inv_loop5 x (l', Oc # list); l' \ []; 0 < x; +lemma inv_loop5_OcE[elim]: + "\inv_loop5 x (l', Oc # list); l' \ []; length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \ length (takeWhile (\a. a = Oc) (rev l' @ Oc # list))\ - \ length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < - length (takeWhile (\a. a = Oc) (rev l' @ Oc # list))" + \ RR" apply(auto simp: inv_loop5.simps) apply(case_tac l', auto) done -lemma[elim]: - "\inv_loop6 x (l', Oc # list); l' \ []; 0 < x; +lemma inv_loop6_OcE[elim]: + "\inv_loop6 x (l', Oc # list); l' \ []; length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) \ length (takeWhile (\a. a = Oc) (rev l' @ Oc # list))\ - \ length (takeWhile (\a. a = Oc) (rev (tl l') @ hd l' # Oc # list)) < - length (takeWhile (\a. a = Oc) (rev l' @ Oc # list))" + \ 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]: "\0 < x; inv_end1 x (b, Bk # list); b \ []\ +lemma inv_end0_Bk_via_1[elim]: "\0 < x; inv_end1 x (b, Bk # list); b \ []\ \ inv_end0 x (tl b, hd b # Bk # list)" by (auto simp: inv_end1.simps inv_end0.simps) -lemma [elim]: "\0 < x; inv_end2 x (b, Bk # list)\ +lemma inv_end3_Oc_via_2[elim]: "\0 < x; inv_end2 x (b, Bk # list)\ \ 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]: "\0 < x; inv_end3 x (b, Bk # list)\ \ inv_end2 x (Bk # b, list)" +lemma inv_end2_Bk_via_3[elim]: "\0 < x; inv_end3 x (b, Bk # list)\ \ inv_end2 x (Bk # b, list)" by (auto simp: inv_end2.simps inv_end3.simps) -lemma [elim]: "\0 < x; inv_end4 x ([], Bk # list)\ \ +lemma inv_end5_Bk_via_4[elim]: "\0 < x; inv_end4 x ([], Bk # list)\ \ inv_end5 x ([], Bk # Bk # list)" by (auto simp: inv_end4.simps inv_end5.simps) -lemma [elim]: "\0 < x; inv_end4 x (b, Bk # list); b \ []\ \ +lemma inv_end5_Bk_tail_via_4[elim]: "\0 < x; inv_end4 x (b, Bk # list); b \ []\ \ 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]: "\0 < x; inv_end5 x (b, Bk # list)\ \ inv_end0 x (Bk # b, list)" +lemma inv_end0_Bk_via_5[elim]: "\0 < x; inv_end5 x (b, Bk # list)\ \ inv_end0 x (Bk # b, list)" apply(auto simp: inv_end5.simps inv_end0.simps) apply(case_tac [!] j, simp_all) done -lemma [elim]: "\0 < x; inv_end1 x (b, Oc # list)\ \ inv_end2 x (Oc # b, list)" +lemma inv_end2_Oc_via_1[elim]: "\0 < x; inv_end1 x (b, Oc # list)\ \ inv_end2 x (Oc # b, list)" by (auto simp: inv_end1.simps inv_end2.simps) -lemma [elim]: "\0 < x; inv_end2 x ([], Oc # list)\ \ +lemma inv_end4_Bk_Oc_via_2[elim]: "\0 < x; inv_end2 x ([], Oc # list)\ \ inv_end4 x ([], Bk # Oc # list)" by (auto simp: inv_end2.simps inv_end4.simps) -lemma [elim]: "\0 < x; inv_end2 x (b, Oc # list); b \ []\ \ +lemma inv_end4_Oc_via_2[elim]: "\0 < x; inv_end2 x (b, Oc # list); b \ []\ \ 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]: "\0 < x; inv_end3 x (b, Oc # list)\ \ inv_end2 x (Oc # b, list)" +lemma inv_end2_Oc_via_3[elim]: "\0 < x; inv_end3 x (b, Oc # list)\ \ inv_end2 x (Oc # b, list)" by (auto simp: inv_end2.simps inv_end3.simps) -lemma [elim]: "\0 < x; inv_end4 x (b, Oc # list)\ \ inv_end4 x (b, Bk # list)" +lemma inv_end4_Bk_via_Oc[elim]: "\0 < x; inv_end4 x (b, Oc # list)\ \ inv_end4 x (b, Bk # list)" by (auto simp: inv_end2.simps inv_end4.simps) -lemma [elim]: "\0 < x; inv_end5 x ([], Oc # list)\ \ inv_end5 x ([], Bk # Oc # list)" +lemma inv_end5_Bk_drop_Oc[elim]: "\0 < x; inv_end5 x ([], Oc # list)\ \ 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]: "\0 < x; inv_end5_loop x (b, Oc # list); b \ []; hd b = Bk\ \ 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]: "\0 < x; inv_end5_loop x (b, Oc # list); b \ []; hd b = Oc\ \ 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]: "\0 < x; inv_end5 x (b, Oc # list); b \ []\ \ +lemma inv_end5_Oc_tail[elim]: "\0 < x; inv_end5 x (b, Oc # list); b \ []\ \ 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: "\wf LE; \n. (\ P (f n) \ (f (Suc n), (f n)) \ LE)\ \ \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 \ {(\tp. tp = ([], ))} p {(\tp. (\k n l. tp = (Bk \ k, @ Bk \ 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 {*