--- a/thys/BitCoded2.thy Sat Aug 10 14:18:15 2019 +0100
+++ b/thys/BitCoded2.thy Sun Aug 11 00:28:14 2019 +0100
@@ -833,6 +833,16 @@
by (metis assms contains6 erase_bder)
+lemma contains7a:
+ assumes "\<Turnstile> v : der c (erase r)"
+ shows "r >> retrieve r (injval (erase r) c v)"
+ using assms
+ apply -
+ apply(drule Prf_injval)
+ apply(drule contains6)
+ apply(simp)
+ done
+
fun
bders_simp :: "arexp \<Rightarrow> string \<Rightarrow> arexp"
where
@@ -2021,7 +2031,9 @@
apply (metis bnullable_correctness erase_fuse)+
done
-lemma qq4:
+
+
+lemma qq4a:
assumes "\<exists>x\<in>set list. bnullable x"
shows "\<exists>x\<in>set (flts list). bnullable x"
using assms
@@ -2079,7 +2091,7 @@
apply(case_tac "list")
apply(simp)
apply(simp)
- apply (simp add: qq4)
+ apply (simp add: qq4a)
apply(simp)
apply(auto)
apply(case_tac list)
@@ -2092,7 +2104,7 @@
apply(simp)
apply (simp add: r0)
apply(simp)
- using qq4 r1 r2 by auto
+ using qq4a r1 r2 by auto
@@ -2145,7 +2157,7 @@
thm q3
apply(subst q3[symmetric])
apply simp
- using b3 qq4 apply auto[1]
+ using b3 qq4a apply auto[1]
apply(subst qs3)
apply simp
using k1 by blast
@@ -2190,59 +2202,6 @@
apply(simp add: blexer_correctness)
done
-
-
-
-
-fun flts2 :: "char \<Rightarrow> arexp list \<Rightarrow> arexp list"
- where
- "flts2 _ [] = []"
-| "flts2 c (AZERO # rs) = flts2 c rs"
-| "flts2 c (AONE _ # rs) = flts2 c rs"
-| "flts2 c (ACHAR bs d # rs) = (if c = d then (ACHAR bs d # flts2 c rs) else flts2 c rs)"
-| "flts2 c ((AALTs bs rs1) # rs) = (map (fuse bs) rs1) @ flts2 c rs"
-| "flts2 c (ASEQ bs r1 r2 # rs) = (if (bnullable(r1) \<and> r2 = AZERO) then
- flts2 c rs
- else ASEQ bs r1 r2 # flts2 c rs)"
-| "flts2 c (r1 # rs) = r1 # flts2 c rs"
-
-lemma flts2_k0:
- shows "flts2 c (r # rs1) = flts2 c [r] @ flts2 c rs1"
- apply(induct r arbitrary: c rs1)
- apply(auto)
- done
-
-lemma flts2_k00:
- shows "flts2 c (rs1 @ rs2) = flts2 c rs1 @ flts2 c rs2"
- apply(induct rs1 arbitrary: rs2 c)
- apply(auto)
- by (metis append.assoc flts2_k0)
-
-
-lemma
- shows "flts (map (bder c) rs) = (map (bder c) (flts2 c rs))"
- apply(induct c rs rule: flts2.induct)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(simp)
- apply(auto simp add: bder_fuse)[1]
- defer
- apply(simp)
- apply(simp del: flts2.simps)
- apply(rule conjI)
- prefer 2
- apply(auto)[1]
- apply(rule impI)
- apply(subst flts2_k0)
- apply(subst map_append)
- apply(subst flts2.simps)
- apply(simp only: flts2.simps)
- apply(auto)
-
-
-
lemma XXX2_helper:
assumes "\<forall>y. asize y < Suc (sum_list (map asize rs)) \<longrightarrow> good y \<longrightarrow> bsimp y = y"
"\<forall>r'\<in>set rs. good r' \<and> nonalt r'"
@@ -2481,97 +2440,6 @@
using assms
using LB LC lexer_correct_Some by auto
-lemma LXXX:
- assumes "s \<in> (erase r) \<rightarrow> v" "s \<in> (erase (bsimp r)) \<rightarrow> v'"
- shows "retrieve r v = retrieve (bsimp r) v'"
- using assms
- apply -
- thm LC
- apply(subst LC)
- apply(assumption)
- apply(subst L0[symmetric])
- using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
- apply(subst (2) LC)
- apply(assumption)
- apply(subst (2) L0[symmetric])
- using bnullable_correctness lexer_correctness(2) lexer_flex apply fastforce
-
- oops
-
-
-lemma L07a:
- assumes "s \<in> L (erase r)"
- shows "retrieve (bsimp r) (flex (erase (bsimp r)) id s (mkeps (ders s (erase (bsimp r)))))
- = retrieve r (flex (erase r) id s (mkeps (ders s (erase r))))"
- using assms
- apply(induct s arbitrary: r)
- apply(simp)
- using L0a apply force
- apply(drule_tac x="(bder a r)" in meta_spec)
- apply(drule meta_mp)
- apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
- apply(drule sym)
- apply(simp)
- apply(subst (asm) bder_retrieve)
- apply (metis Posix_Prf Posix_flex Posix_mkeps ders.simps(2) lexer_correct_None lexer_flex)
- apply(simp only: flex_fun_apply)
- apply(simp)
- using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
- oops
-
-lemma L08:
- assumes "s \<in> L (erase r)"
- shows "retrieve (bders (bsimp r) s) (mkeps (erase (bders (bsimp r) s)))
- = retrieve (bders r s) (mkeps (erase (bders r s)))"
- using assms
- apply(induct s arbitrary: r)
- apply(simp)
- using L0 bnullable_correctness nullable_correctness apply blast
- apply(simp add: bders_append)
- apply(drule_tac x="(bder a (bsimp r))" in meta_spec)
- apply(drule meta_mp)
- apply (metis L_bsimp_erase erase_bder lexer.simps(2) lexer_correct_None option.case(1))
- apply(drule sym)
- apply(simp)
- apply(subst LA)
- apply (metis L0aa L_bsimp_erase Posix1(1) ders.simps(2) ders_correctness erase_bder erase_bders mkeps_nullable nullable_correctness)
- apply(subst LA)
- using lexer_correct_None lexer_flex mkeps_nullable apply force
-
- using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
-
-thm L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars] L07[no_vars]
- oops
-
-lemma test:
- assumes "s = [c]"
- shows "retrieve (bders r s) v = XXX" and "YYY = retrieve r (flex (erase r) id s v)"
- using assms
- apply(simp only: bders.simps)
- defer
- using assms
- apply(simp only: flex.simps id_simps)
- using L0[no_vars] bder_retrieve[no_vars] LA[no_vars] LC[no_vars]
- find_theorems "retrieve (bders _ _) _"
- find_theorems "retrieve _ (mkeps _)"
- oops
-
-lemma L06X:
- assumes "bnullable (bder c a)"
- shows "bmkeps (bder c (bsimp a)) = bmkeps (bder c a)"
- using assms
- apply(induct a arbitrary: c)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- prefer 2
- apply(simp)
-
- defer
- oops
-
lemma L06_2:
assumes "bnullable (bders a [c,d])"
shows "bmkeps (bders (bsimp a) [c,d]) = bmkeps (bsimp (bders (bsimp a) [c,d]))"
@@ -2607,51 +2475,6 @@
shows "decode (bmkeps (bders (intern r) s)) r = Some(flex r id s (mkeps (ders s r)))"
by (metis assms blexer_correctness blexer_def lexer_correct_None lexer_flex)
-
-lemma L02_bders2:
- assumes "bnullable (bders a s)" "s = [c]"
- shows "retrieve (bders (bsimp a) s) (mkeps (erase (bders (bsimp a) s))) =
- retrieve (bders a s) (mkeps (erase (bders a s)))"
- using assms
- apply(simp)
-
- apply(induct s arbitrary: a)
- apply(simp)
- using L0 apply auto[1]
- oops
-
-thm bmkeps_retrieve bmkeps_simp Posix_mkeps
-
-lemma WQ1:
- assumes "s \<in> L (der c r)"
- shows "s \<in> der c r \<rightarrow> mkeps (ders s (der c r))"
- using assms
- oops
-
-lemma L02_bsimp:
- assumes "bnullable (bders a s)"
- shows "retrieve (bsimp a) (flex (erase (bsimp a)) id s (mkeps (erase (bders (bsimp a) s)))) =
- retrieve a (flex (erase a) id s (mkeps (erase (bders a s))))"
- using assms
- apply(induct s arbitrary: a)
- apply(simp)
- apply (simp add: L0)
- apply(simp)
- apply(drule_tac x="bder a aa" in meta_spec)
- apply(simp)
- apply(subst (asm) bder_retrieve)
- using Posix_Prf Posix_flex Posix_mkeps bnullable_correctness apply fastforce
- apply(simp add: flex_fun_apply)
- apply(drule sym)
- apply(simp)
- apply(subst flex_injval)
- apply(subst bder_retrieve[symmetric])
- apply (metis L_bsimp_erase Posix_Prf Posix_flex Posix_mkeps bders.simps(2) bnullable_correctness ders.simps(2) erase_bders lexer_correct_None lexer_flex option.distinct(1))
- apply(simp only: erase_bder[symmetric] erase_bders[symmetric])
- apply(subst LB_sym[symmetric])
- apply(simp)
- oops
-
lemma L1:
assumes "s \<in> r \<rightarrow> v"
shows "decode (bmkeps (bders (intern r) s)) r = Some v"
@@ -2760,19 +2583,6 @@
apply(simp)
using test2 by fastforce
-lemma XXX2a_long_without_good:
- assumes "a = AALTs bs0 [AALTs bs1 [AALTs bs2 [ASTAR [] (AONE bs7), AONE bs6, ASEQ bs3 (ACHAR bs4 d) (AONE bs5)]]]"
- shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- "bsimp (bder c (bsimp a)) = XXX"
- "bsimp (bder c a) = YYY"
- using assms
- apply(simp)
- using assms
- apply(simp)
- prefer 2
- using assms
- apply(simp)
- oops
lemma bder_bsimp_AALTs:
shows "bder c (bsimp_AALTs bs rs) = bsimp_AALTs bs (map (bder c) rs)"
@@ -2810,38 +2620,6 @@
by (metis flts_fuse flts_nothing)
-lemma PP:
- assumes "bnullable (bders r s)"
- shows "bmkeps (bders (bsimp r) s) = bmkeps (bders r s)"
- using assms
- apply(induct s arbitrary: r)
- apply(simp)
- using bmkeps_simp apply auto[1]
- apply(simp add: bders_append bders_simp_append)
- oops
-
-lemma PP:
- assumes "bnullable (bders r s)"
- shows "bmkeps (bders_simp (bsimp r) s) = bmkeps (bders r s)"
- using assms
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- using bmkeps_simp apply auto[1]
- apply(simp add: bders_append bders_simp_append)
- apply(drule_tac x="bder a (bsimp r)" in meta_spec)
- apply(drule_tac meta_mp)
- defer
- oops
-
-
-lemma
- assumes "asize (bsimp a) = asize a" "a = AALTs bs [AALTs bs2 [], AZERO, AONE bs3]"
- shows "bsimp a = a"
- using assms
- apply(simp)
- oops
-
-
lemma iii:
assumes "bsimp_AALTs bs rs \<noteq> AZERO"
shows "rs \<noteq> []"
@@ -2883,14 +2661,6 @@
(* CT *)
-lemma CTU:
- shows "bsimp_AALTs bs as = li bs as"
- apply(induct bs as rule: li.induct)
- apply(auto)
- done
-
-find_theorems "bder _ (bsimp_AALTs _ _)"
-
lemma CTa:
assumes "\<forall>r \<in> set as. nonalt r \<and> r \<noteq> AZERO"
shows "flts as = as"
@@ -2947,446 +2717,44 @@
apply(induct as arbitrary: a)
apply(auto)
using le_add2 le_less_trans not_less_eq by blast
-
-lemma XXX2a_long_without_good:
- shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- (* AALT case *)
- prefer 2
- apply(simp del: bsimp.simps)
- apply(subst (2) CT1)
- apply(subst CT_exp)
- apply(auto)[1]
- using asize_set apply blast
- apply(subst CT1[symmetric])
- apply(simp)
- oops
-
-lemma YY:
- assumes "flts (map bsimp as1) = xs"
- shows "flts (map bsimp (map (fuse bs1) as1)) = map (fuse bs1) xs"
- using assms
- apply(induct as1 arbitrary: bs1 xs)
- apply(simp)
- apply(auto)
- by (metis bsimp_fuse flts_fuse k0 list.simps(9))
-
-
-lemma flts_nonalt:
- assumes "flts (map bsimp xs) = ys"
- shows "\<forall>y \<in> set ys. nonalt y"
- using assms
- apply(induct xs arbitrary: ys)
- apply(auto)
- apply(case_tac xs)
- apply(auto)
- using flts2 good1 apply fastforce
- by (smt ex_map_conv list.simps(9) nn1b nn1c)
-
-
-lemma WWW3:
- shows "flts [bsimp_AALTs bs1 (flts (map bsimp as1))] =
- flts (map bsimp (map (fuse bs1) as1))"
- by (metis CT0 YY flts_nonalt flts_nothing qqq1)
-
-
-
-lemma WWW5:
- shows "map (bsimp \<circ> bder c) as1 = map bsimp (map (bder c) as1)"
- apply(induct as1)
- apply(auto)
- done
-
-lemma big0:
- shows "bsimp (AALT x51 (AALTs bs1 as1) (AALTs bs2 as2)) =
- bsimp (AALTs x51 ((map (fuse bs1) as1) @ (map (fuse bs2) as2)))"
- by (smt WWW3 bsimp.simps(2) k0 k00 list.simps(8) list.simps(9) map_append)
-
-lemma bignA:
- shows "bsimp (AALTs x51 (AALTs bs1 as1 # as2)) =
- bsimp (AALTs x51 ((map (fuse bs1) as1) @ as2))"
- apply(simp)
- apply(subst k0)
- apply(subst WWW3)
- apply(simp add: flts_append)
- done
-
-lemma XXX2a_long_without_good:
- shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- (* SEQ case *)
- apply(simp only:)
- apply(subst CT1_SEQ)
- apply(simp only: bsimp.simps)
-
- (* AALT case *)
- prefer 2
- apply(simp only:)
- apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
- apply(clarify)
- apply(simp del: bsimp.simps)
- apply(subst (2) CT1)
- apply(simp del: bsimp.simps)
- apply(rule_tac t="bsimp (bder c a1)" and s="bsimp (bder c (bsimp a1))" in subst)
- apply(simp del: bsimp.simps)
- apply(rule_tac t="bsimp (bder c a2)" and s="bsimp (bder c (bsimp a2))" in subst)
- apply(simp del: bsimp.simps)
- apply(subst CT1a[symmetric])
- (* \<rightarrow> *)
- apply(rule_tac t="AALT x51 (bder c (bsimp a1)) (bder c (bsimp a2))"
- and s="bder c (AALT x51 (bsimp a1) (bsimp a2))" in subst)
- apply(simp)
- apply(subst bsimp.simps)
- apply(simp del: bsimp.simps bder.simps)
-
- apply(subst bder_bsimp_AALTs)
- apply(subst bsimp.simps)
- apply(subst WWW2[symmetric])
- apply(subst bsimp_AALTs_qq)
- defer
- apply(subst bsimp.simps)
-
- (* <- *)
- apply(subst bsimp.simps)
- apply(simp del: bsimp.simps)
- apply(case_tac "\<exists>bs1 as1. bsimp a1 = AALTs bs1 as1")
- apply(case_tac "\<exists>bs2 as2. bsimp a2 = AALTs bs2 as2")
- apply(clarify)
- apply(simp only:)
- apply(simp del: bsimp.simps bder.simps)
- apply(subst bsimp_AALTs_qq)
- prefer 2
- apply(simp del: bsimp.simps)
- apply(subst big0)
- apply(simp add: WWW4)
- apply (m etis One_nat_def Suc_eq_plus1 Suc_lessI arexp.distinct(7) bsimp.simps(2) bsimp_AALTs.simps(1) bsimp_idem flts.simps(1) length_append length_greater_0_conv length_map not_add_less2 not_less_eq)
- oops
-
-lemma XXX2a_long_without_good:
- shows "bsimp (bder c (bsimp a)) = bsimp (bder c a)"
- apply(induct a arbitrary: c taking: "\<lambda>a. asize a" rule: measure_induct)
- apply(case_tac x)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- (* AALT case *)
- prefer 2
- apply(subgoal_tac "nonnested (bsimp x)")
- prefer 2
- using nn1b apply blast
- apply(simp only:)
- apply(drule_tac x="AALTs x51 (flts x52)" in spec)
- apply(drule mp)
- defer
- apply(drule_tac x="c" in spec)
- apply(simp)
- apply(rotate_tac 2)
-
- apply(drule sym)
- apply(simp)
-
- apply(simp only: bder.simps)
- apply(simp only: bsimp.simps)
- apply(subst bder_bsimp_AALTs)
- apply(case_tac x52)
- apply(simp)
+lemma PPP:
+ assumes "\<Turnstile> v : ders s r"
+ shows "bders (intern r) s >> code v"
+ using assms
+ apply(induct s arbitrary: r v rule: rev_induct)
apply(simp)
- apply(case_tac list)
- apply(simp)
- apply(case_tac a)
- apply(simp)
- apply(simp)
- apply(simp)
- defer
- apply(simp)
-
-
- (* case AALTs list is not empty *)
- apply(simp)
- apply(subst k0)
- apply(subst (2) k0)
- apply(simp)
- apply(case_tac "bsimp a = AZERO")
- apply(subgoal_tac "bsimp (bder c a) = AZERO")
- prefer 2
- using less_iff_Suc_add apply auto[1]
- apply(simp)
- apply(drule_tac x="AALTs x51 list" in spec)
- apply(drule mp)
- apply(simp add: asize0)
- apply(drule_tac x="c" in spec)
- apply(simp add: bder_bsimp_AALTs)
- apply(case_tac "nonalt (bsimp a)")
- prefer 2
- apply(drule_tac x="bsimp (AALTs x51 (a#list))" in spec)
- apply(drule mp)
- apply(rule order_class.order.strict_trans2)
- apply(rule bsimp_AALTs_size3)
- apply(auto)[1]
- apply(simp)
- apply(subst (asm) bsimp_idem)
- apply(drule_tac x="c" in spec)
- apply(simp)
- find_theorems "_ < _ \<Longrightarrow> _ \<le> _ \<Longrightarrow>_ < _"
- apply(rule le_trans)
- apply(subgoal_tac "flts [bsimp a] = [bsimp a]")
- prefer 2
- using k0b apply blast
- apply(simp)
- find_theorems "asize _ < asize _"
-
- using bder_bsimp_AALTs
- apply(case_tac list)
- apply(simp)
- sledgeha mmer [timeout=6000]
-
- apply(case_tac "\<exists>r \<in> set (map bsimp x52). \<not>nonalt r")
- apply(drule_tac x="bsimp (AALTs x51 x52)" in spec)
- apply(drule mp)
- using bsimp_AALTs_size3 apply blast
- apply(drule_tac x="c" in spec)
- apply(subst (asm) (2) test)
+ apply (simp add: Posix_Prf contains2)
+ apply(simp add: bders_append ders_append flex_append)
+ apply(frule Prf_injval)
+ apply(drule meta_spec)
+ apply(drule meta_spec)
+ apply(drule meta_mp)
+ apply(assumption)
+ apply(subst retrieve_code)
+ apply(assumption)
+ apply(subst (asm) retrieve_code)
+ apply(assumption)
+ using contains7 contains7a contains6 retrieve_code
+ apply(rule contains7)
- apply(case_tac x52)
- apply(simp)
- apply(simp)
- apply(case_tac "bsimp a = AZERO")
- apply(simp)
- apply(subgoal_tac "bsimp (bder c a) = AZERO")
- prefer 2
- apply auto[1]
- apply (metis L.simps(1) L_bsimp_erase der.simps(1) der_correctness erase.simps(1) erase_bder xxx_bder2)
- apply(simp)
- apply(drule_tac x="AALTs x51 list" in spec)
- apply(drule mp)
- apply(simp add: asize0)
- apply(simp)
- apply(case_tac list)
- prefer 2
- apply(simp)
- apply(case_tac "bsimp aa = AZERO")
- apply(simp)
- apply(subgoal_tac "bsimp (bder c aa) = AZERO")
- prefer 2
- apply auto[1]
- apply (metis add.left_commute bder.simps(1) bsimp.simps(3) less_add_Suc1)
- apply(simp)
- apply(drule_tac x="AALTs x51 (a#lista)" in spec)
- apply(drule mp)
- apply(simp add: asize0)
- apply(simp)
- apply (metis flts.simps(2) k0)
- apply(subst k0)
- apply(subst (2) k0)
-
-
- using less_add_Suc1 apply fastforce
- apply(subst k0)
-
-
- apply(simp)
- apply(case_tac "bsimp a = AZERO")
- apply(simp)
- apply(subgoal_tac "bsimp (bder c a) = AZERO")
- prefer 2
- apply auto[1]
- apply(simp)
- apply(case_tac "nonalt (bsimp a)")
- apply(subst bsimp_AALTs1)
- apply(simp)
- using less_add_Suc1 apply fastforce
-
- apply(subst bsimp_AALTs1)
-
- using nn11a apply b last
-
- (* SEQ case *)
- apply(clarify)
- apply(subst bsimp.simps)
- apply(simp del: bsimp.simps)
- apply(auto simp del: bsimp.simps)[1]
- apply(subgoal_tac "bsimp x42 \<noteq> AZERO")
- prefer 2
- using b3 apply force
- apply(case_tac "bsimp x43 = AZERO")
- apply(simp)
- apply (simp add: bsimp_ASEQ0)
- apply (metis bder.simps(1) bsimp.simps(3) bsimp_AALTs.simps(1) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) less_add_Suc2)
- apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
- apply(subgoal_tac "bsimp (bder c x42) = AZERO")
- prefer 2
- using less_add_Suc1 apply fastforce
- apply(simp)
- apply(frule_tac x="x43" in spec)
- apply(drule mp)
- apply(simp)
- apply(drule_tac x="c" in spec)
- apply(subst bder_fuse)
- apply(subst bsimp_fuse[symmetric])
- apply(simp)
- apply(subgoal_tac "bmkeps x42 = bs")
- prefer 2
- apply (simp add: bmkeps_simp)
- apply(simp)
- apply(subst bsimp_fuse[symmetric])
- apply(case_tac "nonalt (bsimp (bder c x43))")
- apply(subst bsimp_AALTs1)
- using nn11a apply blast
- using fuse_append apply blast
- apply(subgoal_tac "\<exists>bs rs. bsimp (bder c x43) = AALTs bs rs")
- prefer 2
- using bbbbs1 apply blast
- apply(clarify)
- apply(simp)
- apply(case_tac rs)
- apply(simp)
- apply (metis arexp.distinct(7) good.simps(4) good1)
- apply(simp)
- apply(case_tac list)
- apply(simp)
- apply (metis arexp.distinct(7) good.simps(5) good1)
- apply(simp del: bsimp_AALTs.simps)
- apply(simp only: bsimp_AALTs.simps)
- apply(simp)
+ find_theorems "bder _ _ >> _"
+ find_theorems "code _ = _"
+ find_theorems "\<Turnstile> _ : der _ _"
-
-(* HERE *)
-apply(case_tac "x42 = AZERO")
- apply(simp)
- apply(case_tac "bsimp x43 = AZERO")
- apply(simp)
- apply (simp add: bsimp_ASEQ0)
- apply(subgoal_tac "bsimp (fuse (bmkeps x42) (bder c x43)) = AZERO")
- apply(simp)
- apply (met is bder.simps(1) bsimp.simps(3) bsimp_fuse fuse.simps(1) less_add_Suc2)
- apply(case_tac "\<exists>bs. bsimp x42 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ2)
- apply(subgoal_tac "bsimp (bder c x42) = AZERO")
- apply(simp)
- prefer 2
- using less_add_Suc1 apply fastforce
- apply(subgoal_tac "bmkeps x42 = bs")
- prefer 2
- apply (simp add: bmkeps_simp)
- apply(simp)
- apply(case_tac "nonalt (bsimp (bder c x43))")
- apply (metis bder_fuse bsimp_AALTs.simps(1) bsimp_AALTs.simps(2) bsimp_fuse flts.simps(1) flts.simps(2) fuse.simps(1) fuse_append k0b less_add_Suc2 nn11a)
- apply(subgoal_tac "nonnested (bsimp (bder c x43))")
- prefer 2
- using nn1b apply blast
- apply(case_tac x43)
- apply(simp)
- apply(simp)
- apply(simp)
- prefer 3
- apply(simp)
- apply (metis arexp.distinct(25) arexp.distinct(7) arexp.distinct(9) bsimp_ASEQ.simps(1) bsimp_ASEQ.simps(11) bsimp_ASEQ1 nn11a nonalt.elims(3) nonalt.simps(6))
- apply(simp)
- apply(auto)[1]
- apply(case_tac "(bsimp (bder c x42a)) = AZERO")
- apply(simp)
-
- apply(simp)
-
-
-
- apply(subgoal_tac "(\<exists>bs1 rs1. 1 < length rs1 \<and> bsimp (bder c x43) = AALTs bs1 rs1 ) \<or>
- (\<exists>bs1 r. bsimp (bder c x43) = fuse bs1 r)")
- prefer 2
- apply (metis fuse_empty)
- apply(erule disjE)
- prefer 2
- apply(clarify)
- apply(simp only:)
- apply(simp)
- apply(simp add: fuse_append)
- apply(subst bder_fuse)
- apply(subst bsimp_fuse[symmetric])
- apply(subst bder_fuse)
- apply(subst bsimp_fuse[symmetric])
- apply(subgoal_tac "bsimp (bder c (bsimp x43)) = bsimp (bder c x43)")
- prefer 2
- using less_add_Suc2 apply bl ast
- apply(simp only: )
- apply(subst bsimp_fuse[symmetric])
- apply(simp only: )
-
- apply(simp only: fuse.simps)
+ find_theorems "_ >> (code _)"
+ apply(induct s arbitrary: a bs rule: rev_induct)
+ apply(simp)
+ apply(simp add: bders_simp_append bders_append)
+ apply(rule contains55)
+ find_theorems "bder _ _ >> _"
+ apply(drule_tac x="bder a aa" in meta_spec)
+ apply(drule_tac x="bs" in meta_spec)
apply(simp)
- apply(case_tac rs1)
- apply(simp)
- apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(4) good1 good_fuse)
- apply(simp)
- apply(case_tac list)
- apply(simp)
- apply (me tis arexp.distinct(7) fuse.simps(1) good.simps(5) good1 good_fuse)
- apply(simp only: bsimp_AALTs.simps map_cons.simps)
- apply(auto)[1]
-
-
-
- apply(subst bsimp_fuse[symmetric])
- apply(subgoal_tac "bmkeps x42 = bs")
- prefer 2
- apply (simp add: bmkeps_simp)
-
-
- apply(simp)
-
- using b3 apply force
- using bsimp_ASEQ0 test2 apply fo rce
- thm good_SEQ test2
- apply (simp add: good_SEQ test2)
- apply (simp add: good_SEQ test2)
- apply(case_tac "x42 = AZERO")
- apply(simp)
- apply(case_tac "x43 = AZERO")
- apply(simp)
- apply (simp add: bsimp_ASEQ0)
- apply(case_tac "\<exists>bs. x42 = AONE bs")
- apply(clarify)
- apply(simp)
- apply(subst bsimp_ASEQ1)
- apply(simp)
- using bsimp_ASEQ0 test2 apply fo rce
- apply (simp add: good_SEQ test2)
- apply (simp add: good_SEQ test2)
- apply (simp add: good_SEQ test2)
- (* AALTs case *)
- apply(simp)
- using test2 by fa st force
-
-
-lemma XXX4ab:
- shows "good (bders_simp (bsimp r) s) \<or> bders_simp (bsimp r) s = AZERO"
- apply(induct s arbitrary: r rule: rev_induct)
- apply(simp)
- apply (simp add: good1)
- apply(simp add: bders_simp_append)
- apply (simp add: good1)
- done
+ apply(rule contains55)
+ find_theorems "bsimp _ >> _"
lemma XXX4:
assumes "good a"