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