# Theory Propositional_Formulas

```theory Propositional_Formulas
imports
Abstract_Formula
"HOL-Library.Countable"
"HOL-Library.Infinite_Set"
begin

class infinite =
assumes infinite_UNIV: "infinite (UNIV::'a set)"

instance nat :: infinite
by (intro_classes) simp
instance prod :: (infinite, type) infinite
by intro_classes (simp add: finite_prod infinite_UNIV)
instance list :: (type) infinite

lemma countable_infinite_ex_bij: "∃f::('a::{countable,infinite}⇒'b::{countable,infinite}). bij f"
proof -
have "infinite (range (to_nat::'a ⇒ nat))"
using finite_imageD infinite_UNIV by blast
moreover have "infinite (range (to_nat::'b ⇒ nat))"
using finite_imageD infinite_UNIV by blast
ultimately have "∃f. bij_betw f (range (to_nat::'a ⇒ nat)) (range (to_nat::'b ⇒ nat))"
by (meson bij_betw_inv bij_betw_trans bij_enumerate)
then obtain f where f_def: "bij_betw f (range (to_nat::'a ⇒ nat)) (range (to_nat::'b ⇒ nat))" ..
then have f_range_trans: "f ` (range (to_nat::'a ⇒ nat)) = range (to_nat::'b ⇒ nat)"
unfolding bij_betw_def by simp
have "surj ((from_nat::nat ⇒ 'b) ∘ f ∘ (to_nat::'a ⇒ nat))"
proof (rule surjI)
fix a
obtain b where [simp]: "to_nat (a::'b) = b" by blast
hence "b ∈ range (to_nat::'b ⇒ nat)" by blast
with f_range_trans have "b ∈ f ` (range (to_nat::'a ⇒ nat))" by simp
from imageE [OF this] obtain c where [simp]:"f c = b" and "c ∈ range (to_nat::'a ⇒ nat)"
by auto
with f_def have [simp]: "inv_into (range (to_nat::'a ⇒ nat)) f b = c"
by (meson bij_betw_def inv_into_f_f)
then obtain d where cd: "from_nat c = (d::'a)" by blast
with ‹c ∈ range to_nat› have [simp]:"to_nat d = c" by auto
from ‹to_nat a = b› have [simp]: "from_nat b = a"
using from_nat_to_nat by blast
show "(from_nat ∘ f ∘ to_nat) (((from_nat::nat ⇒ 'a) ∘ inv_into (range (to_nat::'a ⇒ nat)) f ∘ (to_nat::'b ⇒ nat)) a) = a"
by (clarsimp simp: cd)
qed
moreover have "inj ((from_nat::nat ⇒ 'b) ∘ f ∘ (to_nat::'a ⇒ nat))"
apply (rule injI)
apply auto
apply (metis bij_betw_inv_into_left f_def f_inv_into_f f_range_trans from_nat_def image_eqI rangeI to_nat_split)
done
ultimately show ?thesis by (blast intro: bijI)
qed

text ‹Propositional formulas are either a variable from an infinite but countable set,
or a function given by a name and the arguments.›

datatype ('var,'cname) pform =
Var "'var::{countable,infinite}"
| Fun (name:'cname) (params: "('var,'cname) pform list")

text ‹Substitution on and closedness of propositional formulas is straight forward.›

fun subst :: "('var::{countable,infinite} ⇒ ('var,'cname) pform) ⇒ ('var,'cname) pform ⇒ ('var,'cname) pform"
where "subst s (Var v) = s v"
| "subst s (Fun n ps) = Fun n (map (subst s) ps)"

fun closed :: "('var::{countable,infinite},'cname) pform ⇒ bool"
where "closed (Var v) ⟷ False"
| "closed (Fun n ps) ⟷ list_all closed ps"

text ‹Now we can interpret @{term Abstract_Formulas}.
As there are no locally fixed constants in propositional formulas, most of the locale parameters
are dummy values›

interpretation propositional: Abstract_Formulas
― ‹No need to freshen locally fixed constants›
"curry (SOME f. bij f):: nat ⇒ 'var ⇒ 'var"
― ‹also no renaming needed as there are no locally fixed constants›
"λ_. id" "λ_. {}"
― ‹closedness and substitution as defined above›
"closed :: ('var::{countable,infinite},'cname) pform ⇒ bool" subst
― ‹no substitution and renaming of locally fixed constants›
"λ_. {}" "λ_. id"
― ‹most generic formula›
"Var undefined"
proof
fix a v a' v'
from countable_infinite_ex_bij obtain f where "bij (f::nat × 'var ⇒ 'var)" by blast
then show "(curry (SOME f. bij (f::nat × 'var ⇒ 'var)) (a::nat) (v::'var) = curry (SOME f. bij f) (a'::nat) (v'::'var)) =
(a = a' ∧ v = v')"
apply (rule someI2 [where Q="λf. curry f a v = curry f a' v' ⟷ a = a' ∧ v = v'"])
by auto (metis bij_pointE prod.inject)+
next
fix f s
assume "closed (f::('var, 'cname) pform)"
then show "subst s f = f"
proof (induction s f rule: subst.induct)
case (2 s n ps)
thus ?case by (induction ps) auto
qed auto
next
have "subst Var f = f" for f :: "('var,'cname) pform"
by (induction f) (auto intro: map_idI)
then show "∃s. (∀f. subst s (f::('var,'cname) pform) = f) ∧ {} = {}"
by (rule_tac x=Var in exI; clarsimp)
qed auto

declare propositional.subst_lconsts_empty_subst [simp del]

end
```