theory "TTree-HOLCF" imports TTree "HOLCF-Utils" "Set-Cpo" "HOLCF-Join-Classes" begin instantiation ttree :: (type) below begin lift_definition below_ttree :: "'a ttree ⇒ 'a ttree ⇒ bool" is "op ⊆". instance.. end lemma paths_mono: "t ⊑ t' ⟹ paths t ⊑ paths t'" by transfer (auto simp add: below_set_def) lemma paths_mono_iff: "paths t ⊑ paths t' ⟷ t ⊑ t'" by transfer (auto simp add: below_set_def) lemma ttree_belowI: "(⋀ xs. xs ∈ paths t ⟹ xs ∈ paths t') ⟹ t ⊑ t'" by transfer auto lemma paths_belowI: "(⋀ x xs. x#xs ∈ paths t ⟹ x#xs ∈ paths t') ⟹ t ⊑ t'" apply (rule ttree_belowI) apply (case_tac xs) apply auto done instance ttree :: (type) po by standard (transfer, simp)+ lemma is_lub_ttree: "S <<| Either S" unfolding is_lub_def is_ub_def by transfer auto lemma lub_is_either: "lub S = Either S" using is_lub_ttree by (rule lub_eqI) instance ttree :: (type) cpo by standard (rule exI, rule is_lub_ttree) lemma minimal_ttree[simp, intro!]: "empty ⊑ S" by transfer simp instance ttree :: (type) pcpo by standard (rule+) lemma empty_is_bottom: "empty = ⊥" by (metis below_bottom_iff minimal_ttree) lemma carrier_bottom[simp]: "carrier ⊥ = {}" unfolding empty_is_bottom[symmetric] by simp lemma below_anything[simp]: "t ⊑ anything" by transfer auto lemma carrier_mono: "t ⊑ t' ⟹ carrier t ⊆ carrier t'" by transfer auto lemma nxt_mono: "t ⊑ t' ⟹ nxt t x ⊑ nxt t' x" by transfer auto lemma either_above_arg1: "t ⊑ t ⊕⊕ t'" by transfer fastforce lemma either_above_arg2: "t' ⊑ t ⊕⊕ t'" by transfer fastforce lemma either_belowI: "t ⊑ t'' ⟹ t' ⊑ t'' ⟹ t ⊕⊕ t' ⊑ t''" by transfer auto lemma both_above_arg1: "t ⊑ t ⊗⊗ t'" by transfer fastforce lemma both_above_arg2: "t' ⊑ t ⊗⊗ t'" by transfer fastforce lemma both_mono1': "t ⊑ t' ⟹ t ⊗⊗ t'' ⊑ t' ⊗⊗ t''" using both_mono1[folded below_set_def, unfolded paths_mono_iff]. lemma both_mono2': "t ⊑ t' ⟹ t'' ⊗⊗ t ⊑ t'' ⊗⊗ t'" using both_mono2[folded below_set_def, unfolded paths_mono_iff]. lemma nxt_both_left: "possible t x ⟹ nxt t x ⊗⊗ t' ⊑ nxt (t ⊗⊗ t') x" by (auto simp add: nxt_both either_above_arg2) lemma nxt_both_right: "possible t' x ⟹ t ⊗⊗ nxt t' x ⊑ nxt (t ⊗⊗ t') x" by (auto simp add: nxt_both either_above_arg1) lemma substitute_mono1': "f ⊑ f'⟹ substitute f T t ⊑ substitute f' T t" using substitute_mono1[folded below_set_def, unfolded paths_mono_iff] fun_belowD by metis lemma substitute_mono2': "t ⊑ t'⟹ substitute f T t ⊑ substitute f T t'" using substitute_mono2[folded below_set_def, unfolded paths_mono_iff]. lemma substitute_above_arg: "t ⊑ substitute f T t" using substitute_contains_arg[folded below_set_def, unfolded paths_mono_iff]. lemma ttree_contI: assumes "⋀ S. f (Either S) = Either (f ` S)" shows "cont f" proof(rule contI) fix Y :: "nat ⇒ 'a ttree" have "range (λi. f (Y i)) = f ` range Y" by auto also have "Either … = f (Either (range Y))" unfolding assms(1).. also have "Either (range Y) = lub (range Y)" unfolding lub_is_either by simp finally show "range (λi. f (Y i)) <<| f (⨆ i. Y i)" by (metis is_lub_ttree) qed lemma ttree_contI2: assumes "⋀ x. paths (f x) = ⋃(t ` paths x)" assumes "[] ∈ t []" shows "cont f" proof(rule contI) fix Y :: "nat ⇒ 'a ttree" have "paths (Either (range (λi. f (Y i)))) = insert [] (⋃x. paths (f (Y x)))" by (simp add: paths_Either) also have "… = insert [] (⋃x. ⋃(t ` paths (Y x)))" by (simp add: assms(1)) also have "… = ⋃(t ` insert [] (⋃x. paths (Y x)))" using assms(2) by (auto 0 4) also have "… = ⋃(t ` paths (Either (range Y)))" by (auto simp add: paths_Either) also have "… = paths (f (Either (range Y)))" by (simp add: assms(1)) also have "… = paths (f (lub (range Y)))" unfolding lub_is_either by simp finally show "range (λi. f (Y i)) <<| f (⨆ i. Y i)" by (metis is_lub_ttree paths_inj) qed lemma cont_paths[THEN cont_compose, cont2cont, simp]: "cont paths" apply (rule set_contI) apply (thin_tac _) unfolding lub_is_either apply transfer apply auto done lemma ttree_contI3: assumes "cont (λ x. paths (f x))" shows "cont f" apply (rule contI2) apply (rule monofunI) apply (subst paths_mono_iff[symmetric]) apply (erule cont2monofunE[OF assms]) apply (subst paths_mono_iff[symmetric]) apply (subst cont2contlubE[OF cont_paths[OF cont_id]], assumption) apply (subst cont2contlubE[OF assms], assumption) apply rule done lemma cont_substitute[THEN cont_compose, cont2cont, simp]: "cont (substitute f T)" apply (rule ttree_contI2) apply (rule paths_substitute_substitute'') apply (auto intro: substitute''.intros) done lemma cont_both1: "cont (λ x. both x y)" apply (rule ttree_contI2[where t = "λxs . {zs . ∃ys∈paths y. zs ∈ xs ⊗ ys}"]) apply (rule set_eqI) by (auto intro: simp add: paths_both) lemma cont_both2: "cont (λ x. both y x)" apply (rule ttree_contI2[where t = "λys . {zs . ∃xs∈paths y. zs ∈ xs ⊗ ys}"]) apply (rule set_eqI) by (auto intro: simp add: paths_both) lemma cont_both[cont2cont,simp]: "cont f ⟹ cont g ⟹ cont (λ x. f x ⊗⊗ g x)" by (rule cont_compose2[OF cont_both1 cont_both2]) lemma cont_intersect1: "cont (λ x. intersect x y)" by (rule ttree_contI2 [where t = "λxs . (if xs ∈ paths y then {xs} else {})"]) (auto split: if_splits) lemma cont_intersect2: "cont (λ x. intersect y x)" by (rule ttree_contI2 [where t = "λxs . (if xs ∈ paths y then {xs} else {})"]) (auto split: if_splits) lemma cont_intersect[cont2cont,simp]: "cont f ⟹ cont g ⟹ cont (λ x. f x ∩∩ g x)" by (rule cont_compose2[OF cont_intersect1 cont_intersect2]) lemma cont_without[THEN cont_compose, cont2cont,simp]: "cont (without x)" by (rule ttree_contI2[where t = "λ xs.{filter (λ x'. x' ≠ x) xs}"]) (transfer, auto) lemma paths_many_calls_subset: "t ⊑ many_calls x ⊗⊗ without x t" by (metis (full_types) below_set_def paths_many_calls_subset paths_mono_iff) lemma single_below: "[x] ∈ paths t ⟹ single x ⊑ t" by transfer auto lemma cont_ttree_restr[THEN cont_compose, cont2cont,simp]: "cont (ttree_restr S)" by (rule ttree_contI2[where t = "λ xs.{filter (λ x'. x' ∈ S) xs}"]) (transfer, auto) lemmas ttree_restr_mono = cont2monofunE[OF cont_ttree_restr[OF cont_id]] lemma range_filter[simp]: "range (filter P) = {xs. set xs ⊆ Collect P}" apply auto apply (rule_tac x = x in rev_image_eqI) apply simp apply (rule sym) apply (auto simp add: filter_id_conv) done lemma ttree_restr_anything_cont[THEN cont_compose, simp, cont2cont]: "cont (λ S. ttree_restr S anything)" apply (rule ttree_contI3) apply (rule set_contI) apply (auto simp add: filter_paths_conv_free_restr[symmetric] lub_set) apply (rule finite_subset_chain) apply auto done instance ttree :: (type) Finite_Join_cpo proof fix x y :: "'a ttree" show "compatible x y" unfolding compatible_def apply (rule exI) apply (rule is_lub_ttree) done qed lemma ttree_join_is_either: "t ⊔ t' = t ⊕⊕ t'" proof- have "t ⊕⊕ t' = Either {t, t'}" by transfer auto thus "t ⊔ t' = t ⊕⊕ t'" by (metis lub_is_join is_lub_ttree) qed lemma ttree_join_transfer[transfer_rule]: "rel_fun (pcr_ttree op =) (rel_fun (pcr_ttree op =) (pcr_ttree op =)) op ∪ op ⊔" proof- have "op ⊔ = (op ⊕⊕ :: 'a ttree ⇒ 'a ttree ⇒ 'a ttree)" using ttree_join_is_either by blast thus ?thesis using either.transfer by metis qed lemma ttree_restr_join[simp]: "ttree_restr S (t ⊔ t') = ttree_restr S t ⊔ ttree_restr S t'" by transfer auto lemma nxt_singles_below_singles: "nxt (singles S) x ⊑ singles S" apply auto apply transfer apply auto apply (erule_tac x = xc in ballE) apply (erule order_trans[rotated]) apply (rule length_filter_mono) apply simp apply simp done lemma in_carrier_fup[simp]: "x' ∈ carrier (fup⋅f⋅u) ⟷ (∃ u'. u = up⋅u' ∧ x' ∈ carrier (f⋅u'))" by (cases u) auto end