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
```