<commit_before>(*  Title:      HOL/Isar_examples/BasicLogic.thy
    ID:         $Id$
    Author:     <NAME>, TU Muenchen

Basic propositional and quantifier reasoning.
*)

theory BasicLogic = Main:;


text {* Just a few tiny examples to get an idea of how Isabelle/Isar
  proof documents may look like. *};

lemma I: "A --> A";
proof;
  assume A;
  show A; .;
qed;

lemma K: "A --> B --> A";
proof;
  assume A;
  show "B --> A";
  proof;
    show A; .;
  qed;
qed;

lemma K': "A --> B --> A";
proof intro;
  assume A;
  show A; .;
qed;

lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
proof;
  assume "A --> B --> C";
  show "(A --> B) --> A --> C";
  proof;
    assume "A --> B";
    show "A --> C";
    proof;<commit_msg>tuned K;<commit_after>(*  Title:      HOL/Isar_examples/BasicLogic.thy
    ID:         $Id$
    Author:     <NAME>, TU Muenchen

Basic propositional and quantifier reasoning.
*)

theory BasicLogic = Main:;


text {* Just a few tiny examples to get an idea of how Isabelle/Isar
  proof documents may look like. *};

lemma I: "A --> A";
proof;
  assume A;
  show A; .;
qed;


lemma K: "A --> B --> A";
proof;
  assume A;
  show "B --> A";
  proof;
    show A; .;
  qed;
qed;

lemma K': "A --> B --> A";
proof;
  assume A;
  thus "B --> A"; ..;
qed;

lemma K'': "A --> B --> A";
proof intro;
  assume A;
  show A; .;
qed;

lemma K''': "A --> B --> A";
  by intro;


lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
proof;
  assume "A --> B --> C";
  show "(A --> B) --> A --> C";
  proof;
    assume "A --> B";
    show "A --> C";
    proof;
{'fraction_non_alphanumeric': 0.21183206106870228, 'fraction_numerical': 0.0, 'mean_word_length': 1.9075785582255083, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 48, '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': '4806726', 'n_tokens_mistral': 630, 'n_tokens_neox': 629, 'n_words': 219}