Theory FormulaEnumeration

(* Propositional formula  *)

(* Formalization adapted from: 
   Fabián Fernando Serrano Suárez, "Formalización en Isar de la
   Meta-Lógica de Primer Orden." PhD thesis, 
   Departamento de Ciencias de la Computación e Inteligencia Artificial,
   Universidad de Sevilla, Spain, 2012.
   https://idus.us.es/handle/11441/57780.  In Spanish  *)

(*<*)
theory FormulaEnumeration
imports BinaryTreeEnumeration
begin
(*>*)

 
fun formulaP_from_tree_b :: "(nat ⇒ 'b) ⇒ tree_b ⇒ 'b formula" where
  "formulaP_from_tree_b g (Leaf 0) = FF"
| "formulaP_from_tree_b g (Leaf (Suc 0)) = TT"
| "formulaP_from_tree_b g (Leaf (Suc (Suc n))) = (atom (g n))"
| "formulaP_from_tree_b g (Tree (Leaf (Suc 0)) (Tree T1 T2)) =
   ((formulaP_from_tree_b g T1) ∧. (formulaP_from_tree_b g T2))"
| "formulaP_from_tree_b g (Tree (Leaf (Suc (Suc 0))) (Tree T1 T2)) =
   ((formulaP_from_tree_b g T1) ∨. (formulaP_from_tree_b g T2))"
| "formulaP_from_tree_b g (Tree (Leaf (Suc (Suc (Suc 0)))) (Tree T1 T2)) =
   ((formulaP_from_tree_b g T1) →. (formulaP_from_tree_b g T2))"
| "formulaP_from_tree_b g (Tree (Leaf (Suc (Suc (Suc (Suc 0))))) T) =
   (¬. (formulaP_from_tree_b g T))"
(*<*)

lemma "formulaP_from_tree_b  (λn. n) (Leaf  0) = FF"
by simp
(*
normal_form 
  "formulaP_from_tree_b (λn. n) (Tree (Leaf (Suc 0)) (Tree (Leaf 0) (Leaf 0)))"
*)
lemma 
  "formulaP_from_tree_b 
   (λn. n) (Tree (Leaf (Suc 0)) (Tree (Leaf 0) (Leaf 0))) = FF ∧. FF" 
by simp 
(*
normal_form 
  "formulaP_from_tree_b g (Tree (Leaf (Suc 0)) (Tree (Leaf 0) (Leaf 0)))"
*)
lemma 
  "formulaP_from_tree_b g (Tree (Leaf (Suc 0)) (Tree (Leaf 0) (Leaf 0))) 
   = FF ∧. FF" 
by simp
(*
normal_form  "formulaP_from_tree_b (λn. n) (Leaf  0) = FF"
normal_form  "formulaP_from_tree_b (λn. n) (Leaf  0)"
normal_form 
  "formulaP_from_tree_b  
   (λn. n) (Tree (Leaf (Suc (Suc (Suc (Suc 0))))) (Leaf 0))"
*)
lemma 
  "formulaP_from_tree_b 
  (λn. n) (Tree (Leaf (Suc (Suc (Suc (Suc 0))))) (Leaf 0)) = (¬. FF)"
by simp
(*>*)


primrec tree_b_from_formulaP :: "('b ⇒ nat) ⇒  'b formula ⇒ tree_b" where
  "tree_b_from_formulaP  g FF = Leaf 0"
| "tree_b_from_formulaP g TT = Leaf (Suc 0)"
| "tree_b_from_formulaP g (atom P) = Leaf (Suc (Suc (g P)))"
| "tree_b_from_formulaP g (F ∧. G) = Tree (Leaf (Suc 0))
   (Tree (tree_b_from_formulaP g F) (tree_b_from_formulaP g G))"
| "tree_b_from_formulaP g (F ∨. G) = Tree (Leaf (Suc (Suc 0)))
   (Tree (tree_b_from_formulaP g F) (tree_b_from_formulaP g G))"
| "tree_b_from_formulaP g (F →. G) = Tree (Leaf (Suc (Suc (Suc 0))))
   (Tree (tree_b_from_formulaP g F) (tree_b_from_formulaP g G))"
| "tree_b_from_formulaP g (¬. F) = Tree (Leaf (Suc (Suc (Suc (Suc 0)))))
   (tree_b_from_formulaP g F)"



definition ΔP :: "(nat ⇒ 'b) ⇒ nat ⇒ 'b formula" where
  "ΔP g n = formulaP_from_tree_b g (diag_tree_b n)"

definition ΔP' :: "('b ⇒ nat) ⇒ 'b formula ⇒ nat" where
  "ΔP' g' F = undiag_tree_b (tree_b_from_formulaP g' F)"

theorem enumerationformulasP[simp]:
  assumes "∀x. g(g' x) = x" 
  shows "ΔP g (ΔP' g' F) = F"
using assms 
by (induct F)(simp_all add: ΔP_def ΔP'_def)


corollary EnumerationFormulasP:
  assumes "∀P. ∃ n. P = g n" 
  shows "∀F. ∃n. F = ΔP g n"
proof (rule allI)
  fix F
  { have "∀P. P = g (SOME n. P = (g n))"  
    proof(rule allI)
      fix P
      obtain n where n: "P=g(n)" using assms by auto
      thus "P = g (SOME n. P = (g n))" by (rule someI)
    qed }
  hence "∀P. g((λP. SOME n. P = (g n)) P) = P" by simp
  hence "F = ΔP g (ΔP' (λP. SOME n. P = (g n)) F)" 
    using enumerationformulasP by simp
  thus "∃n. F = ΔP g n"
    by blast
qed



corollary EnumerationFormulasP1:
  assumes "enumeration (g:: nat ⇒ 'b)"
  shows "enumeration ((ΔP g):: nat ⇒ 'b formula)"
proof -
  have "∀P. ∃ n. P = g n" using assms by(unfold enumeration_def)
  hence "∀F. ∃n. F = ΔP g n" using EnumerationFormulasP by auto
  thus ?thesis by(unfold enumeration_def)
qed 

corollary EnumeracionFormulasNat:
  shows "∃ f. enumeration (f:: nat ⇒ nat formula)" 
  proof -
    obtain g where g: "enumeration (g:: nat ⇒ nat)" using enum_nat by auto 
    thus  "∃ f. enumeration (f:: nat ⇒ nat formula)"  
      using  enum_nat EnumerationFormulasP1 by auto
qed
(*<*)
end
(*>*)