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