theory "Cardinality-Domain-Lists" imports "Vars" "Nominal-HOLCF" "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