# Theory Propositional_Formulas

theory Propositional_Formulas
imports
Abstract_Formula

begin

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›

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