Quelle  FOL.thy

(*  Title:      FOL/FOL.thy
  Author: Lawrence C Paulson and Markus Wenzel
*)

section ‹Classical first-order logic›

theory FOL
  imports IFOL
  keywords "print_claset" "print_induct_rules" :: diag
begin

ML_file ‹~~/src/Provers/classical.ML›
ML_file ‹~~/src/Provers/blast.ML›
ML_file ‹~~/src/Provers/clasimp.ML›


subsection ‹The classical axiom›

axiomatization where
  classical: ‹(¬ P ==> P) ==> P›


subsection ‹Lemmas and proof tools›

lemma ccontr: ‹(¬ P ==> False) ==> P›
  by (erule FalseE [THEN classical])


subsubsection ‹Classical introduction rules for ‹∨› and ‹∃›\›

lemma disjCI: ‹(¬ Q ==> P) ==> P ∨ Q›
  apply (rule classical)
  apply (assumption | erule meta_mp | rule disjI1 notI)+
  apply (erule notE disjI2)+
  done

text ‹Introduction rule involving only ‹∃›\›
lemma ex_classical:
  assumes r: ‹¬ (∃x. P(x)) ==> P(a)›
  shows ‹∃x. P(x)›
  apply (rule classical)
  apply (rule exI, erule r)
  done

text ‹Version of above, simplifying ‹¬∃› to ‹∀¬›.›
lemma exCI:
  assumes r: ‹∀x. ¬ P(x) ==> P(a)›
  shows ‹∃x. P(x)›
  apply (rule ex_classical)
  apply (rule notI [THEN allI, THEN r])
  apply (erule notE)
  apply (erule exI)
  done

lemma excluded_middle: ‹¬ P ∨ P›
  apply (rule disjCI)
  apply assumption
  done

lemma case_split [case_names True False]:
  assumes r1: ‹P ==> Q›
    and r2: ‹¬ P ==> Q›
  shows ‹Q›
  apply (rule excluded_middle [THEN disjE])
  apply (erule r2)
  apply (erule r1)
  done

ML ‹
  fun case_tac ctxt a fixes =
  Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split};
 ›

method_setup case_tac = ‹
  Args.goal_spec -- Scan.lift (Parse.embedded_inner_syntax -- Parse.for_fixes) >>
  (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
 ›


subsection ‹Special elimination rules›

text ‹Classical implies (‹⟶›) elimination.›
lemma impCE:
  assumes major: ‹P ⟶ Q›
    and r1: ‹¬ P ==> R›
    and r2: ‹Q ==> R›
  shows ‹R›
  apply (rule excluded_middle [THEN disjE])
   apply (erule r1)
  apply (rule r2)
  apply (erule major [THEN mp])
  done

text ‹
  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 r1: ‹Q ==> R›
    and r2: ‹¬ P ==> R›
  shows ‹R›
  apply (rule excluded_middle [THEN disjE])
   apply (erule r2)
  apply (rule r1)
  apply (erule major [THEN mp])
  done

text ‹Double negation law.›
lemma notnotD: ‹¬ ¬ P ==> P›
  apply (rule classical)
  apply (erule notE)
  apply assumption
  done

lemma contrapos2:  ‹[Q; ¬ P ==> ¬ Q] ==> P›
  apply (rule classical)
  apply (drule (1) meta_mp)
  apply (erule (1) notE)
  done


subsubsection ‹Tactics for implication and contradiction›

text ‹
  Classical ‹⟷› elimination. Proof substitutes ‹P = Q› in
  ‹¬ P ==> ¬ Q› and ‹P ==> Q›.
 ›
lemma iffCE:
  assumes major: ‹P ⟷ Q›
    and r1: ‹[P; Q] ==> R›
    and r2: ‹[¬ P; ¬ Q] ==> R›
  shows ‹R›
  apply (rule major [unfolded iff_def, THEN conjE])
  apply (elim impCE)
     apply (erule (1) r2)
    apply (erule (1) notE)+
  apply (erule (1) r1)
  done


(*Better for fast_tac: needs no quantifier duplication!*)
lemma alt_ex1E:
  assumes major: ‹∃! x. P(x)›
    and r: ‹∧x. [P(x); ∀y y'. P(y) ∧ P(y') ⟶ y = y'] ==> R›
  shows ‹R›
  using major
proof (rule ex1E)
  fix x
  assume * : ‹∀y. P(y) ⟶ y = x›
  assume ‹P(x)›
  then show ‹R›
  proof (rule r)
    {
      fix y y'
      assume ‹P(y)› and ‹P(y')›
      with * have ‹x = y› and ‹x = y'›
        by - (tactic "IntPr.fast_tac 🍋 1")+
      then have ‹y = y'› by (rule subst)
    } note r' = this
    show ‹∀y y'. P(y) ∧ P(y') ⟶ y = y'›
      by (intro strip, elim conjE) (rule r')
  qed
qed

lemma imp_elim: ‹P ⟶ Q ==> (¬ R ==> P) ==> (Q ==> R) ==> R›
  by (rule classical) iprover

lemma swap: ‹¬ P ==> (¬ R ==> P) ==> R›
  by (rule classical) iprover


section ‹Classical Reasoner›

ML ‹
 structure Cla = Classical
 (
  val imp_elim = @{thm imp_elim}
  val not_elim = @{thm notE}
  val swap = @{thm swap}
  val classical = @{thm classical}
  val sizef = size_of_thm
  val hyp_subst_tacs = [hyp_subst_tac]
 );
 
 structure Basic_Classical: BASIC_CLASSICAL = Cla;
 open Basic_Classical;
 ›

(*Propositional rules*)
lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
  and [elim!] = conjE disjE impCE FalseE iffCE
ML ‹val prop_cs = claset_of 🍋›

(*Quantifier rules*)
lemmas [intro!] = allI ex_ex1I
  and [intro] = exI
  and [elim!] = exE alt_ex1E
  and [elim] = allE
ML ‹val FOL_cs = claset_of 🍋›

ML ‹
  structure Blast = Blast
  (
  structure Classical = Cla
  val Trueprop_const = dest_Const 🍋‹Trueprop›
    val equality_name = 🍋‹eq›
    val not_name = 🍋‹Not›
    val notE = @{thm notE}
    val ccontr = @{thm ccontr}
    val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
  );
  val blast_tac = Blast.blast_tac;
›


lemma ex1_functional: ‹[∃! z. P(a,z); P(a,b); P(a,c)] ==> b = c›
  by blast

text ‹Elimination of ‹True› from assumptions:›
lemma True_implies_equals: ‹(True ==> PROP P) ≡ PROP P›
proof
  assume ‹True ==> PROP P›
  from this and TrueI show ‹PROP P› .
next
  assume ‹PROP P›
  then show ‹PROP P› .
qed

lemma uncurry: ‹P ⟶ Q ⟶ R ==> P ∧ Q ⟶ R›
  by blast

lemma iff_allI: ‹(∧x. P(x) ⟷ Q(x)) ==> (∀x. P(x)) ⟷ (∀x. Q(x))›
  by blast

lemma iff_exI: ‹(∧x. P(x) ⟷ Q(x)) ==> (∃x. P(x)) ⟷ (∃x. Q(x))›
  by blast

lemma all_comm: ‹(∀x y. P(x,y)) ⟷ (∀y x. P(x,y))›
  by blast

lemma ex_comm: ‹(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))›
  by blast



subsection ‹Classical simplification rules›

text ‹
  Avoids duplication of subgoals after ‹expand_if›,
  false cases boil down to the same thing.
›

lemma cases_simp: ‹(P ⟶ Q) ∧ (¬ P ⟶ Q) ⟷ Q›
  by blast


subsubsection ‹Miniscoping: pushing quantifiers in›

text ‹
  We do NOT distribute of ‹∀› o
  ‹∃› over ‹∨›.

  Baaz and Leitsch, On Skolemization and Proof Complexity (1994) show that
  this step can increase proof length!
›

text ‹Existential miniscoping.›
lemma int_ex_simps:
  ‹∧P Q. (∃x. P(x) ∧ Q) ⟷ (∃x. P(x)) ∧ Q›
  ‹∧P Q. (∃x. P ∧ Q(x)) ⟷ P ∧ (∃x. Q(x))›
  ‹∧P Q. (∃x. P(x) ∨ Q) ⟷ (∃x. P(x)) ∨ Q›
  ‹∧P Q. (∃x. P ∨ Q(x)) ⟷ P ∨ (∃x. Q(x))›
  by iprover+

text ‹Classical rules.›
lemma cla_ex_simps:
  ‹∧P Q. (∃x. P(x) ⟶ Q) ⟷ (∀x. P(x)) ⟶ Q›
  ‹∧P Q. (∃x. P ⟶ Q(x)) ⟷ P ⟶ (∃x. Q(x))›
  by blast+

lemmas ex_simps = int_ex_simps cla_ex_simps

text ‹Universal miniscoping.›
lemma int_all_simps:
  ‹∧P Q. (∀x. P(x) ∧ Q) ⟷ (∀x. P(x)) ∧ Q›
  ‹∧P Q. (∀x. P ∧ Q(x)) ⟷ P ∧ (∀x. Q(x))›
  ‹∧P Q. (∀x. P(x) ⟶ Q) ⟷ (∃ x. P(x)) ⟶ Q›
  ‹∧P Q. (∀x. P ⟶ Q(x)) ⟷ P ⟶ (∀x. Q(x))›
  by iprover+

text ‹Classical rules.›
lemma cla_all_simps:
  ‹∧P Q. (∀x. P(x) ∨ Q) ⟷ (∀x. P(x)) ∨ Q›
  ‹∧P Q. (∀x. P ∨ Q(x)) ⟷ P ∨ (∀x. Q(x))›
  by blast+

lemmas all_simps = int_all_simps cla_all_simps


subsubsection ‹Named rewrite rules proved for IFOL›

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_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 not_all: ‹(¬ (∀x. P(x))) ⟷ (∃x. ¬ P(x))› by blast
lemma imp_all: ‹((∀x. P(x)) ⟶ Q) ⟷ (∃x. P(x) ⟶ Q)› by blast


lemmas meta_simps =
  triv_forall_equality  🍋 ‹prunes params›
  True_implies_equals  🍋 ‹prune asms ‹True›\
lemmas IFOL_simps =
  refl [THEN P_iff_T] conj_simps disj_simps not_simps
  imp_simps iff_simps quant_simps

lemma notFalseI: ‹¬ False› by iprover

lemma cla_simps_misc:
  ‹¬ (P ∧ Q) ⟷ ¬ P ∨ ¬ Q›
  ‹P ∨ ¬ P›
  ‹¬ P ∨ P›
  ‹¬ ¬ P ⟷ P›
  ‹(¬ P ⟶ P) ⟷ P›
  ‹(¬ P ⟷ ¬ Q) ⟷ (P ⟷ Q)› by blast+

lemmas cla_simps =
  de_Morgan_conj de_Morgan_disj imp_disj1 imp_disj2
  not_imp not_all not_ex cases_simp cla_simps_misc


ML_file ‹simpdata.ML›

simproc_setup defined_Ex (‹∃x. P(x)›) = ‹K Quantifier1.rearrange_Ex›
simproc_setup defined_All (‹∀x. P(x)›) = ‹K Quantifier1.rearrange_All›
simproc_setup defined_all("∧x. PROP P(x)") = ‹K Quantifier1.rearrange_all›

ML ‹
(*intuitionistic simprules only*)
val IFOL_ss =
  put_simpset FOL_basic_ss 🍋
  |> Simplifier.add_simps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all}
  |> Simplifier.add_proc 🍋‹defined_All›
  |> Simplifier.add_proc 🍋‹defined_Ex›
  |> Simplifier.add_cong @{thm imp_cong}
  |> simpset_of;

(*classical simprules too*)
val FOL_ss =
  put_simpset IFOL_ss 🍋
  |> Simplifier.add_simps @{thms cla_simps cla_ex_simps cla_all_simps}
  |> simpset_of;
›

setup ‹
  map_theory_simpset (put_simpset FOL_ss) #>
  Simplifier.method_setup Splitter.split_modifiers
 ›

ML_file ‹~~/src/Tools/eqsubst.ML›


subsection ‹Other simple lemmas›

lemma [simp]: ‹((P ⟶ R) ⟷ (Q ⟶ R)) ⟷ ((P ⟷ Q) ∨ R)›
  by blast

lemma [simp]: ‹((P ⟶ Q) ⟷ (P ⟶ R)) ⟷ (P ⟶ (Q ⟷ R))›
  by blast

lemma not_disj_iff_imp: ‹¬ P ∨ Q ⟷ (P ⟶ Q)›
  by blast


subsubsection ‹Monotonicity of implications›

lemma conj_mono: ‹[P1 ⟶ Q1; P2 ⟶ Q2] ==> (P1 ∧ P2) ⟶ (Q1 ∧ Q2)›
  by fast (*or (IntPr.fast_tac 1)*)

lemma disj_mono: ‹[P1 ⟶ Q1; P2 ⟶ Q2] ==> (P1 ∨ P2) ⟶ (Q1 ∨ Q2)›
  by fast (*or (IntPr.fast_tac 1)*)

lemma imp_mono: ‹[Q1 ⟶ P1; P2 ⟶ Q2] ==> (P1 ⟶ P2) ⟶ (Q1 ⟶ Q2)›
  by fast (*or (IntPr.fast_tac 1)*)

lemma imp_refl: ‹P ⟶ P›
  by (rule impI)

text ‹The quantifier monotonicity rules are also intuitionistically valid.›
lemma ex_mono: ‹(∧x. P(x) ⟶ Q(x)) ==> (∃x. P(x)) ⟶ (∃x. Q(x))›
  by blast

lemma all_mono: ‹(∧x. P(x) ⟶ Q(x)) ==> (∀x. P(x)) ⟶ (∀x. Q(x))›
  by blast


subsection ‹Proof by cases and induction›

text ‹Proper handling of non-atomic rule statements.›

context
begin

qualified definition ‹induct_forall(P) ≡ ∀x. P(x)›
qualified definition ‹induct_implies(A, B) ≡ A ⟶ B›
qualified definition ‹induct_equal(x, y) ≡ x = y›
qualified definition ‹induct_conj(A, B) ≡ A ∧ B›

lemma induct_forall_eq: ‹(∧x. P(x)) ≡ Trueprop(induct_forall(λx. P(x)))›
  unfolding atomize_all induct_forall_def .

lemma induct_implies_eq: ‹(A ==> B) ≡ Trueprop(induct_implies(A, B))›
  unfolding atomize_imp induct_implies_def .

lemma induct_equal_eq: ‹(x ≡ y) ≡ Trueprop(induct_equal(x, y))›
  unfolding atomize_eq induct_equal_def .

lemma induct_conj_eq: ‹(A &&& B) ≡ Trueprop(induct_conj(A, B))›
  unfolding atomize_conj induct_conj_def .

lemmas induct_atomize = induct_forall_eq induct_implies_eq induct_equal_eq induct_conj_eq
lemmas induct_rulify [symmetric] = induct_atomize
lemmas induct_rulify_fallback =
  induct_forall_def induct_implies_def induct_equal_def induct_conj_def

text ‹Method setup.›

ML_file ‹~~/src/Tools/induct.ML›
ML ‹
  structure Induct = Induct
  (
  val cases_default = @{thm case_split}
  val atomize = @{thms induct_atomize}
  val rulify = @{thms induct_rulify}
  val rulify_fallback = @{thms induct_rulify_fallback}
  val equal_def = @{thm induct_equal_def}
  fun dest_def _ = NONE
  fun trivial_tac _ _ = no_tac
  );
 ›

declare case_split [cases type: o]

end

ML_file ‹~~/src/Tools/case_product.ML›


hide_const (open) eq

end