Theory UniformNotation

(* 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 
   Last modified: 11 Aug, 2025.
 *)


theory UniformNotation
imports SyntaxAndSemantics
begin       

fun FormulaLiteral :: "'b formula ⇒ bool" where
  "FormulaLiteral ⊥. = True"
| "FormulaLiteral (¬. ⊥.) = True"
| "FormulaLiteral ⊤. = True"
| "FormulaLiteral (¬. ⊤.) = True"
| "FormulaLiteral (atom P) = True" 
| "FormulaLiteral (¬.(atom P)) = True" 
| "FormulaLiteral F = False"

fun FormulaNegNeg :: "'b formula ⇒ bool" where
  "FormulaNegNeg (¬. (¬. F)) = True"
| "FormulaNegNeg F = False" 

fun FormulaAlpha :: "'b formula ⇒ bool" where
  "FormulaAlpha (F ∧. G) = True"
| "FormulaAlpha (¬. (F ∨. G)) = True"
| "FormulaAlpha (¬. (F →. G)) =  True" 
| "FormulaAlpha F = False"

fun FormulaBeta :: "'b formula ⇒ bool" where
  "FormulaBeta (F ∨. G) = True"
| "FormulaBeta (¬. (F ∧. G)) = True"
| "FormulaBeta (F →. G) =  True" 
| "FormulaBeta F = False"

lemma Literal:
  assumes "FormulaLiteral F"
  shows "F = ⊥. ∨ F = ⊤. ∨ F = (¬. ⊥.) ∨ F = (¬. ⊤.) ∨ (∃n. F = (atom n) ∨ F = (¬. (atom n)))"
using assms 
by (induct F rule: FormulaLiteral.induct, auto) 

lemma NegNeg:
  assumes "FormulaNegNeg F"
  shows "∃G. F = (¬. (¬. G))"
using assms
by (induct F rule: FormulaNegNeg.induct, auto) 

lemma Alpha:
  assumes "FormulaAlpha F"
  shows "∃G H.  F = (G ∧. H) ∨ F = (¬. (G ∨. H)) ∨ F = (¬. (G →. H))"
using assms
by (induct F rule: FormulaAlpha.induct, auto) 

lemma Beta:
  assumes "FormulaBeta F"
  shows "∃G H. F = (G ∨. H) ∨ F = (¬. (G ∧. H)) ∨ F = (G →. H)"
using assms
by (induct F rule: FormulaBeta.induct, auto) 

lemma noLiteralNegNeg:
  assumes "FormulaLiteral formula"
  shows "¬(FormulaNegNeg formula)"
using assms Literal NegNeg  
by (induct formula rule: FormulaLiteral.induct, auto)


lemma noLiteralAlpha:
  assumes "FormulaLiteral formula"
  shows "¬(FormulaAlpha formula)"
using assms Literal Alpha
by (induct formula rule: FormulaLiteral.induct, auto)  


lemma noLiteralBeta:
  assumes "FormulaLiteral formula"
  shows "¬(FormulaBeta formula)"
using assms Literal Beta  
by (induct formula rule: FormulaLiteral.induct, auto)


lemma noAlphaNegNeg:
  assumes "FormulaAlpha formula"
  shows "¬(FormulaNegNeg formula)"
using assms Alpha NegNeg 
by (induct formula rule: FormulaAlpha.induct, auto)


lemma noBetaNegNeg:
  assumes "FormulaBeta formula"
  shows "¬(FormulaNegNeg formula)"
using assms Beta NegNeg 
by (induct formula rule: FormulaBeta.induct, auto)


lemma noAlphaBeta:
  assumes "FormulaAlpha formula"
  shows "¬(FormulaBeta formula)"
using assms Alpha Beta 
by (induct formula rule: FormulaAlpha.induct, auto)

fun components  :: "'b formula ⇒ 'b formula list" where 
  "components ⊥. = []"
| "components ⊤. = []"
| "components (¬. ⊥.) =[]"
| "components (¬. ⊤.) =[]"
| "components (atom p) =[]"
| "components (¬.(atom p)) =[]"
| "components (¬. (¬. G)) = [G]"
| "components (G ∧. H) = [G, H]"
| "components (¬. (G ∨. H)) = [¬. G, ¬. H]"
| "components (¬. (G →. H)) = [G, ¬. H]"
| "components (G ∨. H) = [G, H]"
| "components (¬. (G ∧. H)) = [¬. G, ¬. H]"
| "components (G →. H) = [¬.G,  H]"

definition Comp1 :: "'b formula ⇒ 'b formula" where 
  "Comp1 F = hd (components F)"

definition Comp2 :: "'b formula ⇒ 'b formula" where 
  "Comp2 F =  hd (tl (components F))"

primrec t_v_evaluationDisjunctionG :: "('b ⇒ bool) ⇒ ('b formula list) ⇒ bool" where
  "t_v_evaluationDisjunctionG I [] = False"
| "t_v_evaluationDisjunctionG I (F#Fs) = (if t_v_evaluation I F = True 
   then True else t_v_evaluationDisjunctionG I Fs)"

primrec t_v_evaluationConjunctionG :: "('b ⇒ bool) ⇒ ('b formula list) list ⇒ bool " where
  "t_v_evaluationConjunctionG I [] = True"
| "t_v_evaluationConjunctionG I (D#Ds) = 
     (if t_v_evaluationDisjunctionG I D = False then False else t_v_evaluationConjunctionG I Ds)"

definition equivalentG :: "('b formula list) list  ⇒ ('b formula list) list ⇒ bool" where
 "equivalentG C1 C2 ≡ (∀I. ((t_v_evaluationConjunctionG I C1) = (t_v_evaluationConjunctionG I C2)))" 

lemma EquivImpliesEquivG :
  assumes "equivalent F G"
  shows "equivalentG [[F]] [[G]]"
  using assms unfolding equivalentG_def equivalent_def by simp

lemma DoubleNegationEquiv : "equivalent (¬. ¬. F) F"  
  unfolding equivalent_def by auto

lemma EquiNegNeg: 
  assumes "FormulaNegNeg F" 
  shows "equivalent F (Comp1 F)"
  using NegNeg[OF assms] DoubleNegationEquiv
  unfolding Comp1_def
  using equivalent_def by auto

lemma EquiAlphab1: "equivalent (¬. (G ∨. H)) (¬. G ∧. ¬. H)" 
  unfolding equivalent_def by simp

lemma EquiAlphab2: "equivalent (¬. (G →. H)) (G ∧. ¬. H)"
    unfolding equivalent_def by simp

lemma EquivAlpha:
  assumes "FormulaAlpha F"
  shows "equivalent F (Comp1 F ∧. Comp2 F)"
  using Alpha[OF assms]  EquiAlphab1  EquiAlphab2 
  unfolding Comp1_def Comp2_def
  using equivalent_def by fastforce

lemma EquiBetaa: "equivalent (¬.(G ∧. H)) (¬.G ∨. ¬.H)" 
  unfolding equivalent_def by simp

lemma EquiBetab: "equivalent (G →. H) (¬. G ∨. H)" 
  unfolding equivalent_def by simp

lemma EquivBetaComp: 
  assumes "FormulaBeta F"
  shows "equivalent F (Comp1 F ∨. Comp2 F)"
  using Beta[OF assms] EquiBetaa  EquiBetab 
  unfolding Comp1_def Comp2_def 
  using equivalent_def by fastforce

end