src/FOLP/ex/Foundation.thy
author wenzelm
Sun, 02 Nov 2014 18:21:45 +0100
changeset 58889 5b7a9633cfa8
parent 41777 1f7cbe39d425
child 60770 240563fbf41d
permissions -rw-r--r--
modernized header uniformly as section;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41777
1f7cbe39d425 more precise headers;
wenzelm
parents: 41526
diff changeset
     1
(*  Title:      FOLP/ex/Foundation.thy
25991
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
58889
5b7a9633cfa8 modernized header uniformly as section;
wenzelm
parents: 41777
diff changeset
     6
section "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    12
schematic_lemma "?p : A&B  --> (C-->A&C)"
25991
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*}
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    22
schematic_lemma
25991
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"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    26
apply (rule assms)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    27
apply (rule conjunct1)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    28
apply (rule assms)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    29
apply (rule conjunct2)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    30
apply (rule assms)
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    31
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    32
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    33
schematic_lemma
25991
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"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    36
apply (rule assms)
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    51
schematic_lemma
25991
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"
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    54
apply (rule assms)
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    66
schematic_lemma
25991
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)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    71
apply (rule assms)
25991
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)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    75
apply (rule assms)
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    82
schematic_lemma
25991
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)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
    87
apply (rule assms [THEN spec])
25991
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    88
done
31b38a39e589 eliminated some legacy ML files;
wenzelm
parents:
diff changeset
    89
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    90
schematic_lemma "?p : ALL x. EX y. x=y"
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
    96
schematic_lemma "?p : EX y. ALL x. x=y"
25991
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. *}
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
   103
schematic_lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
25991
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
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
   111
schematic_lemma
25991
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)
41526
54b4686704af eliminated global prems;
wenzelm
parents: 36319
diff changeset
   115
apply (rule assms)
25991
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. *}
36319
8feb2c4bef1a mark schematic statements explicitly;
wenzelm
parents: 35762
diff changeset
   125
schematic_lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
25991
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