(* Author: Dmitriy Traytel *) section "Initial Normalization of the Input" (*<*) theory Init_Normalization imports Pi_Regular_Exp "HOL-Library.Simps_Case_Conv" begin (*>*) fun toplevel_inters where "toplevel_inters (Inter r s) = toplevel_inters r ∪ toplevel_inters s" | "toplevel_inters r = {r}" lemma toplevel_inters_nonempty[simp]: "toplevel_inters r ≠ {}" by (induct r) auto lemma toplevel_inters_finite[simp]: "finite (toplevel_inters r)" by (induct r) auto context alphabet begin lemma toplevel_inters_wf: "wf n s = (∀r∈toplevel_inters s. wf n r)" by (induct s) auto end context project begin lemma toplevel_inters_lang: "r ∈ toplevel_inters s ⟹ lang n s ⊆ lang n r" by (induct s) auto lemma toplevel_inters_lang_INT: "lang n s = (⋂r∈toplevel_inters s. lang n r)" by (induct s) auto lemma toplevel_inters_in_lang: "w ∈ lang n s = (∀r∈toplevel_inters s. w ∈ lang n r)" by (induct s) auto lemma lang_flatten_INTERSECT_finite[simp]: "finite X ⟹ w ∈ lang n (flatten INTERSECT X) = (if X = {} then w ∈ lists (Σ n) else (∀r ∈ X. w ∈ lang n r))" unfolding lang_INTERSECT by auto end fun merge_distinct where "merge_distinct [] xs = xs" | "merge_distinct xs [] = xs" | "merge_distinct (a # xs) (b # ys) = (if a = b then merge_distinct xs (b # ys) else if a < b then a # merge_distinct xs (b # ys) else b # merge_distinct (a # xs) ys)" lemma set_merge_distinct[simp]: "set (merge_distinct xs ys) = set xs ∪ set ys" by (induct xs ys rule: merge_distinct.induct) auto lemma sorted_merge_distinct[simp]: "⟦sorted xs; sorted ys⟧ ⟹ sorted (merge_distinct xs ys)" by (induct xs ys rule: merge_distinct.induct) (auto) lemma distinct_merge_distinct[simp]: "⟦sorted xs; distinct xs; sorted ys; distinct ys⟧ ⟹ distinct (merge_distinct xs ys)" by (induct xs ys rule: merge_distinct.induct) (auto) lemma sorted_list_of_set_merge_distinct[simp]: "⟦sorted xs; distinct xs; sorted ys; distinct ys⟧ ⟹ merge_distinct xs ys = sorted_list_of_set (set xs ∪ set ys)" by (auto intro: sorted_distinct_set_unique) fun zip_with_option where "zip_with_option f (Some a) (Some b) = Some (f a b)" | "zip_with_option _ _ _ = None" lemma zip_with_option_eq_Some[simp]: "zip_with_option f x y = Some z ⟷ (∃a b. z = f a b ∧ x = Some a ∧ y = Some b)" by (induct f x y rule: zip_with_option.induct) auto fun Pluss where "Pluss (Plus r s) = zip_with_option merge_distinct (Pluss r) (Pluss s)" | "Pluss Zero = Some []" | "Pluss Full = None" | "Pluss r = Some [r]" lemma Pluss_None[symmetric]: "Pluss r = None ⟷ Full ∈ toplevel_summands r" by (induct r) auto lemma Pluss_Some: "Pluss r = Some xs ⟷ (Full ∉ set xs ∧ xs = sorted_list_of_set (toplevel_summands r - {Zero}))" proof (induct r arbitrary: xs) case (Plus r s) show ?case proof safe assume "Pluss (Plus r s) = Some xs" then obtain a b where *: "Pluss r = Some a" "Pluss s = Some b" "xs = merge_distinct a b" by auto with Plus(1)[of a] Plus(2)[of b] show "xs = sorted_list_of_set (toplevel_summands (Plus r s) - {Zero})" by (simp add: Un_Diff) assume "Full ∈ set xs" with Plus(1)[of a] Plus(2)[of b] * show False by (simp add: Pluss_None) next assume "Full ∉ set (sorted_list_of_set (toplevel_summands (Plus r s) - {Zero}))" with Plus(1)[of "sorted_list_of_set (toplevel_summands r - {Zero})"] Plus(2)[of "sorted_list_of_set (toplevel_summands s - {Zero})"] show "Pluss (Plus r s) = Some (sorted_list_of_set (toplevel_summands (Plus r s) - {Zero}))" by (simp add: Un_Diff) qed qed force+ fun Inters where "Inters (Inter r s) = zip_with_option merge_distinct (Inters r) (Inters s)" | "Inters Zero = None" | "Inters Full = Some []" | "Inters r = Some [r]" lemma Inters_None[symmetric]: "Inters r = None ⟷ Zero ∈ toplevel_inters r" by (induct r) auto lemma Inters_Some: "Inters r = Some xs ⟷ (Zero ∉ set xs ∧ xs = sorted_list_of_set (toplevel_inters r - {Full}))" proof (induct r arbitrary: xs) case (Inter r s) show ?case proof safe assume "Inters (Inter r s) = Some xs" then obtain a b where *: "Inters r = Some a" "Inters s = Some b" "xs = merge_distinct a b" by auto with Inter(1)[of a] Inter(2)[of b] show "xs = sorted_list_of_set (toplevel_inters (Inter r s) - {Full})" by (simp add: Un_Diff) assume "Zero ∈ set xs" with Inter(1)[of a] Inter(2)[of b] * show False by (simp add: Inters_None) next assume "Zero ∉ set (sorted_list_of_set (toplevel_inters (Inter r s) - {Full}))" with Inter(1)[of "sorted_list_of_set (toplevel_inters r - {Full})"] Inter(2)[of "sorted_list_of_set (toplevel_inters s - {Full})"] show "Inters (Inter r s) = Some (sorted_list_of_set (toplevel_inters (Inter r s) - {Full}))" by (simp add: Un_Diff) qed qed force+ definition inPlus where "inPlus r s = (case Pluss (Plus r s) of None ⇒ Full | Some rs ⇒ PLUS rs)" lemma inPlus_alt: "inPlus r s = (let X = toplevel_summands (Plus r s) - {Zero} in flatten PLUS (if Full ∈ X then {Full} else X))" proof (cases "Pluss r" "Pluss s" rule: option.exhaust[case_product option.exhaust]) case Some_Some then show ?thesis by (simp add: inPlus_def Pluss_None) (simp add: Pluss_Some Un_Diff) qed (simp_all add: inPlus_def Pluss_None)