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  *)

(*<*)
theory UniformNotation
imports SyntaxAndSemantics
       
begin 
(*>*)



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



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


fun FormulaAlfa :: "'b formula ⇒ bool" where
  "FormulaAlfa (F ∧. G) = True"
| "FormulaAlfa (¬. (F ∨. G)) = True"
| "FormulaAlfa (¬. (F →. G)) =  True" 
| "FormulaAlfa 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 = FF ∨ F = TT ∨ F = (¬. FF) ∨ F = (¬. TT) ∨ (∃n. F = (atom n) ∨ F = (¬. (atom n)))"
using assms 
by (induct F rule: FormulaLiteral.induct, auto) 


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


lemma Alfa:
  assumes "FormulaAlfa F"
  shows "∃G H.  F = (G ∧. H) ∨ F = (¬. (G ∨. H)) ∨ F = (¬. (G →. H))"
using assms
by (induct F rule: FormulaAlfa.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 noLiteralNoNo:
  assumes "FormulaLiteral formula"
  shows "¬(FormulaNoNo formula)"
using assms Literal NoNo  
by (induct formula rule: FormulaLiteral.induct, auto)


lemma noLiteralAlfa:
  assumes "FormulaLiteral formula"
  shows "¬(FormulaAlfa formula)"
using assms Literal Alfa
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 noAlfaNoNo:
  assumes "FormulaAlfa formula"
  shows "¬(FormulaNoNo formula)"
using assms Alfa NoNo 
by (induct formula rule: FormulaAlfa.induct, auto)


lemma noBetaNoNo:
  assumes "FormulaBeta formula"
  shows "¬(FormulaNoNo formula)"
using assms Beta NoNo 
by (induct formula rule: FormulaBeta.induct, auto)


lemma noAlfaBeta:
  assumes "FormulaAlfa formula"
  shows "¬(FormulaBeta formula)"
using assms Alfa Beta 
by (induct formula rule: FormulaAlfa.induct, auto)


lemma UniformNotation:
 "FormulaLiteral F ∨ FormulaNoNo F ∨ FormulaAlfa F ∨ FormulaBeta F"
(*<*)
by (induct F rule: FormulaLiteral.induct, 
    induct F rule: FormulaNoNo.induct,
    induct F rule: FormulaAlfa.induct, 
    induct F rule: FormulaBeta.induct,
    induct F, 
    auto)
(*>*)


datatype typeUniformNotation = Literal | NoNo | Alfa| Beta 


fun typeFormula :: "'b formula ⇒ typeUniformNotation" where
"typeFormula F = 
  (if FormulaBeta F then Beta 
   else if FormulaNoNo F then NoNo
   else if FormulaAlfa F then Alfa
   else Literal)"

(*<*)

lemma typeLiteral: 
  assumes "typeFormula F = Literal"
  shows "FormulaLiteral F"
(*<*)
  by (metis UniformNotation assms 
      typeFormula.simps typeUniformNotation.distinct(1) typeUniformNotation.distinct(3) typeUniformNotation.distinct(5))
(*>*)


lemma typeAlfa:
  assumes "typeFormula F = Alfa"
  shows "FormulaAlfa F"
(*<*)
by (metis UniformNotation 
          assms 
          typeUniformNotation.distinct 
          typeFormula.simps)
(*>*)


lemma typeBeta:
  assumes "typeFormula F = Beta"
  shows "FormulaBeta F"
(*<*)
by (metis UniformNotation 
          assms 
          typeUniformNotation.distinct 
          typeFormula.simps)
(*>*)


lemma typeNoNo:
  assumes "typeFormula F = NoNo"
  shows "FormulaNoNo F"
(*<*)
by (metis UniformNotation 
          assms 
          typeUniformNotation.distinct 
          typeFormula.simps)
(*>*)


lemma UniformNotation1:
  "FormulaLiteral F ∨ FormulaNoNo F ∨ FormulaAlfa F ∨ FormulaBeta F"
using typeLiteral typeNoNo typeAlfa typeBeta typeUniformNotation.exhaust
by blast
(*>*)


fun componentes  :: "'b formula ⇒ 'b formula list" where 
  "componentes (¬. (¬. G)) = [G]"
| "componentes (G ∧. H) = [G, H]"
| "componentes (¬. (G ∨. H)) = [¬. G, ¬. H]"
| "componentes (¬. (G →. H)) = [G, ¬. H]"
| "componentes (G ∨. H) = [G, H]"
| "componentes (¬. (G ∧. H)) = [¬. G, ¬. H]"
| "componentes (G →. H) = [¬.G,  H]"


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


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



primrec t_v_evaluationDisyuncionG :: "('b ⇒ v_truth) ⇒ ('b formula list) ⇒ v_truth" where
  "t_v_evaluationDisyuncionG I [] = Ffalse"
| "t_v_evaluationDisyuncionG I (F#Fs) = (if t_v_evaluation I F = Ttrue then Ttrue else t_v_evaluationDisyuncionG I Fs)"


primrec t_v_evaluationConjuncionG :: "('b ⇒ v_truth) ⇒ ('b formula list) list ⇒ v_truth" where
  "t_v_evaluationConjuncionG I [] = Ttrue"
| "t_v_evaluationConjuncionG I (D#Ds) = 
     (if t_v_evaluationDisyuncionG I D = Ffalse then Ffalse else t_v_evaluationConjuncionG I Ds)"


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


(*<*) 
lemma EquiNoNoa: "equivalentesG [[¬. ¬. F]] [[F]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[¬. ¬. F]] = t_v_evaluationConjuncionG I [[F]]" 
  proof 
    fix I
    show  "t_v_evaluationConjuncionG I [[¬. ¬. F]] = t_v_evaluationConjuncionG I [[F]]" 
    proof (cases "t_v_evaluation I F")
      text  ‹ Caso 1:  ›          
      { assume 1:"t_v_evaluation I F = Ttrue"        
        thus ?thesis by (simp add: v_negation_def) }     
    next
       text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I F = Ffalse"    
        thus ?thesis by (simp add: v_negation_def) }     
    qed 
  qed
qed  
(*>*)


lemma EquiNoNo: 
  assumes "typeFormula F = NoNo" 
  shows "equivalentesG [[F]] [[Comp1 F]]"
(*<*)
proof -
  have 1: "∃G. F = ¬. ¬. G" using assms typeNoNo NoNo by auto
  obtain G where "F = ¬. ¬. G" using 1 by auto
  moreover
  hence "Comp1 F = G" by(simp add: Comp1_def)
  ultimately
  have "equivalentesG [[F]] [[Comp1 F]] = equivalentesG [[¬. ¬. G]] [[G]]" 
    by simp
  thus ?thesis using EquiNoNoa by simp
qed
(*>*)

(*<*)
lemma EquiAlfaa: "equivalentesG [[G ∧. H]] [[G],[H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[G ∧. H]] = t_v_evaluationConjuncionG I [[G], [H]]" 
  proof 
    fix I
    show  "t_v_evaluationConjuncionG I [[G ∧. H]] = t_v_evaluationConjuncionG I [[G], [H]]" 
    proof (cases "t_v_evaluation I G")
            text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis
        proof(cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis using 1  by (simp add: v_conjunction_def)              
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 1  by (simp add: v_conjunction_def)
        qed }
    next
       text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I G = Ffalse"    
        thus ?thesis by (simp add: v_conjunction_def) }     
    qed 
  qed
qed  

lemma EquiAlfab: "equivalentesG [[¬. (G ∨. H)]] [[¬. G],[¬. H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[¬. (G ∨. H)]] = 
            t_v_evaluationConjuncionG I [[¬. G], [¬. H]]" 
  proof 
    fix I
    show "t_v_evaluationConjuncionG I [[¬. (G ∨. H)]] = 
          t_v_evaluationConjuncionG I [[¬. G], [¬. H]]" 
    proof (cases "t_v_evaluation I G")
           text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis
        proof (cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_disjunction_def)
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_disjunction_def)
        qed }
    next
        text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I G = Ffalse"    
        thus ?thesis 
          by (simp add: v_negation_def, simp add: v_disjunction_def) }     
    qed 
  qed
qed  

lemma EquiAlfac: "equivalentesG [[¬. (G →. H)]] [[G],[¬. H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[¬. (G →. H)]] = 
            t_v_evaluationConjuncionG I [[G], [¬. H]]" 
  proof 
    fix I
    show  "t_v_evaluationConjuncionG I [[¬. (G →. H)]] = 
           t_v_evaluationConjuncionG I [[G], [¬. H]]" 
    proof (cases "t_v_evaluation I G")
               text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis
        proof(cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_implication_def)
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_implication_def)
        qed }
    next
        text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I G = Ffalse"    
        thus ?thesis 
          by (simp add: v_negation_def, simp add: v_implication_def) }     
    qed 
  qed
qed 
(*>*)
 

lemma EquiAlfa:
  assumes "typeFormula F = Alfa" 
  shows "equivalentesG [[F]] [[Comp1 F],[Comp2 F]]"
(*<*)
proof -
  have 1: "∃G H. F = (G ∧. H) ∨ F = (¬. (G ∨. H)) ∨ F = (¬. (G →. H))" 
    using assms typeAlfa Alfa by auto
  obtain G and H 
    where H: "F = (G ∧. H) ∨ F = (¬. (G ∨. H)) ∨ F = (¬. (G →. H))" 
    using 1 by auto
  moreover 
  { assume hip: "F = G ∧. H"  
    hence "Comp1 F = G" and "Comp2 F = H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiAlfaa by simp }
  moreover
  { assume hip:  "F = ¬. (G ∨. H)"
    hence "Comp1 F = ¬. G" and "Comp2 F = ¬. H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiAlfab by simp }
  moreover
  { assume hip:  "F = ¬. (G →. H)"
    hence "Comp1 F = G" and "Comp2 F = ¬. H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiAlfac by simp }
  ultimately show ?thesis by blast  
qed
(*>*) 

(*<*)
lemma EquiBetaa: "equivalentesG [[G ∨. H]] [[G, H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[G ∨. H]] = t_v_evaluationConjuncionG I [[G, H]]" 
  proof 
    fix I
    show  "t_v_evaluationConjuncionG I [[G ∨. H]] = t_v_evaluationConjuncionG I [[G, H]]" 
    proof (cases "t_v_evaluation I G")
        text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis by (simp add: v_disjunction_def) }    
    next
        text  ‹ Caso 2:  › 
      { assume 2: "t_v_evaluation I G = Ffalse"  
        thus ?thesis
        proof(cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis by (simp add: v_disjunction_def)              
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 2 by (simp add: v_disjunction_def)
        qed }
    qed     
  qed
qed  

lemma EquiBetab: "equivalentesG [[¬. (G ∧. H)]] [[¬. G, ¬. H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[¬. (G ∧. H)]] = 
            t_v_evaluationConjuncionG I [[¬. G, ¬. H]]" 
  proof 
    fix I
    show "t_v_evaluationConjuncionG I [[¬. (G ∧. H)]] = 
          t_v_evaluationConjuncionG I [[¬. G, ¬. H]]" 
    proof (cases "t_v_evaluation I G")
             text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis
        proof(cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_conjunction_def)
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_conjunction_def)
        qed }
    next
         text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I G = Ffalse"    
        thus ?thesis 
          by (simp add: v_negation_def, simp add: v_conjunction_def) }     
    qed 
  qed
qed  

lemma EquiBetac: "equivalentesG [[G →. H]] [[¬. G, H]]"
proof (unfold equivalentesG_def)
  show "∀I. t_v_evaluationConjuncionG I [[G →. H]] = t_v_evaluationConjuncionG I [[¬. G, H]]" 
  proof 
    fix I
    show  "t_v_evaluationConjuncionG I [[G →. H]] = t_v_evaluationConjuncionG I [[¬. G, H]]" 
    proof (cases "t_v_evaluation I G")
           text  ‹ Caso 1:  › 
      { assume 1:"t_v_evaluation I G = Ttrue"        
        thus ?thesis
        proof(cases "t_v_evaluation I H")
          assume  "t_v_evaluation I H = Ttrue"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_implication_def)
        next 
          assume  "t_v_evaluation I H = Ffalse"        
          thus ?thesis using 1  
            by (simp add: v_negation_def, simp add: v_implication_def)
        qed }
    next
        text  ‹ Caso 2:  › 
      { assume "t_v_evaluation I G = Ffalse"    
        thus ?thesis 
          by (simp add: v_negation_def, simp add: v_implication_def) }     
    qed 
  qed
qed  
(*>*)


lemma EquiBeta:
  assumes "typeFormula F = Beta" 
  shows "equivalentesG [[F]] [[Comp1 F, Comp2 F]]"
(*<*)
proof -
  have 1: "∃G H. F = (G  ∨. H) ∨ F = (¬. (G ∧. H)) ∨ F = (G →. H)" 
    using assms typeBeta Beta by blast
  obtain G and H
    where H: "F = (G ∨. H) ∨ F = (¬. (G ∧. H)) ∨ F =  (G →. H)" 
    using 1 by auto
  moreover 
  { assume hip: "F = G ∨. H"  
    hence "Comp1 F = G" and "Comp2 F = H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiBetaa by simp }
  moreover
  { assume hip:  "F = ¬. (G ∧. H)"
    hence "Comp1 F = ¬. G" and "Comp2 F = ¬. H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiBetab by simp }
  moreover
  { assume hip:  "F = G →. H"
    hence "Comp1 F = ¬. G" and "Comp2 F = H" 
      by (simp add: Comp1_def, simp add: Comp2_def)
    hence ?thesis using hip EquiBetac by simp }  
  ultimately show ?thesis by blast  
qed
(*>*)
 

lemma EquivNoNoComp:
  assumes "typeFormula F = NoNo"
  shows "equivalent F (Comp1 F)"
(*<*)
proof (unfold equivalent_def)
  show "∀I. t_v_evaluation I F = t_v_evaluation I (Comp1 F)"  
  proof (rule allI)+
    fix I
    have "equivalentesG [[F]] [[Comp1 F]]" using EquiNoNo assms by simp 
    hence 1: "t_v_evaluationConjuncionG I [[F]] = t_v_evaluationConjuncionG I [[Comp1 F]]" 
      by (unfold equivalentesG_def, simp)   
    show "t_v_evaluation I F = t_v_evaluation I (Comp1 F)" 
    proof (cases "t_v_evaluation I F")
      assume hip1: "t_v_evaluation I F =  Ttrue"
      hence "t_v_evaluationConjuncionG I [[F]] = Ttrue" by simp
      hence 2: "t_v_evaluationConjuncionG I [[Comp1 F]] = Ttrue" using 1 by simp 
      have "t_v_evaluation I (Comp1 F) = Ttrue" 
      proof -
        { assume "t_v_evaluation I (Comp1 F) ≠ Ttrue" 
          hence  "t_v_evaluation I (Comp1 F) = Ffalse" using Bivaluation by auto
          hence "t_v_evaluationConjuncionG I [[Comp1 F]] = Ffalse" by simp
          hence "False" using 2 by simp}
        thus "t_v_evaluation I (Comp1 F) = Ttrue" by auto
      qed
      thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F)" using hip1 by simp
    next
      assume hip2: "t_v_evaluation I F =  Ffalse"
      hence "t_v_evaluationConjuncionG I [[F]] = Ffalse" by simp
      hence 2: "t_v_evaluationConjuncionG I [[Comp1 F]] = Ffalse" using 1 by simp 
      have "t_v_evaluation I (Comp1 F) = Ffalse"  
      proof -
       { assume "t_v_evaluation I (Comp1 F) ≠ Ffalse" 
         hence  "t_v_evaluation I (Comp1 F) = Ttrue" using Bivaluation by auto
         hence "t_v_evaluationConjuncionG I [[Comp1 F]] = Ttrue" by simp
         hence "False" using 2 by simp}
       thus "t_v_evaluation I (Comp1 F) = Ffalse" by auto
     qed
     thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F)" using hip2 by simp
   qed
 qed
qed
(*>*)


lemma EquivAlfaComp:
  assumes "typeFormula F = Alfa"
  shows "equivalent F (Comp1 F ∧. Comp2 F)"
(*<*)
proof(unfold equivalent_def)
  show "∀ I. t_v_evaluation I F = t_v_evaluation I (Comp1 F ∧. Comp2 F)"  
  proof (rule allI)+
    fix I
    have "equivalentesG [[F]] [[Comp1 F], [Comp2 F]]" 
      using EquiAlfa assms by simp 
    hence 1: "t_v_evaluationConjuncionG I [[F]] = 
              t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]]"
      by (unfold equivalentesG_def,simp)  
    show "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∧. Comp2 F)" 
    proof (cases "t_v_evaluation I F")
      assume hip1: "t_v_evaluation I F =  Ttrue"
      have "t_v_evaluation I (Comp1 F ∧. Comp2 F) = Ttrue" 
      proof -
        have "t_v_evaluationConjuncionG I [[F]] = Ttrue" using hip1 by simp 
        hence 2:"t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]] = Ttrue"  
          using 1 by simp
        have 3: "t_v_evaluation I (Comp1 F) = Ttrue" 
        proof -
         { assume "t_v_evaluation I (Comp1 F) = Ffalse"
           hence "t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]] = Ffalse" by simp
           hence "False" using 2 by simp}
         hence "t_v_evaluation I (Comp1 F) ≠ Ffalse" by auto
         thus "t_v_evaluation I (Comp1 F) = Ttrue" using Bivaluation by auto
       qed
       have "t_v_evaluation I (Comp2 F) = Ttrue" 
       proof -
         { assume "t_v_evaluation I (Comp2 F) = Ffalse"
           hence "t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]] = Ffalse" by simp
           hence "False" using 2 by simp}
         hence "t_v_evaluation I (Comp2 F) ≠ Ffalse" by auto
         thus "t_v_evaluation I (Comp2 F) = Ttrue" using Bivaluation by auto
       qed    
       thus "t_v_evaluation I (Comp1 F ∧. Comp2 F) = Ttrue" using 3 
         by (auto, unfold v_conjunction_def, simp)
     qed
     thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∧. Comp2 F)" using hip1 by simp
   next
     assume hip2: "t_v_evaluation I F = Ffalse"
     show "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∧. Comp2 F)"  
     proof - 
       have  "t_v_evaluation I (Comp1 F ∧. Comp2 F) = Ffalse" 
       proof -
         have "t_v_evaluationConjuncionG I [[F]] = Ffalse" using hip2 by simp 
         hence 4: "t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]] = Ffalse"  
           using 1 by simp
         have "t_v_evaluation I (Comp1 F) = Ffalse ∨ t_v_evaluation I (Comp2 F) = Ffalse" 
         proof -
           { assume "¬(t_v_evaluation I (Comp1 F) = Ffalse ∨ 
                       t_v_evaluation I (Comp2 F) = Ffalse)"
             hence "(t_v_evaluation I (Comp1 F) ≠ Ffalse ∧ 
                     t_v_evaluation I (Comp2 F) ≠ Ffalse)" 
               by simp
             hence  "(t_v_evaluation I (Comp1 F) = Ttrue ∧  
                      t_v_evaluation I (Comp2 F) = Ttrue)" 
               using Bivaluation by auto          
             hence "t_v_evaluation I (Comp1 F) = Ttrue" and 
               "t_v_evaluation I (Comp2 F) = Ttrue" 
               by auto       
             hence  "t_v_evaluationConjuncionG I [[Comp1 F], [Comp2 F]] = Ttrue" by auto
             hence "False" using 4 by auto}
           thus "t_v_evaluation I (Comp1 F) = Ffalse ∨ t_v_evaluation I (Comp2 F) = Ffalse" 
             by auto 
         qed
         thus "t_v_evaluation I (Comp1 F ∧. Comp2 F) = Ffalse" 
           by (auto, unfold v_conjunction_def, auto)
       qed     
       thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∧. Comp2 F)" using hip2 by simp
     qed
   qed
 qed
qed
(*>*)


lemma EquivBetaComp:
  assumes "typeFormula F = Beta"
  shows "equivalent F (Comp1 F ∨. Comp2 F)"
(*<*)
proof (unfold equivalent_def)
  show "∀ I. t_v_evaluation I F = t_v_evaluation I (Comp1 F ∨. Comp2 F)"  
  proof(rule allI)+
    fix I
    have "equivalentesG [[F]] [[Comp1 F, Comp2 F]]" 
      using EquiBeta assms by simp 
    hence 1: "t_v_evaluationConjuncionG I [[F]] = 
              t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]]" 
      by (unfold equivalentesG_def,simp)   
    show "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∨. Comp2 F)"
    proof (cases "t_v_evaluation I F")
      assume hip1: "t_v_evaluation I F =  Ttrue"
      have "t_v_evaluation I (Comp1 F ∨. Comp2 F) = Ttrue" 
      proof -
        have "t_v_evaluationConjuncionG I [[F]] = Ttrue" using hip1 by simp 
        hence 2:"t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]] = Ttrue"  
          using 1 by simp
        hence "(t_v_evaluation I (Comp1 F) = Ttrue) ∨ (t_v_evaluation I (Comp2 F) = Ttrue)" 
        proof -
         { assume  "¬((t_v_evaluation I (Comp1 F) = Ttrue) ∨ 
                      (t_v_evaluation I (Comp2 F) = Ttrue))"
           hence  "(t_v_evaluation I (Comp1 F) ≠ Ttrue ∧ 
                    t_v_evaluation I (Comp2 F) ≠ Ttrue)" 
            by simp
          hence  "(t_v_evaluation I (Comp1 F) = Ffalse ∧  
                   t_v_evaluation I (Comp2 F) = Ffalse)" 
            using Bivaluation by auto                 
          hence  "t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]] = Ffalse" by auto
          hence "False" using 2 by auto}
          thus "(t_v_evaluation I (Comp1 F) = Ttrue) ∨ (t_v_evaluation I (Comp2 F) = Ttrue)" 
            by auto
        qed
        thus "t_v_evaluation I (Comp1 F ∨. Comp2 F) = Ttrue" 
          by (auto, unfold v_disjunction_def, auto)
      qed     
      thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∨. Comp2 F)" using hip1 by simp
    next
      assume hip2: "t_v_evaluation I F =  Ffalse"
      have "t_v_evaluation I (Comp1 F ∨. Comp2 F) = Ffalse" 
      proof -
        have "t_v_evaluationConjuncionG I [[F]] = Ffalse" using hip2 by simp 
        hence 3:"t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]] = Ffalse"  
          using 1 by simp
        have  4:"t_v_evaluation I (Comp1 F) = Ffalse" 
        proof -
         { assume "t_v_evaluation I (Comp1 F) = Ttrue"
           hence "t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]] = Ttrue" by simp
           hence "False" using 3 by simp}
         hence "t_v_evaluation I (Comp1 F) ≠ Ttrue" by auto
         thus "t_v_evaluation I (Comp1 F) = Ffalse" using Bivaluation by auto
       qed
       have "t_v_evaluation I (Comp2 F) = Ffalse" 
       proof -
         { assume "t_v_evaluation I (Comp2 F) = Ttrue"
           hence "t_v_evaluationConjuncionG I [[Comp1 F, Comp2 F]] = Ttrue" by simp
           hence "False" using 3 by simp}
         hence "t_v_evaluation I (Comp2 F) ≠ Ttrue" by auto
         thus "t_v_evaluation I (Comp2 F) = Ffalse" using Bivaluation by auto
       qed    
       thus "t_v_evaluation I (Comp1 F ∨. Comp2 F) = Ffalse" using 4  
         by (auto, unfold v_disjunction_def, simp)
     qed
     thus "t_v_evaluation I F = t_v_evaluation I (Comp1 F ∨. Comp2 F)" using hip2 by simp
   qed 
 qed
qed

(*>*)

(*<*)
end
(*>*)