theory FBound
imports "BlexerSimp" "ClosedFormsBounds"
begin
fun distinctBy :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b set \<Rightarrow> 'a list"
where
"distinctBy [] f acc = []"
| "distinctBy (x#xs) f acc =
(if (f x) \<in> acc then distinctBy xs f acc
else x # (distinctBy xs f ({f x} \<union> acc)))"
fun rerase :: "arexp \<Rightarrow> rrexp"
where
"rerase AZERO = RZERO"
| "rerase (AONE _) = RONE"
| "rerase (ACHAR _ c) = RCHAR c"
| "rerase (AALTs bs rs) = RALTS (map rerase rs)"
| "rerase (ASEQ _ r1 r2) = RSEQ (rerase r1) (rerase r2)"
| "rerase (ASTAR _ r) = RSTAR (rerase r)"
| "rerase (ANTIMES _ r n) = RNTIMES (rerase r) n"
lemma eq1_rerase:
shows "x ~1 y \<longleftrightarrow> (rerase x) = (rerase y)"
apply(induct x y rule: eq1.induct)
apply(auto)
done
lemma distinctBy_distinctWith:
shows "distinctBy xs f (f ` acc) = distinctWith xs (\<lambda>x y. f x = f y) acc"
apply(induct xs arbitrary: acc)
apply(auto)
by (metis image_insert)
lemma distinctBy_distinctWith2:
shows "distinctBy xs rerase {} = distinctWith xs eq1 {}"
apply(subst distinctBy_distinctWith[of _ _ "{}", simplified])
using eq1_rerase by presburger
lemma asize_rsize:
shows "rsize (rerase r) = asize r"
apply(induct r rule: rerase.induct)
apply(auto)
apply (metis (mono_tags, lifting) comp_apply map_eq_conv)
done
lemma rerase_fuse:
shows "rerase (fuse bs r) = rerase r"
apply(induct r)
apply simp+
done
lemma rerase_bsimp_ASEQ:
shows "rerase (bsimp_ASEQ x1 a1 a2) = rsimp_SEQ (rerase a1) (rerase a2)"
apply(induct x1 a1 a2 rule: bsimp_ASEQ.induct)
apply(auto)
done
lemma rerase_bsimp_AALTs:
shows "rerase (bsimp_AALTs bs rs) = rsimp_ALTs (map rerase rs)"
apply(induct bs rs rule: bsimp_AALTs.induct)
apply(auto simp add: rerase_fuse)
done
fun anonalt :: "arexp \<Rightarrow> bool"
where
"anonalt (AALTs bs2 rs) = False"
| "anonalt r = True"
fun agood :: "arexp \<Rightarrow> bool" where
"agood AZERO = False"
| "agood (AONE cs) = True"
| "agood (ACHAR cs c) = True"
| "agood (AALTs cs []) = False"
| "agood (AALTs cs [r]) = False"
| "agood (AALTs cs (r1#r2#rs)) = (distinct (map rerase (r1 # r2 # rs)) \<and>(\<forall>r' \<in> set (r1#r2#rs). agood r' \<and> anonalt r'))"
| "agood (ASEQ _ AZERO _) = False"
| "agood (ASEQ _ (AONE _) _) = False"
| "agood (ASEQ _ _ AZERO) = False"
| "agood (ASEQ cs r1 r2) = (agood r1 \<and> agood r2)"
| "agood (ASTAR cs r) = True"
fun anonnested :: "arexp \<Rightarrow> bool"
where
"anonnested (AALTs bs2 []) = True"
| "anonnested (AALTs bs2 ((AALTs bs1 rs1) # rs2)) = False"
| "anonnested (AALTs bs2 (r # rs2)) = anonnested (AALTs bs2 rs2)"
| "anonnested r = True"
lemma asize0:
shows "0 < asize r"
apply(induct r)
apply(auto)
done
lemma rnullable:
shows "rnullable (rerase r) = bnullable r"
apply(induct r rule: rerase.induct)
apply(auto)
done
lemma rder_bder_rerase:
shows "rder c (rerase r ) = rerase (bder c r)"
apply (induct r)
apply (auto)
using rerase_fuse apply presburger
using rnullable apply blast
using rnullable by blast
lemma rerase_map_bsimp:
assumes "\<And> r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = (rsimp \<circ> rerase) r"
shows "map rerase (map bsimp rs) = map (rsimp \<circ> rerase) rs"
using assms
apply(induct rs)
by simp_all
lemma rerase_flts:
shows "map rerase (flts rs) = rflts (map rerase rs)"
apply(induct rs rule: flts.induct)
apply(auto simp add: rerase_fuse)
done
lemma rerase_dB:
shows "map rerase (distinctBy rs rerase acc) = rdistinct (map rerase rs) acc"
apply(induct rs arbitrary: acc)
apply simp+
done
lemma rerase_earlier_later_same:
assumes " \<And>r. r \<in> set rs \<Longrightarrow> rerase (bsimp r) = rsimp (rerase r)"
shows " (map rerase (distinctBy (flts (map bsimp rs)) rerase {})) =
(rdistinct (rflts (map (rsimp \<circ> rerase) rs)) {})"
apply(subst rerase_dB)
apply(subst rerase_flts)
apply(subst rerase_map_bsimp)
apply auto
using assms
apply simp
done
lemma bsimp_rerase:
shows "rerase (bsimp a) = rsimp (rerase a)"
apply(induct a rule: bsimp.induct)
apply(auto)
using rerase_bsimp_ASEQ apply presburger
using distinctBy_distinctWith2 rerase_bsimp_AALTs rerase_earlier_later_same by fastforce
lemma rders_simp_size:
shows "rders_simp (rerase r) s = rerase (bders_simp r s)"
apply(induct s rule: rev_induct)
apply simp
by (simp add: bders_simp_append rder_bder_rerase rders_simp_append bsimp_rerase)
corollary aders_simp_finiteness:
assumes "\<exists>N. \<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
shows " \<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
proof -
from assms obtain N where "\<forall>s. rsize (rders_simp (rerase r) s) \<le> N"
by blast
then have "\<forall>s. rsize (rerase (bders_simp r s)) \<le> N"
by (simp add: rders_simp_size)
then have "\<forall>s. asize (bders_simp r s) \<le> N"
by (simp add: asize_rsize)
then show "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N" by blast
qed
theorem annotated_size_bound:
shows "\<exists>N. \<forall>s. asize (bders_simp r s) \<le> N"
apply(insert aders_simp_finiteness)
by (simp add: rders_simp_bounded)
definition bitcode_agnostic :: "(arexp \<Rightarrow> arexp ) \<Rightarrow> bool"
where " bitcode_agnostic f = (\<forall>a1 a2. rerase a1 = rerase a2 \<longrightarrow> rerase (f a1) = rerase (f a2)) "
lemma bitcode_agnostic_bsimp:
shows "bitcode_agnostic bsimp"
by (simp add: bitcode_agnostic_def bsimp_rerase)
thm bsimp_rerase
lemma cant1:
shows "\<lbrakk> bsimp a = b; rerase a = rerase b; a = ASEQ bs r1 r2 \<rbrakk> \<Longrightarrow>
\<exists>bs' r1' r2'. b = ASEQ bs' r1' r2' \<and> rerase r1' = rerase r1 \<and> rerase r2' = rerase r2"
sorry
(*"part is less than whole" thm for rrexp, since rrexp is always finite*)
lemma rrexp_finite1:
shows "\<lbrakk> bsimp_ASEQ bs1 (bsimp ra1) (bsimp ra2) = ASEQ bs2 rb1 rb2; ra1 ~1 rb1; ra2 ~1 rb2 \<rbrakk> \<Longrightarrow> rerase ra1 = rerase (bsimp ra1) "
apply(case_tac ra1 )
apply simp+
apply(case_tac rb1)
apply simp+
sorry
lemma unsure_unchanging:
assumes "bsimp a = bsimp b"
and "a ~1 b"
shows "a = b"
using assms
apply(induct rule: eq1.induct)
apply simp+
oops
lemma eq1rerase:
shows "rerase r1 = rerase r2 \<longleftrightarrow> r1 ~1 r2"
using eq1_rerase by presburger
thm contrapos_pp
lemma r_part_neq_whole:
shows "RSEQ r1 r2 \<noteq> r2"
apply simp
done
lemma r_part_neq_whole2:
shows "RSEQ r1 r2 \<noteq> rsimp r2"
by (metis good.simps(7) good.simps(8) good1 good_SEQ r_part_neq_whole rrexp.distinct(5) rsimp.simps(3) test)
lemma arexpfiniteaux1:
shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> \<forall>bs. bsimp x42 \<noteq> AONE bs"
apply(erule contrapos_pp)
apply simp
apply(erule exE)
apply simp
by (metis bsimp_rerase r_part_neq_whole2 rerase_fuse)
lemma arexpfiniteaux2:
shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> bsimp x42 \<noteq> AZERO "
apply(erule contrapos_pp)
apply simp
done
lemma arexpfiniteaux3:
shows "rerase (bsimp_ASEQ x41 (bsimp x42) (bsimp x43)) = RSEQ (rerase x42) (rerase x43) \<Longrightarrow> bsimp x43 \<noteq> AZERO "
apply(erule contrapos_pp)
apply simp
done
lemma aux_aux_aux:
shows "map rerase (flts (map bsimp rs)) = map rerase rs \<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
oops
inductive leq1 ("_ \<le>1 _" [80, 80] 80) where
"r1 \<le>1 r1"
| "AZERO \<le>1 ASEQ bs AZERO r"
| "AZERO \<le>1 ASEQ bs r AZERO"
| "fuse (bs @ bs1) r2 \<le>1 ASEQ bs (AONE bs1) r2"
| " AALTs bs (rs1 @ rs) \<le>1 AALTs bs (rs1 @( AZERO # rs))"
| "r2 \<le>1 r1 \<Longrightarrow> AALTs bs (rs1 @ r2 # rs) \<le>1 AALTs bs (rs1 @ r1 # rs)"
| "AALTs bs1 (rsa @ (map (fuse bs1) rs1) @ rsb) \<le>1 AALTs bs1 (rsa @ (AALTs bs1 rs1) # rsb)"
| "rerase a1 = rerase a2 \<Longrightarrow> AALTs bs (rsa @ [a1] @ rsb @ rsc) \<le>1 AALTs bs (rsa @ [a1] @ rsb @ [a2] @ rsc) "
| "r1 \<le>1 r2 \<Longrightarrow> r1 \<le>1 ASEQ bs (AONE bs1) r2"
lemma leq1_less_or_equal: shows
"r1 \<le>1 r2 \<Longrightarrow> r1 = r2 \<or> rerase r1 \<noteq> rerase r2"
apply(induct rule: leq1.induct)
apply simp+
sorry
lemma bsimp_leq1:
shows "bsimp r \<le>1 r"
sorry
lemma arexpfiniteaux4_aux:
shows" \<lbrakk>rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs) \<rbrakk>
\<Longrightarrow> map rerase (map bsimp rs) = map rerase rs"
apply(induct rs)
apply simp
apply simp
apply auto
prefer 2
sorry
lemma arexpfiniteaux4:
shows"
\<lbrakk>\<And>x. \<lbrakk>x \<in> set rs; rerase (bsimp x) = rerase x\<rbrakk> \<Longrightarrow> bsimp x = x;
rerase (bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {})) = RALTS (map rerase rs)\<rbrakk>
\<Longrightarrow> bsimp_AALTs bs1 (distinctWith (flts (map bsimp rs)) eq1 {}) = AALTs bs1 rs"
apply(induct rs)
apply simp
sorry
lemma arexp_finite1:
shows "rerase (bsimp b) = rerase b \<Longrightarrow> bsimp b = b"
apply(induct rule: bsimp.induct)
apply simp
apply (smt (verit) arexpfiniteaux1 arexpfiniteaux2 arexpfiniteaux3 bsimp_ASEQ1 rerase.simps(5) rrexp.inject(2))
apply simp
using arexpfiniteaux4 apply blast
apply simp+
done
(*
apply(induct b)
apply simp+
apply(case_tac "bsimp b2 = AZERO")
apply simp
apply (case_tac "bsimp b1 = AZERO")
apply simp
apply(case_tac "\<exists>bs. bsimp b1 = AONE bs")
using arexpfiniteaux1 apply blast
apply simp
apply(subgoal_tac "bsimp_ASEQ x1 (bsimp b1) (bsimp b2) = ASEQ x1 (bsimp b1) (bsimp b2)")
apply simp
using bsimp_ASEQ1 apply presburger
apply simp
sorry
*)
lemma bitcodes_unchanging2:
assumes "bsimp a = b"
and "a ~1 b"
shows "a = b"
using assms
apply(induct rule: eq1.induct)
apply simp
apply simp
apply simp
apply auto
sorry
lemma bitcodes_unchanging:
shows "\<lbrakk>bsimp a = b; rerase a = rerase b \<rbrakk> \<Longrightarrow> a = b"
apply(induction a arbitrary: b)
apply simp+
apply(case_tac "\<exists>bs. bsimp a1 = AONE bs")
apply(erule exE)
apply simp
prefer 2
apply(case_tac "bsimp a1 = AZERO")
apply simp
apply simp
apply (metis BlexerSimp.bsimp_ASEQ0 bsimp_ASEQ1 rerase.simps(1) rerase.simps(5) rrexp.distinct(5) rrexp.inject(2))
sorry
lemma bagnostic_shows_bsimp_idem:
assumes "bitcode_agnostic bsimp"
and "rerase (bsimp a) = rsimp (rerase a)"
and "rsimp r = rsimp (rsimp r)"
shows "bsimp a = bsimp (bsimp a)"
oops
theorem bsimp_idem:
shows "bsimp (bsimp a) = bsimp a"
using bitcodes_unchanging bsimp_rerase rsimp_idem by auto
unused_thms
end