src/FOL/ex/Intro.thy
author wenzelm
Fri Jan 01 10:49:00 2016 +0100 (2016-01-01)
changeset 62020 5d208fd2507d
parent 61489 b8d375aee0df
child 69590 e65314985426
permissions -rw-r--r--
isabelle update_cartouches -c -t;
     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: "P \<or> P \<longrightarrow> P"
    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 "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)"
    25 apply (rule impI)
    26 apply (erule disjE)
    27 apply (drule conjunct1)
    28 apply (rule disjI1)
    29 apply (rule_tac [2] disjI2)
    30 apply assumption+
    31 done
    32 
    33 text \<open>Correct version, delaying use of \<open>spec\<close> until last.\<close>
    34 lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))"
    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 "(\<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))"
    47 apply fast
    48 done
    49 
    50 
    51 lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
    52 apply fast
    53 done
    54 
    55 
    56 subsubsection \<open>Derivation of conjunction elimination rule\<close>
    57 
    58 lemma
    59   assumes major: "P \<and> Q"
    60     and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
    61   shows R
    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 "P \<Longrightarrow> False"
    74   shows "\<not> P"
    75 apply (unfold not_def)
    76 apply (rule impI)
    77 apply (rule assms)
    78 apply assumption
    79 done
    80 
    81 lemma
    82   assumes major: "\<not> P"
    83     and minor: P
    84   shows R
    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: "\<not> P"
    94     and minor: P
    95   shows R
    96 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
    97 done
    98 
    99 end