Theory Cardinality-Domain-Lists

theory "Cardinality-Domain-Lists"
imports Launchbury.Vars "Launchbury.Nominal-HOLCF" Launchbury.Env "Cardinality-Domain" "Set-Cpo" "Env-Set-Cpo"
begin

fun no_call_in_path where
  "no_call_in_path x [] ⟷ True"
 | "no_call_in_path x (y#xs) ⟷ y ≠ x ∧ no_call_in_path x xs"

fun one_call_in_path where
  "one_call_in_path x [] ⟷ True"
 | "one_call_in_path x (y#xs) ⟷ (if x = y then no_call_in_path x xs else one_call_in_path x xs)"

lemma no_call_in_path_set_conv:
  "no_call_in_path x p ⟷ x ∉ set p"
  by(induction p) auto 

lemma one_call_in_path_filter_conv:
  "one_call_in_path x p ⟷ length (filter (λ x'. x' = x) p) ≤ 1"
  by(induction p) (auto simp add: no_call_in_path_set_conv filter_empty_conv)

lemma no_call_in_tail: "no_call_in_path x (tl p) ⟷ (no_call_in_path x p ∨ one_call_in_path x p ∧ hd p = x)"
  by(induction p) auto

lemma no_imp_one: "no_call_in_path x p ⟹ one_call_in_path x p"
  by (induction p) auto

lemma one_imp_one_tail: "one_call_in_path x p ⟹ one_call_in_path x (tl p)"
  by (induction p) (auto split: if_splits intro: no_imp_one)

lemma more_than_one_setD:
  "¬ one_call_in_path x p ⟹ x ∈ set p" 
  by (induction p) (auto split: if_splits)

lemma no_call_in_path[eqvt]: "no_call_in_path p x ⟹ no_call_in_path (π ∙ p) (π ∙ x)"
  by (induction p x rule: no_call_in_path.induct) auto

lemma one_call_in_path[eqvt]: "one_call_in_path p x ⟹ one_call_in_path (π ∙ p) (π ∙ x)"
  by (induction p x rule: one_call_in_path.induct) (auto dest: no_call_in_path)

definition pathCard :: "var list  ⇒ (var ⇒ two)"
  where "pathCard p x = (if no_call_in_path x p then none else (if one_call_in_path x p then once else many))"

lemma pathCard_Nil[simp]: "pathCard [] = ⊥"
   by rule (simp add: pathCard_def)

lemma pathCard_Cons[simp]: "pathCard (x#xs) x = two_add⋅once⋅(pathCard xs x)"
  unfolding pathCard_def
  by (auto simp add: two_add_simp)

lemma pathCard_Cons_other[simp]: "x' ≠ x ⟹ pathCard (x#xs) x' = pathCard xs x'"
  unfolding pathCard_def by auto

lemma no_call_in_path_filter[simp]: "no_call_in_path x [x←xs . x ∈ S] ⟷ no_call_in_path x xs ∨ x ∉ S"
  by (induction xs) auto

lemma one_call_in_path_filter[simp]: "one_call_in_path x [x←xs . x ∈ S] ⟷ one_call_in_path x xs ∨ x ∉ S"
  by (induction xs) auto

definition pathsCard :: "var list set ⇒ (var ⇒ two)"
  where "pathsCard ps x = (if (∀ p ∈ ps. no_call_in_path x p) then none else (if (∀ p∈ps. one_call_in_path x p) then once else many))"

lemma paths_Card_above:
  "p ∈ ps ⟹ pathCard p ⊑ pathsCard ps"
  by (rule fun_belowI) (auto simp add: pathsCard_def pathCard_def)

lemma pathsCard_below:
  assumes  "⋀ p. p ∈ ps ⟹ pathCard p ⊑ ce"
  shows "pathsCard ps ⊑ ce"
proof(rule fun_belowI)
  fix x
  show "pathsCard ps x ⊑ ce x"
    by (auto simp add: pathsCard_def pathCard_def split: if_splits dest!: fun_belowD[OF assms, where x = x] elim: below_trans[rotated] dest: no_imp_one)
qed

lemma pathsCard_mono:
  "ps ⊆ ps' ⟹ pathsCard ps ⊑ pathsCard ps'"
  by (auto intro: pathsCard_below paths_Card_above)

lemmas pathsCard_mono' = pathsCard_mono[folded below_set_def]

lemma record_call_pathsCard: 
  "pathsCard ({ tl p | p . p ∈ fs ∧ hd p = x}) ⊑ record_call x⋅(pathsCard fs)"
proof (rule pathsCard_below)
  fix p'
  assume "p' ∈ {tl p |p. p ∈ fs ∧ hd p = x}"
  then obtain p where "p' = tl p" and "p ∈ fs" and "hd p = x" by auto
  
  have "pathCard (tl p) ⊑ record_call x⋅(pathCard p)"
    apply (rule fun_belowI)
    using ‹hd p = x› by (auto simp add: pathCard_def record_call_simp no_call_in_tail dest: one_imp_one_tail)
    
  hence "pathCard (tl p) ⊑ record_call x⋅(pathsCard fs)"
    by (rule below_trans[OF _ monofun_cfun_arg[OF  paths_Card_above[OF ‹p ∈ fs›]]])
  thus "pathCard p' ⊑ record_call x⋅(pathsCard fs)" using ‹p' = _› by simp
qed
  
lemma pathCards_noneD:
  "pathsCard ps x = none ⟹ x ∉ ⋃(set ` ps)"
  by (auto simp add: pathsCard_def no_call_in_path_set_conv split:if_splits)

lemma cont_pathsCard[THEN cont_compose, cont2cont, simp]:
  "cont pathsCard"
  by(fastforce intro!: cont2cont_lambda cont_if_else_above simp add: pathsCard_def below_set_def)

lemma pathsCard_eqvt[eqvt]: "π ∙ pathsCard ps x = pathsCard (π ∙ ps) (π ∙ x)"
  unfolding pathsCard_def by perm_simp rule

lemma edom_pathsCard[simp]: "edom (pathsCard ps) = ⋃(set ` ps)"
  unfolding edom_def pathsCard_def
  by (auto simp add:  no_call_in_path_set_conv)

lemma env_restr_pathsCard[simp]: "pathsCard ps f|` S = pathsCard (filter (λ x. x ∈ S) ` ps)"
  by (auto simp add: pathsCard_def lookup_env_restr_eq)


end