From 76dfd5bb2dc2db04a3e388d392958afc3d67f315 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 16 Jul 2002 10:47:51 +0000 Subject: Example of using pbp --- etc/lego/pbp.l | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 etc/lego/pbp.l (limited to 'etc/lego') diff --git a/etc/lego/pbp.l b/etc/lego/pbp.l new file mode 100644 index 00000000..82318dce --- /dev/null +++ b/etc/lego/pbp.l @@ -0,0 +1,28 @@ +(* How to prove a sample theorem by PBP. *) + +(* All using middle-clicks. + + 1. Click on -> (Intros A B) + 2. Click on -> again (Intros H; Try Refine H) + 3. Click on A (Intros H1; Try Refine H1) + 4. Click on B (Intros H2; Try Refine H2) + 5. Click on A in A/\B (Refine pair; Try Assumption) + 6. Click on final B (Try Assumption) + QED!! +*) + +Module pbp Import lib_logic; + +Goal {A,B:Prop}(A /\ B) -> (B /\ A); +Intros A B; +Intros H; Try Refine H; +Intros H1; Try Refine H1; +Intros H2; Try Refine H2; +Refine pair; Try Assumption; +Try Assumption; +Save and_comms; + + + + + -- cgit v1.2.3