(******************************************************************************)
theory i140309aa__semantab
imports Complex_Main (*"../../iHelp/i"*) (*"../../IsaN/work/IsaN" *)
begin

(*( \<turnstile> ): Turnstile to shorten the notation for meta-implication.*)
no_notation ==> (infixr "\<turnstile>" 4)
abbreviation mimp_turn :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
  "mimp_turn P Q == (PROP P \<Longrightarrow> PROP Q)"
  notation mimp_turn (infixr "\<turnstile>" 4)

(*( \<cedilla> ): Cedilla, to act as a comma, for formulas such as P\<cedilla> Q \<turnstile> R.*)  
notation (input) ==> (infixr "\<cedilla>" 4)

(*( \<bottom> ): False, to shorten the notation. The output is bold for visibility.*)
notation (input) False ("\<bottom>") 
notation (output) False ("\<^bold>\<bottom>")

(*( \<cdot>~\<cdot> ): notP, PROP not.*)
abbreviation notP :: "prop \<Rightarrow> prop" where
  "notP P == (PROP P \<Longrightarrow> False)"
  notation notP ("\<cdot>~\<cdot>'(_')") (* \<cdot>~\<cdot> *)

(*( \<or>\<^sub>p ): orP, PROP disjunction.*)  
(*PROP or: orP*)
abbreviation orP :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
  "orP P Q == ((PROP P \<Longrightarrow> False) \<Longrightarrow> PROP Q)"
notation 
  orP (infixr "(\<or>\<^sub>p)" 4)

(*( \<and>\<^sub>p ): andP, PROP conjunction.*)    
abbreviation andP :: "prop \<Rightarrow> prop \<Rightarrow> prop" where
  "andP P Q == ((PROP P \<Longrightarrow> PROP Q \<Longrightarrow> False) \<Longrightarrow> False)"
notation
  andP (infixr "(\<and>\<^sub>p)" 4) 

(*( \<and>\<^sub>4 ): and4, bool conjunction with the same priority as andP. For conversions 
  from bool to PROP, to ensure that the same parenthesizing applies.*)
abbreviation (input) and4 :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
  "and4 P Q == (P \<and> Q)"
notation 
  and4 (infixr "(\<and>\<^sub>4)" 4) 
    
(*******************************)
(* LOGIC RULES *****************)
(*******************************)

lemma mimp2in_to_3and_mimps_False:
  "P\<cedilla> Q \<turnstile> R == P \<and>\<^sub>4 Q \<and>\<^sub>4 \<not>R \<turnstile> False"
by(rule equal_intr_rule, auto)

lemma or6_mimps_False_to_6andP_of_notPs:
  "P\<^sub>1 \<or> P\<^sub>2 \<or> P\<^sub>3 \<or> P\<^sub>4 \<or> P\<^sub>5 \<or> P\<^sub>6 \<turnstile> False
    == \<cdot>~\<cdot>(P\<^sub>1) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>2) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>3) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>4) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>5) \<and>\<^sub>p \<cdot>~\<cdot>(P\<^sub>6)"
by(rule equal_intr_rule, auto)

lemma and_eq_andP:
  "Trueprop(P \<and> Q) == P \<and>\<^sub>p Q"
by(rule equal_intr_rule, auto)

lemma not_eq_notP:
  "Trueprop(\<not>P) == \<cdot>~\<cdot>(P)"
by(rule equal_intr_rule, auto)

lemmas semantab_bool_expansion =
  simp_thms(1)
  imp_conv_disj
  de_Morgan_conj
  de_Morgan_disj
  conj_comms
  conj_disj_distribL
  disj_assoc
  
lemmas semantab_bool_to_prop =
  and_eq_andP
  not_eq_notP
  
(**************************)
(* THEOREM ****************)
(**************************)

notation Trueprop ("_\<Colon>\<^sub>T" [1000] 1000)
declare[[show_sorts=false, show_types=false, show_brackets=true]]

lemma 
  "(A \<and> B) \<longrightarrow> C\<cedilla> \<not>A \<longrightarrow> D \<turnstile> B \<longrightarrow> (C \<or> D)" 
  unfolding mimp2in_to_3and_mimps_False
  unfolding semantab_bool_expansion
  unfolding or6_mimps_False_to_6andP_of_notPs
  unfolding semantab_bool_to_prop
by(auto)

lemma 
  "(A \<and> B) \<longrightarrow> C\<cedilla> \<not>A \<longrightarrow> D \<turnstile> B \<longrightarrow> (C \<or> D)" 
(*|Negate the conclusion and convert it to a 3-bool-and that mimps False.
  The notation for (P \<turnstile> False) is \<cdot>~\<cdot>(P). Because of requirements due to Trueprop 
  and other low priorities, notP needs to be in parentheses.|*)
  unfolding mimp2in_to_3and_mimps_False
  
(*|Expand the bool formulas. The result will be a 6-bool-or that is nested to 
  the left, and that mimps False.|*)
  unfolding 
    simp_thms(1)
    imp_conv_disj
    de_Morgan_conj
    de_Morgan_disj
    conj_comms
    conj_disj_distribL 
  
(*|Nest the 6-bool-or to the right.|*)
  unfolding disj_assoc 
  
(*|Convert the 6-bool-or to 6 chains of andP-ands that each mimp False.|*)
  unfolding or6_mimps_False_to_6andP_of_notPs
  
(*|Convert the bool-nots and bool-ands to notP-nots and andP-ands.|*)  
  unfolding and_eq_andP
  unfolding not_eq_notP
  
(*Now, there is no use of HOL in the formula except for the use of Trueprop
  and False. This can be seen by the fact that all of A, B, C, and D are being
  coerced by Trueprop. To turn the Trueprop printing off, change notation above  
  to no_notation.*)
  using[[show_sorts=false, show_types=false, show_brackets=false]]
  
(*The definition is shown as follows, from HOL.thy:

    defs
    True_def:     "True      == ((%x::bool. x) = (%x. x))"
    All_def:      "All(P)    == (P = (%x. True))"
    Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"
    False_def:    "False     == (!P. P)"
  
  It's defined using only All and True, however, obviously, it's totally tied 
  into the logic of HOL. But then, that's what makes auto work by magic when
  used above, and below. 
  
  Of course, auto doesn't need any of this to be done for this theorem, but 
  it could be that auto will be grateful someday. On the other hand, it's more
  likely that auto is an emotionless automaton, who doesn't care whether I live
  or die. In that case, it will be me who is grateful someday.*)
by(auto)
  
(******************************************************************************)
end