src/FOL/ex/Foundation.thy
author wenzelm
Sun, 26 Nov 2006 23:43:53 +0100
changeset 21539 c5cf9243ad62
parent 19819 14de4d05d275
child 26682 310c3b1a4157
permissions -rw-r--r--
converted legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19819
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     1
(*  Title:      FOL/ex/Foundation.ML
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     5
*)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     6
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     7
header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     8
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
     9
theory Foundation
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    10
imports IFOL
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    11
begin
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    12
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    13
lemma "A&B  --> (C-->A&C)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    14
apply (rule impI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    15
apply (rule impI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    16
apply (rule conjI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    17
prefer 2 apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    18
apply (rule conjunct1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    19
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    20
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    21
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    22
text {*A form of conj-elimination*}
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    23
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    24
  assumes "A & B"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    25
    and "A ==> B ==> C"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    26
  shows C
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    27
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    28
apply (rule conjunct1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    29
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    30
apply (rule conjunct2)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    31
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    32
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    33
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    34
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    35
  assumes "!!A. ~ ~A ==> A"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    36
  shows "B | ~B"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    37
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    38
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    39
apply (rule_tac P = "~B" in notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    40
apply (rule_tac [2] notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    41
apply (rule_tac [2] P = "B | ~B" in notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    42
prefer 2 apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    43
apply (rule_tac [2] disjI1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    44
prefer 2 apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    45
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    46
apply (rule_tac P = "B | ~B" in notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    47
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    48
apply (rule disjI2)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    49
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    50
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    51
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    52
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    53
  assumes "!!A. ~ ~A ==> A"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    54
  shows "B | ~B"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    55
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    56
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    57
apply (rule notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    58
apply (rule_tac [2] notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    59
apply (erule_tac [2] notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    60
apply (erule_tac [2] disjI1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    61
apply (rule notI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    62
apply (erule notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    63
apply (erule disjI2)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    64
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    65
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    66
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    67
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    68
  assumes "A | ~A"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    69
    and "~ ~A"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    70
  shows A
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    71
apply (rule disjE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    72
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    73
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    74
apply (rule FalseE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    75
apply (rule_tac P = "~A" in notE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    76
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    77
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    78
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    79
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    80
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    81
subsection "Examples with quantifiers"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    82
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    83
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    84
  assumes "ALL z. G(z)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    85
  shows "ALL z. G(z)|H(z)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    86
apply (rule allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    87
apply (rule disjI1)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    88
apply (rule prems [THEN spec])
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    89
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    90
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    91
lemma "ALL x. EX y. x=y"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    92
apply (rule allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    93
apply (rule exI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    94
apply (rule refl)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    95
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    96
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    97
lemma "EX y. ALL x. x=y"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    98
apply (rule exI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
    99
apply (rule allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   100
apply (rule refl)?
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   101
oops
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   102
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   103
text {* Parallel lifting example. *}
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   104
lemma "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   105
apply (rule exI allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   106
apply (rule exI allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   107
apply (rule exI allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   108
apply (rule exI allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   109
apply (rule exI allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   110
oops
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   111
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   112
lemma
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   113
  assumes "(EX z. F(z)) & B"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   114
  shows "EX z. F(z) & B"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   115
apply (rule conjE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   116
apply (rule prems)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   117
apply (rule exE)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   118
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   119
apply (rule exI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   120
apply (rule conjI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   121
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   122
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   123
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   124
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   125
text {* A bigger demonstration of quantifiers -- not in the paper. *}
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   126
lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   127
apply (rule impI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   128
apply (rule allI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   129
apply (rule exE, assumption)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   130
apply (rule exI)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   131
apply (rule allE, assumption)
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   132
apply assumption
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   133
done
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   134
14de4d05d275 removed obsolete ML files;
wenzelm
parents:
diff changeset
   135
end