header {*
Sets modelled as FinFuns
*}
theory FinFunSet imports FinFun begin
text {* Instantiate FinFun predicates just like predicates as sets in Set.thy *}
types 'a setf = "'a =>f bool"
instantiation "finfun" :: (type, ord) ord
begin
definition
le_finfun_def [code del]: "f ≤ g <-> (∀x. ff x ≤ gf x)"
definition
less_fun_def: "(f::'a =>f 'b) < g <-> f ≤ g ∧ f ≠ g"
instance ..
lemma le_finfun_code [code]:
"f ≤ g <-> finfun_All ((λ(x, y). x ≤ y) of (f, g)f)"
by(simp add: le_finfun_def finfun_All_All o_def)
end
instantiation "finfun" :: (type, minus) minus
begin
definition
finfun_diff_def: "A - B = split (op -) of (A, B)f"
instance ..
end
instantiation "finfun" :: (type, uminus) uminus
begin
definition
finfun_Compl_def: "- A = uminus of A"
instance ..
end
text {*
Replicate set operations for FinFuns
*}
definition finfun_empty :: "'a setf" ("{}f")
where "{}f ≡ (λf False)"
definition finfun_insert :: "'a => 'a setf => 'a setf" ("insertf")
where "insertf a A = A(f a := True)"
definition finfun_mem :: "'a => 'a setf => bool" ("_/ ∈f _" [50, 51] 50)
where "a ∈f A = Af a"
definition finfun_UNIV :: "'a setf"
where "finfun_UNIV = (λf True)"
definition finfun_Un :: "'a setf => 'a setf => 'a setf" (infixl "∪f" 65)
where "A ∪f B = split (op ∨) of (A, B)f"
definition finfun_Int :: "'a =>f bool => 'a =>f bool => 'a =>f bool" (infixl "∩f" 65)
where "A ∩f B = split (op ∧) of (A, B)f"
abbreviation finfun_subset_eq :: "'a setf => 'a setf => bool" where
"finfun_subset_eq ≡ less_eq"
abbreviation
finfun_subset :: "'a setf => 'a setf => bool" where
"finfun_subset ≡ less"
notation (output)
finfun_subset ("op <f") and
finfun_subset ("(_/ <f _)" [50, 51] 50) and
finfun_subset_eq ("op <=f") and
finfun_subset_eq ("(_/ <=f _)" [50, 51] 50)
notation (xsymbols)
finfun_subset ("op ⊂f") and
finfun_subset ("(_/ ⊂f _)" [50, 51] 50) and
finfun_subset_eq ("op ⊆f") and
finfun_subset_eq ("(_/ ⊆f _)" [50, 51] 50)
notation (HTML output)
finfun_subset ("op ⊂f") and
finfun_subset ("(_/ ⊂f _)" [50, 51] 50) and
finfun_subset_eq ("op ⊆f") and
finfun_subset_eq ("(_/ ⊆f _)" [50, 51] 50)
lemma finfun_mem_empty [simp]: "a ∈f {}f = False"
by(simp add: finfun_mem_def finfun_empty_def)
lemma finfun_subsetI [intro!]: "(!!x. x ∈f A ==> x ∈f B) ==> A ⊆f B"
by(auto simp add: finfun_mem_def le_finfun_def le_bool_def)
lemma finfun_subsetD [elim]: "A ⊆f B ==> c ∈f A ==> c ∈f B"
by(simp add: finfun_mem_def le_finfun_def le_bool_def)
lemma finfun_subset_refl [simp]: "A ⊆f A"
by fast
lemma finfun_set_ext: "(!!x. (x ∈f A) = (x ∈f B)) ==> A = B"
by(simp add: expand_finfun_eq finfun_mem_def expand_fun_eq)
lemma finfun_subset_antisym [intro!]: "A ⊆f B ==> B ⊆f A ==> A = B"
by (iprover intro: finfun_set_ext finfun_subsetD)
lemma finfun_Compl_iff [simp]: "(c ∈f -A) = (¬ c ∈f A)"
by (simp add: finfun_mem_def finfun_Compl_def bool_Compl_def)
lemma finfun_Un_iff [simp]: "(c ∈f A ∪f B) = (c ∈f A | c ∈f B)"
by (simp add: finfun_Un_def finfun_mem_def)
lemma finfun_Int_iff [simp]: "(c ∈f A ∩f B) = (c ∈f A & c ∈f B)"
by(simp add: finfun_Int_def finfun_mem_def)
lemma finfun_Diff_iff [simp]: "(c ∈f A - B) = (c ∈f A & ¬ c ∈f B)"
by (simp add: finfun_mem_def finfun_diff_def bool_diff_def)
lemma finfun_insert_iff [simp]: "(a ∈f insertf b A) = (a = b | a ∈f A)"
by(simp add: finfun_insert_def finfun_mem_def finfun_upd_apply)
text {* A tail-recursive function that never terminates in the code generator *}
definition loop_counting :: "nat => (unit => 'a) => 'a"
where [simp, code del]: "loop_counting n f = f ()"
lemma loop_counting_code [code]: "loop_counting n = loop_counting (Suc n)"
by(simp add: expand_fun_eq)
definition loop :: "(unit => 'a) => 'a"
where [simp, code del]: "loop f = f ()"
lemma loop_code [code]: "loop = loop_counting 0"
by(simp add: expand_fun_eq)
lemma mem_finfun_apply_conv: "x ∈ ff <-> ff x"
by(simp add: mem_def)
text {* Bounded quantification.
Warning: @{text "finfun_Ball"} and @{text "finfun_Ex"} may fail to terminate, they should not be used for quickcheck
*}
definition finfun_Ball_except :: "'a list => 'a setf => ('a => bool) => bool"
where [code del]: "finfun_Ball_except xs A P = (∀a∈Af. a ∈ set xs ∨ P a)"
lemma finfun_Ball_except_const:
"finfun_Ball_except xs (λf b) P <-> ¬ b ∨ set xs = UNIV ∨ loop (λu. finfun_Ball_except xs (λf b) P)"
by(auto simp add: finfun_Ball_except_def mem_finfun_apply_conv)
lemma finfun_Ball_except_const_finfun_UNIV_code [code]:
"finfun_Ball_except xs (λf b) P <-> ¬ b ∨ is_list_UNIV xs ∨ loop (λu. finfun_Ball_except xs (λf b) P)"
by(auto simp add: finfun_Ball_except_def is_list_UNIV_iff mem_finfun_apply_conv)
lemma finfun_Ball_except_update:
"finfun_Ball_except xs (A(f a := b)) P = ((a ∈ set xs ∨ (b --> P a)) ∧ finfun_Ball_except (a # xs) A P)"
by(fastsimp simp add: finfun_Ball_except_def mem_finfun_apply_conv finfun_upd_apply dest: bspec split: split_if_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)"
by(simp add: finfun_Ball_except_update)
definition finfun_Ball :: "'a setf => ('a => bool) => bool"
where [code del]: "finfun_Ball A P = Ball (Af) 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 setf => ('a => bool) => bool"
where [code del]: "finfun_Bex_except xs A P = (∃a∈Af. a ∉ set xs ∧ P a)"
lemma finfun_Bex_except_const: "finfun_Bex_except xs (λf b) P <-> b ∧ set xs ≠ UNIV ∧ loop (λu. finfun_Bex_except xs (λf b) P)"
by(auto simp add: finfun_Bex_except_def mem_finfun_apply_conv)
lemma finfun_Bex_except_const_finfun_UNIV_code [code]:
"finfun_Bex_except xs (λf b) P <-> b ∧ ¬ is_list_UNIV xs ∧ loop (λu. finfun_Bex_except xs (λf b) P)"
by(auto simp add: finfun_Bex_except_def is_list_UNIV_iff mem_finfun_apply_conv)
lemma finfun_Bex_except_update:
"finfun_Bex_except xs (A(f a := b)) P <-> (a ∉ set xs ∧ b ∧ P a) ∨ finfun_Bex_except (a # xs) A P"
by(fastsimp simp add: finfun_Bex_except_def mem_finfun_apply_conv finfun_upd_apply dest: bspec split: split_if_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)"
by(simp add: finfun_Bex_except_update)
definition finfun_Bex :: "'a setf => ('a => bool) => bool"
where [code del]: "finfun_Bex A P = Bex (Af) 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 set operations by finfun set operations where possible *}
lemma iso_finfun_mem_mem [code_inline]: "x ∈ Af <-> x ∈f A"
by(auto simp add: mem_def finfun_mem_def)
declare iso_finfun_mem_mem [simp]
lemma iso_finfun_subset_subset [code_inline]:
"Af ⊆ Bf <-> A ⊆f B"
by(auto)
lemma iso_finfun_eq [code_inline]:
fixes A :: "'a =>f bool"
shows "Af = Bf <-> A = B"
by(simp add: expand_finfun_eq)
lemma iso_finfun_Un_Un [code_inline]:
"Af ∪ Bf = (A ∪f B)f"
by(auto)
lemma iso_finfun_Int_Int [code_inline]:
"Af ∩ Bf = (A ∩f B)f"
by(auto)
lemma iso_finfun_empty_conv [code_inline]:
"{} = {}ff"
by(auto)
lemma iso_finfun_insert_insert [code_inline]:
"insert a Af = (insertf a A)f"
by(auto)
lemma iso_finfun_Compl_Compl [code_inline]:
fixes A :: "'a setf"
shows "- Af = (- A)f"
by(auto)
lemma iso_finfun_diff_diff [code_inline]:
fixes A :: "'a setf"
shows "Af - Bf = (A - B)f"
by(auto)
text {*
Do not declare the following two theorems as @{text "[code_inline]"}, because this causes quickcheck to loop frequently when bounded quantification is used.
For code generation, the same problems occur, but then, no randomly generated FinFun is usually around.
*}
lemma iso_finfun_Ball_Ball:
"Ball (Af) P <-> finfun_Ball A P"
by(simp add: finfun_Ball_def)
lemma iso_finfun_Bex_Bex:
"Bex (Af) P <-> finfun_Bex A P"
by(simp add: finfun_Bex_def)
declare iso_finfun_mem_mem [simp del]
end