--- a/thys3/FBound.thy Sat Apr 30 00:50:08 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,180 +0,0 @@
-
-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)"
-
-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)
-
-
-unused_thms
-
-end