doc-src/Logics/CTT-eg.txt

 print_depth 0;
 
 
 (*** Type inference, from CTT/ex/typechk.ML ***)
 
-goal CTT_Rule.thy "lam n. rec(n, 0, %x y.x) : ?A";
+goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
 by (resolve_tac [ProdI] 1);
 by (eresolve_tac [NE] 2);
 by (resolve_tac [NI0] 2);
 by (assume_tac 2);
 by (resolve_tac [NF] 1);
 
 
 
 (*** Logical reasoning, from CTT/ex/elim.ML ***)
 
-val prems = goal CTT_Rule.thy
+val prems = goal CTT.thy
     "[| A type;  \
 \       !!x. x:A ==> B(x) type;       \
 \       !!x. x:A ==> C(x) type;       \
 \       p: SUM x:A. B(x) + C(x)       \
 \    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";

 by (pc_tac prems 1);
 
 
 (*** Currying, from CTT/ex/elim.ML ***)
 
-val prems = goal CTT_Rule.thy
+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 z : (SUM x:A . B(x)) . C(z)) \
 \         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
 by (intr_tac prems);

 by (intr_tac prems);
 
 
 (*** Axiom of Choice ***)
 
-val prems = goal CTT_Rule.thy   
+val prems = goal CTT.thy   
     "[| 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))    \
 \               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
 by (intr_tac prems);

 by (typechk_tac prems);
 
 
 
 
-> goal CTT_Rule.thy "lam n. rec(n, 0, %x y.x) : ?A";
+> 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

 No subgoals!
 
 
 
 
-> val prems = goal CTT_Rule.thy
+> val prems = goal CTT.thy
 #     "[| A type;  \
 # \       !!x. x:A ==> B(x) type;       \
 # \       !!x. x:A ==> C(x) type;       \
 # \       p: SUM x:A. B(x) + C(x)       \
 # \    |] ==>  ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";

 No subgoals!
 
 
 
 
-> val prems = goal CTT_Rule.thy
+> 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 z : (SUM x:A . B(x)) . C(z)) \
 # \         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
 Level 0

 No subgoals!
 
 
 
 
-> val prems = goal CTT_Rule.thy
+> val prems = goal CTT.thy
 #     "[| 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))    \
 # \               --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
 Level 0