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