src/FOLP/ex/Intro.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 41526 54b4686704af
child 58957 c9e744ea8a38
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      FOLP/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 {* Examples for the manual ``Introduction to Isabelle'' *}
     9 
    10 theory Intro
    11 imports FOLP
    12 begin
    13 
    14 subsubsection {* Some simple backward proofs *}
    15 
    16 schematic_lemma mythm: "?p : P|P --> 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 schematic_lemma "?p : (P & Q) | R --> (P | 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 (*Correct version, delaying use of "spec" until last*)
    34 schematic_lemma "?p : (ALL x y. P(x,y)) --> (ALL 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 {* Demonstration of @{text "fast"} *}
    45 
    46 schematic_lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    47         -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
    48 apply (tactic {* fast_tac FOLP_cs 1 *})
    49 done
    50 
    51 
    52 schematic_lemma "?p : ALL x. P(x,f(x)) <->
    53         (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
    54 apply (tactic {* fast_tac FOLP_cs 1 *})
    55 done
    56 
    57 
    58 subsubsection {* Derivation of conjunction elimination rule *}
    59 
    60 schematic_lemma
    61   assumes major: "p : P&Q"
    62     and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
    63   shows "?p : R"
    64 apply (rule minor)
    65 apply (rule major [THEN conjunct1])
    66 apply (rule major [THEN conjunct2])
    67 done
    68 
    69 
    70 subsection {* Derived rules involving definitions *}
    71 
    72 text {* Derivation of negation introduction *}
    73 
    74 schematic_lemma
    75   assumes "!!x. x : P ==> f(x) : False"
    76   shows "?p : ~ P"
    77 apply (unfold not_def)
    78 apply (rule impI)
    79 apply (rule assms)
    80 apply assumption
    81 done
    82 
    83 schematic_lemma
    84   assumes major: "p : ~P"
    85     and minor: "q : P"
    86   shows "?p : R"
    87 apply (rule FalseE)
    88 apply (rule mp)
    89 apply (rule major [unfolded not_def])
    90 apply (rule minor)
    91 done
    92 
    93 text {* Alternative proof of the result above *}
    94 schematic_lemma
    95   assumes major: "p : ~P"
    96     and minor: "q : P"
    97   shows "?p : R"
    98 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
    99 done
   100 
   101 end