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
  by intro_classes (simp add: infinite_UNIV_listI)

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