src/FOLP/ex/Intro.thy
author wenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187 cca43ca13f4f
parent 25991 31b38a39e589
child 35762 af3ff2ba4c54
permissions -rw-r--r--
renamed structure Display_Goal to Goal_Display;
     1 (*  Title:      FOLP/ex/Intro.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Derives some inference rules, illustrating the use of definitions.
     7 *)
     8 
     9 header {* Examples for the manual ``Introduction to Isabelle'' *}
    10 
    11 theory Intro
    12 imports FOLP
    13 begin
    14 
    15 subsubsection {* Some simple backward proofs *}
    16 
    17 lemma mythm: "?p : P|P --> P"
    18 apply (rule impI)
    19 apply (rule disjE)
    20 prefer 3 apply (assumption)
    21 prefer 2 apply (assumption)
    22 apply assumption
    23 done
    24 
    25 lemma "?p : (P & Q) | R --> (P | R)"
    26 apply (rule impI)
    27 apply (erule disjE)
    28 apply (drule conjunct1)
    29 apply (rule disjI1)
    30 apply (rule_tac [2] disjI2)
    31 apply assumption+
    32 done
    33 
    34 (*Correct version, delaying use of "spec" until last*)
    35 lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
    36 apply (rule impI)
    37 apply (rule allI)
    38 apply (rule allI)
    39 apply (drule spec)
    40 apply (drule spec)
    41 apply assumption
    42 done
    43 
    44 
    45 subsubsection {* Demonstration of @{text "fast"} *}
    46 
    47 lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    48         -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
    49 apply (tactic {* fast_tac FOLP_cs 1 *})
    50 done
    51 
    52 
    53 lemma "?p : ALL x. P(x,f(x)) <->
    54         (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
    55 apply (tactic {* fast_tac FOLP_cs 1 *})
    56 done
    57 
    58 
    59 subsubsection {* Derivation of conjunction elimination rule *}
    60 
    61 lemma
    62   assumes major: "p : P&Q"
    63     and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
    64   shows "?p : R"
    65 apply (rule minor)
    66 apply (rule major [THEN conjunct1])
    67 apply (rule major [THEN conjunct2])
    68 done
    69 
    70 
    71 subsection {* Derived rules involving definitions *}
    72 
    73 text {* Derivation of negation introduction *}
    74 
    75 lemma
    76   assumes "!!x. x : P ==> f(x) : False"
    77   shows "?p : ~ P"
    78 apply (unfold not_def)
    79 apply (rule impI)
    80 apply (rule prems)
    81 apply assumption
    82 done
    83 
    84 lemma
    85   assumes major: "p : ~P"
    86     and minor: "q : P"
    87   shows "?p : R"
    88 apply (rule FalseE)
    89 apply (rule mp)
    90 apply (rule major [unfolded not_def])
    91 apply (rule minor)
    92 done
    93 
    94 text {* Alternative proof of the result above *}
    95 lemma
    96   assumes major: "p : ~P"
    97     and minor: "q : P"
    98   shows "?p : R"
    99 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
   100 done
   101 
   102 end