Mercurial Mercurial > repos > isabelle / diff
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.
doc-src/Logics/CTT-eg.txt
changeset 5151 1e944fe5ce96
parent 359 b5a2e9503a7a 
--- a/doc-src/Logics/CTT-eg.txt	Thu Jul 16 10:35:31 1998 +0200
+++ b/doc-src/Logics/CTT-eg.txt	Thu Jul 16 11:50:01 1998 +0200
@@ -6,7 +6,7 @@
 
 (*** Type inference, from CTT/ex/typechk.ML ***)
 
-goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
+Goal "lam n. rec(n, 0, %x y. x) : ?A";
 by (resolve_tac [ProdI] 1);
 by (eresolve_tac [NE] 2);
 by (resolve_tac [NI0] 2);
@@ -17,7 +17,7 @@
 
 (*** Logical reasoning, from CTT/ex/elim.ML ***)
 
-val prems = goal CTT.thy
+val prems = Goal
     "[| A type;  \
 \       !!x. x:A ==> B(x) type;       \
 \       !!x. x:A ==> C(x) type;       \
@@ -35,10 +35,10 @@
 
 (*** Currying, from CTT/ex/elim.ML ***)
 
-val prems = goal CTT.thy
-    "[| A type; !!x. x:A ==> B(x) type; 			\
-\               !!z. z: (SUM x:A. B(x)) ==> C(z) type 		\
-\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).	\
+val prems = Goal
+    "[| A type; !!x. x:A ==> B(x) type;                         \
+\               !!z. z: (SUM x:A. B(x)) ==> C(z) type           \
+\    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).    \
 \                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
 by (intr_tac prems);
 by (eresolve_tac [ProdE] 1);
@@ -47,7 +47,7 @@
 
 (*** Axiom of Choice ***)
 
-val prems = goal CTT.thy   
+val prems = Goal   
     "[| A type;  !!x. x:A ==> B(x) type;  \
 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).    \
@@ -65,39 +65,11 @@
 
 
 
-> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
-Level 0
-lam n. rec(n,0,%x y. x) : ?A
- 1. lam n. rec(n,0,%x y. x) : ?A
-> by (resolve_tac [ProdI] 1);
-Level 1
-lam n. rec(n,0,%x y. x) : PROD x:?A1. ?B1(x)
- 1. ?A1 type
- 2. !!n. n : ?A1 ==> rec(n,0,%x y. x) : ?B1(n)
-> by (eresolve_tac [NE] 2);
-Level 2
-lam n. rec(n,0,%x y. x) : PROD x:N. ?C2(x,x)
- 1. N type
- 2. !!n. 0 : ?C2(n,0)
- 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))
-> by (resolve_tac [NI0] 2);
-Level 3
-lam n. rec(n,0,%x y. x) : N --> N
- 1. N type
- 2. !!n x y. [| x : N; y : N |] ==> x : N
-> by (assume_tac 2);
-Level 4
-lam n. rec(n,0,%x y. x) : N --> N
- 1. N type
-> by (resolve_tac [NF] 1);
-Level 5
-lam n. rec(n,0,%x y. x) : N --> N
-No subgoals!
+
+STOP_HERE;
 
 
-
-
-> val prems = goal CTT.thy
+> val prems = Goal
 #     "[| A type;  \
 # \       !!x. x:A ==> B(x) type;       \
 # \       !!x. x:A ==> C(x) type;       \
@@ -174,7 +146,7 @@
 
 
 
-> val prems = goal CTT.thy
+> val prems = Goal
 #     "[| A type; !!x. x:A ==> B(x) type; \
 # \               !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
 # \    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
@@ -204,7 +176,7 @@
 
 
 
-> val prems = goal CTT.thy
+> val prems = Goal
 #     "[| A type;  !!x. x:A ==> B(x) type;  \
 # \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type  \
 # \    |] ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
isabelle