tm: comparison thys/Recursive.thy

equal deleted inserted replaced

-:6e1c03614d36
+:93db7414931d
 lemma wf_additon_LE[simp]: "wf addition_LE"
 by(auto simp: addition_LE_def lex_triple_def lex_pair_def)
 declare addition_inv.simps[simp del]
+lemma update_zero_to_zero[simp]: "\<lbrakk>am ! n = (0::nat); n < length am\<rbrakk> \<Longrightarrow> am[n := 0] = am"
+apply(simp add: list_update_same_conv)
+done
 lemma addition_inv_init:
 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
 addition_inv (0, lm) m n p lm"
-apply(simp add: addition_inv.simps Let_def)
+apply(simp add: addition_inv.simps Let_def )
 apply(rule_tac x = "lm ! m" in exI, simp)
 done
-lemma abs_fetch_0[simp]: "abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+lemma abs_fetch[simp]:
-by(simp add: abc_fetch.simps addition.simps)
+"abc_fetch 0 (addition m n p) = Some (Dec m 4)"
+"abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
-lemma abs_fetch_1[simp]: "abc_fetch (Suc 0) (addition m n p) = Some (Inc n)"
+"abc_fetch 2 (addition m n p) = Some (Inc p)"
-by(simp add: abc_fetch.simps addition.simps)
+"abc_fetch 3 (addition m n p) = Some (Goto 0)"
+"abc_fetch 4 (addition m n p) = Some (Dec p 7)"
-lemma abs_fetch_2[simp]: "abc_fetch 2 (addition m n p) = Some (Inc p)"
+"abc_fetch 5 (addition m n p) = Some (Inc m)"
-by(simp add: abc_fetch.simps addition.simps)
+"abc_fetch 6 (addition m n p) = Some (Goto 4)"
+by(simp_all add: abc_fetch.simps addition.simps)
-lemma abs_fetch_3[simp]: "abc_fetch 3 (addition m n p) = Some (Goto 0)"
-by(simp add: abc_fetch.simps addition.simps)
-lemma abs_fetch_4[simp]: "abc_fetch 4 (addition m n p) = Some (Dec p 7)"
-by(simp add: abc_fetch.simps addition.simps)
-lemma abs_fetch_5[simp]: "abc_fetch 5 (addition m n p) = Some (Inc m)"
-by(simp add: abc_fetch.simps addition.simps)
-lemma abs_fetch_6[simp]: "abc_fetch 6 (addition m n p) = Some (Goto 4)"
-by(simp add: abc_fetch.simps addition.simps)
 lemma exists_small_list_elem1[simp]:
 "\<lbrakk>m \<noteq> n; p < length lm; lm ! p = 0; m < p; n < p; x \<le> lm ! m; 0 < x\<rbrakk>
 \<Longrightarrow> \<exists>xa<lm ! m. lm[m := x, n := lm ! n + lm ! m - x,
 p := lm ! m - x, m := x - Suc 0] =
 apply(simp_all add: addition.simps abc_steps_l.simps)
 apply(auto simp add: addition_LE_def lex_triple_def lex_pair_def
 abc_step_l.simps addition_inv.simps
 abc_lm_v.simps abc_lm_s.simps nth_append
 split: if_splits)
-apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc)
+apply(rule_tac [!] x = x in exI, simp_all add: list_update_overwrite Suc_diff_Suc )
 by (metis list_update_overwrite list_update_swap nat_neq_iff)
 lemma  addition_correct':
 "\<lbrakk>m \<noteq> n; max m n < p; length lm > p; lm ! p = 0\<rbrakk> \<Longrightarrow>
 \<exists> stp. (\<lambda> (as, lm'). as = 7 \<and> addition_inv (as, lm') m n p lm)
 apply(simp add: abc_steps_l.simps mv_box_inv.simps)
 apply(rule_tac x = "initlm ! m" in exI,
 rule_tac x = "initlm ! n" in exI, simp)
 done
-lemma abc_fetch_0[simp]: "abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
+lemma abc_fetch[simp]:
-apply(simp add: mv_box.simps abc_fetch.simps)
+"abc_fetch 0 (mv_box m n) = Some (Dec m 3)"
-done
+"abc_fetch (Suc 0) (mv_box m n) = Some (Inc n)"
+"abc_fetch 2 (mv_box m n) = Some (Goto 0)"
-lemma abc_fetch_1[simp]: "abc_fetch (Suc 0) (mv_box m n) =
+"abc_fetch 3 (mv_box m n) = None"
-Some (Inc n)"
+apply(simp_all add: mv_box.simps abc_fetch.simps)
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-lemma abc_fetch_2[simp]: "abc_fetch 2 (mv_box m n) = Some (Goto 0)"
-apply(simp add: mv_box.simps abc_fetch.simps)
-done
-lemma abc_fetch_3[simp]: "abc_fetch 3 (mv_box m n) = None"
-apply(simp add: mv_box.simps abc_fetch.simps)
 done
 lemma replicate_Suc_iff_anywhere: "x # x\<up>b @ ys = x\<up>(Suc b) @ ys"
 by simp
 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)")
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ")
 apply(arith)
 apply(case_tac "Suc k = length ap", simp)
 apply(rule_tac start_of_less, simp)
-apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps startof_not0)
+apply(auto simp: tinc_b_def shift.simps start_of_suc_inc length_of.simps )
 done
 lemma findnth_le[elim]:
 "(a, b) \<in> set (shift (findnth n) (start_of (layout_of ap) k - Suc 0))
 \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)"
 apply(arith)
 apply(case_tac "Suc k = length ap", simp)
 apply(rule_tac start_of_less, simp)
 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and>
 start_of (layout_of ap) k + 2*n + 1 \<le>  start_of (layout_of ap) (Suc k)", auto)
-apply(auto simp: tinc_b_def shift.simps length_of.simps startof_not0 start_of_suc_inc)
+apply(auto simp: tinc_b_def shift.simps length_of.simps  start_of_suc_inc)
 done
 lemma start_of_eq: "length ap < as \<Longrightarrow> start_of (layout_of ap) as = start_of (layout_of ap) (length ap)"
 apply(induct as, simp)
 apply(case_tac "length ap < as", simp add: start_of.simps)
 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)"
 apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0")
 prefer 2
 apply(subgoal_tac "start_of (layout_of ap) (Suc k) = start_of (layout_of ap) k + 2*n + 16
 \<and> start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)")
-apply(simp add: startof_not0, rule_tac conjI)
+apply(simp, rule_tac conjI)
 apply(simp add: start_of_suc_dec)
 apply(rule_tac start_of_all_le)
 apply(auto simp: tdec_b_def shift.simps)
 done
 using compile
 using wf_tm_from_abacus[of "tm_of (a [+] dummy_abc b)" "(a [+] dummy_abc b)" b]
 by simp
 qed
-unused_thms
 end

changeset 291	93db7414931d
parent 290	6e1c03614d36
child 292	293e9c6f22e1