doc-src/Logics/LK-eg.txt

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/LK-eg.txt	Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,117 @@
+(**** LK examples -- process using Doc/tout LK-eg.txt ****)
+
+Pretty.setmargin 72;  (*existing macros just allow this margin*)
+print_depth 0;
+
+goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
+by (resolve_tac [exR] 1);
+by (resolve_tac [allR] 1);
+by (resolve_tac [impR] 1);
+by (resolve_tac [basic] 1);
+(*previous step fails!*)
+by (resolve_tac [exR_thin] 1);
+by (resolve_tac [allR] 1);
+by (resolve_tac [impR] 1);
+by (resolve_tac [basic] 1);
+goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
+by (best_tac LK_dup_pack 1);
+
+
+
+goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+by (resolve_tac [notR] 1);
+by (resolve_tac [exL] 1);
+by (resolve_tac [allL_thin] 1);
+by (resolve_tac [iffL] 1);
+by (resolve_tac [notL] 2);
+by (resolve_tac [basic] 2);
+by (resolve_tac [notR] 1);
+by (resolve_tac [basic] 1);
+
+
+
+> goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
+Level 0
+ |- EX y. ALL x. P(y) --> P(x)
+ 1.  |- EX y. ALL x. P(y) --> P(x)
+> by (resolve_tac [exR] 1);
+Level 1
+ |- EX y. ALL x. P(y) --> P(x)
+ 1.  |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
+> by (resolve_tac [allR] 1);
+Level 2
+ |- EX y. ALL x. P(y) --> P(x)
+ 1. !!x.  |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)
+> by (resolve_tac [impR] 1);
+Level 3
+ |- EX y. ALL x. P(y) --> P(x)
+ 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)
+> by (resolve_tac [basic] 1);
+by: tactic failed
+> by (resolve_tac [exR_thin] 1);
+Level 4
+ |- EX y. ALL x. P(y) --> P(x)
+ 1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)
+> by (resolve_tac [allR] 1);
+Level 5
+ |- EX y. ALL x. P(y) --> P(x)
+ 1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)
+> by (resolve_tac [impR] 1);
+Level 6
+ |- EX y. ALL x. P(y) --> P(x)
+ 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)
+> by (resolve_tac [basic] 1);
+Level 7
+ |- EX y. ALL x. P(y) --> P(x)
+No subgoals!
+
+> goal LK_Rule.thy "|- EX y. ALL x. P(y)-->P(x)";
+Level 0
+ |- EX y. ALL x. P(y) --> P(x)
+ 1.  |- EX y. ALL x. P(y) --> P(x)
+> by (best_tac LK_dup_pack 1);
+Level 1
+ |- EX y. ALL x. P(y) --> P(x)
+No subgoals!
+
+
+
+
+> goal LK_Rule.thy "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+Level 0
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1.  |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+> by (resolve_tac [notR] 1);
+Level 1
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. EX x. ALL y. F(y,x) <-> ~F(y,y) |-
+> by (resolve_tac [exL] 1);
+Level 2
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x. ALL y. F(y,x) <-> ~F(y,y) |-
+> by (resolve_tac [allL_thin] 1);
+Level 3
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x. F(?x2(x),x) <-> ~F(?x2(x),?x2(x)) |-
+> by (resolve_tac [iffL] 1);
+Level 4
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
+ 2. !!x. ~F(?x2(x),?x2(x)), F(?x2(x),x) |-
+> by (resolve_tac [notL] 2);
+Level 5
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x.  |- F(?x2(x),x), ~F(?x2(x),?x2(x))
+ 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))
+> by (resolve_tac [basic] 2);
+Level 6
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x.  |- F(x,x), ~F(x,x)
+> by (resolve_tac [notR] 1);
+Level 7
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+ 1. !!x. F(x,x) |- F(x,x)
+> by (resolve_tac [basic] 1);
+Level 8
+ |- ~(EX x. ALL y. F(y,x) <-> ~F(y,y))
+No subgoals!