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  notI)
```
```    41 apply (rule_tac  P = "B | ~B" in notE)
```
```    42 prefer 2 apply assumption
```
```    43 apply (rule_tac  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  notI)
```
```    59 apply (erule_tac  notE)
```
```    60 apply (erule_tac  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
```