Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/FOLP/ex/foundn.ML
changeset 17480 fd19f77dcf60
parent 3836 f1a1817659e6
child 18678 dd0c569fa43d
equal deleted inserted replaced
17479:68a7acb5f22e 17480:fd19f77dcf60 
     4     Copyright   1991  University of Cambridge
 
     4     Copyright   1991  University of Cambridge
 
     5 
     5 
     6 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
 
     6 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
 
     7 *)
 
     7 *)
 
     8 
     8 
     9 writeln"File FOLP/ex/foundn.ML";
 
     9 goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
 
    10 
       
    11 goal IFOLP.thy "?p : A&B  --> (C-->A&C)";
 
       
    12 by (rtac impI 1);
 
    10 by (rtac impI 1);
 
    13 by (rtac impI 1);
 
    11 by (rtac impI 1);
 
    14 by (rtac conjI 1);
 
    12 by (rtac conjI 1);
 
    15 by (assume_tac 2);
 
    13 by (assume_tac 2);
 
    16 by (rtac conjunct1 1);
 
    14 by (rtac conjunct1 1);
 
    17 by (assume_tac 1);
 
    15 by (assume_tac 1);
 
    18 result();
 
    16 result();
 
    19 
    17 
    20 (*A form of conj-elimination*)
 
    18 (*A form of conj-elimination*)
 
    21 val prems = 
    19 val prems = 
    22 goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
 
    20 goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
 
    23 by (resolve_tac prems 1);
 
    21 by (resolve_tac prems 1);
 
    24 by (rtac conjunct1 1);
 
    22 by (rtac conjunct1 1);
 
    25 by (resolve_tac prems 1);
 
    23 by (resolve_tac prems 1);
 
    26 by (rtac conjunct2 1);
 
    24 by (rtac conjunct2 1);
 
    27 by (resolve_tac prems 1);
 
    25 by (resolve_tac prems 1);
 
    28 result();
 
    26 result();
 
    29 
    27 
    30 
    28 
    31 val prems = 
    29 val prems = 
    32 goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
 
    30 goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
 
    33 by (resolve_tac prems 1);
 
    31 by (resolve_tac prems 1);
 
    34 by (rtac notI 1);
 
    32 by (rtac notI 1);
 
    35 by (res_inst_tac [ ("P", "~B") ]  notE  1);
 
    33 by (res_inst_tac [ ("P", "~B") ]  notE  1);
 
    36 by (rtac notI 2);
 
    34 by (rtac notI 2);
 
    37 by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
 
    35 by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
 
    45 by (assume_tac 1);
 
    43 by (assume_tac 1);
 
    46 result();
 
    44 result();
 
    47 
    45 
    48 
    46 
    49 val prems = 
    47 val prems = 
    50 goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
 
    48 goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
 
    51 by (resolve_tac prems 1);
 
    49 by (resolve_tac prems 1);
 
    52 by (rtac notI 1);
 
    50 by (rtac notI 1);
 
    53 by (rtac notE 1);
 
    51 by (rtac notE 1);
 
    54 by (rtac notI 2);
 
    52 by (rtac notI 2);
 
    55 by (etac notE 2);
 
    53 by (etac notE 2);
 
    59 by (etac disjI2 1);
 
    57 by (etac disjI2 1);
 
    60 result();
 
    58 result();
 
    61 
    59 
    62 
    60 
    63 val prems = 
    61 val prems = 
    64 goal IFOLP.thy "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
 
    62 goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
 
    65 by (rtac disjE 1);
 
    63 by (rtac disjE 1);
 
    66 by (resolve_tac prems 1);
 
    64 by (resolve_tac prems 1);
 
    67 by (assume_tac 1);
 
    65 by (assume_tac 1);
 
    68 by (rtac FalseE 1);
 
    66 by (rtac FalseE 1);
 
    69 by (res_inst_tac [ ("P", "~A") ]  notE  1);
 
    67 by (res_inst_tac [ ("P", "~A") ]  notE  1);
 
    73 
    71 
    74 
    72 
    75 writeln"Examples with quantifiers";
 
    73 writeln"Examples with quantifiers";
 
    76 
    74 
    77 val prems =
 
    75 val prems =
 
    78 goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
 
    76 goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
 
    79 by (rtac allI 1);
 
    77 by (rtac allI 1);
 
    80 by (rtac disjI1 1);
 
    78 by (rtac disjI1 1);
 
    81 by (resolve_tac (prems RL [spec]) 1); 
    79 by (resolve_tac (prems RL [spec]) 1); 
    82   (*can use instead
 
    80   (*can use instead
 
    83     by (rtac spec 1);  by (resolve_tac prems 1); *)
 
    81     by (rtac spec 1);  by (resolve_tac prems 1); *)
 
    84 result();
 
    82 result();
 
    85 
    83 
    86 
    84 
    87 goal IFOLP.thy "?p : ALL x. EX y. x=y";
 
    85 goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
 
    88 by (rtac allI 1);
 
    86 by (rtac allI 1);
 
    89 by (rtac exI 1);
 
    87 by (rtac exI 1);
 
    90 by (rtac refl 1);
 
    88 by (rtac refl 1);
 
    91 result();
 
    89 result();
 
    92 
    90 
    93 
    91 
    94 goal IFOLP.thy "?p : EX y. ALL x. x=y";
 
    92 goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
 
    95 by (rtac exI 1);
 
    93 by (rtac exI 1);
 
    96 by (rtac allI 1);
 
    94 by (rtac allI 1);
 
    97 by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
    95 by (rtac refl 1) handle ERROR => writeln"Failed, as expected";  
    98 getgoal 1; 
    96 getgoal 1; 
    99 
    97 
   100 
    98 
   101 (*Parallel lifting example. *)
 
    99 (*Parallel lifting example. *)
 
   102 goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
 
   100 goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
 
   103 by (resolve_tac [exI, allI] 1);
 
   101 by (resolve_tac [exI, allI] 1);
 
   104 by (resolve_tac [exI, allI] 1);
 
   102 by (resolve_tac [exI, allI] 1);
 
   105 by (resolve_tac [exI, allI] 1);
 
   103 by (resolve_tac [exI, allI] 1);
 
   106 by (resolve_tac [exI, allI] 1);
 
   104 by (resolve_tac [exI, allI] 1);
 
   107 by (resolve_tac [exI, allI] 1);
 
   105 by (resolve_tac [exI, allI] 1);
 
   108 
   106 
   109 
   107 
   110 val prems =
 
   108 val prems =
 
   111 goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
 
   109 goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
 
   112 by (rtac conjE 1);
 
   110 by (rtac conjE 1);
 
   113 by (resolve_tac prems 1);
 
   111 by (resolve_tac prems 1);
 
   114 by (rtac exE 1);
 
   112 by (rtac exE 1);
 
   115 by (assume_tac 1);
 
   113 by (assume_tac 1);
 
   116 by (rtac exI 1);
 
   114 by (rtac exI 1);
 
   119 by (assume_tac 1);
 
   117 by (assume_tac 1);
 
   120 result();
 
   118 result();
 
   121 
   119 
   122 
   120 
   123 (*A bigger demonstration of quantifiers -- not in the paper*)
 
   121 (*A bigger demonstration of quantifiers -- not in the paper*)
 
   124 goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
 
   122 goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
 
   125 by (rtac impI 1);
 
   123 by (rtac impI 1);
 
   126 by (rtac allI 1);
 
   124 by (rtac allI 1);
 
   127 by (rtac exE 1 THEN assume_tac 1);
 
   125 by (rtac exE 1 THEN assume_tac 1);
 
   128 by (rtac exI 1);
 
   126 by (rtac exI 1);
 
   129 by (rtac allE 1 THEN assume_tac 1);
 
   127 by (rtac allE 1 THEN assume_tac 1);
 
   130 by (assume_tac 1);
 
   128 by (assume_tac 1);
 
   131 result();  
   129 result();  
   132 
       
   133 
       
   134 writeln"Reached end of file.";
isabelle