# Theory HOL

Up to index of Isabelle/HOL

theory HOL
imports CPure
uses (cladata.ML) (blastdata.ML) (simpdata.ML) (eqrule_HOL_data.ML) ($ISABELLE_HOME/src/Provers/eqsubst.ML) [HOL.ML]
begin

    (*  Title:      HOL/HOL.thy
        ID:         $Id: HOL.thy,v 1.155 2005/09/25 18:19:31 berghofe Exp $
        Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
    *)

    header {* The basis of Higher-Order Logic *}

    theory HOL
    imports CPure
    uses ("cladata.ML") ("blastdata.ML") ("simpdata.ML") ("eqrule_HOL_data.ML")
          ("~~/src/Provers/eqsubst.ML")

    begin

    subsection {* Primitive logic *}

    subsubsection {* Core syntax *}

    classes type
    defaultsort type

    global

    typedecl bool

    arities
      bool :: type
      fun :: (type, type) type

    judgment
      Trueprop      :: "bool => prop"                   ("(_)" 5)

    consts
      Not           :: "bool => bool"                   ("~ _" [40] 40)
      True          :: bool
      False         :: bool
      arbitrary     :: 'a

      The           :: "('a => bool) => 'a"
      All           :: "('a => bool) => bool"           (binder "ALL " 10)
      Ex            :: "('a => bool) => bool"           (binder "EX " 10)
      Ex1           :: "('a => bool) => bool"           (binder "EX! " 10)
      Let           :: "['a, 'a => 'b] => 'b"

      "="           :: "['a, 'a] => bool"               (infixl 50)
      &             :: "[bool, bool] => bool"           (infixr 35)
      "|"           :: "[bool, bool] => bool"           (infixr 30)
      -->           :: "[bool, bool] => bool"           (infixr 25)

    local

    consts
      If            :: "[bool, 'a, 'a] => 'a"           ("(if (_)/ then (_)/ else (_))" 10)

    subsubsection {* Additional concrete syntax *}

    nonterminals
      letbinds  letbind
      case_syn  cases_syn

    syntax
      "_not_equal"  :: "['a, 'a] => bool"                    (infixl "~=" 50)
      "_The"        :: "[pttrn, bool] => 'a"                 ("(3THE _./ _)" [0, 10] 10)

      "_bind"       :: "[pttrn, 'a] => letbind"              ("(2_ =/ _)" 10)
      ""            :: "letbind => letbinds"                 ("_")
      "_binds"      :: "[letbind, letbinds] => letbinds"     ("_;/ _")
      "_Let"        :: "[letbinds, 'a] => 'a"                ("(let (_)/ in (_))" 10)

      "_case_syntax":: "['a, cases_syn] => 'b"               ("(case _ of/ _)" 10)
      "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
      ""            :: "case_syn => cases_syn"               ("_")
      "_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ | _")

    translations
      "x ~= y"                == "~ (x = y)"
      "THE x. P"              == "The (%x. P)"
      "_Let (_binds b bs) e"  == "_Let b (_Let bs e)"
      "let x = a in e"        == "Let a (%x. e)"

    print_translation {*
    (* To avoid eta-contraction of body: *)
    [("The", fn [Abs abs] =>
         let val (x,t) = atomic_abs_tr' abs
         in Syntax.const "_The" $ x $ t end)]
    *}

    syntax (output)
      "="           :: "['a, 'a] => bool"                    (infix 50)
      "_not_equal"  :: "['a, 'a] => bool"                    (infix "~=" 50)

    syntax (xsymbols)
      Not           :: "bool => bool"                        ("¬ _" [40] 40)
      "op &"        :: "[bool, bool] => bool"                (infixr "∧" 35)
      "op |"        :: "[bool, bool] => bool"                (infixr "∨" 30)
      "op -->"      :: "[bool, bool] => bool"                (infixr "-->" 25)
      "_not_equal"  :: "['a, 'a] => bool"                    (infix "≠" 50)
      "ALL "        :: "[idts, bool] => bool"                ("(3∀_./ _)" [0, 10] 10)
      "EX "         :: "[idts, bool] => bool"                ("(3∃_./ _)" [0, 10] 10)
      "EX! "        :: "[idts, bool] => bool"                ("(3∃!_./ _)" [0, 10] 10)
      "_case1"      :: "['a, 'b] => case_syn"                ("(2_ =>/ _)" 10)
    (*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)

    syntax (xsymbols output)
      "_not_equal"  :: "['a, 'a] => bool"                    (infix "≠" 50)

    syntax (HTML output)
      "_not_equal"  :: "['a, 'a] => bool"                    (infix "≠" 50)
      Not           :: "bool => bool"                        ("¬ _" [40] 40)
      "op &"        :: "[bool, bool] => bool"                (infixr "∧" 35)
      "op |"        :: "[bool, bool] => bool"                (infixr "∨" 30)
      "_not_equal"  :: "['a, 'a] => bool"                    (infix "≠" 50)
      "ALL "        :: "[idts, bool] => bool"                ("(3∀_./ _)" [0, 10] 10)
      "EX "         :: "[idts, bool] => bool"                ("(3∃_./ _)" [0, 10] 10)
      "EX! "        :: "[idts, bool] => bool"                ("(3∃!_./ _)" [0, 10] 10)

    syntax (HOL)
      "ALL "        :: "[idts, bool] => bool"                ("(3! _./ _)" [0, 10] 10)
      "EX "         :: "[idts, bool] => bool"                ("(3? _./ _)" [0, 10] 10)
      "EX! "        :: "[idts, bool] => bool"                ("(3?! _./ _)" [0, 10] 10)

    subsubsection {* Axioms and basic definitions *}

    axioms
      eq_reflection:  "(x=y) ==> (x==y)"

      refl:           "t = (t::'a)"

      ext:            "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
        -- {*Extensionality is built into the meta-logic, and this rule expresses
             a related property.  It is an eta-expanded version of the traditional
             rule, and similar to the ABS rule of HOL*}

      the_eq_trivial: "(THE x. x = a) = (a::'a)"

      impI:           "(P ==> Q) ==> P-->Q"
      mp:             "[| P-->Q;  P |] ==> Q"

    text{*Thanks to Stephan Merz*}
    theorem subst:
      assumes eq: "s = t" and p: "P(s)"
      shows "P(t::'a)"
    proof -
      from eq have meta: "s ≡ t"
        by (rule eq_reflection)
      from p show ?thesis
        by (unfold meta)
    qed

    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)"
      not_def:      "~ P       == P-->False"
      and_def:      "P & Q     == !R. (P-->Q-->R) --> R"
      or_def:       "P | Q     == !R. (P-->R) --> (Q-->R) --> R"
      Ex1_def:      "Ex1(P)    == ? x. P(x) & (! y. P(y) --> y=x)"

    axioms
      iff:          "(P-->Q) --> (Q-->P) --> (P=Q)"
      True_or_False:  "(P=True) | (P=False)"

    defs
      Let_def:      "Let s f == f(s)"
      if_def:       "If P x y == THE z::'a. (P=True --> z=x) & (P=False --> z=y)"

    finalconsts
      "op ="
      "op -->"
      The
      arbitrary

    subsubsection {* Generic algebraic operations *}

    axclass zero < type
    axclass one < type
    axclass plus < type
    axclass minus < type
    axclass times < type
    axclass inverse < type

    global

    consts
      "0"           :: "'a::zero"                       ("0")
      "1"           :: "'a::one"                        ("1")
      "+"           :: "['a::plus, 'a]  => 'a"          (infixl 65)
      -             :: "['a::minus, 'a] => 'a"          (infixl 65)
      uminus        :: "['a::minus] => 'a"              ("- _" [81] 80)
      *             :: "['a::times, 'a] => 'a"          (infixl 70)

    syntax
      "_index1"  :: index    ("1")
    translations
      (index) "1" => (index) "\<struct>"

    local

    typed_print_translation {*
      let
        fun tr' c = (c, fn show_sorts => fn T => fn ts =>
          if T = dummyT orelse not (! show_types) andalso can Term.dest_Type T then raise Match
          else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
      in [tr' "0", tr' "1"] end;
    *} -- {* show types that are presumably too general *}

    consts
      abs           :: "'a::minus => 'a"
      inverse       :: "'a::inverse => 'a"
      divide        :: "['a::inverse, 'a] => 'a"        (infixl "'/" 70)

    syntax (xsymbols)
      abs :: "'a::minus => 'a"    ("¦_¦")
    syntax (HTML output)
      abs :: "'a::minus => 'a"    ("¦_¦")

    subsection {*Equality*}

    lemma sym: "s=t ==> t=s"
    apply (erule subst)
    apply (rule refl)
    done

    (*calling "standard" reduces maxidx to 0*)
    lemmas ssubst = sym [THEN subst, standard]

    lemma trans: "[| r=s; s=t |] ==> r=t"
    apply (erule subst , assumption)
    done

    lemma def_imp_eq:  assumes meq: "A == B" shows "A = B"
    apply (unfold meq)
    apply (rule refl)
    done

    (*Useful with eresolve_tac for proving equalties from known equalities.
            a = b
            |   |
            c = d   *)
    lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
    apply (rule trans)
    apply (rule trans)
    apply (rule sym)
    apply assumption+
    done

    text {* For calculational reasoning: *}

    lemma forw_subst: "a = b ==> P b ==> P a"
      by (rule ssubst)

    lemma back_subst: "P a ==> a = b ==> P b"
      by (rule subst)

    subsection {*Congruence rules for application*}

    (*similar to AP_THM in Gordon's HOL*)
    lemma fun_cong: "(f::'a=>'b) = g ==> f(x)=g(x)"
    apply (erule subst)
    apply (rule refl)
    done

    (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    lemma arg_cong: "x=y ==> f(x)=f(y)"
    apply (erule subst)
    apply (rule refl)
    done

    lemma arg_cong2: "[| a = b; c = d |] ==> f a c = f b d"
    apply (erule ssubst)+
    apply (rule refl)
    done

    lemma cong: "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    apply (erule subst)+
    apply (rule refl)
    done

    subsection {*Equality of booleans -- iff*}

    lemma iffI: assumes prems: "P ==> Q" "Q ==> P" shows "P=Q"
    apply (iprover intro: iff [THEN mp, THEN mp] impI prems)
    done

    lemma iffD2: "[| P=Q; Q |] ==> P"
    apply (erule ssubst)
    apply assumption
    done

    lemma rev_iffD2: "[| Q; P=Q |] ==> P"
    apply (erule iffD2)
    apply assumption
    done

    lemmas iffD1 = sym [THEN iffD2, standard]
    lemmas rev_iffD1 = sym [THEN [2] rev_iffD2, standard]

    lemma iffE:
      assumes major: "P=Q"
          and minor: "[| P --> Q; Q --> P |] ==> R"
      shows "R"
    by (iprover intro: minor impI major [THEN iffD2] major [THEN iffD1])

    subsection {*True*}

    lemma TrueI: "True"
    apply (unfold True_def)
    apply (rule refl)
    done

    lemma eqTrueI: "P ==> P=True"
    by (iprover intro: iffI TrueI)

    lemma eqTrueE: "P=True ==> P"
    apply (erule iffD2)
    apply (rule TrueI)
    done

    subsection {*Universal quantifier*}

    lemma allI: assumes p: "!!x::'a. P(x)" shows "ALL x. P(x)"
    apply (unfold All_def)
    apply (iprover intro: ext eqTrueI p)
    done

    lemma spec: "ALL x::'a. P(x) ==> P(x)"
    apply (unfold All_def)
    apply (rule eqTrueE)
    apply (erule fun_cong)
    done

    lemma allE:
      assumes major: "ALL x. P(x)"
          and minor: "P(x) ==> R"
      shows "R"
    by (iprover intro: minor major [THEN spec])

    lemma all_dupE:
      assumes major: "ALL x. P(x)"
          and minor: "[| P(x); ALL x. P(x) |] ==> R"
      shows "R"
    by (iprover intro: minor major major [THEN spec])

    subsection {*False*}
    (*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)

    lemma FalseE: "False ==> P"
    apply (unfold False_def)
    apply (erule spec)
    done

    lemma False_neq_True: "False=True ==> P"
    by (erule eqTrueE [THEN FalseE])

    subsection {*Negation*}

    lemma notI:
      assumes p: "P ==> False"
      shows "~P"
    apply (unfold not_def)
    apply (iprover intro: impI p)
    done

    lemma False_not_True: "False ~= True"
    apply (rule notI)
    apply (erule False_neq_True)
    done

    lemma True_not_False: "True ~= False"
    apply (rule notI)
    apply (drule sym)
    apply (erule False_neq_True)
    done

    lemma notE: "[| ~P;  P |] ==> R"
    apply (unfold not_def)
    apply (erule mp [THEN FalseE])
    apply assumption
    done

    (* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
    lemmas notI2 = notE [THEN notI, standard]

    subsection {*Implication*}

    lemma impE:
      assumes "P-->Q" "P" "Q ==> R"
      shows "R"
    by (iprover intro: prems mp)

    (* Reduces Q to P-->Q, allowing substitution in P. *)
    lemma rev_mp: "[| P;  P --> Q |] ==> Q"
    by (iprover intro: mp)

    lemma contrapos_nn:
      assumes major: "~Q"
          and minor: "P==>Q"
      shows "~P"
    by (iprover intro: notI minor major [THEN notE])

    (*not used at all, but we already have the other 3 combinations *)
    lemma contrapos_pn:
      assumes major: "Q"
          and minor: "P ==> ~Q"
      shows "~P"
    by (iprover intro: notI minor major notE)

    lemma not_sym: "t ~= s ==> s ~= t"
    apply (erule contrapos_nn)
    apply (erule sym)
    done

    (*still used in HOLCF*)
    lemma rev_contrapos:
      assumes pq: "P ==> Q"
          and nq: "~Q"
      shows "~P"
    apply (rule nq [THEN contrapos_nn])
    apply (erule pq)
    done

    subsection {*Existential quantifier*}

    lemma exI: "P x ==> EX x::'a. P x"
    apply (unfold Ex_def)
    apply (iprover intro: allI allE impI mp)
    done

    lemma exE:
      assumes major: "EX x::'a. P(x)"
          and minor: "!!x. P(x) ==> Q"
      shows "Q"
    apply (rule major [unfolded Ex_def, THEN spec, THEN mp])
    apply (iprover intro: impI [THEN allI] minor)
    done

    subsection {*Conjunction*}

    lemma conjI: "[| P; Q |] ==> P&Q"
    apply (unfold and_def)
    apply (iprover intro: impI [THEN allI] mp)
    done

    lemma conjunct1: "[| P & Q |] ==> P"
    apply (unfold and_def)
    apply (iprover intro: impI dest: spec mp)
    done

    lemma conjunct2: "[| P & Q |] ==> Q"
    apply (unfold and_def)
    apply (iprover intro: impI dest: spec mp)
    done

    lemma conjE:
      assumes major: "P&Q"
          and minor: "[| P; Q |] ==> R"
      shows "R"
    apply (rule minor)
    apply (rule major [THEN conjunct1])
    apply (rule major [THEN conjunct2])
    done

    lemma context_conjI:
      assumes prems: "P" "P ==> Q" shows "P & Q"
    by (iprover intro: conjI prems)

    subsection {*Disjunction*}

    lemma disjI1: "P ==> P|Q"
    apply (unfold or_def)
    apply (iprover intro: allI impI mp)
    done

    lemma disjI2: "Q ==> P|Q"
    apply (unfold or_def)
    apply (iprover intro: allI impI mp)
    done

    lemma disjE:
      assumes major: "P|Q"
          and minorP: "P ==> R"
          and minorQ: "Q ==> R"
      shows "R"
    by (iprover intro: minorP minorQ impI
                     major [unfolded or_def, THEN spec, THEN mp, THEN mp])

    subsection {*Classical logic*}

    lemma classical:
      assumes prem: "~P ==> P"
      shows "P"
    apply (rule True_or_False [THEN disjE, THEN eqTrueE])
    apply assumption
    apply (rule notI [THEN prem, THEN eqTrueI])
    apply (erule subst)
    apply assumption
    done

    lemmas ccontr = FalseE [THEN classical, standard]

    (*notE with premises exchanged; it discharges ~R so that it can be used to
      make elimination rules*)
    lemma rev_notE:
      assumes premp: "P"
          and premnot: "~R ==> ~P"
      shows "R"
    apply (rule ccontr)
    apply (erule notE [OF premnot premp])
    done

    (*Double negation law*)
    lemma notnotD: "~~P ==> P"
    apply (rule classical)
    apply (erule notE)
    apply assumption
    done

    lemma contrapos_pp:
      assumes p1: "Q"
          and p2: "~P ==> ~Q"
      shows "P"
    by (iprover intro: classical p1 p2 notE)

    subsection {*Unique existence*}

    lemma ex1I:
      assumes prems: "P a" "!!x. P(x) ==> x=a"
      shows "EX! x. P(x)"
    by (unfold Ex1_def, iprover intro: prems exI conjI allI impI)

    text{*Sometimes easier to use: the premises have no shared variables.  Safe!*}
    lemma ex_ex1I:
      assumes ex_prem: "EX x. P(x)"
          and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
      shows "EX! x. P(x)"
    by (iprover intro: ex_prem [THEN exE] ex1I eq)

    lemma ex1E:
      assumes major: "EX! x. P(x)"
          and minor: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
      shows "R"
    apply (rule major [unfolded Ex1_def, THEN exE])
    apply (erule conjE)
    apply (iprover intro: minor)
    done

    lemma ex1_implies_ex: "EX! x. P x ==> EX x. P x"
    apply (erule ex1E)
    apply (rule exI)
    apply assumption
    done

    subsection {*THE: definite description operator*}

    lemma the_equality:
      assumes prema: "P a"
          and premx: "!!x. P x ==> x=a"
      shows "(THE x. P x) = a"
    apply (rule trans [OF _ the_eq_trivial])
    apply (rule_tac f = "The" in arg_cong)
    apply (rule ext)
    apply (rule iffI)
     apply (erule premx)
    apply (erule ssubst, rule prema)
    done

    lemma theI:
      assumes "P a" and "!!x. P x ==> x=a"
      shows "P (THE x. P x)"
    by (iprover intro: prems the_equality [THEN ssubst])

    lemma theI': "EX! x. P x ==> P (THE x. P x)"
    apply (erule ex1E)
    apply (erule theI)
    apply (erule allE)
    apply (erule mp)
    apply assumption
    done

    (*Easier to apply than theI: only one occurrence of P*)
    lemma theI2:
      assumes "P a" "!!x. P x ==> x=a" "!!x. P x ==> Q x"
      shows "Q (THE x. P x)"
    by (iprover intro: prems theI)

    lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
    apply (rule the_equality)
    apply  assumption
    apply (erule ex1E)
    apply (erule all_dupE)
    apply (drule mp)
    apply  assumption
    apply (erule ssubst)
    apply (erule allE)
    apply (erule mp)
    apply assumption
    done

    lemma the_sym_eq_trivial: "(THE y. x=y) = x"
    apply (rule the_equality)
    apply (rule refl)
    apply (erule sym)
    done

    subsection {*Classical intro rules for disjunction and existential quantifiers*}

    lemma disjCI:
      assumes "~Q ==> P" shows "P|Q"
    apply (rule classical)
    apply (iprover intro: prems disjI1 disjI2 notI elim: notE)
    done

    lemma excluded_middle: "~P | P"
    by (iprover intro: disjCI)

    text{*case distinction as a natural deduction rule. Note that @{term "~P"}
       is the second case, not the first.*}
    lemma case_split_thm:
      assumes prem1: "P ==> Q"
          and prem2: "~P ==> Q"
      shows "Q"
    apply (rule excluded_middle [THEN disjE])
    apply (erule prem2)
    apply (erule prem1)
    done

    (*Classical implies (-->) elimination. *)
    lemma impCE:
      assumes major: "P-->Q"
          and minor: "~P ==> R" "Q ==> R"
      shows "R"
    apply (rule excluded_middle [of P, THEN disjE])
    apply (iprover intro: minor major [THEN mp])+
    done

    (*This version of --> elimination works on Q before P.  It works best for
      those cases in which P holds "almost everywhere".  Can't install as
      default: would break old proofs.*)
    lemma impCE':
      assumes major: "P-->Q"
          and minor: "Q ==> R" "~P ==> R"
      shows "R"
    apply (rule excluded_middle [of P, THEN disjE])
    apply (iprover intro: minor major [THEN mp])+
    done

    (*Classical <-> elimination. *)
    lemma iffCE:
      assumes major: "P=Q"
          and minor: "[| P; Q |] ==> R"  "[| ~P; ~Q |] ==> R"
      shows "R"
    apply (rule major [THEN iffE])
    apply (iprover intro: minor elim: impCE notE)
    done

    lemma exCI:
      assumes "ALL x. ~P(x) ==> P(a)"
      shows "EX x. P(x)"
    apply (rule ccontr)
    apply (iprover intro: prems exI allI notI notE [of "∃x. P x"])
    done

    subsection {* Theory and package setup *}

    ML
    {*
    val eq_reflection = thm "eq_reflection"
    val refl = thm "refl"
    val subst = thm "subst"
    val ext = thm "ext"
    val impI = thm "impI"
    val mp = thm "mp"
    val True_def = thm "True_def"
    val All_def = thm "All_def"
    val Ex_def = thm "Ex_def"
    val False_def = thm "False_def"
    val not_def = thm "not_def"
    val and_def = thm "and_def"
    val or_def = thm "or_def"
    val Ex1_def = thm "Ex1_def"
    val iff = thm "iff"
    val True_or_False = thm "True_or_False"
    val Let_def = thm "Let_def"
    val if_def = thm "if_def"
    val sym = thm "sym"
    val ssubst = thm "ssubst"
    val trans = thm "trans"
    val def_imp_eq = thm "def_imp_eq"
    val box_equals = thm "box_equals"
    val fun_cong = thm "fun_cong"
    val arg_cong = thm "arg_cong"
    val cong = thm "cong"
    val iffI = thm "iffI"
    val iffD2 = thm "iffD2"
    val rev_iffD2 = thm "rev_iffD2"
    val iffD1 = thm "iffD1"
    val rev_iffD1 = thm "rev_iffD1"
    val iffE = thm "iffE"
    val TrueI = thm "TrueI"
    val eqTrueI = thm "eqTrueI"
    val eqTrueE = thm "eqTrueE"
    val allI = thm "allI"
    val spec = thm "spec"
    val allE = thm "allE"
    val all_dupE = thm "all_dupE"
    val FalseE = thm "FalseE"
    val False_neq_True = thm "False_neq_True"
    val notI = thm "notI"
    val False_not_True = thm "False_not_True"
    val True_not_False = thm "True_not_False"
    val notE = thm "notE"
    val notI2 = thm "notI2"
    val impE = thm "impE"
    val rev_mp = thm "rev_mp"
    val contrapos_nn = thm "contrapos_nn"
    val contrapos_pn = thm "contrapos_pn"
    val not_sym = thm "not_sym"
    val rev_contrapos = thm "rev_contrapos"
    val exI = thm "exI"
    val exE = thm "exE"
    val conjI = thm "conjI"
    val conjunct1 = thm "conjunct1"
    val conjunct2 = thm "conjunct2"
    val conjE = thm "conjE"
    val context_conjI = thm "context_conjI"
    val disjI1 = thm "disjI1"
    val disjI2 = thm "disjI2"
    val disjE = thm "disjE"
    val classical = thm "classical"
    val ccontr = thm "ccontr"
    val rev_notE = thm "rev_notE"
    val notnotD = thm "notnotD"
    val contrapos_pp = thm "contrapos_pp"
    val ex1I = thm "ex1I"
    val ex_ex1I = thm "ex_ex1I"
    val ex1E = thm "ex1E"
    val ex1_implies_ex = thm "ex1_implies_ex"
    val the_equality = thm "the_equality"
    val theI = thm "theI"
    val theI' = thm "theI'"
    val theI2 = thm "theI2"
    val the1_equality = thm "the1_equality"
    val the_sym_eq_trivial = thm "the_sym_eq_trivial"
    val disjCI = thm "disjCI"
    val excluded_middle = thm "excluded_middle"
    val case_split_thm = thm "case_split_thm"
    val impCE = thm "impCE"
    val impCE = thm "impCE"
    val iffCE = thm "iffCE"
    val exCI = thm "exCI"

    (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
    local
      fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
      |   wrong_prem (Bound _) = true
      |   wrong_prem _ = false
      val filter_right = List.filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))))
    in
      fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp])
      fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
    end

    fun strip_tac i = REPEAT(resolve_tac [impI,allI] i)

    (*Obsolete form of disjunctive case analysis*)
    fun excluded_middle_tac sP =
        res_inst_tac [("Q",sP)] (excluded_middle RS disjE)

    fun case_tac a = res_inst_tac [("P",a)] case_split_thm
    *}

    theorems case_split = case_split_thm [case_names True False]

    subsubsection {* Intuitionistic Reasoning *}

    lemma impE':
      assumes 1: "P --> Q"
        and 2: "Q ==> R"
        and 3: "P --> Q ==> P"
      shows R
    proof -
      from 3 and 1 have P .
      with 1 have Q by (rule impE)
      with 2 show R .
    qed

    lemma allE':
      assumes 1: "ALL x. P x"
        and 2: "P x ==> ALL x. P x ==> Q"
      shows Q
    proof -
      from 1 have "P x" by (rule spec)
      from this and 1 show Q by (rule 2)
    qed

    lemma notE':
      assumes 1: "~ P"
        and 2: "~ P ==> P"
      shows R
    proof -
      from 2 and 1 have P .
      with 1 show R by (rule notE)
    qed

    lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
      and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
      and [Pure.elim 2] = allE notE' impE'
      and [Pure.intro] = exI disjI2 disjI1

    lemmas [trans] = trans
      and [sym] = sym not_sym
      and [Pure.elim?] = iffD1 iffD2 impE

    subsubsection {* Atomizing meta-level connectives *}

    lemma atomize_all [atomize]: "(!!x. P x) == Trueprop (ALL x. P x)"
    proof
      assume "!!x. P x"
      show "ALL x. P x" by (rule allI)
    next
      assume "ALL x. P x"
      thus "!!x. P x" by (rule allE)
    qed

    lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
    proof
      assume r: "A ==> B"
      show "A --> B" by (rule impI) (rule r)
    next
      assume "A --> B" and A
      thus B by (rule mp)
    qed

    lemma atomize_not: "(A ==> False) == Trueprop (~A)"
    proof
      assume r: "A ==> False"
      show "~A" by (rule notI) (rule r)
    next
      assume "~A" and A
      thus False by (rule notE)
    qed

    lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
    proof
      assume "x == y"
      show "x = y" by (unfold prems) (rule refl)
    next
      assume "x = y"
      thus "x == y" by (rule eq_reflection)
    qed

    lemma atomize_conj [atomize]:
      "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
    proof
      assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
      show "A & B" by (rule conjI)
    next
      fix C
      assume "A & B"
      assume "A ==> B ==> PROP C"
      thus "PROP C"
      proof this
        show A by (rule conjunct1)
        show B by (rule conjunct2)
      qed
    qed

    lemmas [symmetric, rulify] = atomize_all atomize_imp

    subsubsection {* Classical Reasoner setup *}

    use "cladata.ML"
    setup hypsubst_setup

    setup {*
      [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)]
    *}

    setup Classical.setup
    setup clasetup

    lemmas [intro?] = ext
      and [elim?] = ex1_implies_ex

    use "blastdata.ML"
    setup Blast.setup

    subsubsection {* Simplifier setup *}

    lemma meta_eq_to_obj_eq: "x == y ==> x = y"
    proof -
      assume r: "x == y"
      show "x = y" by (unfold r) (rule refl)
    qed

    lemma eta_contract_eq: "(%s. f s) = f" ..

    lemma simp_thms:
      shows not_not: "(~ ~ P) = P"
      and Not_eq_iff: "((~P) = (~Q)) = (P = Q)"
      and
        "(P ~= Q) = (P = (~Q))"
        "(P | ~P) = True"    "(~P | P) = True"
        "(x = x) = True"
        "(~True) = False"  "(~False) = True"
        "(~P) ~= P"  "P ~= (~P)"
        "(True=P) = P"  "(P=True) = P"  "(False=P) = (~P)"  "(P=False) = (~P)"
        "(True --> P) = P"  "(False --> P) = True"
        "(P --> True) = True"  "(P --> P) = True"
        "(P --> False) = (~P)"  "(P --> ~P) = (~P)"
        "(P & True) = P"  "(True & P) = P"
        "(P & False) = False"  "(False & P) = False"
        "(P & P) = P"  "(P & (P & Q)) = (P & Q)"
        "(P & ~P) = False"    "(~P & P) = False"
        "(P | True) = True"  "(True | P) = True"
        "(P | False) = P"  "(False | P) = P"
        "(P | P) = P"  "(P | (P | Q)) = (P | Q)" and
        "(ALL x. P) = P"  "(EX x. P) = P"  "EX x. x=t"  "EX x. t=x"
        -- {* needed for the one-point-rule quantifier simplification procs *}
        -- {* essential for termination!! *} and
        "!!P. (EX x. x=t & P(x)) = P(t)"
        "!!P. (EX x. t=x & P(x)) = P(t)"
        "!!P. (ALL x. x=t --> P(x)) = P(t)"
        "!!P. (ALL x. t=x --> P(x)) = P(t)"
      by (blast, blast, blast, blast, blast, iprover+)

    lemma imp_cong: "(P = P') ==> (P' ==> (Q = Q')) ==> ((P --> Q) = (P' --> Q'))"
      by iprover

    lemma ex_simps:
      "!!P Q. (EX x. P x & Q)   = ((EX x. P x) & Q)"
      "!!P Q. (EX x. P & Q x)   = (P & (EX x. Q x))"
      "!!P Q. (EX x. P x | Q)   = ((EX x. P x) | Q)"
      "!!P Q. (EX x. P | Q x)   = (P | (EX x. Q x))"
      "!!P Q. (EX x. P x --> Q) = ((ALL x. P x) --> Q)"
      "!!P Q. (EX x. P --> Q x) = (P --> (EX x. Q x))"
      -- {* Miniscoping: pushing in existential quantifiers. *}
      by (iprover | blast)+

    lemma all_simps:
      "!!P Q. (ALL x. P x & Q)   = ((ALL x. P x) & Q)"
      "!!P Q. (ALL x. P & Q x)   = (P & (ALL x. Q x))"
      "!!P Q. (ALL x. P x | Q)   = ((ALL x. P x) | Q)"
      "!!P Q. (ALL x. P | Q x)   = (P | (ALL x. Q x))"
      "!!P Q. (ALL x. P x --> Q) = ((EX x. P x) --> Q)"
      "!!P Q. (ALL x. P --> Q x) = (P --> (ALL x. Q x))"
      -- {* Miniscoping: pushing in universal quantifiers. *}
      by (iprover | blast)+

    lemma disj_absorb: "(A | A) = A"
      by blast

    lemma disj_left_absorb: "(A | (A | B)) = (A | B)"
      by blast

    lemma conj_absorb: "(A & A) = A"
      by blast

    lemma conj_left_absorb: "(A & (A & B)) = (A & B)"
      by blast

    lemma eq_ac:
      shows eq_commute: "(a=b) = (b=a)"
        and eq_left_commute: "(P=(Q=R)) = (Q=(P=R))"
        and eq_assoc: "((P=Q)=R) = (P=(Q=R))" by (iprover, blast+)
    lemma neq_commute: "(a~=b) = (b~=a)" by iprover

    lemma conj_comms:
      shows conj_commute: "(P&Q) = (Q&P)"
        and conj_left_commute: "(P&(Q&R)) = (Q&(P&R))" by iprover+
    lemma conj_assoc: "((P&Q)&R) = (P&(Q&R))" by iprover

    lemma disj_comms:
      shows disj_commute: "(P|Q) = (Q|P)"
        and disj_left_commute: "(P|(Q|R)) = (Q|(P|R))" by iprover+
    lemma disj_assoc: "((P|Q)|R) = (P|(Q|R))" by iprover

    lemma conj_disj_distribL: "(P&(Q|R)) = (P&Q | P&R)" by iprover
    lemma conj_disj_distribR: "((P|Q)&R) = (P&R | Q&R)" by iprover

    lemma disj_conj_distribL: "(P|(Q&R)) = ((P|Q) & (P|R))" by iprover
    lemma disj_conj_distribR: "((P&Q)|R) = ((P|R) & (Q|R))" by iprover

    lemma imp_conjR: "(P --> (Q&R)) = ((P-->Q) & (P-->R))" by iprover
    lemma imp_conjL: "((P&Q) -->R)  = (P --> (Q --> R))" by iprover
    lemma imp_disjL: "((P|Q) --> R) = ((P-->R)&(Q-->R))" by iprover

    text {* These two are specialized, but @{text imp_disj_not1} is useful in @{text "Auth/Yahalom"}. *}
    lemma imp_disj_not1: "(P --> Q | R) = (~Q --> P --> R)" by blast
    lemma imp_disj_not2: "(P --> Q | R) = (~R --> P --> Q)" by blast

    lemma imp_disj1: "((P-->Q)|R) = (P--> Q|R)" by blast
    lemma imp_disj2: "(Q|(P-->R)) = (P--> Q|R)" by blast

    lemma de_Morgan_disj: "(~(P | Q)) = (~P & ~Q)" by iprover
    lemma de_Morgan_conj: "(~(P & Q)) = (~P | ~Q)" by blast
    lemma not_imp: "(~(P --> Q)) = (P & ~Q)" by blast
    lemma not_iff: "(P~=Q) = (P = (~Q))" by blast
    lemma disj_not1: "(~P | Q) = (P --> Q)" by blast
    lemma disj_not2: "(P | ~Q) = (Q --> P)"  -- {* changes orientation :-( *}
      by blast
    lemma imp_conv_disj: "(P --> Q) = ((~P) | Q)" by blast

    lemma iff_conv_conj_imp: "(P = Q) = ((P --> Q) & (Q --> P))" by iprover

    lemma cases_simp: "((P --> Q) & (~P --> Q)) = Q"
      -- {* Avoids duplication of subgoals after @{text split_if}, when the true and false *}
      -- {* cases boil down to the same thing. *}
      by blast

    lemma not_all: "(~ (! x. P(x))) = (? x.~P(x))" by blast
    lemma imp_all: "((! x. P x) --> Q) = (? x. P x --> Q)" by blast
    lemma not_ex: "(~ (? x. P(x))) = (! x.~P(x))" by iprover
    lemma imp_ex: "((? x. P x) --> Q) = (! x. P x --> Q)" by iprover

    lemma ex_disj_distrib: "(? x. P(x) | Q(x)) = ((? x. P(x)) | (? x. Q(x)))" by iprover
    lemma all_conj_distrib: "(!x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))" by iprover

    text {*
      \medskip The @{text "&"} congruence rule: not included by default!
      May slow rewrite proofs down by as much as 50\% *}

    lemma conj_cong:
        "(P = P') ==> (P' ==> (Q = Q')) ==> ((P & Q) = (P' & Q'))"
      by iprover

    lemma rev_conj_cong:
        "(Q = Q') ==> (Q' ==> (P = P')) ==> ((P & Q) = (P' & Q'))"
      by iprover

    text {* The @{text "|"} congruence rule: not included by default! *}

    lemma disj_cong:
        "(P = P') ==> (~P' ==> (Q = Q')) ==> ((P | Q) = (P' | Q'))"
      by blast

    lemma eq_sym_conv: "(x = y) = (y = x)"
      by iprover

    text {* \medskip if-then-else rules *}

    lemma if_True: "(if True then x else y) = x"
      by (unfold if_def) blast

    lemma if_False: "(if False then x else y) = y"
      by (unfold if_def) blast

    lemma if_P: "P ==> (if P then x else y) = x"
      by (unfold if_def) blast

    lemma if_not_P: "~P ==> (if P then x else y) = y"
      by (unfold if_def) blast

    lemma split_if: "P (if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))"
      apply (rule case_split [of Q])
       apply (simplesubst if_P)
        prefer 3 apply (simplesubst if_not_P, blast+)
      done

    lemma split_if_asm: "P (if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
    by (simplesubst split_if, blast)

    lemmas if_splits = split_if split_if_asm

    lemma if_def2: "(if Q then x else y) = ((Q --> x) & (~ Q --> y))"
      by (rule split_if)

    lemma if_cancel: "(if c then x else x) = x"
    by (simplesubst split_if, blast)

    lemma if_eq_cancel: "(if x = y then y else x) = x"
    by (simplesubst split_if, blast)

    lemma if_bool_eq_conj: "(if P then Q else R) = ((P-->Q) & (~P-->R))"
      -- {* This form is useful for expanding @{text if}s on the RIGHT of the @{text "==>"} symbol. *}
      by (rule split_if)

    lemma if_bool_eq_disj: "(if P then Q else R) = ((P&Q) | (~P&R))"
      -- {* And this form is useful for expanding @{text if}s on the LEFT. *}
      apply (simplesubst split_if, blast)
      done

    lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) iprover
    lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) iprover

    text {* \medskip let rules for simproc *}

    lemma Let_folded: "f x ≡ g x ==>  Let x f ≡ Let x g"
      by (unfold Let_def)

    lemma Let_unfold: "f x ≡ g ==>  Let x f ≡ g"
      by (unfold Let_def)

    text {*
      The following copy of the implication operator is useful for
      fine-tuning congruence rules.  It instructs the simplifier to simplify
      its premise.
    *}

    constdefs
      simp_implies :: "[prop, prop] => prop"  (infixr "=simp=>" 1)
      "simp_implies ≡ op ==>"

    lemma simp_impliesI:
      assumes PQ: "(PROP P ==> PROP Q)"
      shows "PROP P =simp=> PROP Q"
      apply (unfold simp_implies_def)
      apply (rule PQ)
      apply assumption
      done

    lemma simp_impliesE:
      assumes PQ:"PROP P =simp=> PROP Q"
      and P: "PROP P"
      and QR: "PROP Q ==> PROP R"
      shows "PROP R"
      apply (rule QR)
      apply (rule PQ [unfolded simp_implies_def])
      apply (rule P)
      done

    lemma simp_implies_cong:
      assumes PP' :"PROP P == PROP P'"
      and P'QQ': "PROP P' ==> (PROP Q == PROP Q')"
      shows "(PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')"
    proof (unfold simp_implies_def, rule equal_intr_rule)
      assume PQ: "PROP P ==> PROP Q"
      and P': "PROP P'"
      from PP' [symmetric] and P' have "PROP P"
        by (rule equal_elim_rule1)
      hence "PROP Q" by (rule PQ)
      with P'QQ' [OF P'] show "PROP Q'" by (rule equal_elim_rule1)
    next
      assume P'Q': "PROP P' ==> PROP Q'"
      and P: "PROP P"
      from PP' and P have P': "PROP P'" by (rule equal_elim_rule1)
      hence "PROP Q'" by (rule P'Q')
      with P'QQ' [OF P', symmetric] show "PROP Q"
        by (rule equal_elim_rule1)
    qed

    text {* \medskip Actual Installation of the Simplifier. *}

    use "simpdata.ML"
    setup "Simplifier.method_setup Splitter.split_modifiers" setup simpsetup
    setup Splitter.setup setup Clasimp.setup

    text {* \medskip Lucas Dixon's eqstep tactic. *}

    use "~~/src/Provers/eqsubst.ML";
    use "eqrule_HOL_data.ML";
    setup EQSubstTac.setup

    subsubsection {* Code generator setup *}

    types_code
      "bool"  ("bool")
    attach (term_of) {*
    fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
    *}
    attach (test) {*
    fun gen_bool i = one_of [false, true];
    *}

    consts_code
      "True"    ("true")
      "False"   ("false")
      "Not"     ("not")
      "op |"    ("(_ orelse/ _)")
      "op &"    ("(_ andalso/ _)")
      "HOL.If"      ("(if _/ then _/ else _)")

    ML {*
    local

    fun eq_codegen thy defs gr dep thyname b t =
        (case strip_comb t of
           (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
         | (Const ("op =", _), [t, u]) =>
              let
                val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
                val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
                val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
              in
                SOME (gr''', Codegen.parens
                  (Pretty.block [pt, Pretty.str " =", Pretty.brk 1, pu]))
              end
         | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
             thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
         | _ => NONE);

    in

    val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];

    end;
    *}

    setup eq_codegen_setup

    subsection {* Other simple lemmas *}

    declare disj_absorb [simp] conj_absorb [simp]

    lemma ex1_eq[iff]: "EX! x. x = t" "EX! x. t = x"
    by blast+

    theorem choice_eq: "(ALL x. EX! y. P x y) = (EX! f. ALL x. P x (f x))"
      apply (rule iffI)
      apply (rule_tac a = "%x. THE y. P x y" in ex1I)
      apply (fast dest!: theI')
      apply (fast intro: ext the1_equality [symmetric])
      apply (erule ex1E)
      apply (rule allI)
      apply (rule ex1I)
      apply (erule spec)
      apply (erule_tac x = "%z. if z = x then y else f z" in allE)
      apply (erule impE)
      apply (rule allI)
      apply (rule_tac P = "xa = x" in case_split_thm)
      apply (drule_tac [3] x = x in fun_cong, simp_all)
      done

    text{*Needs only HOL-lemmas:*}
    lemma mk_left_commute:
      assumes a: "!!x y z. f (f x y) z = f x (f y z)" and
              c: "!!x y. f x y = f y x"
      shows "f x (f y z) = f y (f x z)"
    by(rule trans[OF trans[OF c a] arg_cong[OF c, of "f y"]])

    subsection {* Generic cases and induction *}

    constdefs
      induct_forall :: "('a => bool) => bool"
      "induct_forall P == ∀x. P x"
      induct_implies :: "bool => bool => bool"
      "induct_implies A B == A --> B"
      induct_equal :: "'a => 'a => bool"
      "induct_equal x y == x = y"
      induct_conj :: "bool => bool => bool"
      "induct_conj A B == A & B"

    lemma induct_forall_eq: "(!!x. P x) == Trueprop (induct_forall (λx. P x))"
      by (simp only: atomize_all induct_forall_def)

    lemma induct_implies_eq: "(A ==> B) == Trueprop (induct_implies A B)"
      by (simp only: atomize_imp induct_implies_def)

    lemma induct_equal_eq: "(x == y) == Trueprop (induct_equal x y)"
      by (simp only: atomize_eq induct_equal_def)

    lemma induct_forall_conj: "induct_forall (λx. induct_conj (A x) (B x)) =
        induct_conj (induct_forall A) (induct_forall B)"
      by (unfold induct_forall_def induct_conj_def) iprover

    lemma induct_implies_conj: "induct_implies C (induct_conj A B) =
        induct_conj (induct_implies C A) (induct_implies C B)"
      by (unfold induct_implies_def induct_conj_def) iprover

    lemma induct_conj_curry: "(induct_conj A B ==> PROP C) == (A ==> B ==> PROP C)"
    proof
      assume r: "induct_conj A B ==> PROP C" and A B
      show "PROP C" by (rule r) (simp! add: induct_conj_def)
    next
      assume r: "A ==> B ==> PROP C" and "induct_conj A B"
      show "PROP C" by (rule r) (simp! add: induct_conj_def)+
    qed

    lemma induct_impliesI: "(A ==> B) ==> induct_implies A B"
      by (simp add: induct_implies_def)

    lemmas induct_atomize = atomize_conj induct_forall_eq induct_implies_eq induct_equal_eq
    lemmas induct_rulify1 [symmetric, standard] = induct_forall_eq induct_implies_eq induct_equal_eq
    lemmas induct_rulify2 = induct_forall_def induct_implies_def induct_equal_def induct_conj_def
    lemmas induct_conj = induct_forall_conj induct_implies_conj induct_conj_curry

    hide const induct_forall induct_implies induct_equal induct_conj

    text {* Method setup. *}

    ML {*
      structure InductMethod = InductMethodFun
      (struct
        val dest_concls = HOLogic.dest_concls
        val cases_default = thm "case_split"
        val local_impI = thm "induct_impliesI"
        val conjI = thm "conjI"
        val atomize = thms "induct_atomize"
        val rulify1 = thms "induct_rulify1"
        val rulify2 = thms "induct_rulify2"
        val localize = [Thm.symmetric (thm "induct_implies_def")]
      end);
    *}

    setup InductMethod.setup

    subsubsection{*Tags, for the ATP Linkup*}

    constdefs
      tag :: "bool => bool"
       "tag P == P"

    text{*These label the distinguished literals of introduction and elimination
    rules.*}

    lemma tagI: "P ==> tag P"
    by (simp add: tag_def)

    lemma tagD: "tag P ==> P"
    by (simp add: tag_def)

    text{*Applications of "tag" to True and False must go!*}

    lemma tag_True: "tag True = True"
    by (simp add: tag_def)

    lemma tag_False: "tag False = False"
    by (simp add: tag_def)

    end

### Primitive logic

#### Core syntax

#### Additional concrete syntax

#### Axioms and basic definitions

theorem subst:

      [| s = t; P s |] ==> P t

#### Generic algebraic operations

### Equality

lemma sym:

      s = t ==> t = s

lemmas ssubst:

      [| t = s; P s |] ==> P t

lemmas ssubst:

      [| t = s; P s |] ==> P t

lemma trans:

      [| r = s; s = t |] ==> r = t

lemma def_imp_eq:

      A == B ==> A = B

lemma box_equals:

      [| a = b; a = c; b = d |] ==> c = d

lemma forw_subst:

      [| a = b; P b |] ==> P a

lemma back_subst:

      [| P a; a = b |] ==> P b

### Congruence rules for application

lemma fun_cong:

      f = g ==> f x = g x

lemma arg_cong:

      x = y ==> f x = f y

lemma arg_cong2:

      [| a = b; c = d |] ==> f a c = f b d

lemma cong:

      [| f = g; x = y |] ==> f x = g y

### Equality of booleans -- iff

lemma iffI:

      [| P ==> Q; Q ==> P |] ==> P = Q

lemma iffD2:

      [| P = Q; Q |] ==> P

lemma rev_iffD2:

      [| Q; P = Q |] ==> P

lemmas iffD1:

      [| Q = P; Q |] ==> P

lemmas iffD1:

      [| Q = P; Q |] ==> P

lemmas rev_iffD1:

      [| Q; Q = P |] ==> P

lemmas rev_iffD1:

      [| Q; Q = P |] ==> P

lemma iffE:

      [| P = Q; [| P --> Q; Q --> P |] ==> R |] ==> R

### True

lemma TrueI:

      True

lemma eqTrueI:

      P ==> P = True

lemma eqTrueE:

      P = True ==> P

### Universal quantifier

lemma allI:

      (!!x. P x) ==> ∀x. P x

lemma spec:

      ∀x. P x ==> P x

lemma allE:

      [| ∀x. P x; P x ==> R |] ==> R

lemma all_dupE:

      [| ∀x. P x; [| P x; ∀x. P x |] ==> R |] ==> R

### False

lemma FalseE:

      False ==> P

lemma False_neq_True:

      False = True ==> P

### Negation

lemma notI:

      (P ==> False) ==> ¬ P

lemma False_not_True:

      False ≠ True

lemma True_not_False:

      True ≠ False

lemma notE:

      [| ¬ P; P |] ==> R

lemmas notI2:

      [| P ==> ¬ Pa; P ==> Pa |] ==> ¬ P

lemmas notI2:

      [| P ==> ¬ Pa; P ==> Pa |] ==> ¬ P

### Implication

lemma impE:

      [| P --> Q; P; Q ==> R |] ==> R

lemma rev_mp:

      [| P; P --> Q |] ==> Q

lemma contrapos_nn:

      [| ¬ Q; P ==> Q |] ==> ¬ P

lemma contrapos_pn:

      [| Q; P ==> ¬ Q |] ==> ¬ P

lemma not_sym:

      t ≠ s ==> s ≠ t

lemma rev_contrapos:

      [| P ==> Q; ¬ Q |] ==> ¬ P

### Existential quantifier

lemma exI:

      P x ==> ∃x. P x

lemma exE:

      [| ∃x. P x; !!x. P x ==> Q |] ==> Q

### Conjunction

lemma conjI:

      [| P; Q |] ==> P ∧ Q

lemma conjunct1:

      P ∧ Q ==> P

lemma conjunct2:

      P ∧ Q ==> Q

lemma conjE:

      [| P ∧ Q; [| P; Q |] ==> R |] ==> R

lemma context_conjI:

      [| P; P ==> Q |] ==> P ∧ Q

### Disjunction

lemma disjI1:

      P ==> P ∨ Q

lemma disjI2:

      Q ==> P ∨ Q

lemma disjE:

      [| P ∨ Q; P ==> R; Q ==> R |] ==> R

### Classical logic

lemma classical:

      (¬ P ==> P) ==> P

lemmas ccontr:

      (¬ P ==> False) ==> P

lemmas ccontr:

      (¬ P ==> False) ==> P

lemma rev_notE:

      [| P; ¬ R ==> ¬ P |] ==> R

lemma notnotD:

      ¬ ¬ P ==> P

lemma contrapos_pp:

      [| Q; ¬ P ==> ¬ Q |] ==> P

### Unique existence

lemma ex1I:

      [| P a; !!x. P x ==> x = a |] ==> ∃!x. P x

lemma ex_ex1I:

      [| ∃x. P x; !!x y. [| P x; P y |] ==> x = y |] ==> ∃!x. P x

lemma ex1E:

      [| ∃!x. P x; !!x. [| P x; ∀y. P y --> y = x |] ==> R |] ==> R

lemma ex1_implies_ex:

      ∃!x. P x ==> ∃x. P x

### THE: definite description operator

lemma the_equality:

      [| P a; !!x. P x ==> x = a |] ==> (THE x. P x) = a

lemma theI:

      [| P a; !!x. P x ==> x = a |] ==> P (THE x. P x)

lemma theI':

      ∃!x. P x ==> P (THE x. P x)

lemma theI2:

      [| P a; !!x. P x ==> x = a; !!x. P x ==> Q x |] ==> Q (THE x. P x)

lemma the1_equality:

      [| ∃!x. P x; P a |] ==> (THE x. P x) = a

lemma the_sym_eq_trivial:

      (THE y. x = y) = x

### Classical intro rules for disjunction and existential quantifiers

lemma disjCI:

      (¬ Q ==> P) ==> P ∨ Q

lemma excluded_middle:

      ¬ P ∨ P

lemma case_split_thm:

      [| P ==> Q; ¬ P ==> Q |] ==> Q

lemma impCE:

      [| P --> Q; ¬ P ==> R; Q ==> R |] ==> R

lemma impCE':

      [| P --> Q; Q ==> R; ¬ P ==> R |] ==> R

lemma iffCE:

      [| P = Q; [| P; Q |] ==> R; [| ¬ P; ¬ Q |] ==> R |] ==> R

lemma exCI:

      (∀x. ¬ P x ==> P a) ==> ∃x. P x

### Theory and package setup

theorems case_split:

      [| P ==> Q; ¬ P ==> Q |] ==> Q

theorems case_split:

      [| P ==> Q; ¬ P ==> Q |] ==> Q

#### Intuitionistic Reasoning

lemma impE':

      [| P --> Q; Q ==> R; P --> Q ==> P |] ==> R

lemma allE':

      [| ∀x. P x; [| P x; ∀x. P x |] ==> Q |] ==> Q

lemma notE':

      [| ¬ P; ¬ P ==> P |] ==> R

lemmas

      [| P ∨ Q; P ==> R; Q ==> R |] ==> R

      [| P = Q; [| P --> Q; Q --> P |] ==> R |] ==> R

      False ==> P

      [| P ∧ Q; [| P; Q |] ==> R |] ==> R

      [| ∃x. P x; !!x. P x ==> Q |] ==> Q

and

      [| P ==> Q; Q ==> P |] ==> P = Q

      [| P; Q |] ==> P ∧ Q

      (P ==> Q) ==> P --> Q

      True

      (P ==> False) ==> ¬ P

      (!!x. P x) ==> ∀x. P x

      t = t

and

      [| ∀x. P x; P x ==> R |] ==> R

      [| ¬ P; ¬ P ==> P |] ==> R

      [| P --> Q; Q ==> R; P --> Q ==> P |] ==> R

and

      P x ==> ∃x. P x

      Q ==> P ∨ Q

      P ==> P ∨ Q

lemmas

      [| P ∨ Q; P ==> R; Q ==> R |] ==> R

      [| P = Q; [| P --> Q; Q --> P |] ==> R |] ==> R

      False ==> P

      [| P ∧ Q; [| P; Q |] ==> R |] ==> R

      [| ∃x. P x; !!x. P x ==> Q |] ==> Q

and

      [| P ==> Q; Q ==> P |] ==> P = Q

      [| P; Q |] ==> P ∧ Q

      (P ==> Q) ==> P --> Q

      True

      (P ==> False) ==> ¬ P

      (!!x. P x) ==> ∀x. P x

      t = t

and

      [| ∀x. P x; P x ==> R |] ==> R

      [| ¬ P; ¬ P ==> P |] ==> R

      [| P --> Q; Q ==> R; P --> Q ==> P |] ==> R

and

      P x ==> ∃x. P x

      Q ==> P ∨ Q

      P ==> P ∨ Q

lemmas

      [| r = s; s = t |] ==> r = t

and

      s = t ==> t = s

      t ≠ s ==> s ≠ t

and

      [| Q = P; Q |] ==> P

      [| P = Q; Q |] ==> P

      [| P --> Q; P; Q ==> R |] ==> R

lemmas

      [| r = s; s = t |] ==> r = t

and

      s = t ==> t = s

      t ≠ s ==> s ≠ t

and

      [| Q = P; Q |] ==> P

      [| P = Q; Q |] ==> P

      [| P --> Q; P; Q ==> R |] ==> R

#### Atomizing meta-level connectives

lemma atomize_all:

      (!!x. P x) == ∀x. P x

lemma atomize_imp:

      (A ==> B) == A --> B

lemma atomize_not:

      (A ==> False) == ¬ A

lemma atomize_eq:

      (x == y) == x = y

lemma atomize_conj:

      (A && B) == A ∧ B

lemmas

      ∀x. P1 x == (!!x. P1 x)

      A1 --> B1 == (A1 ==> B1)

lemmas

      ∀x. P1 x == (!!x. P1 x)

      A1 --> B1 == (A1 ==> B1)

#### Classical Reasoner setup

## Classical Reasoner

theorem imp_elim:

      [| P --> Q; ¬ Z_ ==> P; Q ==> Z_ |] ==> Z_

theorem swap:

      [| ¬ Pa; ¬ P ==> Pa |] ==> P

theorem contrapos_np:

      [| ¬ Q; ¬ P ==> Q |] ==> P

lemmas

      (!!x. f x = g x) ==> f = g

and

      ∃!x. P x ==> ∃x. P x

lemmas

      (!!x. f x = g x) ==> f = g

and

      ∃!x. P x ==> ∃x. P x

theorem alt_ex1E:

      [| ∃!x. P x; !!x. [| P x; ∀y y'. P y ∧ P y' --> y = y' |] ==> R |] ==> R

#### Simplifier setup

lemma meta_eq_to_obj_eq:

      x == y ==> x = y

lemma eta_contract_eq:

      f = f

lemma not_not:

      (¬ ¬ P) = P

and Not_eq_iff:

      ((¬ P) = (¬ Q)) = (P = Q)

and simp_thms(3-34):

      (P ≠ Q) = (P = (¬ Q))

      (P ∨ ¬ P) = True

      (¬ P ∨ P) = True

      (x = x) = True

      (¬ True) = False

      (¬ False) = True

      (¬ P) ≠ P

      P ≠ (¬ P)

      (True = P) = P

      (P = True) = P

      (False = P) = (¬ P)

      (P = False) = (¬ P)

      (True --> P) = P

      (False --> P) = True

      (P --> True) = True

      (P --> P) = True

      (P --> False) = (¬ P)

      (P --> ¬ P) = (¬ P)

      (P ∧ True) = P

      (True ∧ P) = P

      (P ∧ False) = False

      (False ∧ P) = False

      (P ∧ P) = P

      (P ∧ P ∧ Q) = (P ∧ Q)

      (P ∧ ¬ P) = False

      (¬ P ∧ P) = False

      (P ∨ True) = True

      (True ∨ P) = True

      (P ∨ False) = P

      (False ∨ P) = P

      (P ∨ P) = P

      (P ∨ P ∨ Q) = (P ∨ Q)

and simp_thms(35-38):

      (∀x. P) = P

      (∃x. P) = P

      ∃x. x = t

      ∃x. t = x

and simp_thms(39-42):

      (∃x. x = t ∧ P x) = P t

      (∃x. t = x ∧ P x) = P t

      (∀x. x = t --> P x) = P t

      (∀x. t = x --> P x) = P t

lemma imp_cong:

      [| P = P'; P' ==> Q = Q' |] ==> (P --> Q) = (P' --> Q')

lemma ex_simps:

      (∃x. P x ∧ Q) = ((∃x. P x) ∧ Q)

      (∃x. P ∧ Q x) = (P ∧ (∃x. Q x))

      (∃x. P x ∨ Q) = ((∃x. P x) ∨ Q)

      (∃x. P ∨ Q x) = (P ∨ (∃x. Q x))

      (∃x. P x --> Q) = ((∀x. P x) --> Q)

      (∃x. P --> Q x) = (P --> (∃x. Q x))

lemma all_simps:

      (∀x. P x ∧ Q) = ((∀x. P x) ∧ Q)

      (∀x. P ∧ Q x) = (P ∧ (∀x. Q x))

      (∀x. P x ∨ Q) = ((∀x. P x) ∨ Q)

      (∀x. P ∨ Q x) = (P ∨ (∀x. Q x))

      (∀x. P x --> Q) = ((∃x. P x) --> Q)

      (∀x. P --> Q x) = (P --> (∀x. Q x))

lemma disj_absorb:

      (A ∨ A) = A

lemma disj_left_absorb:

      (A ∨ A ∨ B) = (A ∨ B)

lemma conj_absorb:

      (A ∧ A) = A

lemma conj_left_absorb:

      (A ∧ A ∧ B) = (A ∧ B)

lemma eq_commute:

      (a = b) = (b = a)

and eq_left_commute:

      (P = (Q = R)) = (Q = (P = R))

and eq_assoc:

      ((P = Q) = R) = (P = (Q = R))

lemma neq_commute:

      (a ≠ b) = (b ≠ a)

lemma conj_commute:

      (P ∧ Q) = (Q ∧ P)

and conj_left_commute:

      (P ∧ Q ∧ R) = (Q ∧ P ∧ R)

lemma conj_assoc:

      ((P ∧ Q) ∧ R) = (P ∧ Q ∧ R)

lemma disj_commute:

      (P ∨ Q) = (Q ∨ P)

and disj_left_commute:

      (P ∨ Q ∨ R) = (Q ∨ P ∨ R)

lemma disj_assoc:

      ((P ∨ Q) ∨ R) = (P ∨ Q ∨ R)

lemma conj_disj_distribL:

      (P ∧ (Q ∨ R)) = (P ∧ Q ∨ P ∧ R)

lemma conj_disj_distribR:

      ((P ∨ Q) ∧ R) = (P ∧ R ∨ Q ∧ R)

lemma disj_conj_distribL:

      (P ∨ Q ∧ R) = ((P ∨ Q) ∧ (P ∨ R))

lemma disj_conj_distribR:

      (P ∧ Q ∨ R) = ((P ∨ R) ∧ (Q ∨ R))

lemma imp_conjR:

      (P --> Q ∧ R) = ((P --> Q) ∧ (P --> R))

lemma imp_conjL:

      (P ∧ Q --> R) = (P --> Q --> R)

lemma imp_disjL:

      (P ∨ Q --> R) = ((P --> R) ∧ (Q --> R))

lemma imp_disj_not1:

      (P --> Q ∨ R) = (¬ Q --> P --> R)

lemma imp_disj_not2:

      (P --> Q ∨ R) = (¬ R --> P --> Q)

lemma imp_disj1:

      ((P --> Q) ∨ R) = (P --> Q ∨ R)

lemma imp_disj2:

      (Q ∨ (P --> R)) = (P --> Q ∨ R)

lemma de_Morgan_disj:

      (¬ (P ∨ Q)) = (¬ P ∧ ¬ Q)

lemma de_Morgan_conj:

      (¬ (P ∧ Q)) = (¬ P ∨ ¬ Q)

lemma not_imp:

      (¬ (P --> Q)) = (P ∧ ¬ Q)

lemma not_iff:

      (P ≠ Q) = (P = (¬ Q))

lemma disj_not1:

      (¬ P ∨ Q) = (P --> Q)

lemma disj_not2:

      (P ∨ ¬ Q) = (Q --> P)

lemma imp_conv_disj:

      (P --> Q) = (¬ P ∨ Q)

lemma iff_conv_conj_imp:

      (P = Q) = ((P --> Q) ∧ (Q --> P))

lemma cases_simp:

      ((P --> Q) ∧ (¬ P --> Q)) = Q

lemma not_all:

      (¬ (∀x. P x)) = (∃x. ¬ P x)

lemma imp_all:

      ((∀x. P x) --> Q) = (∃x. P x --> Q)

lemma not_ex:

      (¬ (∃x. P x)) = (∀x. ¬ P x)

lemma imp_ex:

      ((∃x. P x) --> Q) = (∀x. P x --> Q)

lemma ex_disj_distrib:

      (∃x. P x ∨ Q x) = ((∃x. P x) ∨ (∃x. Q x))

lemma all_conj_distrib:

      (∀x. P x ∧ Q x) = ((∀x. P x) ∧ (∀x. Q x))

lemma conj_cong:

      [| P = P'; P' ==> Q = Q' |] ==> (P ∧ Q) = (P' ∧ Q')

lemma rev_conj_cong:

      [| Q = Q'; Q' ==> P = P' |] ==> (P ∧ Q) = (P' ∧ Q')

lemma disj_cong:

      [| P = P'; ¬ P' ==> Q = Q' |] ==> (P ∨ Q) = (P' ∨ Q')

lemma eq_sym_conv:

      (x = y) = (y = x)

lemma if_True:

      (if True then x else y) = x

lemma if_False:

      (if False then x else y) = y

lemma if_P:

      P ==> (if P then x else y) = x

lemma if_not_P:

      ¬ P ==> (if P then x else y) = y

lemma split_if:

      P (if Q then x else y) = ((Q --> P x) ∧ (¬ Q --> P y))

lemma split_if_asm:

      P (if Q then x else y) = (¬ (Q ∧ ¬ P x ∨ ¬ Q ∧ ¬ P y))

lemmas if_splits:

      P (if Q then x else y) = ((Q --> P x) ∧ (¬ Q --> P y))

      P (if Q then x else y) = (¬ (Q ∧ ¬ P x ∨ ¬ Q ∧ ¬ P y))

lemmas if_splits:

      P (if Q then x else y) = ((Q --> P x) ∧ (¬ Q --> P y))

      P (if Q then x else y) = (¬ (Q ∧ ¬ P x ∨ ¬ Q ∧ ¬ P y))

lemma if_def2:

      (if Q then x else y) = ((Q --> x) ∧ (¬ Q --> y))

lemma if_cancel:

      (if c then x else x) = x

lemma if_eq_cancel:

      (if x = y then y else x) = x

lemma if_bool_eq_conj:

      (if P then Q else R) = ((P --> Q) ∧ (¬ P --> R))

lemma if_bool_eq_disj:

      (if P then Q else R) = (P ∧ Q ∨ ¬ P ∧ R)

lemma Eq_TrueI:

      P ==> P == True

lemma Eq_FalseI:

      ¬ P ==> P == False

lemma Let_folded:

      f x == g x ==> Let x f == Let x g

lemma Let_unfold:

      f x == g ==> Let x f == g

lemma simp_impliesI:

      (PROP P ==> PROP Q) ==> PROP P =simp=> PROP Q

lemma simp_impliesE:

      [| PROP P =simp=> PROP Q; PROP P; PROP Q ==> PROP R |] ==> PROP R

lemma simp_implies_cong:

      [| PROP P == PROP P'; PROP P' ==> PROP Q == PROP Q' |]
      ==> (PROP P =simp=> PROP Q) == (PROP P' =simp=> PROP Q')

theorem if_cong:

      [| b = c; c ==> x = u; ¬ c ==> y = v |]
      ==> (if b then x else y) = (if c then u else v)

theorem if_weak_cong:

      b = c ==> (if b then x else y) = (if c then x else y)

theorem let_weak_cong:

      a = b ==> Let a t = Let b t

theorem eq_cong2:

      u = u' ==> (t == u) == t == u'

theorem if_distrib:

      f (if c then x else y) = (if c then f x else f y)

theorem expand_case:

      [| P ==> Q True; ¬ P ==> Q False |] ==> Q P

theorem restrict_to_left:

      x = y ==> (x = z) = (y = z)

#### Code generator setup

### Other simple lemmas

lemma ex1_eq:

      ∃!x. x = t

      ∃!x. t = x

theorem choice_eq:

      (∀x. ∃!y. P x y) = (∃!f. ∀x. P x (f x))

lemma mk_left_commute:

      [| !!x y z. f (f x y) z = f x (f y z); !!x y. f x y = f y x |]
      ==> f x (f y z) = f y (f x z)

### Generic cases and induction

lemma induct_forall_eq:

      (!!x. P x) == induct_forall P

lemma induct_implies_eq:

      (A ==> B) == induct_implies A B

lemma induct_equal_eq:

      (x == y) == induct_equal x y

lemma induct_forall_conj:

      induct_forall (%x. induct_conj (A x) (B x)) =
      induct_conj (induct_forall A) (induct_forall B)

lemma induct_implies_conj:

      induct_implies C (induct_conj A B) =
      induct_conj (induct_implies C A) (induct_implies C B)

lemma induct_conj_curry:

      (induct_conj A B ==> PROP C) == ([| A; B |] ==> PROP C)

lemma induct_impliesI:

      (A ==> B) ==> induct_implies A B

lemmas induct_atomize:

      (A && B) == A ∧ B

      (!!x. P x) == induct_forall P

      (A ==> B) == induct_implies A B

      (x == y) == induct_equal x y

lemmas induct_atomize:

      (A && B) == A ∧ B

      (!!x. P x) == induct_forall P

      (A ==> B) == induct_implies A B

      (x == y) == induct_equal x y

lemmas induct_rulify1:

      induct_forall P == (!!x. P x)

      induct_implies A B == (A ==> B)

      induct_equal x y == x == y

lemmas induct_rulify1:

      induct_forall P == (!!x. P x)

      induct_implies A B == (A ==> B)

      induct_equal x y == x == y

lemmas induct_rulify2:

      induct_forall P == ∀x. P x

      induct_implies A B == A --> B

      induct_equal x y == x = y

      induct_conj A B == A ∧ B

lemmas induct_rulify2:

      induct_forall P == ∀x. P x

      induct_implies A B == A --> B

      induct_equal x y == x = y

      induct_conj A B == A ∧ B

lemmas induct_conj:

      induct_forall (%x. induct_conj (A x) (B x)) =
      induct_conj (induct_forall A) (induct_forall B)

      induct_implies C (induct_conj A B) =
      induct_conj (induct_implies C A) (induct_implies C B)

      (induct_conj A B ==> PROP C) == ([| A; B |] ==> PROP C)

lemmas induct_conj:

      induct_forall (%x. induct_conj (A x) (B x)) =
      induct_conj (induct_forall A) (induct_forall B)

      induct_implies C (induct_conj A B) =
      induct_conj (induct_implies C A) (induct_implies C B)

      (induct_conj A B ==> PROP C) == ([| A; B |] ==> PROP C)

#### Tags, for the ATP Linkup

lemma tagI:

      P ==> tag P

lemma tagD:

      tag P ==> P

lemma tag_True:

      tag True = True

lemma tag_False:

      tag False = False