<commit_before>(*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
    Author:     <NAME>, T<NAME>
    Copyright   2009

Refute examples adapted to Nitpick.
*)

header {* Refute Examples Adapted to Nitpick *}

theory Refute_Nits
imports Main
begin

lemma "P \<and> Q"
apply (rule conjI)
nitpick [expect = genuine] 1
nitpick [expect = genuine] 2
nitpick [expect = genuine]
nitpick [card = 5, expect = genuine]
nitpick [sat_solver = MiniSat, expect = genuine] 2
oops

subsection {* Examples and Test Cases *}

subsubsection {* Propositional logic *}

lemma "True"
nitpick [expect = none]
apply auto
done

lemma "False"
nitpick [expect = genuine]
oops

lemma "P"
nitpick [expect = genuine]
oops

lemma "\<not> P"
nitpick [expect = genuine]
oops

lemma "P \<and> Q"
nitpick [expect = genuine]<commit_msg>use SAT solver that's available everywhere for this example<commit_after>(*  Title:      HOL/Nitpick_Examples/Refute_Nits.thy
    Author:     <NAME>, T<NAME>
    Copyright   2009

Refute examples adapted to Nitpick.
*)

header {* Refute Examples Adapted to Nitpick *}

theory Refute_Nits
imports Main
begin

lemma "P \<and> Q"
apply (rule conjI)
nitpick [expect = genuine] 1
nitpick [expect = genuine] 2
nitpick [expect = genuine]
nitpick [card = 5, expect = genuine]
nitpick [sat_solver = SAT4J, expect = genuine] 2
oops

subsection {* Examples and Test Cases *}

subsubsection {* Propositional logic *}

lemma "True"
nitpick [expect = none]
apply auto
done

lemma "False"
nitpick [expect = genuine]
oops

lemma "P"
nitpick [expect = genuine]
oops

lemma "\<not> P"
nitpick [expect = genuine]
oops

lemma "P \<and> Q"
nitpick [expect = genuine]
{'fraction_non_alphanumeric': 0.106318347509113, 'fraction_numerical': 0.010328068043742407, 'mean_word_length': 4.261980830670926, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, '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': '2259618', 'n_tokens_mistral': 595, 'n_tokens_neox': 567, 'n_words': 199}