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