<commit_before>(*  Title:      HOL/Meson.thy
    Author:     <NAME>, Cambridge University Computer Laboratory
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Copyright   2001  University of Cambridge
*)

header {* MESON Proof Method *}

theory Meson
imports Datatype
begin

subsection {* Negation Normal Form *}

text {* de Morgan laws *}

lemma not_conjD: "~(P&Q) ==> ~P | ~Q"
  and not_disjD: "~(P|Q) ==> ~P & ~Q"
  and not_notD: "~~P ==> P"
  and not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
  and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
  by fast+

text {* Removal of @{text "-->"} and @{text "<->"} (positive and
negative occurrences) *}

lemma imp_to_disjD: "P-->Q ==> ~P | Q"
  and not_impD: "~(P-->Q) ==> P & ~Q"
  and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
  and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
  and not_refl_disj_D: "x ~= x | P ==> P"
  by fast+


subsection {* Pulling out the existential quantifiers *}
<commit_msg>moved meson up the dependency chain<commit_after>(*  Title:      HOL/Meson.thy
    Author:     <NAME>, Cambridge University Computer Laboratory
    Author:     <NAME>, TU Muenchen
    Author:     <NAME>, TU Muenchen
    Copyright   2001  University of Cambridge
*)

header {* MESON Proof Method *}

theory Meson
imports Nat
begin

subsection {* Negation Normal Form *}

text {* de Morgan laws *}

lemma not_conjD: "~(P&Q) ==> ~P | ~Q"
  and not_disjD: "~(P|Q) ==> ~P & ~Q"
  and not_notD: "~~P ==> P"
  and not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
  and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
  by fast+

text {* Removal of @{text "-->"} and @{text "<->"} (positive and
negative occurrences) *}

lemma imp_to_disjD: "P-->Q ==> ~P | Q"
  and not_impD: "~(P-->Q) ==> P & ~Q"
  and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
  and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
  and not_refl_disj_D: "x ~= x | P ==> P"
  by fast+


subsection {* Pulling out the existential quantifiers *}

{'fraction_non_alphanumeric': 0.21392808375056896, 'fraction_numerical': 0.0036413290851160674, 'mean_word_length': 3.162878787878788, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 45, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5350154', 'n_tokens_mistral': 939, 'n_tokens_neox': 925, 'n_words': 263}