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