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