# Theory FinFunPred

theory FinFunPred
imports FinFun
```(*  Author:     Andreas Lochbihler *)

section ‹Predicates modelled as FinFuns›

theory FinFunPred
imports "~~/src/HOL/Library/FinFun"
begin

unbundle finfun_syntax

text ‹Instantiate FinFun predicates just like predicates›

type_synonym 'a pred⇩f = "'a ⇒f bool"

instantiation "finfun" :: (type, ord) ord
begin

definition le_finfun_def [code del]: "f ≤ g ⟷ (∀x. f \$ x ≤ g \$ x)"

definition [code del]: "(f::'a ⇒f 'b) < g ⟷ f ≤ g ∧ ¬ g ≤ f"

instance ..

lemma le_finfun_code [code]:
"f ≤ g ⟷ finfun_All ((λ(x, y). x ≤ y) ∘\$ (\$f, g\$))"

end

instance "finfun" :: (type, preorder) preorder
by(intro_classes)(auto simp add: less_finfun_def le_finfun_def intro: order_trans)

instance "finfun" :: (type, order) order
by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)

instantiation "finfun" :: (type, order_bot) order_bot begin
definition "bot = finfun_const bot"
end

lemma bot_finfun_apply [simp]: "op \$ bot = (λ_. bot)"

instantiation "finfun" :: (type, order_top) order_top begin
definition "top = finfun_const top"
end

lemma top_finfun_apply [simp]: "op \$ top = (λ_. top)"

instantiation "finfun" :: (type, inf) inf begin
definition [code]: "inf f g = (λ(x, y). inf x y) ∘\$ (\$f, g\$)"
instance ..
end

lemma inf_finfun_apply [simp]: "op \$ (inf f g) = inf (op \$ f) (op \$ g)"
by(auto simp add: inf_finfun_def o_def inf_fun_def)

instantiation "finfun" :: (type, sup) sup begin
definition [code]: "sup f g = (λ(x, y). sup x y) ∘\$ (\$f, g\$)"
instance ..
end

lemma sup_finfun_apply [simp]: "op \$ (sup f g) = sup (op \$ f) (op \$ g)"
by(auto simp add: sup_finfun_def o_def sup_fun_def)

instance "finfun" :: (type, semilattice_inf) semilattice_inf

instance "finfun" :: (type, semilattice_sup) semilattice_sup

instance "finfun" :: (type, lattice) lattice ..

instance "finfun" :: (type, bounded_lattice) bounded_lattice
by(intro_classes)

instance "finfun" :: (type, distrib_lattice) distrib_lattice
by(intro_classes)(simp add: sup_finfun_def inf_finfun_def expand_finfun_eq o_def sup_inf_distrib1)

instantiation "finfun" :: (type, minus) minus begin
definition "f - g = case_prod (op -) ∘\$ (\$f, g\$)"
instance ..
end

lemma minus_finfun_apply [simp]: "op \$ (f - g) = op \$ f - op \$ g"

instantiation "finfun" :: (type, uminus) uminus begin
definition "- A = uminus ∘\$ A"
instance ..
end

lemma uminus_finfun_apply [simp]: "op \$ (- g) = - op \$ g"

instance "finfun" :: (type, boolean_algebra) boolean_algebra
by(intro_classes)
(simp_all add: uminus_finfun_def inf_finfun_def expand_finfun_eq sup_fun_def inf_fun_def fun_Compl_def o_def inf_compl_bot sup_compl_top diff_eq)

text ‹
Replicate predicate operations for FinFuns
›

abbreviation finfun_empty :: "'a pred⇩f" ("{}⇩f")
where "{}⇩f ≡ bot"

abbreviation finfun_UNIV :: "'a pred⇩f"
where "finfun_UNIV ≡ top"

definition finfun_single :: "'a ⇒ 'a pred⇩f"
where [code]: "finfun_single x = finfun_empty(x \$:= True)"

lemma finfun_single_apply [simp]:
"finfun_single x \$ y ⟷ x = y"

lemma [iff]:
shows finfun_single_neq_bot: "finfun_single x ≠ bot"
and bot_neq_finfun_single: "bot ≠ finfun_single x"

lemma finfun_leI [intro!]: "(!!x. A \$ x ⟹ B \$ x) ⟹ A ≤ B"

lemma finfun_leD [elim]: "⟦ A ≤ B; A \$ x ⟧ ⟹ B \$ x"

text ‹Bounded quantification.
Warning: ‹finfun_Ball› and ‹finfun_Ex› may raise an exception, they should not be used for quickcheck
›

definition finfun_Ball_except :: "'a list ⇒ 'a pred⇩f ⇒ ('a ⇒ bool) ⇒ bool"
where [code del]: "finfun_Ball_except xs A P = (∀a. A \$ a ⟶ a ∈ set xs ∨ P a)"

lemma finfun_Ball_except_const:
"finfun_Ball_except xs (K\$ b) P ⟷ ¬ b ∨ set xs = UNIV ∨ Code.abort (STR ''finfun_ball_except'') (λu. finfun_Ball_except xs (K\$ b) P)"

lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
"finfun_Ball_except xs (K\$ b) P ⟷ ¬ b ∨ is_list_UNIV xs ∨ Code.abort (STR ''finfun_ball_except'') (λu. finfun_Ball_except xs (K\$ b) P)"

lemma finfun_Ball_except_update:
"finfun_Ball_except xs (A(a \$:= b)) P = ((a ∈ set xs ∨ (b ⟶ P a)) ∧ finfun_Ball_except (a # xs) A P)"
by(fastforce simp add: finfun_Ball_except_def finfun_upd_apply split: if_split_asm)

lemma finfun_Ball_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
shows "finfun_Ball_except xs (finfun_update_code f a b) P = ((a ∈ set xs ∨ (b ⟶ P a)) ∧ finfun_Ball_except (a # xs) f P)"

definition finfun_Ball :: "'a pred⇩f ⇒ ('a ⇒ bool) ⇒ bool"
where [code del]: "finfun_Ball A P = Ball {x. A \$ x} P"

lemma finfun_Ball_code [code]: "finfun_Ball = finfun_Ball_except []"
by(auto intro!: ext simp add: finfun_Ball_except_def finfun_Ball_def)

definition finfun_Bex_except :: "'a list ⇒ 'a pred⇩f ⇒ ('a ⇒ bool) ⇒ bool"
where [code del]: "finfun_Bex_except xs A P = (∃a. A \$ a ∧ a ∉ set xs ∧ P a)"

lemma finfun_Bex_except_const:
"finfun_Bex_except xs (K\$ b) P ⟷ b ∧ set xs ≠ UNIV ∧ Code.abort (STR ''finfun_Bex_except'') (λu. finfun_Bex_except xs (K\$ b) P)"

lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
"finfun_Bex_except xs (K\$ b) P ⟷ b ∧ ¬ is_list_UNIV xs ∧ Code.abort (STR ''finfun_Bex_except'') (λu. finfun_Bex_except xs (K\$ b) P)"

lemma finfun_Bex_except_update:
"finfun_Bex_except xs (A(a \$:= b)) P ⟷ (a ∉ set xs ∧ b ∧ P a) ∨ finfun_Bex_except (a # xs) A P"
by(fastforce simp add: finfun_Bex_except_def finfun_upd_apply dest: bspec split: if_split_asm)

lemma finfun_Bex_except_update_code [code]:
fixes a :: "'a :: card_UNIV"
shows "finfun_Bex_except xs (finfun_update_code f a b) P ⟷ ((a ∉ set xs ∧ b ∧ P a) ∨ finfun_Bex_except (a # xs) f P)"

definition finfun_Bex :: "'a pred⇩f ⇒ ('a ⇒ bool) ⇒ bool"
where [code del]: "finfun_Bex A P = Bex {x. A \$ x} P"

lemma finfun_Bex_code [code]: "finfun_Bex = finfun_Bex_except []"
by(auto intro!: ext simp add: finfun_Bex_except_def finfun_Bex_def)

text ‹Automatically replace predicate operations by finfun predicate operations where possible›

lemma iso_finfun_le [code_unfold]:
"op \$ A ≤ op \$ B ⟷ A ≤ B"
by (metis le_finfun_def le_funD le_funI)

lemma iso_finfun_less [code_unfold]:
"op \$ A < op \$ B ⟷ A < B"
by (metis iso_finfun_le less_finfun_def less_fun_def)

lemma iso_finfun_eq [code_unfold]:
"op \$ A = op \$ B ⟷ A = B"
by(simp only: expand_finfun_eq)

lemma iso_finfun_sup [code_unfold]:
"sup (op \$ A) (op \$ B) = op \$ (sup A B)"
by(simp)

lemma iso_finfun_disj [code_unfold]:
"A \$ x ∨ B \$ x ⟷ sup A B \$ x"

lemma iso_finfun_inf [code_unfold]:
"inf (op \$ A) (op \$ B) = op \$ (inf A B)"
by(simp)

lemma iso_finfun_conj [code_unfold]:
"A \$ x ∧ B \$ x ⟷ inf A B \$ x"

lemma iso_finfun_empty_conv [code_unfold]:
"(λ_. False) = op \$ {}⇩f"
by simp

lemma iso_finfun_UNIV_conv [code_unfold]:
"(λ_. True) = op \$ finfun_UNIV"
by simp

lemma iso_finfun_upd [code_unfold]:
fixes A :: "'a pred⇩f"
shows "(op \$ A)(x := b) = op \$ (A(x \$:= b))"

lemma iso_finfun_uminus [code_unfold]:
fixes A :: "'a pred⇩f"
shows "- op \$ A = op \$ (- A)"
by(simp)

lemma iso_finfun_minus [code_unfold]:
fixes A :: "'a pred⇩f"
shows "op \$ A - op \$ B = op \$ (A - B)"
by(simp)

text ‹
Do not declare the following two theorems as ‹[code_unfold]›,
because this causes quickcheck to fail frequently when bounded quantification is used which raises an exception.
For code generation, the same problems occur, but then, no randomly generated FinFun is usually around.
›

lemma iso_finfun_Ball_Ball:
"(∀x. A \$ x ⟶ P x) ⟷ finfun_Ball A P"

lemma iso_finfun_Bex_Bex:
"(∃x. A \$ x ∧ P x) ⟷ finfun_Bex A P"

text ‹Test code setup›

have "inf ((λ_ :: nat. False)(1 := True, 2 := True)) ((λ_. True)(3 := False)) ≤
sup ((λ_. False)(1 := True, 5 := True)) (- ((λ_. True)(2 := False, 3 := False)))"
by eval
end

declare iso_finfun_Ball_Ball[code_unfold]