Theory Propositional_Formulas

theory Propositional_Formulas
imports
  Abstract_Formula
  "HOL-Library.Countable"
  "HOL-Library.Infinite_Set"
  "HOL-Library.Infinite_Typeclass"
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›
  "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