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