src/FOL/ex/Intro.thy
 author wenzelm Thu Jan 03 22:19:19 2019 +0100 (8 months ago) changeset 69590 e65314985426 parent 62020 5d208fd2507d permissions -rw-r--r--
isabelle update_inner_syntax_cartouches;
```     1 (*  Title:      FOL/ex/Intro.thy
```
```     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     3     Copyright   1992  University of Cambridge
```
```     4
```
```     5 Derives some inference rules, illustrating the use of definitions.
```
```     6 *)
```
```     7
```
```     8 section \<open>Examples for the manual ``Introduction to Isabelle''\<close>
```
```     9
```
```    10 theory Intro
```
```    11 imports FOL
```
```    12 begin
```
```    13
```
```    14 subsubsection \<open>Some simple backward proofs\<close>
```
```    15
```
```    16 lemma mythm: \<open>P \<or> P \<longrightarrow> P\<close>
```
```    17 apply (rule impI)
```
```    18 apply (rule disjE)
```
```    19 prefer 3 apply (assumption)
```
```    20 prefer 2 apply (assumption)
```
```    21 apply assumption
```
```    22 done
```
```    23
```
```    24 lemma \<open>(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)\<close>
```
```    25 apply (rule impI)
```
```    26 apply (erule disjE)
```
```    27 apply (drule conjunct1)
```
```    28 apply (rule disjI1)
```
```    29 apply (rule_tac  disjI2)
```
```    30 apply assumption+
```
```    31 done
```
```    32
```
```    33 text \<open>Correct version, delaying use of \<open>spec\<close> until last.\<close>
```
```    34 lemma \<open>(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))\<close>
```
```    35 apply (rule impI)
```
```    36 apply (rule allI)
```
```    37 apply (rule allI)
```
```    38 apply (drule spec)
```
```    39 apply (drule spec)
```
```    40 apply assumption
```
```    41 done
```
```    42
```
```    43
```
```    44 subsubsection \<open>Demonstration of \<open>fast\<close>\<close>
```
```    45
```
```    46 lemma \<open>(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))\<close>
```
```    47 apply fast
```
```    48 done
```
```    49
```
```    50
```
```    51 lemma \<open>\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))\<close>
```
```    52 apply fast
```
```    53 done
```
```    54
```
```    55
```
```    56 subsubsection \<open>Derivation of conjunction elimination rule\<close>
```
```    57
```
```    58 lemma
```
```    59   assumes major: \<open>P \<and> Q\<close>
```
```    60     and minor: \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R\<close>
```
```    61   shows \<open>R\<close>
```
```    62 apply (rule minor)
```
```    63 apply (rule major [THEN conjunct1])
```
```    64 apply (rule major [THEN conjunct2])
```
```    65 done
```
```    66
```
```    67
```
```    68 subsection \<open>Derived rules involving definitions\<close>
```
```    69
```
```    70 text \<open>Derivation of negation introduction\<close>
```
```    71
```
```    72 lemma
```
```    73   assumes \<open>P \<Longrightarrow> False\<close>
```
```    74   shows \<open>\<not> P\<close>
```
```    75 apply (unfold not_def)
```
```    76 apply (rule impI)
```
```    77 apply (rule assms)
```
```    78 apply assumption
```
```    79 done
```
```    80
```
```    81 lemma
```
```    82   assumes major: \<open>\<not> P\<close>
```
```    83     and minor: \<open>P\<close>
```
```    84   shows \<open>R\<close>
```
```    85 apply (rule FalseE)
```
```    86 apply (rule mp)
```
```    87 apply (rule major [unfolded not_def])
```
```    88 apply (rule minor)
```
```    89 done
```
```    90
```
```    91 text \<open>Alternative proof of the result above\<close>
```
```    92 lemma
```
```    93   assumes major: \<open>\<not> P\<close>
```
```    94     and minor: \<open>P\<close>
```
```    95   shows \<open>R\<close>
```
```    96 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
```
```    97 done
```
```    98
```
```    99 end
```