summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/FOLP/ex/foundn.ML

author | paulson |

Fri, 05 Oct 2007 09:59:03 +0200 | |

changeset 24854 | 0ebcd575d3c6 |

parent 18678 | dd0c569fa43d |

permissions | -rw-r--r-- |

filtering out some package theorems

(* Title: FOLP/ex/foundn.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover *) goal (theory "IFOLP") "?p : A&B --> (C-->A&C)"; by (rtac impI 1); by (rtac impI 1); by (rtac conjI 1); by (assume_tac 2); by (rtac conjunct1 1); by (assume_tac 1); result(); (*A form of conj-elimination*) val prems = goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C"; by (resolve_tac prems 1); by (rtac conjunct1 1); by (resolve_tac prems 1); by (rtac conjunct2 1); by (resolve_tac prems 1); result(); val prems = goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B"; by (resolve_tac prems 1); by (rtac notI 1); by (res_inst_tac [ ("P", "~B") ] notE 1); by (rtac notI 2); by (res_inst_tac [ ("P", "B | ~B") ] notE 2); by (assume_tac 2); by (rtac disjI1 2); by (assume_tac 2); by (rtac notI 1); by (res_inst_tac [ ("P", "B | ~B") ] notE 1); by (assume_tac 1); by (rtac disjI2 1); by (assume_tac 1); result(); val prems = goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B"; by (resolve_tac prems 1); by (rtac notI 1); by (rtac notE 1); by (rtac notI 2); by (etac notE 2); by (etac disjI1 2); by (rtac notI 1); by (etac notE 1); by (etac disjI2 1); result(); val prems = goal (theory "IFOLP") "[| p:A | ~A; q:~ ~A |] ==> ?p:A"; by (rtac disjE 1); by (resolve_tac prems 1); by (assume_tac 1); by (rtac FalseE 1); by (res_inst_tac [ ("P", "~A") ] notE 1); by (resolve_tac prems 1); by (assume_tac 1); result(); writeln"Examples with quantifiers"; val prems = goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)"; by (rtac allI 1); by (rtac disjI1 1); by (resolve_tac (prems RL [spec]) 1); (*can use instead by (rtac spec 1); by (resolve_tac prems 1); *) result(); goal (theory "IFOLP") "?p : ALL x. EX y. x=y"; by (rtac allI 1); by (rtac exI 1); by (rtac refl 1); result(); goal (theory "IFOLP") "?p : EX y. ALL x. x=y"; by (rtac exI 1); by (rtac allI 1); by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected"; getgoal 1; (*Parallel lifting example. *) goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; by (resolve_tac [exI, allI] 1); by (resolve_tac [exI, allI] 1); by (resolve_tac [exI, allI] 1); by (resolve_tac [exI, allI] 1); by (resolve_tac [exI, allI] 1); val prems = goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)"; by (rtac conjE 1); by (resolve_tac prems 1); by (rtac exE 1); by (assume_tac 1); by (rtac exI 1); by (rtac conjI 1); by (assume_tac 1); by (assume_tac 1); result(); (*A bigger demonstration of quantifiers -- not in the paper*) goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; by (rtac impI 1); by (rtac allI 1); by (rtac exE 1 THEN assume_tac 1); by (rtac exI 1); by (rtac allE 1 THEN assume_tac 1); by (assume_tac 1); result();