Theory TTree-HOLCF

theory "TTree-HOLCF"
imports TTree "Launchbury.HOLCF-Utils" "Set-Cpo" "Launchbury.HOLCF-Join-Classes"
begin

instantiation ttree :: (type) below
begin
  lift_definition below_ttree :: "'a ttree ⇒ 'a ttree ⇒ bool" is "(⊆)".
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 cong add: SUP_cong_simp)
  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 (=)) (rel_fun (pcr_ttree (=)) (pcr_ttree (=))) (∪) (⊔)"
proof-
  have "(⊔) = ((⊕⊕) :: '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