--- a/doc-src/Intro/Makefile Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = intro
-FILES = intro.tex foundations.tex getting.tex advanced.tex \
- ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle.eps
- $(LATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(LATEX) $(NAME)
- $(LATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle.pdf
- $(PDFLATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(FIXBOOKMARKS) $(NAME).out
- $(PDFLATEX) $(NAME)
--- a/doc-src/Logics/CTT-eg.txt Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,282 +0,0 @@
-(**** CTT examples -- process using Doc/tout CTT-eg.txt ****)
-
-Pretty.setmargin 72; (*existing macros just allow this margin*)
-print_depth 0;
-
-
-(*** Type inference, from CTT/ex/typechk.ML ***)
-
-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);
-by (assume_tac 2);
-by (resolve_tac [NF] 1);
-
-
-
-(*** Logical reasoning, from CTT/ex/elim.ML ***)
-
-val prems = Goal
- "[| 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 (resolve_tac (prems RL [SumE]) 1);
-by (eresolve_tac [PlusE] 1);
-by (resolve_tac [PlusI_inl] 1);
-by (resolve_tac [SumI] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (typechk_tac prems);
-by (pc_tac prems 1);
-
-
-(*** Currying, from CTT/ex/elim.ML ***)
-
-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);
-by (intr_tac prems);
-
-
-(*** Axiom of Choice ***)
-
-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)). \
-\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-by (intr_tac prems);
-by (eresolve_tac [ProdE RS SumE_fst] 1);
-by (assume_tac 1);
-by (resolve_tac [replace_type] 1);
-by (resolve_tac [subst_eqtyparg] 1);
-by (resolve_tac [ProdC] 1);
-by (typechk_tac (SumE_fst::prems));
-by (eresolve_tac [ProdE RS SumE_snd] 1);
-by (typechk_tac prems);
-
-
-
-
-
-STOP_HERE;
-
-
-> val prems = Goal
-# "[| 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))";
-Level 0
-?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (resolve_tac (prems RL [SumE]) 1);
-Level 1
-split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y.
- [| x : A; y : B(x) + C(x) |] ==>
- ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (eresolve_tac [PlusE] 1);
-Level 2
-split(p,%x y. when(y,?c2(x,y),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y xa.
- [| x : A; xa : B(x) |] ==>
- ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))
- 2. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (resolve_tac [PlusI_inl] 1);
-Level 3
-split(p,%x y. when(y,%xa. inl(?a3(x,y,xa)),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)
- 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
- 3. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (resolve_tac [SumI] 1);
-Level 4
-split(p,%x y. when(y,%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A
- 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))
- 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
- 4. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (assume_tac 1);
-Level 5
-split(p,%x y. when(y,%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)
- 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
- 3. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (assume_tac 1);
-Level 6
-split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type
- 2. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (typechk_tac prems);
-Level 7
-split(p,%x y. when(y,%xa. inl(<x,xa>),?d2(x,y)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
- 1. !!x y ya.
- [| x : A; ya : C(x) |] ==>
- ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))
-> by (pc_tac prems 1);
-Level 8
-split(p,%x y. when(y,%xa. inl(<x,xa>),%y. inr(<x,y>)))
-: (SUM x:A. B(x)) + (SUM x:A. C(x))
-No subgoals!
-
-
-
-
-> 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)) \
-# \ --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
-Level 0
-?a : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
- 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->
- (PROD x:A. PROD y:B(x). C(<x,y>))
-> by (intr_tac prems);
-Level 1
-lam x xa xb. ?b7(x,xa,xb)
-: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
- 1. !!uu x y.
- [| uu : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>
- ?b7(uu,x,y) : C(<x,y>)
-> by (eresolve_tac [ProdE] 1);
-Level 2
-lam x xa xb. x ` <xa,xb>
-: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
- 1. !!uu x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)
-> by (intr_tac prems);
-Level 3
-lam x xa xb. x ` <xa,xb>
-: (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))
-No subgoals!
-
-
-
-
-> 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)) \
-# \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-Level 0
-?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))
- 1. ?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);
-Level 1
-lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b7(uu,x) : B(x)
- 2. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,(lam x. ?b7(uu,x)) ` x)
-> by (eresolve_tac [ProdE RS SumE_fst] 1);
-Level 2
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x. x : A ==> x : A
- 2. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
-> by (assume_tac 1);
-Level 3
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,(lam x. fst(uu ` x)) ` x)
-> by (resolve_tac [replace_type] 1);
-Level 4
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- C(x,(lam x. fst(uu ` x)) ` x) = ?A13(uu,x)
- 2. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : ?A13(uu,x)
-> by (resolve_tac [subst_eqtyparg] 1);
-Level 5
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- (lam x. fst(uu ` x)) ` x = ?c14(uu,x) : ?A14(uu,x)
- 2. !!uu x z.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
- z : ?A14(uu,x) |] ==>
- C(x,z) type
- 3. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,?c14(uu,x))
-> by (resolve_tac [ProdC] 1);
-Level 6
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==> x : ?A15(uu,x)
- 2. !!uu x xa.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
- xa : ?A15(uu,x) |] ==>
- fst(uu ` xa) : ?B15(uu,x,xa)
- 3. !!uu x z.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A;
- z : ?B15(uu,x,x) |] ==>
- C(x,z) type
- 4. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,fst(uu ` x))
-> by (typechk_tac (SumE_fst::prems));
-Level 7
-lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x.
- [| uu : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>
- ?b8(uu,x) : C(x,fst(uu ` x))
-> by (eresolve_tac [ProdE RS SumE_snd] 1);
-Level 8
-lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
- 1. !!uu x. x : A ==> x : A
- 2. !!uu x. x : A ==> B(x) type
- 3. !!uu x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type
-> by (typechk_tac prems);
-Level 9
-lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>
-: (PROD x:A. SUM y:B(x). C(x,y)) -->
- (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))
-No subgoals!
--- a/doc-src/Logics/CTT-rules.txt Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,241 +0,0 @@
-\idx{refl_type} A type ==> A = A),
-\idx{refl_elem} a : A ==> a = a : A
-
-\idx{sym_type} A = B ==> B = A
-\idx{sym_elem} a = b : A ==> b = a : A
-
-\idx{trans_type} [| A = B; B = C |] ==> A = C
-\idx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A
-
-\idx{equal_types} [| a : A; A = B |] ==> a : B
-\idx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B
-
-\idx{subst_type} [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type
-
-\idx{subst_typeL} [| a = c : A; !!z. z:A ==> B(z) = D(z)
- |] ==> B(a) = D(c)
-\idx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
-
-\idx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)
- |] ==> b(a) = d(c) : B(a)
-
-\idx{refl_red} Reduce(a,a)
-\idx{red_if_equal} a = b : A ==> Reduce(a,b)
-\idx{trans_red} [| a = b : A; Reduce(b,c) |] ==> a = c : A
-
-
-\idx{NF} N type
-
-\idx{NI0} 0 : N
-\idx{NI_succ} a : N ==> succ(a) : N
-\idx{NI_succL} a = b : N ==> succ(a) = succ(b) : N
-
-\idx{NE} [| p: N; a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(p, a, %u v.b(u,v)) : C(p)
-
-\idx{NEL} [| p = q : N; a = c : C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v) = d(u,v): C(succ(u))
- |] ==> rec(p, a, %u v.b(u,v)) = rec(q,c,d) : C(p)
-
-\idx{NC0} [| a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(0, a, %u v.b(u,v)) = a : C(0)
-
-\idx{NC_succ} [| p: N; a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(succ(p), a, %u v.b(u,v)) =
- b(p, rec(p, a, %u v.b(u,v))) : C(succ(p))
-
-\idx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F
-
-
-\idx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A.B(x) type
-\idx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
- PROD x:A.B(x) = PROD x:C.D(x)
-
-\idx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
- |] ==> lam x.b(x) : PROD x:A.B(x)
-\idx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x)
- |] ==> lam x.b(x) = lam x.c(x) : PROD x:A.B(x)
-
-\idx{ProdE} [| p : PROD x:A.B(x); a : A |] ==> p`a : B(a)
-\idx{ProdEL} [| p=q: PROD x:A.B(x); a=b : A |] ==> p`a = q`b : B(a)
-
-\idx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
- |] ==> (lam x.b(x)) ` a = b(a) : B(a)
-
-\idx{ProdC2} p : PROD x:A.B(x) ==> (lam x. p`x) = p : PROD x:A.B(x)
-
-
-\idx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A.B(x) type
-\idx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
- |] ==> SUM x:A.B(x) = SUM x:C.D(x)
-
-\idx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A.B(x)
-\idx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A.B(x)
-
-\idx{SumE} [| p: SUM x:A.B(x);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
- |] ==> split(p, %x y.c(x,y)) : C(p)
-
-\idx{SumEL} [| p=q : SUM x:A.B(x);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
- |] ==> split(p, %x y.c(x,y)) = split(q, % x y.d(x,y)) : C(p)
-
-\idx{SumC} [| a: A; b: B(a);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
- |] ==> split(<a,b>, %x y.c(x,y)) = c(a,b) : C(<a,b>)
-
-\idx{fst_def} fst(a) == split(a, %x y.x)
-\idx{snd_def} snd(a) == split(a, %x y.y)
-
-
-\idx{PlusF} [| A type; B type |] ==> A+B type
-\idx{PlusFL} [| A = C; B = D |] ==> A+B = C+D
-
-\idx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B
-\idx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B
-
-\idx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B
-\idx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B
-
-\idx{PlusE} [| p: A+B;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(p, %x.c(x), %y.d(y)) : C(p)
-
-\idx{PlusEL} [| p = q : A+B;
- !!x. x: A ==> c(x) = e(x) : C(inl(x));
- !!y. y: B ==> d(y) = f(y) : C(inr(y))
- |] ==> when(p, %x.c(x), %y.d(y)) = when(q, %x.e(x), %y.f(y)) : C(p)
-
-\idx{PlusC_inl} [| a: A;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(inl(a), %x.c(x), %y.d(y)) = c(a) : C(inl(a))
-
-\idx{PlusC_inr} [| b: B;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(inr(b), %x.c(x), %y.d(y)) = d(b) : C(inr(b))
-
-\idx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type
-\idx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
-\idx{EqI} a = b : A ==> eq : Eq(A,a,b)
-\idx{EqE} p : Eq(A,a,b) ==> a = b : A
-\idx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
-
-\idx{FF} F type
-\idx{FE} [| p: F; C type |] ==> contr(p) : C
-\idx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C
-
-\idx{TF} T type
-\idx{TI} tt : T
-\idx{TE} [| p : T; c : C(tt) |] ==> c : C(p)
-\idx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)
-\idx{TC} p : T ==> p = tt : T)
-
-
-\idx{replace_type} [| B = A; a : A |] ==> a : B
-\idx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
-
-\idx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)
- |] ==> c(p`a): C(p`a)
-
-\idx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
-
-\idx{SumE_fst} p : Sum(A,B) ==> fst(p) : A
-
-\idx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type
- |] ==> snd(p) : B(fst(p))
-
-
-
-\idx{add_def} a#+b == rec(a, b, %u v.succ(v))
-\idx{diff_def} a-b == rec(b, a, %u v.rec(v, 0, %x y.x))
-\idx{absdiff_def} a|-|b == (a-b) #+ (b-a)
-\idx{mult_def} a#*b == rec(a, 0, %u v. b #+ v)
-
-\idx{mod_def} a//b == rec(a, 0, %u v.
- rec(succ(v) |-| b, 0, %x y.succ(v)))
-
-\idx{quo_def} a/b == rec(a, 0, %u v.
- rec(succ(u) // b, succ(v), %x y.v))
-
-
-\idx{add_typing} [| a:N; b:N |] ==> a #+ b : N
-\idx{add_typingL} [| a=c:N; b=d:N |] ==> a #+ b = c #+ d : N
-\idx{addC0} b:N ==> 0 #+ b = b : N
-\idx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
-\idx{mult_typing} [| a:N; b:N |] ==> a #* b : N
-\idx{mult_typingL} [| a=c:N; b=d:N |] ==> a #* b = c #* d : N
-\idx{multC0} b:N ==> 0 #* b = 0 : N
-\idx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a #* b) : N
-\idx{diff_typing} [| a:N; b:N |] ==> a - b : N
-\idx{diff_typingL} [| a=c:N; b=d:N |] ==> a - b = c - d : N
-\idx{diffC0} a:N ==> a - 0 = a : N
-\idx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
-
-\idx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
-
-\idx{add_assoc} [| a:N; b:N; c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N
-
-\idx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
-
-\idx{mult_right0} a:N ==> a #* 0 = 0 : N
-
-\idx{mult_right_succ} [| a:N; b:N |] ==> a #* succ(b) = a #+ (a #* b) : N
-
-\idx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N
-
-\idx{add_mult_dist} [| a:N; b:N; c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N
-
-\idx{mult_assoc} [| a:N; b:N; c:N |] ==> (a #* b) #* c = a #* (b #* c) : N
-
-\idx{diff_self_eq_0} a:N ==> a - a = 0 : N
-
-\idx{add_inverse_diff_lemma}
- b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)
-
-\idx{add_inverse_diff} [| a:N; b:N; b-a = 0 : N |] ==> b #+ (a-b) = a : N
-
-\idx{absdiff_typing} [| a:N; b:N |] ==> a |-| b : N
-\idx{absdiff_typingL} [| a=c:N; b=d:N |] ==> a |-| b = c |-| d : N
-\idx{absdiff_self_eq_0} a:N ==> a |-| a = 0 : N
-\idx{absdiffC0} a:N ==> 0 |-| a = a : N
-
-\idx{absdiff_succ_succ} [| a:N; b:N |] ==> succ(a) |-| succ(b) = a |-| b : N
-\idx{absdiff_commute} [| a:N; b:N |] ==> a |-| b = b |-| a : N
-
-\idx{add_eq0_lemma} [| a:N; b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) . Eq(N,a,0)
-
-\idx{add_eq0} [| a:N; b:N; a #+ b = 0 : N |] ==> a = 0 : N
-
-\idx{absdiff_eq0_lem}
- [| a:N; b:N; a |-| b = 0 : N |] ==>
- ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)
-
-\idx{absdiff_eq0} [| a |-| b = 0 : N; a:N; b:N |] ==> a = b : N
-
-\idx{mod_typing} [| a:N; b:N |] ==> a//b : N
-\idx{mod_typingL} [| a=c:N; b=d:N |] ==> a//b = c//d : N
-\idx{modC0} b:N ==> 0//b = 0 : N
-\idx{modC_succ}
-[| a:N; b:N |] ==> succ(a)//b = rec(succ(a//b) |-| b, 0, %x y.succ(a//b)) : N
-
-\idx{quo_typing} [| a:N; b:N |] ==> a / b : N
-\idx{quo_typingL} [| a=c:N; b=d:N |] ==> a / b = c / d : N
-\idx{quoC0} b:N ==> 0 / b = 0 : N
-[| a:N; b:N |] ==> succ(a) / b =
- rec(succ(a)//b, succ(a / b), %x y. a / b) : N
-\idx{quoC_succ2} [| a:N; b:N |] ==>
- succ(a) / b =rec(succ(a//b) |-| b, succ(a / b), %x y. a / b) : N
-
-\idx{iszero_decidable}
- a:N ==> rec(a, inl(eq), %ka kb.inr(<ka, eq>)) :
- Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))
-
-\idx{mod_quo_equality} [| a:N; b:N |] ==> a//b #+ (a/b) #* b = a : N
-
-
--- a/doc-src/Logics/CTT.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1257 +0,0 @@
-\chapter{Constructive Type Theory}
-\index{Constructive Type Theory|(}
-
-\underscoreoff %this file contains _ in rule names
-
-Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
-be viewed at many different levels. It is a formal system that embodies
-the principles of intuitionistic mathematics; it embodies the
-interpretation of propositions as types; it is a vehicle for deriving
-programs from proofs.
-
-Thompson's book~\cite{thompson91} gives a readable and thorough account of
-Type Theory. Nuprl is an elaborate implementation~\cite{constable86}.
-{\sc alf} is a more recent tool that allows proof terms to be edited
-directly~\cite{alf}.
-
-Isabelle's original formulation of Type Theory was a kind of sequent
-calculus, following Martin-L\"of~\cite{martinlof84}. It included rules for
-building the context, namely variable bindings with their types. A typical
-judgement was
-\[ a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \;
- [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
-\]
-This sequent calculus was not satisfactory because assumptions like
-`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$'
-could not be formalized.
-
-The theory~\thydx{CTT} implements Constructive Type Theory, using
-natural deduction. The judgement above is expressed using $\Forall$ and
-$\Imp$:
-\[ \begin{array}{r@{}l}
- \Forall x@1\ldots x@n. &
- \List{x@1\in A@1;
- x@2\in A@2(x@1); \cdots \;
- x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
- & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)
- \end{array}
-\]
-Assumptions can use all the judgement forms, for instance to express that
-$B$ is a family of types over~$A$:
-\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
-To justify the CTT formulation it is probably best to appeal directly to the
-semantic explanations of the rules~\cite{martinlof84}, rather than to the
-rules themselves. The order of assumptions no longer matters, unlike in
-standard Type Theory. Contexts, which are typical of many modern type
-theories, are difficult to represent in Isabelle. In particular, it is
-difficult to enforce that all the variables in a context are distinct.
-\index{assumptions!in CTT}
-
-The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the
-type of individuals. Types in CTT have type~\tydx{t}.
-
-\begin{figure} \tabcolsep=1em %wider spacing in tables
-\begin{center}
-\begin{tabular}{rrr}
- \it name & \it meta-type & \it description \\
- \cdx{Type} & $t \to prop$ & judgement form \\
- \cdx{Eqtype} & $[t,t]\to prop$ & judgement form\\
- \cdx{Elem} & $[i, t]\to prop$ & judgement form\\
- \cdx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
- \cdx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
-
- \cdx{N} & $t$ & natural numbers type\\
- \cdx{0} & $i$ & constructor\\
- \cdx{succ} & $i\to i$ & constructor\\
- \cdx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex]
- \cdx{Prod} & $[t,i\to t]\to t$ & general product type\\
- \cdx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]
- \cdx{Sum} & $[t, i\to t]\to t$ & general sum type\\
- \cdx{pair} & $[i,i]\to i$ & constructor\\
- \cdx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\
- \cdx{fst} \cdx{snd} & $i\to i$ & projections\\[2ex]
- \cdx{inl} \cdx{inr} & $i\to i$ & constructors for $+$\\
- \cdx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex]
- \cdx{Eq} & $[t,i,i]\to t$ & equality type\\
- \cdx{eq} & $i$ & constructor\\[2ex]
- \cdx{F} & $t$ & empty type\\
- \cdx{contr} & $i\to i$ & eliminator\\[2ex]
- \cdx{T} & $t$ & singleton type\\
- \cdx{tt} & $i$ & constructor
-\end{tabular}
-\end{center}
-\caption{The constants of CTT} \label{ctt-constants}
-\end{figure}
-
-
-CTT supports all of Type Theory apart from list types, well-ordering types,
-and universes. Universes could be introduced {\em\`a la Tarski}, adding new
-constants as names for types. The formulation {\em\`a la Russell}, where
-types denote themselves, is only possible if we identify the meta-types~{\tt
- i} and~{\tt t}. Most published formulations of well-ordering types have
-difficulties involving extensionality of functions; I suggest that you use
-some other method for defining recursive types. List types are easy to
-introduce by declaring new rules.
-
-CTT uses the 1982 version of Type Theory, with extensional equality. The
-computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
-Its rewriting tactics prove theorems of the form $a=b\in A$. It could be
-modified to have intensional equality, but rewriting tactics would have to
-prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
-require a separate simplifier.
-
-
-\begin{figure} \tabcolsep=1em %wider spacing in tables
-\index{lambda abs@$\lambda$-abstractions!in CTT}
-\begin{center}
-\begin{tabular}{llrrr}
- \it symbol &\it name &\it meta-type & \it priority & \it description \\
- \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
-\end{tabular}
-\end{center}
-\subcaption{Binders}
-
-\begin{center}
-\index{*"` symbol}\index{function applications!in CTT}
-\index{*"+ symbol}
-\begin{tabular}{rrrr}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt ` & $[i,i]\to i$ & Left 55 & function application\\
- \tt + & $[t,t]\to t$ & Right 30 & sum of two types
-\end{tabular}
-\end{center}
-\subcaption{Infixes}
-
-\index{*"* symbol}
-\index{*"-"-"> symbol}
-\begin{center} \tt\frenchspacing
-\begin{tabular}{rrr}
- \it external & \it internal & \it standard notation \\
- \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) &
- \rm product $\prod@{x\in A}B[x]$ \\
- \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) &
- \rm sum $\sum@{x\in A}B[x]$ \\
- $A$ --> $B$ & Prod($A$, $\lambda x. B$) &
- \rm function space $A\to B$ \\
- $A$ * $B$ & Sum($A$, $\lambda x. B$) &
- \rm binary product $A\times B$
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-
-\index{*"= symbol}
-\begin{center}
-\dquotes
-\[ \begin{array}{rcl}
-prop & = & type " type" \\
- & | & type " = " type \\
- & | & term " : " type \\
- & | & term " = " term " : " type
-\\[2ex]
-type & = & \hbox{expression of type~$t$} \\
- & | & "PROD~" id " : " type " . " type \\
- & | & "SUM~~" id " : " type " . " type
-\\[2ex]
-term & = & \hbox{expression of type~$i$} \\
- & | & "lam " id~id^* " . " term \\
- & | & "< " term " , " term " >"
-\end{array}
-\]
-\end{center}
-\subcaption{Grammar}
-\caption{Syntax of CTT} \label{ctt-syntax}
-\end{figure}
-
-%%%%\section{Generic Packages} typedsimp.ML????????????????
-
-
-\section{Syntax}
-The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include
-the function application operator (sometimes called `apply'), and the 2-place
-type operators. Note that meta-level abstraction and application, $\lambda
-x.b$ and $f(a)$, differ from object-level abstraction and application,
-\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
-individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
-$i\To i$.
-
-The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
-et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
-type is $T$; other finite types are built as $T+T+T$, etc.
-
-\index{*SUM symbol}\index{*PROD symbol}
-Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
-products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
- Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
- PROD $x$:$A$.\ $B[x]$}. For example, we may write
-\begin{ttbox}
-SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y)))
-\end{ttbox}
-The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate
-general sums and products over a constant family.\footnote{Unlike normal
-infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are
-no constants~{\tt op~*} and~\hbox{\tt op~-->}.} Isabelle accepts these
-abbreviations in parsing and uses them whenever possible for printing.
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{refl_type} A type ==> A = A
-\tdx{refl_elem} a : A ==> a = a : A
-
-\tdx{sym_type} A = B ==> B = A
-\tdx{sym_elem} a = b : A ==> b = a : A
-
-\tdx{trans_type} [| A = B; B = C |] ==> A = C
-\tdx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A
-
-\tdx{equal_types} [| a : A; A = B |] ==> a : B
-\tdx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B
-
-\tdx{subst_type} [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type
-\tdx{subst_typeL} [| a = c : A; !!z. z:A ==> B(z) = D(z)
- |] ==> B(a) = D(c)
-
-\tdx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
-\tdx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)
- |] ==> b(a) = d(c) : B(a)
-
-\tdx{refl_red} Reduce(a,a)
-\tdx{red_if_equal} a = b : A ==> Reduce(a,b)
-\tdx{trans_red} [| a = b : A; Reduce(b,c) |] ==> a = c : A
-\end{ttbox}
-\caption{General equality rules} \label{ctt-equality}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{NF} N type
-
-\tdx{NI0} 0 : N
-\tdx{NI_succ} a : N ==> succ(a) : N
-\tdx{NI_succL} a = b : N ==> succ(a) = succ(b) : N
-
-\tdx{NE} [| p: N; a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
-
-\tdx{NEL} [| p = q : N; a = c : C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
- |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
-
-\tdx{NC0} [| a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
-
-\tdx{NC_succ} [| p: N; a: C(0);
- !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
- |] ==> rec(succ(p), a, \%u v. b(u,v)) =
- b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
-
-\tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F
-\end{ttbox}
-\caption{Rules for type~$N$} \label{ctt-N}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
-\tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
- PROD x:A. B(x) = PROD x:C. D(x)
-
-\tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
- |] ==> lam x. b(x) : PROD x:A. B(x)
-\tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x)
- |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
-
-\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)
-\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)
-
-\tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
- |] ==> (lam x. b(x)) ` a = b(a) : B(a)
-
-\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
-\end{ttbox}
-\caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
-\tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
- |] ==> SUM x:A. B(x) = SUM x:C. D(x)
-
-\tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)
-\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
-
-\tdx{SumE} [| p: SUM x:A. B(x);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
- |] ==> split(p, \%x y. c(x,y)) : C(p)
-
-\tdx{SumEL} [| p=q : SUM x:A. B(x);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
- |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
-
-\tdx{SumC} [| a: A; b: B(a);
- !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
- |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
-
-\tdx{fst_def} fst(a) == split(a, \%x y. x)
-\tdx{snd_def} snd(a) == split(a, \%x y. y)
-\end{ttbox}
-\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{PlusF} [| A type; B type |] ==> A+B type
-\tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D
-
-\tdx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B
-\tdx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B
-
-\tdx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B
-\tdx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B
-
-\tdx{PlusE} [| p: A+B;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
-
-\tdx{PlusEL} [| p = q : A+B;
- !!x. x: A ==> c(x) = e(x) : C(inl(x));
- !!y. y: B ==> d(y) = f(y) : C(inr(y))
- |] ==> when(p, \%x. c(x), \%y. d(y)) =
- when(q, \%x. e(x), \%y. f(y)) : C(p)
-
-\tdx{PlusC_inl} [| a: A;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
-
-\tdx{PlusC_inr} [| b: B;
- !!x. x:A ==> c(x): C(inl(x));
- !!y. y:B ==> d(y): C(inr(y))
- |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
-\end{ttbox}
-\caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{FF} F type
-\tdx{FE} [| p: F; C type |] ==> contr(p) : C
-\tdx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C
-
-\tdx{TF} T type
-\tdx{TI} tt : T
-\tdx{TE} [| p : T; c : C(tt) |] ==> c : C(p)
-\tdx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)
-\tdx{TC} p : T ==> p = tt : T)
-\end{ttbox}
-
-\caption{Rules for types $F$ and $T$} \label{ctt-ft}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type
-\tdx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
-\tdx{EqI} a = b : A ==> eq : Eq(A,a,b)
-\tdx{EqE} p : Eq(A,a,b) ==> a = b : A
-\tdx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
-\end{ttbox}
-\caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{replace_type} [| B = A; a : A |] ==> a : B
-\tdx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
-
-\tdx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)
- |] ==> c(p`a): C(p`a)
-
-\tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
-
-\tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A
-
-\tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type
- |] ==> snd(p) : B(fst(p))
-\end{ttbox}
-
-\caption{Derived rules for CTT} \label{ctt-derived}
-\end{figure}
-
-
-\section{Rules of inference}
-The rules obey the following naming conventions. Type formation rules have
-the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@.
-Elimination rules have the suffix~{\tt E}\@. Computation rules, which
-describe the reduction of eliminators, have the suffix~{\tt C}\@. The
-equality versions of the rules (which permit reductions on subterms) are
-called {\bf long} rules; their names have the suffix~{\tt L}\@.
-Introduction and computation rules are often further suffixed with
-constructor names.
-
-Figure~\ref{ctt-equality} presents the equality rules. Most of them are
-straightforward: reflexivity, symmetry, transitivity and substitution. The
-judgement \cdx{Reduce} does not belong to Type Theory proper; it has
-been added to implement rewriting. The judgement ${\tt Reduce}(a,b)$ holds
-when $a=b:A$ holds. It also holds when $a$ and $b$ are syntactically
-identical, even if they are ill-typed, because rule {\tt refl_red} does
-not verify that $a$ belongs to $A$.
-
-The {\tt Reduce} rules do not give rise to new theorems about the standard
-judgements. The only rule with {\tt Reduce} in a premise is
-{\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus
-$c$) are well-typed.
-
-Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
-They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$. This is
-the fourth Peano axiom and cannot be derived without universes \cite[page
-91]{martinlof84}.
-
-The constant \cdx{rec} constructs proof terms when mathematical
-induction, rule~\tdx{NE}, is applied. It can also express primitive
-recursion. Since \cdx{rec} can be applied to higher-order functions,
-it can even express Ackermann's function, which is not primitive recursive
-\cite[page~104]{thompson91}.
-
-Figure~\ref{ctt-prod} shows the rules for general product types, which
-include function types as a special case. The rules correspond to the
-predicate calculus rules for universal quantifiers and implication. They
-also permit reasoning about functions, with the rules of a typed
-$\lambda$-calculus.
-
-Figure~\ref{ctt-sum} shows the rules for general sum types, which
-include binary product types as a special case. The rules correspond to the
-predicate calculus rules for existential quantifiers and conjunction. They
-also permit reasoning about ordered pairs, with the projections
-\cdx{fst} and~\cdx{snd}.
-
-Figure~\ref{ctt-plus} shows the rules for binary sum types. They
-correspond to the predicate calculus rules for disjunction. They also
-permit reasoning about disjoint sums, with the injections \cdx{inl}
-and~\cdx{inr} and case analysis operator~\cdx{when}.
-
-Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
-and~$T$. They correspond to the predicate calculus rules for absurdity and
-truth.
-
-Figure~\ref{ctt-eq} shows the rules for equality types. If $a=b\in A$ is
-provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
-and vice versa. These rules define extensional equality; the most recent
-versions of Type Theory use intensional equality~\cite{nordstrom90}.
-
-Figure~\ref{ctt-derived} presents the derived rules. The rule
-\tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
-in backwards proof. The rules \tdx{SumE_fst} and \tdx{SumE_snd}
-express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
-roughly equivalent to~{\tt SumE} with the advantage of creating no
-parameters. Section~\ref{ctt-choice} below demonstrates these rules in a
-proof of the Axiom of Choice.
-
-All the rules are given in $\eta$-expanded form. For instance, every
-occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
-rules for~$N$. The expanded form permits Isabelle to preserve bound
-variable names during backward proof. Names of bound variables in the
-conclusion (here, $u$ and~$v$) are matched with corresponding bound
-variables in the premises.
-
-
-\section{Rule lists}
-The Type Theory tactics provide rewriting, type inference, and logical
-reasoning. Many proof procedures work by repeatedly resolving certain Type
-Theory rules against a proof state. CTT defines lists --- each with
-type
-\hbox{\tt thm list} --- of related rules.
-\begin{ttdescription}
-\item[\ttindexbold{form_rls}]
-contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
-$F$, and $T$.
-
-\item[\ttindexbold{formL_rls}]
-contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$. (For
-other types use \tdx{refl_type}.)
-
-\item[\ttindexbold{intr_rls}]
-contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
-$T$.
-
-\item[\ttindexbold{intrL_rls}]
-contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$. (For
-$T$ use \tdx{refl_elem}.)
-
-\item[\ttindexbold{elim_rls}]
-contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
-$F$. The rules for $Eq$ and $T$ are omitted because they involve no
-eliminator.
-
-\item[\ttindexbold{elimL_rls}]
-contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
-
-\item[\ttindexbold{comp_rls}]
-contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$.
-Those for $Eq$ and $T$ involve no eliminator.
-
-\item[\ttindexbold{basic_defs}]
-contains the definitions of {\tt fst} and {\tt snd}.
-\end{ttdescription}
-
-
-\section{Tactics for subgoal reordering}
-\begin{ttbox}
-test_assume_tac : int -> tactic
-typechk_tac : thm list -> tactic
-equal_tac : thm list -> tactic
-intr_tac : thm list -> tactic
-\end{ttbox}
-Blind application of CTT rules seldom leads to a proof. The elimination
-rules, especially, create subgoals containing new unknowns. These subgoals
-unify with anything, creating a huge search space. The standard tactic
-\ttindex{filt_resolve_tac}
-(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
- {\S\ref{filt_resolve_tac}})
-%
-fails for goals that are too flexible; so does the CTT tactic {\tt
- test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
-achieve a simple kind of subgoal reordering: the less flexible subgoals are
-attempted first. Do some single step proofs, or study the examples below,
-to see why this is necessary.
-\begin{ttdescription}
-\item[\ttindexbold{test_assume_tac} $i$]
-uses {\tt assume_tac} to solve the subgoal by assumption, but only if
-subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
-Otherwise, it fails.
-
-\item[\ttindexbold{typechk_tac} $thms$]
-uses $thms$ with formation, introduction, and elimination rules to check
-the typing of constructions. It is designed to solve goals of the form
-$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
-performs type inference. The tactic can also solve goals of
-the form $A\;\rm type$.
-
-\item[\ttindexbold{equal_tac} $thms$]
-uses $thms$ with the long introduction and elimination rules to solve goals
-of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving
-the long rules for defined constants such as the arithmetic operators. The
-tactic can also perform type-checking.
-
-\item[\ttindexbold{intr_tac} $thms$]
-uses $thms$ with the introduction rules to break down a type. It is
-designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
-rigid. These typically arise when trying to prove a proposition~$A$,
-expressed as a type.
-\end{ttdescription}
-
-
-
-\section{Rewriting tactics}
-\begin{ttbox}
-rew_tac : thm list -> tactic
-hyp_rew_tac : thm list -> tactic
-\end{ttbox}
-Object-level simplification is accomplished through proof, using the {\tt
- CTT} equality rules and the built-in rewriting functor
-{\tt TSimpFun}.%
-\footnote{This should not be confused with Isabelle's main simplifier; {\tt
- TSimpFun} is only useful for CTT and similar logics with type inference
- rules. At present it is undocumented.}
-%
-The rewrites include the computation rules and other equations. The long
-versions of the other rules permit rewriting of subterms and subtypes.
-Also used are transitivity and the extra judgement form \cdx{Reduce}.
-Meta-level simplification handles only definitional equality.
-\begin{ttdescription}
-\item[\ttindexbold{rew_tac} $thms$]
-applies $thms$ and the computation rules as left-to-right rewrites. It
-solves the goal $a=b\in A$ by rewriting $a$ to $b$. If $b$ is an unknown
-then it is assigned the rewritten form of~$a$. All subgoals are rewritten.
-
-\item[\ttindexbold{hyp_rew_tac} $thms$]
-is like {\tt rew_tac}, but includes as rewrites any equations present in
-the assumptions.
-\end{ttdescription}
-
-
-\section{Tactics for logical reasoning}
-Interpreting propositions as types lets CTT express statements of
-intuitionistic logic. However, Constructive Type Theory is not just another
-syntax for first-order logic. There are fundamental differences.
-
-\index{assumptions!in CTT}
-Can assumptions be deleted after use? Not every occurrence of a type
-represents a proposition, and Type Theory assumptions declare variables.
-In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
-creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
-can be deleted safely. In Type Theory, $+$-elimination with the assumption
-$z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in
-B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions
-refer to $z$ may render the subgoal unprovable: arguably,
-meaningless.
-
-Isabelle provides several tactics for predicate calculus reasoning in CTT:
-\begin{ttbox}
-mp_tac : int -> tactic
-add_mp_tac : int -> tactic
-safestep_tac : thm list -> int -> tactic
-safe_tac : thm list -> int -> tactic
-step_tac : thm list -> int -> tactic
-pc_tac : thm list -> int -> tactic
-\end{ttbox}
-These are loosely based on the intuitionistic proof procedures
-of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for
-propositional reasoning may be unsafe for type-checking; thus, some of the
-`safe' tactics are misnamed.
-\begin{ttdescription}
-\item[\ttindexbold{mp_tac} $i$]
-searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
-$a\in A$, where~$A$ may be found by unification. It replaces
-$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter. The tactic
-can produce multiple outcomes for each suitable pair of assumptions. In
-short, {\tt mp_tac} performs Modus Ponens among the assumptions.
-
-\item[\ttindexbold{add_mp_tac} $i$]
-is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It
-avoids information loss but obviously loops if repeated.
-
-\item[\ttindexbold{safestep_tac} $thms$ $i$]
-attacks subgoal~$i$ using formation rules and certain other `safe' rules
-(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
-{\tt mp_tac} when appropriate. It also uses~$thms$,
-which are typically premises of the rule being derived.
-
-\item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by
- means of backtracking, using {\tt safestep_tac}.
-
-\item[\ttindexbold{step_tac} $thms$ $i$]
-tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe
-rules. It may produce multiple outcomes.
-
-\item[\ttindexbold{pc_tac} $thms$ $i$]
-tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
-\end{ttdescription}
-
-
-
-\begin{figure}
-\index{#+@{\tt\#+} symbol}
-\index{*"- symbol}
-\index{#*@{\tt\#*} symbol}
-\index{*div symbol}
-\index{*mod symbol}
-
-\index{absolute difference}
-\index{"!-"!@{\tt\char124-\char124} symbol}
-%\char124 is vertical bar. We use ! because | stopped working
-
-\begin{constants}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\
- \tt div & $[i,i]\To i$ & Left 70 & division\\
- \tt mod & $[i,i]\To i$ & Left 70 & modulus\\
- \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\
- \tt - & $[i,i]\To i$ & Left 65 & subtraction\\
- \verb'|-|' & $[i,i]\To i$ & Left 65 & absolute difference
-\end{constants}
-
-\begin{ttbox}
-\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v))
-\tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x))
-\tdx{absdiff_def} a|-|b == (a-b) #+ (b-a)
-\tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v)
-
-\tdx{mod_def} a mod b ==
- rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
-
-\tdx{div_def} a div b ==
- rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
-
-\tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N
-\tdx{addC0} b:N ==> 0 #+ b = b : N
-\tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
-
-\tdx{add_assoc} [| a:N; b:N; c:N |] ==>
- (a #+ b) #+ c = a #+ (b #+ c) : N
-
-\tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
-
-\tdx{mult_typing} [| a:N; b:N |] ==> a #* b : N
-\tdx{multC0} b:N ==> 0 #* b = 0 : N
-\tdx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
-\tdx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N
-
-\tdx{add_mult_dist} [| a:N; b:N; c:N |] ==>
- (a #+ b) #* c = (a #* c) #+ (b #* c) : N
-
-\tdx{mult_assoc} [| a:N; b:N; c:N |] ==>
- (a #* b) #* c = a #* (b #* c) : N
-
-\tdx{diff_typing} [| a:N; b:N |] ==> a - b : N
-\tdx{diffC0} a:N ==> a - 0 = a : N
-\tdx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
-\tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
-\tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
-\tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
-\end{ttbox}
-\caption{The theory of arithmetic} \label{ctt_arith}
-\end{figure}
-
-
-\section{A theory of arithmetic}
-\thydx{Arith} is a theory of elementary arithmetic. It proves the
-properties of addition, multiplication, subtraction, division, and
-remainder, culminating in the theorem
-\[ a \bmod b + (a/b)\times b = a. \]
-Figure~\ref{ctt_arith} presents the definitions and some of the key
-theorems, including commutative, distributive, and associative laws.
-
-The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
-and~\verb'div' stand for sum, difference, absolute difference, product,
-remainder and quotient, respectively. Since Type Theory has only primitive
-recursion, some of their definitions may be obscure.
-
-The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
-the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
-
-The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
-as the successor of~$b-1$. Absolute difference is used to test the
-equality $succ(v)=b$.
-
-The quotient $a/b$ is computed by adding one for every number $x$
-such that $0\leq x \leq a$ and $x\bmod b = 0$.
-
-
-
-\section{The examples directory}
-This directory contains examples and experimental proofs in CTT.
-\begin{ttdescription}
-\item[CTT/ex/typechk.ML]
-contains simple examples of type-checking and type deduction.
-
-\item[CTT/ex/elim.ML]
-contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
-{\tt pc_tac}.
-
-\item[CTT/ex/equal.ML]
-contains simple examples of rewriting.
-
-\item[CTT/ex/synth.ML]
-demonstrates the use of unknowns with some trivial examples of program
-synthesis.
-\end{ttdescription}
-
-
-\section{Example: type inference}
-Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
-is a term and $\Var{A}$ is an unknown standing for its type. The type,
-initially
-unknown, takes shape in the course of the proof. Our example is the
-predecessor function on the natural numbers.
-\begin{ttbox}
-Goal "lam n. rec(n, 0, \%x y. x) : ?A";
-{\out Level 0}
-{\out lam n. rec(n,0,\%x y. x) : ?A}
-{\out 1. lam n. rec(n,0,\%x y. x) : ?A}
-\end{ttbox}
-Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
-be confused with a meta-level abstraction), we apply the rule
-\tdx{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a
-product type of unknown domain and range.
-\begin{ttbox}
-by (resolve_tac [ProdI] 1);
-{\out Level 1}
-{\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
-{\out 1. ?A1 type}
-{\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
-\end{ttbox}
-Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$
-to any type, but most instantiations will invalidate subgoal~2. We
-therefore tackle the latter subgoal. It asks the type of a term beginning
-with {\tt rec}, which can be found by $N$-elimination.%
-\index{*NE theorem}
-\begin{ttbox}
-by (eresolve_tac [NE] 2);
-{\out Level 2}
-{\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
-{\out 1. N type}
-{\out 2. !!n. 0 : ?C2(n,0)}
-{\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
-\end{ttbox}
-Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
-natural numbers. However, let us continue proving nontrivial subgoals.
-Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
-\begin{ttbox}
-by (resolve_tac [NI0] 2);
-{\out Level 3}
-{\out lam n. rec(n,0,\%x y. x) : N --> N}
-{\out 1. N type}
-{\out 2. !!n x y. [| x : N; y : N |] ==> x : N}
-\end{ttbox}
-The type~$\Var{A}$ is now fully determined. It is the product type
-$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
-there is no dependence on~$x$. But we must prove all the subgoals to show
-that the original term is validly typed. Subgoal~2 is provable by
-assumption and the remaining subgoal falls by $N$-formation.%
-\index{*NF theorem}
-\begin{ttbox}
-by (assume_tac 2);
-{\out Level 4}
-{\out lam n. rec(n,0,\%x y. x) : N --> N}
-{\out 1. N type}
-\ttbreak
-by (resolve_tac [NF] 1);
-{\out Level 5}
-{\out lam n. rec(n,0,\%x y. x) : N --> N}
-{\out No subgoals!}
-\end{ttbox}
-Calling \ttindex{typechk_tac} can prove this theorem in one step.
-
-Even if the original term is ill-typed, one can infer a type for it, but
-unprovable subgoals will be left. As an exercise, try to prove the
-following invalid goal:
-\begin{ttbox}
-Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
-\end{ttbox}
-
-
-
-\section{An example of logical reasoning}
-Logical reasoning in Type Theory involves proving a goal of the form
-$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
-for its proof term, a value of type $A$. The proof term is initially
-unknown and takes shape during the proof.
-
-Our example expresses a theorem about quantifiers in a sorted logic:
-\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
- {\ex{x\in A}P(x)\disj Q(x)}
-\]
-By the propositions-as-types principle, this is encoded
-using~$\Sigma$ and~$+$ types. A special case of it expresses a
-distributive law of Type Theory:
-\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
-Generalizing this from $\times$ to $\Sigma$, and making the typing
-conditions explicit, yields the rule we must derive:
-\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
- {\hbox{$A$ type} &
- \infer*{\hbox{$B(x)$ type}}{[x\in A]} &
- \infer*{\hbox{$C(x)$ type}}{[x\in A]} &
- p\in \sum@{x\in A} B(x)+C(x)}
-\]
-To begin, we bind the rule's premises --- returned by the~{\tt goal}
-command --- to the {\ML} variable~{\tt prems}.
-\begin{ttbox}
-val prems = Goal
- "[| A type; \ttback
-\ttback !!x. x:A ==> B(x) type; \ttback
-\ttback !!x. x:A ==> C(x) type; \ttback
-\ttback p: SUM x:A. B(x) + C(x) \ttback
-\ttback |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
-{\out Level 0}
-{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\ttbreak
-{\out val prems = ["A type [A type]",}
-{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
-{\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",}
-{\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]}
-{\out : thm list}
-\end{ttbox}
-The last premise involves the sum type~$\Sigma$. Since it is a premise
-rather than the assumption of a goal, it cannot be found by {\tt
- eresolve_tac}. We could insert it (and the other atomic premise) by
-calling
-\begin{ttbox}
-cut_facts_tac prems 1;
-\end{ttbox}
-A forward proof step is more straightforward here. Let us resolve the
-$\Sigma$-elimination rule with the premises using~\ttindex{RL}. This
-inference yields one result, which we supply to {\tt
- resolve_tac}.\index{*SumE theorem}
-\begin{ttbox}
-by (resolve_tac (prems RL [SumE]) 1);
-{\out Level 1}
-{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y.}
-{\out [| x : A; y : B(x) + C(x) |] ==>}
-{\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-The subgoal has two new parameters, $x$ and~$y$. In the main goal,
-$\Var{a}$ has been instantiated with a \cdx{split} term. The
-assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
-creating the parameter~$xa$. This inference also inserts~\cdx{when}
-into the main goal.\index{*PlusE theorem}
-\begin{ttbox}
-by (eresolve_tac [PlusE] 1);
-{\out Level 2}
-{\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y xa.}
-{\out [| x : A; xa : B(x) |] ==>}
-{\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\ttbreak
-{\out 2. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-To complete the proof object for the main goal, we need to instantiate the
-terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by
-a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
-injection~(\cdx{inl}).
-\index{*PlusI_inl theorem}
-\begin{ttbox}
-by (resolve_tac [PlusI_inl] 1);
-{\out Level 3}
-{\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
-{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
-\ttbreak
-{\out 3. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
-Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
-This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
-an ordered pair, whose components are two new unknowns.%
-\index{*SumI theorem}
-\begin{ttbox}
-by (resolve_tac [SumI] 1);
-{\out Level 4}
-{\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
-{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
-{\out 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
-{\out 4. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-The two new subgoals both hold by assumption. Observe how the unknowns
-$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
-\begin{ttbox}
-by (assume_tac 1);
-{\out Level 5}
-{\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\ttbreak
-{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
-{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
-{\out 3. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\ttbreak
-by (assume_tac 1);
-{\out Level 6}
-{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
-{\out 2. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
-Such subgoals are usually trivial; this one yields to
-\ttindex{typechk_tac}, given the current list of premises.
-\begin{ttbox}
-by (typechk_tac prems);
-{\out Level 7}
-{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out 1. !!x y ya.}
-{\out [| x : A; ya : C(x) |] ==>}
-{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-\end{ttbox}
-This subgoal is the other case from the $+$-elimination above, and can be
-proved similarly. Quicker is to apply \ttindex{pc_tac}. The main goal
-finally gets a fully instantiated proof object.
-\begin{ttbox}
-by (pc_tac prems 1);
-{\out Level 8}
-{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
-{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
-{\out No subgoals!}
-\end{ttbox}
-Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
-proves this theorem.
-
-
-\section{Example: deriving a currying functional}
-In simply-typed languages such as {\ML}, a currying functional has the type
-\[ (A\times B \to C) \to (A\to (B\to C)). \]
-Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.
-The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
-to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
-$C(\langle x,y\rangle)$.
-
-Formally, there are three typing premises. $A$ is a type; $B$ is an
-$A$-indexed family of types; $C$ is a family of types indexed by
-$\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure
-that the parameter corresponding to the functional's argument is really
-called~$f$; Isabelle echoes the type using \verb|-->| because there is no
-explicit dependence upon~$f$.
-\begin{ttbox}
-val prems = Goal
- "[| A type; !!x. x:A ==> B(x) type; \ttback
-\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback
-\ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback
-\ttback (PROD x:A . PROD y:B(x) . C(<x,y>))";
-\ttbreak
-{\out Level 0}
-{\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
-{\out (PROD x:A. PROD y:B(x). C(<x,y>))}
-{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
-{\out (PROD x:A. PROD y:B(x). C(<x,y>))}
-\ttbreak
-{\out val prems = ["A type [A type]",}
-{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
-{\out "?z : SUM x:A. B(x) ==> C(?z) type}
-{\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
-\end{ttbox}
-This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic
-repeatedly applies $\Pi$-introduction and proves the rather
-tiresome typing conditions.
-
-Note that $\Var{a}$ becomes instantiated to three nested
-$\lambda$-abstractions. It would be easier to read if the bound variable
-names agreed with the parameters in the subgoal. Isabelle attempts to give
-parameters the same names as corresponding bound variables in the goal, but
-this does not always work. In any event, the goal is logically correct.
-\begin{ttbox}
-by (intr_tac prems);
-{\out Level 1}
-{\out lam x xa xb. ?b7(x,xa,xb)}
-{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
-{\out 1. !!f x y.}
-{\out [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
-{\out ?b7(f,x,y) : C(<x,y>)}
-\end{ttbox}
-Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
-\index{*ProdE theorem}
-\begin{ttbox}
-by (eresolve_tac [ProdE] 1);
-{\out Level 2}
-{\out lam x xa xb. x ` <xa,xb>}
-{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
-{\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
-\end{ttbox}
-Finally, we verify that the argument's type is suitable for the function
-application. This is straightforward using introduction rules.
-\index{*intr_tac}
-\begin{ttbox}
-by (intr_tac prems);
-{\out Level 3}
-{\out lam x xa xb. x ` <xa,xb>}
-{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
-{\out No subgoals!}
-\end{ttbox}
-Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
-also prove an example by Martin-L\"of, related to $\disj$-elimination
-\cite[page~58]{martinlof84}.
-
-
-\section{Example: proving the Axiom of Choice} \label{ctt-choice}
-Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
-which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
-Interpreting propositions as types, this asserts that for all $x\in A$
-there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts
-that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
-$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
-function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
-
-In principle, the Axiom of Choice is simple to derive in Constructive Type
-Theory. The following definitions work:
-\begin{eqnarray*}
- f & \equiv & {\tt fst} \circ h \\
- g & \equiv & {\tt snd} \circ h
-\end{eqnarray*}
-But a completely formal proof is hard to find. The rules can be applied in
-countless ways, yielding many higher-order unifiers. The proof can get
-bogged down in the details. But with a careful selection of derived rules
-(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
-prove the theorem in nine steps.
-\begin{ttbox}
-val prems = Goal
- "[| A type; !!x. x:A ==> B(x) type; \ttback
-\ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback
-\ttback |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback
-\ttback (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
-{\out Level 0}
-{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-{\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out val prems = ["A type [A type]",}
-{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
-{\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
-{\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
-{\out : thm list}
-\end{ttbox}
-First, \ttindex{intr_tac} applies introduction rules and performs routine
-type-checking. This instantiates~$\Var{a}$ to a construction involving
-a $\lambda$-abstraction and an ordered pair. The pair's components are
-themselves $\lambda$-abstractions and there is a subgoal for each.
-\begin{ttbox}
-by (intr_tac prems);
-{\out Level 1}
-{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b7(h,x) : B(x)}
-\ttbreak
-{\out 2. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
-\end{ttbox}
-Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
-$\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof
-object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
-result lie in the relation~$C$. This latter task will take up most of the
-proof.
-\index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
-\begin{ttbox}
-by (eresolve_tac [ProdE RS SumE_fst] 1);
-{\out Level 2}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x. x : A ==> x : A}
-{\out 2. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
-\end{ttbox}
-Above, we have composed {\tt fst} with the function~$h$. Unification
-has deduced that the function must be applied to $x\in A$. We have our
-choice function.
-\begin{ttbox}
-by (assume_tac 1);
-{\out Level 3}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
-\end{ttbox}
-Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
-simplified. The derived rule \tdx{replace_type} lets us replace a type
-by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
-\begin{ttbox}
-by (resolve_tac [replace_type] 1);
-{\out Level 4}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
-\ttbreak
-{\out 2. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : ?A13(h,x)}
-\end{ttbox}
-The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
-argument (by currying, $C(x)$ is a unary type operator):
-\begin{ttbox}
-by (resolve_tac [subst_eqtyparg] 1);
-{\out Level 5}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
-\ttbreak
-{\out 2. !!h x z.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
-{\out z : ?A14(h,x) |] ==>}
-{\out C(x,z) type}
-\ttbreak
-{\out 3. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,?c14(h,x))}
-\end{ttbox}
-Subgoal~1 requires simply $\beta$-contraction, which is the rule
-\tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal
-receives the contracted result.
-\begin{ttbox}
-by (resolve_tac [ProdC] 1);
-{\out Level 6}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out x : ?A15(h,x)}
-\ttbreak
-{\out 2. !!h x xa.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
-{\out xa : ?A15(h,x) |] ==>}
-{\out fst(h ` xa) : ?B15(h,x,xa)}
-\ttbreak
-{\out 3. !!h x z.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
-{\out z : ?B15(h,x,x) |] ==>}
-{\out C(x,z) type}
-\ttbreak
-{\out 4. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,fst(h ` x))}
-\end{ttbox}
-Routine type-checking goals proliferate in Constructive Type Theory, but
-\ttindex{typechk_tac} quickly solves them. Note the inclusion of
-\tdx{SumE_fst} along with the premises.
-\begin{ttbox}
-by (typechk_tac (SumE_fst::prems));
-{\out Level 7}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x.}
-{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
-{\out ?b8(h,x) : C(x,fst(h ` x))}
-\end{ttbox}
-We are finally ready to compose {\tt snd} with~$h$.
-\index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
-\begin{ttbox}
-by (eresolve_tac [ProdE RS SumE_snd] 1);
-{\out Level 8}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-\ttbreak
-{\out 1. !!h x. x : A ==> x : A}
-{\out 2. !!h x. x : A ==> B(x) type}
-{\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
-\end{ttbox}
-The proof object has reached its final form. We call \ttindex{typechk_tac}
-to finish the type-checking.
-\begin{ttbox}
-by (typechk_tac prems);
-{\out Level 9}
-{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
-{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
-{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
-{\out No subgoals!}
-\end{ttbox}
-It might be instructive to compare this proof with Martin-L\"of's forward
-proof of the Axiom of Choice \cite[page~50]{martinlof84}.
-
-\index{Constructive Type Theory|)}
--- a/doc-src/Logics/LK-eg.txt Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-(**** LK examples -- process using Doc/tout LK-eg.txt ****)
-
-Pretty.setmargin 72; (*existing macros just allow this margin*)
-print_depth 0;
-
-context LK.thy;
-
-Goal "|- 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 "|- EX y. ALL x. P(y)-->P(x)";
-by (best_tac LK_dup_pack 1);
-
-
-
-Goal "|- ~ (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);
-
-
-STOP_HERE;
-
-
-> Goal "|- 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 "|- 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 "|- ~ (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!
--- a/doc-src/Logics/LK.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,711 +0,0 @@
-\chapter{First-Order Sequent Calculus}
-\index{sequent calculus|(}
-
-The theory~\thydx{LK} implements classical first-order logic through Gentzen's
-sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).
-Resembling the method of semantic tableaux, the calculus is well suited for
-backwards proof. Assertions have the form \(\Gamma\turn \Delta\), where
-\(\Gamma\) and \(\Delta\) are lists of formulae. Associative unification,
-simulated by higher-order unification, handles lists
-(\S\ref{sec:assoc-unification} presents details, if you are interested).
-
-The logic is many-sorted, using Isabelle's type classes. The class of
-first-order terms is called \cldx{term}. No types of individuals are
-provided, but extensions can define types such as {\tt nat::term} and type
-constructors such as {\tt list::(term)term}. Below, the type variable
-$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
-are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
-belongs to class {\tt logic}.
-
-LK implements a classical logic theorem prover that is nearly as powerful as
-the generic classical reasoner. The simplifier is now available too.
-
-To work in LK, start up Isabelle specifying \texttt{Sequents} as the
-object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:
-\begin{ttbox}
-isabelle Sequents
-context LK.thy;
-\end{ttbox}
-Modal logic and linear logic are also available, but unfortunately they are
-not documented.
-
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
- \it name &\it meta-type & \it description \\
- \cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\
- \cdx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\
- \cdx{Not} & $o\To o$ & negation ($\neg$) \\
- \cdx{True} & $o$ & tautology ($\top$) \\
- \cdx{False} & $o$ & absurdity ($\bot$)
-\end{tabular}
-\end{center}
-\subcaption{Constants}
-
-\begin{center}
-\begin{tabular}{llrrr}
- \it symbol &\it name &\it meta-type & \it priority & \it description \\
- \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &
- universal quantifier ($\forall$) \\
- \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
- existential quantifier ($\exists$) \\
- \sdx{THE} & \cdx{The} & $(\alpha\To o)\To \alpha$ & 10 &
- definite description ($\iota$)
-\end{tabular}
-\end{center}
-\subcaption{Binders}
-
-\begin{center}
-\index{*"= symbol}
-\index{&@{\tt\&} symbol}
-\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
-\index{*"-"-"> symbol}
-\index{*"<"-"> symbol}
-\begin{tabular}{rrrr}
- \it symbol & \it meta-type & \it priority & \it description \\
- \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
- \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
- \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
- \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
- \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)
-\end{tabular}
-\end{center}
-\subcaption{Infixes}
-
-\begin{center}
-\begin{tabular}{rrr}
- \it external & \it internal & \it description \\
- \tt $\Gamma$ |- $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) &
- sequent $\Gamma\turn \Delta$
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-\caption{Syntax of {\tt LK}} \label{lk-syntax}
-\end{figure}
-
-
-\begin{figure}
-\dquotes
-\[\begin{array}{rcl}
- prop & = & sequence " |- " sequence
-\\[2ex]
-sequence & = & elem \quad (", " elem)^* \\
- & | & empty
-\\[2ex]
- elem & = & "\$ " term \\
- & | & formula \\
- & | & "<<" sequence ">>"
-\\[2ex]
- formula & = & \hbox{expression of type~$o$} \\
- & | & term " = " term \\
- & | & "\ttilde\ " formula \\
- & | & formula " \& " formula \\
- & | & formula " | " formula \\
- & | & formula " --> " formula \\
- & | & formula " <-> " formula \\
- & | & "ALL~" id~id^* " . " formula \\
- & | & "EX~~" id~id^* " . " formula \\
- & | & "THE~" id~ " . " formula
- \end{array}
-\]
-\caption{Grammar of {\tt LK}} \label{lk-grammar}
-\end{figure}
-
-
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{basic} $H, P, $G |- $E, P, $F
-
-\tdx{contRS} $H |- $E, $S, $S, $F ==> $H |- $E, $S, $F
-\tdx{contLS} $H, $S, $S, $G |- $E ==> $H, $S, $G |- $E
-
-\tdx{thinRS} $H |- $E, $F ==> $H |- $E, $S, $F
-\tdx{thinLS} $H, $G |- $E ==> $H, $S, $G |- $E
-
-\tdx{cut} [| $H |- $E, P; $H, P |- $E |] ==> $H |- $E
-\subcaption{Structural rules}
-
-\tdx{refl} $H |- $E, a=a, $F
-\tdx{subst} $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)
-\subcaption{Equality rules}
-\end{ttbox}
-
-\caption{Basic Rules of {\tt LK}} \label{lk-basic-rules}
-\end{figure}
-
-\begin{figure}
-\begin{ttbox}
-\tdx{True_def} True == False-->False
-\tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)
-
-\tdx{conjR} [| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F
-\tdx{conjL} $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
-
-\tdx{disjR} $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
-\tdx{disjL} [| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
-
-\tdx{impR} $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F
-\tdx{impL} [| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
-
-\tdx{notR} $H, P |- $E, $F ==> $H |- $E, ~P, $F
-\tdx{notL} $H, $G |- $E, P ==> $H, ~P, $G |- $E
-
-\tdx{FalseL} $H, False, $G |- $E
-
-\tdx{allR} (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F
-\tdx{allL} $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E
-
-\tdx{exR} $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F
-\tdx{exL} (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E
-
-\tdx{The} [| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] ==>
- $H |- $E, P(THE x. P(x)), $F
-\subcaption{Logical rules}
-\end{ttbox}
-
-\caption{Rules of {\tt LK}} \label{lk-rules}
-\end{figure}
-
-
-\section{Syntax and rules of inference}
-\index{*sobj type}
-
-Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
-by the representation of sequents. Type $sobj\To sobj$ represents a list
-of formulae.
-
-The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
-satisfying~$P[a]$, if one exists and is unique. Since all terms in LK denote
-something, a description is always meaningful, but we do not know its value
-unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE
- $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not
-entail the Axiom of Choice because it requires uniqueness.
-
-Conditional expressions are available with the notation
-\[ \dquotes
- "if"~formula~"then"~term~"else"~term. \]
-
-Figure~\ref{lk-grammar} presents the grammar of LK. Traditionally,
-\(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's
-notation, the prefix~\verb|$| on a term makes it range over sequences.
-In a sequent, anything not prefixed by \verb|$| is taken as a formula.
-
-The notation \texttt{<<$sequence$>>} stands for a sequence of formul\ae{}.
-For example, you can declare the constant \texttt{imps} to consist of two
-implications:
-\begin{ttbox}
-consts P,Q,R :: o
-constdefs imps :: seq'=>seq'
- "imps == <<P --> Q, Q --> R>>"
-\end{ttbox}
-Then you can use it in axioms and goals, for example
-\begin{ttbox}
-Goalw [imps_def] "P, $imps |- R";
-{\out Level 0}
-{\out P, $imps |- R}
-{\out 1. P, P --> Q, Q --> R |- R}
-by (Fast_tac 1);
-{\out Level 1}
-{\out P, $imps |- R}
-{\out No subgoals!}
-\end{ttbox}
-
-Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory
-\thydx{LK}. The connective $\bimp$ is defined using $\conj$ and $\imp$. The
-axiom for basic sequents is expressed in a form that provides automatic
-thinning: redundant formulae are simply ignored. The other rules are
-expressed in the form most suitable for backward proof; exchange and
-contraction rules are not normally required, although they are provided
-anyway.
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{thinR} $H |- $E, $F ==> $H |- $E, P, $F
-\tdx{thinL} $H, $G |- $E ==> $H, P, $G |- $E
-
-\tdx{contR} $H |- $E, P, P, $F ==> $H |- $E, P, $F
-\tdx{contL} $H, P, P, $G |- $E ==> $H, P, $G |- $E
-
-\tdx{symR} $H |- $E, $F, a=b ==> $H |- $E, b=a, $F
-\tdx{symL} $H, $G, b=a |- $E ==> $H, a=b, $G |- $E
-
-\tdx{transR} [| $H|- $E, $F, a=b; $H|- $E, $F, b=c |]
- ==> $H|- $E, a=c, $F
-
-\tdx{TrueR} $H |- $E, True, $F
-
-\tdx{iffR} [| $H, P |- $E, Q, $F; $H, Q |- $E, P, $F |]
- ==> $H |- $E, P<->Q, $F
-
-\tdx{iffL} [| $H, $G |- $E, P, Q; $H, Q, P, $G |- $E |]
- ==> $H, P<->Q, $G |- $E
-
-\tdx{allL_thin} $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E
-\tdx{exR_thin} $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F
-
-\tdx{the_equality} [| $H |- $E, P(a), $F;
- !!x. $H, P(x) |- $E, x=a, $F |]
- ==> $H |- $E, (THE x. P(x)) = a, $F
-\end{ttbox}
-
-\caption{Derived rules for {\tt LK}} \label{lk-derived}
-\end{figure}
-
-Figure~\ref{lk-derived} presents derived rules, including rules for
-$\bimp$. The weakened quantifier rules discard each quantification after a
-single use; in an automatic proof procedure, they guarantee termination,
-but are incomplete. Multiple use of a quantifier can be obtained by a
-contraction rule, which in backward proof duplicates a formula. The tactic
-{\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
-specifying the formula to duplicate.
-See theory {\tt Sequents/LK0} in the sources for complete listings of
-the rules and derived rules.
-
-To support the simplifier, hundreds of equivalences are proved for
-the logical connectives and for if-then-else expressions. See the file
-\texttt{Sequents/simpdata.ML}.
-
-\section{Automatic Proof}
-
-LK instantiates Isabelle's simplifier. Both equality ($=$) and the
-biconditional ($\bimp$) may be used for rewriting. The tactic
-\texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With
-sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
-required; all the formulae{} in the sequent will be simplified. The left-hand
-formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would
-normally expect from calling \texttt{Asm_full_simp_tac}.)
-
-For classical reasoning, several tactics are available:
-\begin{ttbox}
-Safe_tac : int -> tactic
-Step_tac : int -> tactic
-Fast_tac : int -> tactic
-Best_tac : int -> tactic
-Pc_tac : int -> tactic
-\end{ttbox}
-These refer not to the standard classical reasoner but to a separate one
-provided for the sequent calculus. Two commands are available for adding new
-sequent calculus rules, safe or unsafe, to the default ``theorem pack'':
-\begin{ttbox}
-Add_safes : thm list -> unit
-Add_unsafes : thm list -> unit
-\end{ttbox}
-To control the set of rules for individual invocations, lower-case versions of
-all these primitives are available. Sections~\ref{sec:thm-pack}
-and~\ref{sec:sequent-provers} give full details.
-
-
-\section{Tactics for the cut rule}
-
-According to the cut-elimination theorem, the cut rule can be eliminated
-from proofs of sequents. But the rule is still essential. It can be used
-to structure a proof into lemmas, avoiding repeated proofs of the same
-formula. More importantly, the cut rule cannot be eliminated from
-derivations of rules. For example, there is a trivial cut-free proof of
-the sequent \(P\conj Q\turn Q\conj P\).
-Noting this, we might want to derive a rule for swapping the conjuncts
-in a right-hand formula:
-\[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]
-The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj
-P$. Most cuts directly involve a premise of the rule being derived (a
-meta-assumption). In a few cases, the cut formula is not part of any
-premise, but serves as a bridge between the premises and the conclusion.
-In such proofs, the cut formula is specified by calling an appropriate
-tactic.
-
-\begin{ttbox}
-cutR_tac : string -> int -> tactic
-cutL_tac : string -> int -> tactic
-\end{ttbox}
-These tactics refine a subgoal into two by applying the cut rule. The cut
-formula is given as a string, and replaces some other formula in the sequent.
-\begin{ttdescription}
-\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
- applies the cut rule to subgoal~$i$. It then deletes some formula from the
- right side of subgoal~$i$, replacing that formula by~$P$.
-
-\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
- applies the cut rule to subgoal~$i$. It then deletes some formula from the
- left side of the new subgoal $i+1$, replacing that formula by~$P$.
-\end{ttdescription}
-All the structural rules --- cut, contraction, and thinning --- can be
-applied to particular formulae using {\tt res_inst_tac}.
-
-
-\section{Tactics for sequents}
-\begin{ttbox}
-forms_of_seq : term -> term list
-could_res : term * term -> bool
-could_resolve_seq : term * term -> bool
-filseq_resolve_tac : thm list -> int -> int -> tactic
-\end{ttbox}
-Associative unification is not as efficient as it might be, in part because
-the representation of lists defeats some of Isabelle's internal
-optimisations. The following operations implement faster rule application,
-and may have other uses.
-\begin{ttdescription}
-\item[\ttindexbold{forms_of_seq} {\it t}]
-returns the list of all formulae in the sequent~$t$, removing sequence
-variables.
-
-\item[\ttindexbold{could_res} ($t$,$u$)]
-tests whether two formula lists could be resolved. List $t$ is from a
-premise or subgoal, while $u$ is from the conclusion of an object-rule.
-Assuming that each formula in $u$ is surrounded by sequence variables, it
-checks that each conclusion formula is unifiable (using {\tt could_unify})
-with some subgoal formula.
-
-\item[\ttindexbold{could_resolve_seq} ($t$,$u$)]
- tests whether two sequents could be resolved. Sequent $t$ is a premise
- or subgoal, while $u$ is the conclusion of an object-rule. It simply
- calls {\tt could_res} twice to check that both the left and the right
- sides of the sequents are compatible.
-
-\item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}]
-uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
-applicable to subgoal~$i$. If more than {\it maxr\/} theorems are
-applicable then the tactic fails. Otherwise it calls {\tt resolve_tac}.
-Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
-\end{ttdescription}
-
-
-\section{A simple example of classical reasoning}
-The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
-classical treatment of the existential quantifier. Classical reasoning is
-easy using~LK, as you can see by comparing this proof with the one given in
-the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs
-are essentially the same; the key step here is to use \tdx{exR} rather than
-the weaker~\tdx{exR_thin}.
-\begin{ttbox}
-Goal "|- EX y. ALL x. P(y)-->P(x)";
-{\out Level 0}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. |- EX y. ALL x. P(y) --> P(x)}
-by (resolve_tac [exR] 1);
-{\out Level 1}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
-\end{ttbox}
-There are now two formulae on the right side. Keeping the existential one
-in reserve, we break down the universal one.
-\begin{ttbox}
-by (resolve_tac [allR] 1);
-{\out Level 2}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. !!x. |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
-by (resolve_tac [impR] 1);
-{\out Level 3}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
-\end{ttbox}
-Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
-assumption; instead, it moves to the left side. The resulting subgoal cannot
-be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
-with the unknown~$\Var{x}$.
-\begin{ttbox}
-by (resolve_tac [basic] 1);
-{\out by: tactic failed}
-\end{ttbox}
-We reuse the existential formula using~\tdx{exR_thin}, which discards
-it; we shall not need it a third time. We again break down the resulting
-formula.
-\begin{ttbox}
-by (resolve_tac [exR_thin] 1);
-{\out Level 4}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
-by (resolve_tac [allR] 1);
-{\out Level 5}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
-by (resolve_tac [impR] 1);
-{\out Level 6}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
-\end{ttbox}
-Subgoal~1 seems to offer lots of possibilities. Actually the only useful
-step is instantiating~$\Var{x@7}$ to $\lambda x. x$,
-transforming~$\Var{x@7}(x)$ into~$x$.
-\begin{ttbox}
-by (resolve_tac [basic] 1);
-{\out Level 7}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out No subgoals!}
-\end{ttbox}
-This theorem can be proved automatically. Because it involves quantifier
-duplication, we employ best-first search:
-\begin{ttbox}
-Goal "|- EX y. ALL x. P(y)-->P(x)";
-{\out Level 0}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out 1. |- EX y. ALL x. P(y) --> P(x)}
-by (best_tac LK_dup_pack 1);
-{\out Level 1}
-{\out |- EX y. ALL x. P(y) --> P(x)}
-{\out No subgoals!}
-\end{ttbox}
-
-
-
-\section{A more complex proof}
-Many of Pelletier's test problems for theorem provers \cite{pelletier86}
-can be solved automatically. Problem~39 concerns set theory, asserting
-that there is no Russell set --- a set consisting of those sets that are
-not members of themselves:
-\[ \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
-This does not require special properties of membership; we may generalize
-$x\in y$ to an arbitrary predicate~$F(x,y)$. The theorem, which is trivial
-for \texttt{Fast_tac}, has a short manual proof. See the directory {\tt
- Sequents/LK} for many more examples.
-
-We set the main goal and move the negated formula to the left.
-\begin{ttbox}
-Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
-{\out Level 0}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-by (resolve_tac [notR] 1);
-{\out Level 1}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
-\end{ttbox}
-The right side is empty; we strip both quantifiers from the formula on the
-left.
-\begin{ttbox}
-by (resolve_tac [exL] 1);
-{\out Level 2}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
-by (resolve_tac [allL_thin] 1);
-{\out Level 3}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
-\end{ttbox}
-The rule \tdx{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
-both true or both false. It yields two subgoals.
-\begin{ttbox}
-by (resolve_tac [iffL] 1);
-{\out Level 4}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
-{\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
-\end{ttbox}
-We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
-subgoals. Beginning with subgoal~2, we move a negated formula to the left
-and create a basic sequent.
-\begin{ttbox}
-by (resolve_tac [notL] 2);
-{\out Level 5}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
-{\out 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
-by (resolve_tac [basic] 2);
-{\out Level 6}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. |- F(x,x), ~ F(x,x)}
-\end{ttbox}
-Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
-\begin{ttbox}
-by (resolve_tac [notR] 1);
-{\out Level 7}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out 1. !!x. F(x,x) |- F(x,x)}
-by (resolve_tac [basic] 1);
-{\out Level 8}
-{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
-{\out No subgoals!}
-\end{ttbox}
-
-\section{*Unification for lists}\label{sec:assoc-unification}
-
-Higher-order unification includes associative unification as a special
-case, by an encoding that involves function composition
-\cite[page~37]{huet78}. To represent lists, let $C$ be a new constant.
-The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is
-represented by
-\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))). \]
-The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
-of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
-
-Unlike orthodox associative unification, this technique can represent certain
-infinite sets of unifiers by flex-flex equations. But note that the term
-$\lambda x. C(t,\Var{a})$ does not represent any list. Flex-flex constraints
-containing such garbage terms may accumulate during a proof.
-\index{flex-flex constraints}
-
-This technique lets Isabelle formalize sequent calculus rules,
-where the comma is the associative operator:
-\[ \infer[(\conj\hbox{-left})]
- {\Gamma,P\conj Q,\Delta \turn \Theta}
- {\Gamma,P,Q,\Delta \turn \Theta} \]
-Multiple unifiers occur whenever this is resolved against a goal containing
-more than one conjunction on the left.
-
-LK exploits this representation of lists. As an alternative, the sequent
-calculus can be formalized using an ordinary representation of lists, with a
-logic program for removing a formula from a list. Amy Felty has applied this
-technique using the language $\lambda$Prolog~\cite{felty91a}.
-
-Explicit formalization of sequents can be tiresome. But it gives precise
-control over contraction and weakening, and is essential to handle relevant
-and linear logics.
-
-
-\section{*Packaging sequent rules}\label{sec:thm-pack}
-
-The sequent calculi come with simple proof procedures. These are incomplete
-but are reasonably powerful for interactive use. They expect rules to be
-classified as \textbf{safe} or \textbf{unsafe}. A rule is safe if applying it to a
-provable goal always yields provable subgoals. If a rule is safe then it can
-be applied automatically to a goal without destroying our chances of finding a
-proof. For instance, all the standard rules of the classical sequent calculus
-{\sc lk} are safe. An unsafe rule may render the goal unprovable; typical
-examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.
-
-Proof procedures use safe rules whenever possible, using an unsafe rule as a
-last resort. Those safe rules are preferred that generate the fewest
-subgoals. Safe rules are (by definition) deterministic, while the unsafe
-rules require a search strategy, such as backtracking.
-
-A \textbf{pack} is a pair whose first component is a list of safe rules and
-whose second is a list of unsafe rules. Packs can be extended in an obvious
-way to allow reasoning with various collections of rules. For clarity, LK
-declares \mltydx{pack} as an \ML{} datatype, although is essentially a type
-synonym:
-\begin{ttbox}
-datatype pack = Pack of thm list * thm list;
-\end{ttbox}
-Pattern-matching using constructor {\tt Pack} can inspect a pack's
-contents. Packs support the following operations:
-\begin{ttbox}
-pack : unit -> pack
-pack_of : theory -> pack
-empty_pack : pack
-prop_pack : pack
-LK_pack : pack
-LK_dup_pack : pack
-add_safes : pack * thm list -> pack \hfill\textbf{infix 4}
-add_unsafes : pack * thm list -> pack \hfill\textbf{infix 4}
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{pack}] returns the pack attached to the current theory.
-
-\item[\ttindexbold{pack_of $thy$}] returns the pack attached to theory $thy$.
-
-\item[\ttindexbold{empty_pack}] is the empty pack.
-
-\item[\ttindexbold{prop_pack}] contains the propositional rules, namely
-those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the
-rules {\tt basic} and {\tt refl}. These are all safe.
-
-\item[\ttindexbold{LK_pack}]
-extends {\tt prop_pack} with the safe rules {\tt allR}
-and~{\tt exL} and the unsafe rules {\tt allL_thin} and
-{\tt exR_thin}. Search using this is incomplete since quantified
-formulae are used at most once.
-
-\item[\ttindexbold{LK_dup_pack}]
-extends {\tt prop_pack} with the safe rules {\tt allR}
-and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.
-Search using this is complete, since quantified formulae may be reused, but
-frequently fails to terminate. It is generally unsuitable for depth-first
-search.
-
-\item[$pack$ \ttindexbold{add_safes} $rules$]
-adds some safe~$rules$ to the pack~$pack$.
-
-\item[$pack$ \ttindexbold{add_unsafes} $rules$]
-adds some unsafe~$rules$ to the pack~$pack$.
-\end{ttdescription}
-
-
-\section{*Proof procedures}\label{sec:sequent-provers}
-
-The LK proof procedure is similar to the classical reasoner described in
-\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
- {Chap.\ts\ref{chap:classical}}.
-%
-In fact it is simpler, since it works directly with sequents rather than
-simulating them. There is no need to distinguish introduction rules from
-elimination rules, and of course there is no swap rule. As always,
-Isabelle's classical proof procedures are less powerful than resolution
-theorem provers. But they are more natural and flexible, working with an
-open-ended set of rules.
-
-Backtracking over the choice of a safe rule accomplishes nothing: applying
-them in any order leads to essentially the same result. Backtracking may
-be necessary over basic sequents when they perform unification. Suppose
-that~0, 1, 2,~3 are constants in the subgoals
-\[ \begin{array}{c}
- P(0), P(1), P(2) \turn P(\Var{a}) \\
- P(0), P(2), P(3) \turn P(\Var{a}) \\
- P(1), P(3), P(2) \turn P(\Var{a})
- \end{array}
-\]
-The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,
-and this can only be discovered by search. The tactics given below permit
-backtracking only over axioms, such as {\tt basic} and {\tt refl};
-otherwise they are deterministic.
-
-
-\subsection{Method A}
-\begin{ttbox}
-reresolve_tac : thm list -> int -> tactic
-repeat_goal_tac : pack -> int -> tactic
-pc_tac : pack -> int -> tactic
-\end{ttbox}
-These tactics use a method developed by Philippe de Groote. A subgoal is
-refined and the resulting subgoals are attempted in reverse order. For
-some reason, this is much faster than attempting the subgoals in order.
-The method is inherently depth-first.
-
-At present, these tactics only work for rules that have no more than two
-premises. They fail --- return no next state --- if they can do nothing.
-\begin{ttdescription}
-\item[\ttindexbold{reresolve_tac} $thms$ $i$]
-repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
-
-\item[\ttindexbold{repeat_goal_tac} $pack$ $i$]
-applies the safe rules in the pack to a goal and the resulting subgoals.
-If no safe rule is applicable then it applies an unsafe rule and continues.
-
-\item[\ttindexbold{pc_tac} $pack$ $i$]
-applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
-\end{ttdescription}
-
-
-\subsection{Method B}
-\begin{ttbox}
-safe_tac : pack -> int -> tactic
-step_tac : pack -> int -> tactic
-fast_tac : pack -> int -> tactic
-best_tac : pack -> int -> tactic
-\end{ttbox}
-These tactics are analogous to those of the generic classical
-reasoner. They use `Method~A' only on safe rules. They fail if they
-can do nothing.
-\begin{ttdescription}
-\item[\ttindexbold{safe_goal_tac} $pack$ $i$]
-applies the safe rules in the pack to a goal and the resulting subgoals.
-It ignores the unsafe rules.
-
-\item[\ttindexbold{step_tac} $pack$ $i$]
-either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
-rule.
-
-\item[\ttindexbold{fast_tac} $pack$ $i$]
-applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
-Despite its name, it is frequently slower than {\tt pc_tac}.
-
-\item[\ttindexbold{best_tac} $pack$ $i$]
-applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
-particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
-\end{ttdescription}
-
-
-
-\index{sequent calculus|)}
--- a/doc-src/Logics/Makefile Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = logics
-FILES = logics.tex preface.tex syntax.tex LK.tex Sequents.tex CTT.tex \
- ../proof.sty ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle.eps
- $(LATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(LATEX) $(NAME)
- $(LATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle.pdf
- $(PDFLATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(FIXBOOKMARKS) $(NAME).out
- $(PDFLATEX) $(NAME)
--- a/doc-src/Logics/Sequents.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,200 +0,0 @@
-\chapter{Defining A Sequent-Based Logic}
-\label{chap:sequents}
-
-\underscoreon %this file contains the @ character
-
-The Isabelle theory \texttt{Sequents.thy} provides facilities for using
-sequent notation in users' object logics. This theory allows users to
-easily interface the surface syntax of sequences with an underlying
-representation suitable for higher-order unification.
-
-\section{Concrete syntax of sequences}
-
-Mathematicians and logicians have used sequences in an informal way
-much before proof systems such as Isabelle were created. It seems
-sensible to allow people using Isabelle to express sequents and
-perform proofs in this same informal way, and without requiring the
-theory developer to spend a lot of time in \ML{} programming.
-
-By using {\tt Sequents.thy}
-appropriately, a logic developer can allow users to refer to sequences
-in several ways:
-%
-\begin{itemize}
-\item A sequence variable is any alphanumeric string with the first
- character being a \verb%$% sign.
-So, consider the sequent \verb%$A |- B%, where \verb%$A%
-is intended to match a sequence of zero or more items.
-
-\item A sequence with unspecified sub-sequences and unspecified or
-individual items is written as a comma-separated list of regular
-variables (representing items), particular items, and
-sequence variables, as in
-\begin{ttbox}
-$A, B, C, $D(x) |- E
-\end{ttbox}
-Here both \verb%$A% and \verb%$D(x)%
-are allowed to match any subsequences of items on either side of the
-two items that match $B$ and $C$. Moreover, the sequence matching
-\verb%$D(x)% may contain occurrences of~$x$.
-
-\item An empty sequence can be represented by a blank space, as in
-\verb? |- true?.
-\end{itemize}
-
-These syntactic constructs need to be assimilated into the object
-theory being developed. The type that we use for these visible objects
-is given the name {\tt seq}.
-A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
-{\tt seqobj} followed by a {\tt seq}, with a comma between them. A
-{\tt seqobj} is either an item or a variable representing a
-sequence. Thus, a theory designer can specify a function that takes
-two sequences and returns a meta-level proposition by giving it the
-Isabelle type \verb|[seq, seq] => prop|.
-
-This is all part of the concrete syntax, but one may wish to
-exploit Isabelle's higher-order abstract syntax by actually having a
-different, more powerful {\em internal} syntax.
-
-
-
-\section{ Basis}
-
-One could opt to represent sequences as first-order objects (such as
-simple lists), but this would not allow us to use many facilities
-Isabelle provides for matching. By using a slightly more complex
-representation, users of the logic can reap many benefits in
-facilities for proofs and ease of reading logical terms.
-
-A sequence can be represented as a function --- a constructor for
-further sequences --- by defining a binary {\em abstract} function
-\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
-sequence such as \verb|A, B, C| into
-\begin{ttbox}
-\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))
-\end{ttbox}
-This sequence can therefore be seen as a constructor
-for further sequences. The constructor \verb|Seq0'| is never given a
-value, and therefore it is not possible to evaluate this expression
-into a basic value.
-
-Furthermore, if we want to represent the sequence \verb|A, $B, C|,
-we note that \verb|$B| already represents a sequence, so we can use
-\verb|B| itself to refer to the function, and therefore the sequence
-can be mapped to the internal form:
-\verb|%s. SeqO'(A, B(SeqO'(C, s)))|.
-
-So, while we wish to continue with the standard, well-liked {\em
-external} representation of sequences, we can represent them {\em
-internally} as functions of type \verb|seq'=>seq'|.
-
-
-\section{Object logics}
-
-Recall that object logics are defined by mapping elements of
-particular types to the Isabelle type \verb|prop|, usually with a
-function called {\tt Trueprop}. So, an object
-logic proposition {\tt P} is matched to the Isabelle proposition
-{\tt Trueprop(P)}\@. The name of the function is often hidden, so the
-user just sees {\tt P}\@. Isabelle is eager to make types match, so it
-inserts {\tt Trueprop} automatically when an object of type {\tt prop}
-is expected. This mechanism can be observed in most of the object
-logics which are direct descendants of {\tt Pure}.
-
-In order to provide the desired syntactic facilities for sequent
-calculi, rather than use just one function that maps object-level
-propositions to meta-level propositions, we use two functions, and
-separate internal from the external representation.
-
-These functions need to be given a type that is appropriate for the particular
-form of sequents required: single or multiple conclusions. So
-multiple-conclusion sequents (used in the LK logic) can be
-specified by the following two definitions, which are lifted from the inbuilt
-{\tt Sequents/LK.thy}:
-\begin{ttbox}
- Trueprop :: two_seqi
- "@Trueprop" :: two_seqe ("((_)/ |- (_))" [6,6] 5)
-\end{ttbox}
-%
-where the types used are defined in {\tt Sequents.thy} as
-abbreviations:
-\begin{ttbox}
- two_seqi = [seq'=>seq', seq'=>seq'] => prop
- two_seqe = [seq, seq] => prop
-\end{ttbox}
-
-The next step is to actually create links into the low-level parsing
-and pretty-printing mechanisms, which map external and internal
-representations. These functions go below the user level and capture
-the underlying structure of Isabelle terms in \ML{}\@. Fortunately the
-theory developer need not delve in this level; {\tt Sequents.thy}
-provides the necessary facilities. All the theory developer needs to
-add in the \ML{} section is a specification of the two translation
-functions:
-\begin{ttbox}
-ML
-val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
-val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
-\end{ttbox}
-
-In summary: in the logic theory being developed, the developer needs
-to specify the types for the internal and external representation of
-the sequences, and use the appropriate parsing and pretty-printing
-functions.
-
-\section{What's in \texttt{Sequents.thy}}
-
-Theory \texttt{Sequents.thy} makes many declarations that you need to know
-about:
-\begin{enumerate}
-\item The Isabelle types given below, which can be used for the
-constants that map object-level sequents and meta-level propositions:
-%
-\begin{ttbox}
- single_seqe = [seq,seqobj] => prop
- single_seqi = [seq'=>seq',seq'=>seq'] => prop
- two_seqi = [seq'=>seq', seq'=>seq'] => prop
- two_seqe = [seq, seq] => prop
- three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- three_seqe = [seq, seq, seq] => prop
- four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
- four_seqe = [seq, seq, seq, seq] => prop
-\end{ttbox}
-
-The \verb|single_| and \verb|two_| sets of mappings for internal and
-external representations are the ones used for, say single and
-multiple conclusion sequents. The other functions are provided to
-allow rules that manipulate more than two functions, as can be seen in
-the inbuilt object logics.
-
-\item An auxiliary syntactic constant has been
-defined that directly maps a sequence to its internal representation:
-\begin{ttbox}
-"@Side" :: seq=>(seq'=>seq') ("<<(_)>>")
-\end{ttbox}
-Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this
-syntax, it is translated into the appropriate internal representation. This
-form can be used only where a sequence is expected.
-
-\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},
- \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the
- translation from external to internal form. Analogously there are
- \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
- \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from
- internal to external form. These functions can be used in the \ML{} section
- of a theory file to specify the translations to be used. As an example of
- use, note that in {\tt LK.thy} we declare two identifiers:
-\begin{ttbox}
-val parse_translation =
- [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
-val print_translation =
- [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
-\end{ttbox}
-The given parse translation will be applied whenever a \verb|@Trueprop|
-constant is found, translating using \verb|two_seq_tr| and inserting the
-constant \verb|Trueprop|. The pretty-printing translation is applied
-analogously; a term that contains \verb|Trueprop| is printed as a
-\verb|@Trueprop|.
-\end{enumerate}
-
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/CTT.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,1257 @@
+\chapter{Constructive Type Theory}
+\index{Constructive Type Theory|(}
+
+\underscoreoff %this file contains _ in rule names
+
+Martin-L\"of's Constructive Type Theory \cite{martinlof84,nordstrom90} can
+be viewed at many different levels. It is a formal system that embodies
+the principles of intuitionistic mathematics; it embodies the
+interpretation of propositions as types; it is a vehicle for deriving
+programs from proofs.
+
+Thompson's book~\cite{thompson91} gives a readable and thorough account of
+Type Theory. Nuprl is an elaborate implementation~\cite{constable86}.
+{\sc alf} is a more recent tool that allows proof terms to be edited
+directly~\cite{alf}.
+
+Isabelle's original formulation of Type Theory was a kind of sequent
+calculus, following Martin-L\"of~\cite{martinlof84}. It included rules for
+building the context, namely variable bindings with their types. A typical
+judgement was
+\[ a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n) \;
+ [ x@1\in A@1, x@2\in A@2(x@1), \ldots, x@n\in A@n(x@1,\ldots,x@{n-1}) ]
+\]
+This sequent calculus was not satisfactory because assumptions like
+`suppose $A$ is a type' or `suppose $B(x)$ is a type for all $x$ in $A$'
+could not be formalized.
+
+The theory~\thydx{CTT} implements Constructive Type Theory, using
+natural deduction. The judgement above is expressed using $\Forall$ and
+$\Imp$:
+\[ \begin{array}{r@{}l}
+ \Forall x@1\ldots x@n. &
+ \List{x@1\in A@1;
+ x@2\in A@2(x@1); \cdots \;
+ x@n\in A@n(x@1,\ldots,x@{n-1})} \Imp \\
+ & \qquad\qquad a(x@1,\ldots,x@n)\in A(x@1,\ldots,x@n)
+ \end{array}
+\]
+Assumptions can use all the judgement forms, for instance to express that
+$B$ is a family of types over~$A$:
+\[ \Forall x . x\in A \Imp B(x)\;{\rm type} \]
+To justify the CTT formulation it is probably best to appeal directly to the
+semantic explanations of the rules~\cite{martinlof84}, rather than to the
+rules themselves. The order of assumptions no longer matters, unlike in
+standard Type Theory. Contexts, which are typical of many modern type
+theories, are difficult to represent in Isabelle. In particular, it is
+difficult to enforce that all the variables in a context are distinct.
+\index{assumptions!in CTT}
+
+The theory does not use polymorphism. Terms in CTT have type~\tydx{i}, the
+type of individuals. Types in CTT have type~\tydx{t}.
+
+\begin{figure} \tabcolsep=1em %wider spacing in tables
+\begin{center}
+\begin{tabular}{rrr}
+ \it name & \it meta-type & \it description \\
+ \cdx{Type} & $t \to prop$ & judgement form \\
+ \cdx{Eqtype} & $[t,t]\to prop$ & judgement form\\
+ \cdx{Elem} & $[i, t]\to prop$ & judgement form\\
+ \cdx{Eqelem} & $[i, i, t]\to prop$ & judgement form\\
+ \cdx{Reduce} & $[i, i]\to prop$ & extra judgement form\\[2ex]
+
+ \cdx{N} & $t$ & natural numbers type\\
+ \cdx{0} & $i$ & constructor\\
+ \cdx{succ} & $i\to i$ & constructor\\
+ \cdx{rec} & $[i,i,[i,i]\to i]\to i$ & eliminator\\[2ex]
+ \cdx{Prod} & $[t,i\to t]\to t$ & general product type\\
+ \cdx{lambda} & $(i\to i)\to i$ & constructor\\[2ex]
+ \cdx{Sum} & $[t, i\to t]\to t$ & general sum type\\
+ \cdx{pair} & $[i,i]\to i$ & constructor\\
+ \cdx{split} & $[i,[i,i]\to i]\to i$ & eliminator\\
+ \cdx{fst} \cdx{snd} & $i\to i$ & projections\\[2ex]
+ \cdx{inl} \cdx{inr} & $i\to i$ & constructors for $+$\\
+ \cdx{when} & $[i,i\to i, i\to i]\to i$ & eliminator for $+$\\[2ex]
+ \cdx{Eq} & $[t,i,i]\to t$ & equality type\\
+ \cdx{eq} & $i$ & constructor\\[2ex]
+ \cdx{F} & $t$ & empty type\\
+ \cdx{contr} & $i\to i$ & eliminator\\[2ex]
+ \cdx{T} & $t$ & singleton type\\
+ \cdx{tt} & $i$ & constructor
+\end{tabular}
+\end{center}
+\caption{The constants of CTT} \label{ctt-constants}
+\end{figure}
+
+
+CTT supports all of Type Theory apart from list types, well-ordering types,
+and universes. Universes could be introduced {\em\`a la Tarski}, adding new
+constants as names for types. The formulation {\em\`a la Russell}, where
+types denote themselves, is only possible if we identify the meta-types~{\tt
+ i} and~{\tt t}. Most published formulations of well-ordering types have
+difficulties involving extensionality of functions; I suggest that you use
+some other method for defining recursive types. List types are easy to
+introduce by declaring new rules.
+
+CTT uses the 1982 version of Type Theory, with extensional equality. The
+computation $a=b\in A$ and the equality $c\in Eq(A,a,b)$ are interchangeable.
+Its rewriting tactics prove theorems of the form $a=b\in A$. It could be
+modified to have intensional equality, but rewriting tactics would have to
+prove theorems of the form $c\in Eq(A,a,b)$ and the computation rules might
+require a separate simplifier.
+
+
+\begin{figure} \tabcolsep=1em %wider spacing in tables
+\index{lambda abs@$\lambda$-abstractions!in CTT}
+\begin{center}
+\begin{tabular}{llrrr}
+ \it symbol &\it name &\it meta-type & \it priority & \it description \\
+ \sdx{lam} & \cdx{lambda} & $(i\To o)\To i$ & 10 & $\lambda$-abstraction
+\end{tabular}
+\end{center}
+\subcaption{Binders}
+
+\begin{center}
+\index{*"` symbol}\index{function applications!in CTT}
+\index{*"+ symbol}
+\begin{tabular}{rrrr}
+ \it symbol & \it meta-type & \it priority & \it description \\
+ \tt ` & $[i,i]\to i$ & Left 55 & function application\\
+ \tt + & $[t,t]\to t$ & Right 30 & sum of two types
+\end{tabular}
+\end{center}
+\subcaption{Infixes}
+
+\index{*"* symbol}
+\index{*"-"-"> symbol}
+\begin{center} \tt\frenchspacing
+\begin{tabular}{rrr}
+ \it external & \it internal & \it standard notation \\
+ \sdx{PROD} $x$:$A$ . $B[x]$ & Prod($A$, $\lambda x. B[x]$) &
+ \rm product $\prod@{x\in A}B[x]$ \\
+ \sdx{SUM} $x$:$A$ . $B[x]$ & Sum($A$, $\lambda x. B[x]$) &
+ \rm sum $\sum@{x\in A}B[x]$ \\
+ $A$ --> $B$ & Prod($A$, $\lambda x. B$) &
+ \rm function space $A\to B$ \\
+ $A$ * $B$ & Sum($A$, $\lambda x. B$) &
+ \rm binary product $A\times B$
+\end{tabular}
+\end{center}
+\subcaption{Translations}
+
+\index{*"= symbol}
+\begin{center}
+\dquotes
+\[ \begin{array}{rcl}
+prop & = & type " type" \\
+ & | & type " = " type \\
+ & | & term " : " type \\
+ & | & term " = " term " : " type
+\\[2ex]
+type & = & \hbox{expression of type~$t$} \\
+ & | & "PROD~" id " : " type " . " type \\
+ & | & "SUM~~" id " : " type " . " type
+\\[2ex]
+term & = & \hbox{expression of type~$i$} \\
+ & | & "lam " id~id^* " . " term \\
+ & | & "< " term " , " term " >"
+\end{array}
+\]
+\end{center}
+\subcaption{Grammar}
+\caption{Syntax of CTT} \label{ctt-syntax}
+\end{figure}
+
+%%%%\section{Generic Packages} typedsimp.ML????????????????
+
+
+\section{Syntax}
+The constants are shown in Fig.\ts\ref{ctt-constants}. The infixes include
+the function application operator (sometimes called `apply'), and the 2-place
+type operators. Note that meta-level abstraction and application, $\lambda
+x.b$ and $f(a)$, differ from object-level abstraction and application,
+\hbox{\tt lam $x$. $b$} and $b{\tt`}a$. A CTT function~$f$ is simply an
+individual as far as Isabelle is concerned: its Isabelle type is~$i$, not say
+$i\To i$.
+
+The notation for~CTT (Fig.\ts\ref{ctt-syntax}) is based on that of Nordstr\"om
+et al.~\cite{nordstrom90}. The empty type is called $F$ and the one-element
+type is $T$; other finite types are built as $T+T+T$, etc.
+
+\index{*SUM symbol}\index{*PROD symbol}
+Quantification is expressed by sums $\sum@{x\in A}B[x]$ and
+products $\prod@{x\in A}B[x]$. Instead of {\tt Sum($A$,$B$)} and {\tt
+ Prod($A$,$B$)} we may write \hbox{\tt SUM $x$:$A$.\ $B[x]$} and \hbox{\tt
+ PROD $x$:$A$.\ $B[x]$}. For example, we may write
+\begin{ttbox}
+SUM y:B. PROD x:A. C(x,y) {\rm for} Sum(B, \%y. Prod(A, \%x. C(x,y)))
+\end{ttbox}
+The special cases as \hbox{\tt$A$*$B$} and \hbox{\tt$A$-->$B$} abbreviate
+general sums and products over a constant family.\footnote{Unlike normal
+infix operators, {\tt*} and {\tt-->} merely define abbreviations; there are
+no constants~{\tt op~*} and~\hbox{\tt op~-->}.} Isabelle accepts these
+abbreviations in parsing and uses them whenever possible for printing.
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{refl_type} A type ==> A = A
+\tdx{refl_elem} a : A ==> a = a : A
+
+\tdx{sym_type} A = B ==> B = A
+\tdx{sym_elem} a = b : A ==> b = a : A
+
+\tdx{trans_type} [| A = B; B = C |] ==> A = C
+\tdx{trans_elem} [| a = b : A; b = c : A |] ==> a = c : A
+
+\tdx{equal_types} [| a : A; A = B |] ==> a : B
+\tdx{equal_typesL} [| a = b : A; A = B |] ==> a = b : B
+
+\tdx{subst_type} [| a : A; !!z. z:A ==> B(z) type |] ==> B(a) type
+\tdx{subst_typeL} [| a = c : A; !!z. z:A ==> B(z) = D(z)
+ |] ==> B(a) = D(c)
+
+\tdx{subst_elem} [| a : A; !!z. z:A ==> b(z):B(z) |] ==> b(a):B(a)
+\tdx{subst_elemL} [| a = c : A; !!z. z:A ==> b(z) = d(z) : B(z)
+ |] ==> b(a) = d(c) : B(a)
+
+\tdx{refl_red} Reduce(a,a)
+\tdx{red_if_equal} a = b : A ==> Reduce(a,b)
+\tdx{trans_red} [| a = b : A; Reduce(b,c) |] ==> a = c : A
+\end{ttbox}
+\caption{General equality rules} \label{ctt-equality}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{NF} N type
+
+\tdx{NI0} 0 : N
+\tdx{NI_succ} a : N ==> succ(a) : N
+\tdx{NI_succL} a = b : N ==> succ(a) = succ(b) : N
+
+\tdx{NE} [| p: N; a: C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
+ |] ==> rec(p, a, \%u v. b(u,v)) : C(p)
+
+\tdx{NEL} [| p = q : N; a = c : C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v)=d(u,v): C(succ(u))
+ |] ==> rec(p, a, \%u v. b(u,v)) = rec(q,c,d) : C(p)
+
+\tdx{NC0} [| a: C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
+ |] ==> rec(0, a, \%u v. b(u,v)) = a : C(0)
+
+\tdx{NC_succ} [| p: N; a: C(0);
+ !!u v. [| u: N; v: C(u) |] ==> b(u,v): C(succ(u))
+ |] ==> rec(succ(p), a, \%u v. b(u,v)) =
+ b(p, rec(p, a, \%u v. b(u,v))) : C(succ(p))
+
+\tdx{zero_ne_succ} [| a: N; 0 = succ(a) : N |] ==> 0: F
+\end{ttbox}
+\caption{Rules for type~$N$} \label{ctt-N}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{ProdF} [| A type; !!x. x:A ==> B(x) type |] ==> PROD x:A. B(x) type
+\tdx{ProdFL} [| A = C; !!x. x:A ==> B(x) = D(x) |] ==>
+ PROD x:A. B(x) = PROD x:C. D(x)
+
+\tdx{ProdI} [| A type; !!x. x:A ==> b(x):B(x)
+ |] ==> lam x. b(x) : PROD x:A. B(x)
+\tdx{ProdIL} [| A type; !!x. x:A ==> b(x) = c(x) : B(x)
+ |] ==> lam x. b(x) = lam x. c(x) : PROD x:A. B(x)
+
+\tdx{ProdE} [| p : PROD x:A. B(x); a : A |] ==> p`a : B(a)
+\tdx{ProdEL} [| p=q: PROD x:A. B(x); a=b : A |] ==> p`a = q`b : B(a)
+
+\tdx{ProdC} [| a : A; !!x. x:A ==> b(x) : B(x)
+ |] ==> (lam x. b(x)) ` a = b(a) : B(a)
+
+\tdx{ProdC2} p : PROD x:A. B(x) ==> (lam x. p`x) = p : PROD x:A. B(x)
+\end{ttbox}
+\caption{Rules for the product type $\prod\sb{x\in A}B[x]$} \label{ctt-prod}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{SumF} [| A type; !!x. x:A ==> B(x) type |] ==> SUM x:A. B(x) type
+\tdx{SumFL} [| A = C; !!x. x:A ==> B(x) = D(x)
+ |] ==> SUM x:A. B(x) = SUM x:C. D(x)
+
+\tdx{SumI} [| a : A; b : B(a) |] ==> <a,b> : SUM x:A. B(x)
+\tdx{SumIL} [| a=c:A; b=d:B(a) |] ==> <a,b> = <c,d> : SUM x:A. B(x)
+
+\tdx{SumE} [| p: SUM x:A. B(x);
+ !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
+ |] ==> split(p, \%x y. c(x,y)) : C(p)
+
+\tdx{SumEL} [| p=q : SUM x:A. B(x);
+ !!x y. [| x:A; y:B(x) |] ==> c(x,y)=d(x,y): C(<x,y>)
+ |] ==> split(p, \%x y. c(x,y)) = split(q, \%x y. d(x,y)) : C(p)
+
+\tdx{SumC} [| a: A; b: B(a);
+ !!x y. [| x:A; y:B(x) |] ==> c(x,y): C(<x,y>)
+ |] ==> split(<a,b>, \%x y. c(x,y)) = c(a,b) : C(<a,b>)
+
+\tdx{fst_def} fst(a) == split(a, \%x y. x)
+\tdx{snd_def} snd(a) == split(a, \%x y. y)
+\end{ttbox}
+\caption{Rules for the sum type $\sum\sb{x\in A}B[x]$} \label{ctt-sum}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{PlusF} [| A type; B type |] ==> A+B type
+\tdx{PlusFL} [| A = C; B = D |] ==> A+B = C+D
+
+\tdx{PlusI_inl} [| a : A; B type |] ==> inl(a) : A+B
+\tdx{PlusI_inlL} [| a = c : A; B type |] ==> inl(a) = inl(c) : A+B
+
+\tdx{PlusI_inr} [| A type; b : B |] ==> inr(b) : A+B
+\tdx{PlusI_inrL} [| A type; b = d : B |] ==> inr(b) = inr(d) : A+B
+
+\tdx{PlusE} [| p: A+B;
+ !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y))
+ |] ==> when(p, \%x. c(x), \%y. d(y)) : C(p)
+
+\tdx{PlusEL} [| p = q : A+B;
+ !!x. x: A ==> c(x) = e(x) : C(inl(x));
+ !!y. y: B ==> d(y) = f(y) : C(inr(y))
+ |] ==> when(p, \%x. c(x), \%y. d(y)) =
+ when(q, \%x. e(x), \%y. f(y)) : C(p)
+
+\tdx{PlusC_inl} [| a: A;
+ !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y))
+ |] ==> when(inl(a), \%x. c(x), \%y. d(y)) = c(a) : C(inl(a))
+
+\tdx{PlusC_inr} [| b: B;
+ !!x. x:A ==> c(x): C(inl(x));
+ !!y. y:B ==> d(y): C(inr(y))
+ |] ==> when(inr(b), \%x. c(x), \%y. d(y)) = d(b) : C(inr(b))
+\end{ttbox}
+\caption{Rules for the binary sum type $A+B$} \label{ctt-plus}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{FF} F type
+\tdx{FE} [| p: F; C type |] ==> contr(p) : C
+\tdx{FEL} [| p = q : F; C type |] ==> contr(p) = contr(q) : C
+
+\tdx{TF} T type
+\tdx{TI} tt : T
+\tdx{TE} [| p : T; c : C(tt) |] ==> c : C(p)
+\tdx{TEL} [| p = q : T; c = d : C(tt) |] ==> c = d : C(p)
+\tdx{TC} p : T ==> p = tt : T)
+\end{ttbox}
+
+\caption{Rules for types $F$ and $T$} \label{ctt-ft}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{EqF} [| A type; a : A; b : A |] ==> Eq(A,a,b) type
+\tdx{EqFL} [| A=B; a=c: A; b=d : A |] ==> Eq(A,a,b) = Eq(B,c,d)
+\tdx{EqI} a = b : A ==> eq : Eq(A,a,b)
+\tdx{EqE} p : Eq(A,a,b) ==> a = b : A
+\tdx{EqC} p : Eq(A,a,b) ==> p = eq : Eq(A,a,b)
+\end{ttbox}
+\caption{Rules for the equality type $Eq(A,a,b)$} \label{ctt-eq}
+\end{figure}
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{replace_type} [| B = A; a : A |] ==> a : B
+\tdx{subst_eqtyparg} [| a=c : A; !!z. z:A ==> B(z) type |] ==> B(a)=B(c)
+
+\tdx{subst_prodE} [| p: Prod(A,B); a: A; !!z. z: B(a) ==> c(z): C(z)
+ |] ==> c(p`a): C(p`a)
+
+\tdx{SumIL2} [| c=a : A; d=b : B(a) |] ==> <c,d> = <a,b> : Sum(A,B)
+
+\tdx{SumE_fst} p : Sum(A,B) ==> fst(p) : A
+
+\tdx{SumE_snd} [| p: Sum(A,B); A type; !!x. x:A ==> B(x) type
+ |] ==> snd(p) : B(fst(p))
+\end{ttbox}
+
+\caption{Derived rules for CTT} \label{ctt-derived}
+\end{figure}
+
+
+\section{Rules of inference}
+The rules obey the following naming conventions. Type formation rules have
+the suffix~{\tt F}\@. Introduction rules have the suffix~{\tt I}\@.
+Elimination rules have the suffix~{\tt E}\@. Computation rules, which
+describe the reduction of eliminators, have the suffix~{\tt C}\@. The
+equality versions of the rules (which permit reductions on subterms) are
+called {\bf long} rules; their names have the suffix~{\tt L}\@.
+Introduction and computation rules are often further suffixed with
+constructor names.
+
+Figure~\ref{ctt-equality} presents the equality rules. Most of them are
+straightforward: reflexivity, symmetry, transitivity and substitution. The
+judgement \cdx{Reduce} does not belong to Type Theory proper; it has
+been added to implement rewriting. The judgement ${\tt Reduce}(a,b)$ holds
+when $a=b:A$ holds. It also holds when $a$ and $b$ are syntactically
+identical, even if they are ill-typed, because rule {\tt refl_red} does
+not verify that $a$ belongs to $A$.
+
+The {\tt Reduce} rules do not give rise to new theorems about the standard
+judgements. The only rule with {\tt Reduce} in a premise is
+{\tt trans_red}, whose other premise ensures that $a$ and~$b$ (and thus
+$c$) are well-typed.
+
+Figure~\ref{ctt-N} presents the rules for~$N$, the type of natural numbers.
+They include \tdx{zero_ne_succ}, which asserts $0\not=n+1$. This is
+the fourth Peano axiom and cannot be derived without universes \cite[page
+91]{martinlof84}.
+
+The constant \cdx{rec} constructs proof terms when mathematical
+induction, rule~\tdx{NE}, is applied. It can also express primitive
+recursion. Since \cdx{rec} can be applied to higher-order functions,
+it can even express Ackermann's function, which is not primitive recursive
+\cite[page~104]{thompson91}.
+
+Figure~\ref{ctt-prod} shows the rules for general product types, which
+include function types as a special case. The rules correspond to the
+predicate calculus rules for universal quantifiers and implication. They
+also permit reasoning about functions, with the rules of a typed
+$\lambda$-calculus.
+
+Figure~\ref{ctt-sum} shows the rules for general sum types, which
+include binary product types as a special case. The rules correspond to the
+predicate calculus rules for existential quantifiers and conjunction. They
+also permit reasoning about ordered pairs, with the projections
+\cdx{fst} and~\cdx{snd}.
+
+Figure~\ref{ctt-plus} shows the rules for binary sum types. They
+correspond to the predicate calculus rules for disjunction. They also
+permit reasoning about disjoint sums, with the injections \cdx{inl}
+and~\cdx{inr} and case analysis operator~\cdx{when}.
+
+Figure~\ref{ctt-ft} shows the rules for the empty and unit types, $F$
+and~$T$. They correspond to the predicate calculus rules for absurdity and
+truth.
+
+Figure~\ref{ctt-eq} shows the rules for equality types. If $a=b\in A$ is
+provable then \cdx{eq} is a canonical element of the type $Eq(A,a,b)$,
+and vice versa. These rules define extensional equality; the most recent
+versions of Type Theory use intensional equality~\cite{nordstrom90}.
+
+Figure~\ref{ctt-derived} presents the derived rules. The rule
+\tdx{subst_prodE} is derived from {\tt prodE}, and is easier to use
+in backwards proof. The rules \tdx{SumE_fst} and \tdx{SumE_snd}
+express the typing of~\cdx{fst} and~\cdx{snd}; together, they are
+roughly equivalent to~{\tt SumE} with the advantage of creating no
+parameters. Section~\ref{ctt-choice} below demonstrates these rules in a
+proof of the Axiom of Choice.
+
+All the rules are given in $\eta$-expanded form. For instance, every
+occurrence of $\lambda u\,v. b(u,v)$ could be abbreviated to~$b$ in the
+rules for~$N$. The expanded form permits Isabelle to preserve bound
+variable names during backward proof. Names of bound variables in the
+conclusion (here, $u$ and~$v$) are matched with corresponding bound
+variables in the premises.
+
+
+\section{Rule lists}
+The Type Theory tactics provide rewriting, type inference, and logical
+reasoning. Many proof procedures work by repeatedly resolving certain Type
+Theory rules against a proof state. CTT defines lists --- each with
+type
+\hbox{\tt thm list} --- of related rules.
+\begin{ttdescription}
+\item[\ttindexbold{form_rls}]
+contains formation rules for the types $N$, $\Pi$, $\Sigma$, $+$, $Eq$,
+$F$, and $T$.
+
+\item[\ttindexbold{formL_rls}]
+contains long formation rules for $\Pi$, $\Sigma$, $+$, and $Eq$. (For
+other types use \tdx{refl_type}.)
+
+\item[\ttindexbold{intr_rls}]
+contains introduction rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
+$T$.
+
+\item[\ttindexbold{intrL_rls}]
+contains long introduction rules for $N$, $\Pi$, $\Sigma$, and $+$. (For
+$T$ use \tdx{refl_elem}.)
+
+\item[\ttindexbold{elim_rls}]
+contains elimination rules for the types $N$, $\Pi$, $\Sigma$, $+$, and
+$F$. The rules for $Eq$ and $T$ are omitted because they involve no
+eliminator.
+
+\item[\ttindexbold{elimL_rls}]
+contains long elimination rules for $N$, $\Pi$, $\Sigma$, $+$, and $F$.
+
+\item[\ttindexbold{comp_rls}]
+contains computation rules for the types $N$, $\Pi$, $\Sigma$, and $+$.
+Those for $Eq$ and $T$ involve no eliminator.
+
+\item[\ttindexbold{basic_defs}]
+contains the definitions of {\tt fst} and {\tt snd}.
+\end{ttdescription}
+
+
+\section{Tactics for subgoal reordering}
+\begin{ttbox}
+test_assume_tac : int -> tactic
+typechk_tac : thm list -> tactic
+equal_tac : thm list -> tactic
+intr_tac : thm list -> tactic
+\end{ttbox}
+Blind application of CTT rules seldom leads to a proof. The elimination
+rules, especially, create subgoals containing new unknowns. These subgoals
+unify with anything, creating a huge search space. The standard tactic
+\ttindex{filt_resolve_tac}
+(see \iflabelundefined{filt_resolve_tac}{the {\em Reference Manual\/}}%
+ {\S\ref{filt_resolve_tac}})
+%
+fails for goals that are too flexible; so does the CTT tactic {\tt
+ test_assume_tac}. Used with the tactical \ttindex{REPEAT_FIRST} they
+achieve a simple kind of subgoal reordering: the less flexible subgoals are
+attempted first. Do some single step proofs, or study the examples below,
+to see why this is necessary.
+\begin{ttdescription}
+\item[\ttindexbold{test_assume_tac} $i$]
+uses {\tt assume_tac} to solve the subgoal by assumption, but only if
+subgoal~$i$ has the form $a\in A$ and the head of $a$ is not an unknown.
+Otherwise, it fails.
+
+\item[\ttindexbold{typechk_tac} $thms$]
+uses $thms$ with formation, introduction, and elimination rules to check
+the typing of constructions. It is designed to solve goals of the form
+$a\in \Var{A}$, where $a$ is rigid and $\Var{A}$ is flexible; thus it
+performs type inference. The tactic can also solve goals of
+the form $A\;\rm type$.
+
+\item[\ttindexbold{equal_tac} $thms$]
+uses $thms$ with the long introduction and elimination rules to solve goals
+of the form $a=b\in A$, where $a$ is rigid. It is intended for deriving
+the long rules for defined constants such as the arithmetic operators. The
+tactic can also perform type-checking.
+
+\item[\ttindexbold{intr_tac} $thms$]
+uses $thms$ with the introduction rules to break down a type. It is
+designed for goals like $\Var{a}\in A$ where $\Var{a}$ is flexible and $A$
+rigid. These typically arise when trying to prove a proposition~$A$,
+expressed as a type.
+\end{ttdescription}
+
+
+
+\section{Rewriting tactics}
+\begin{ttbox}
+rew_tac : thm list -> tactic
+hyp_rew_tac : thm list -> tactic
+\end{ttbox}
+Object-level simplification is accomplished through proof, using the {\tt
+ CTT} equality rules and the built-in rewriting functor
+{\tt TSimpFun}.%
+\footnote{This should not be confused with Isabelle's main simplifier; {\tt
+ TSimpFun} is only useful for CTT and similar logics with type inference
+ rules. At present it is undocumented.}
+%
+The rewrites include the computation rules and other equations. The long
+versions of the other rules permit rewriting of subterms and subtypes.
+Also used are transitivity and the extra judgement form \cdx{Reduce}.
+Meta-level simplification handles only definitional equality.
+\begin{ttdescription}
+\item[\ttindexbold{rew_tac} $thms$]
+applies $thms$ and the computation rules as left-to-right rewrites. It
+solves the goal $a=b\in A$ by rewriting $a$ to $b$. If $b$ is an unknown
+then it is assigned the rewritten form of~$a$. All subgoals are rewritten.
+
+\item[\ttindexbold{hyp_rew_tac} $thms$]
+is like {\tt rew_tac}, but includes as rewrites any equations present in
+the assumptions.
+\end{ttdescription}
+
+
+\section{Tactics for logical reasoning}
+Interpreting propositions as types lets CTT express statements of
+intuitionistic logic. However, Constructive Type Theory is not just another
+syntax for first-order logic. There are fundamental differences.
+
+\index{assumptions!in CTT}
+Can assumptions be deleted after use? Not every occurrence of a type
+represents a proposition, and Type Theory assumptions declare variables.
+In first-order logic, $\disj$-elimination with the assumption $P\disj Q$
+creates one subgoal assuming $P$ and another assuming $Q$, and $P\disj Q$
+can be deleted safely. In Type Theory, $+$-elimination with the assumption
+$z\in A+B$ creates one subgoal assuming $x\in A$ and another assuming $y\in
+B$ (for arbitrary $x$ and $y$). Deleting $z\in A+B$ when other assumptions
+refer to $z$ may render the subgoal unprovable: arguably,
+meaningless.
+
+Isabelle provides several tactics for predicate calculus reasoning in CTT:
+\begin{ttbox}
+mp_tac : int -> tactic
+add_mp_tac : int -> tactic
+safestep_tac : thm list -> int -> tactic
+safe_tac : thm list -> int -> tactic
+step_tac : thm list -> int -> tactic
+pc_tac : thm list -> int -> tactic
+\end{ttbox}
+These are loosely based on the intuitionistic proof procedures
+of~\thydx{FOL}. For the reasons discussed above, a rule that is safe for
+propositional reasoning may be unsafe for type-checking; thus, some of the
+`safe' tactics are misnamed.
+\begin{ttdescription}
+\item[\ttindexbold{mp_tac} $i$]
+searches in subgoal~$i$ for assumptions of the form $f\in\Pi(A,B)$ and
+$a\in A$, where~$A$ may be found by unification. It replaces
+$f\in\Pi(A,B)$ by $z\in B(a)$, where~$z$ is a new parameter. The tactic
+can produce multiple outcomes for each suitable pair of assumptions. In
+short, {\tt mp_tac} performs Modus Ponens among the assumptions.
+
+\item[\ttindexbold{add_mp_tac} $i$]
+is like {\tt mp_tac}~$i$ but retains the assumption $f\in\Pi(A,B)$. It
+avoids information loss but obviously loops if repeated.
+
+\item[\ttindexbold{safestep_tac} $thms$ $i$]
+attacks subgoal~$i$ using formation rules and certain other `safe' rules
+(\tdx{FE}, \tdx{ProdI}, \tdx{SumE}, \tdx{PlusE}), calling
+{\tt mp_tac} when appropriate. It also uses~$thms$,
+which are typically premises of the rule being derived.
+
+\item[\ttindexbold{safe_tac} $thms$ $i$] attempts to solve subgoal~$i$ by
+ means of backtracking, using {\tt safestep_tac}.
+
+\item[\ttindexbold{step_tac} $thms$ $i$]
+tries to reduce subgoal~$i$ using {\tt safestep_tac}, then tries unsafe
+rules. It may produce multiple outcomes.
+
+\item[\ttindexbold{pc_tac} $thms$ $i$]
+tries to solve subgoal~$i$ by backtracking, using {\tt step_tac}.
+\end{ttdescription}
+
+
+
+\begin{figure}
+\index{#+@{\tt\#+} symbol}
+\index{*"- symbol}
+\index{#*@{\tt\#*} symbol}
+\index{*div symbol}
+\index{*mod symbol}
+
+\index{absolute difference}
+\index{"!-"!@{\tt\char124-\char124} symbol}
+%\char124 is vertical bar. We use ! because | stopped working
+
+\begin{constants}
+ \it symbol & \it meta-type & \it priority & \it description \\
+ \tt \#* & $[i,i]\To i$ & Left 70 & multiplication \\
+ \tt div & $[i,i]\To i$ & Left 70 & division\\
+ \tt mod & $[i,i]\To i$ & Left 70 & modulus\\
+ \tt \#+ & $[i,i]\To i$ & Left 65 & addition\\
+ \tt - & $[i,i]\To i$ & Left 65 & subtraction\\
+ \verb'|-|' & $[i,i]\To i$ & Left 65 & absolute difference
+\end{constants}
+
+\begin{ttbox}
+\tdx{add_def} a#+b == rec(a, b, \%u v. succ(v))
+\tdx{diff_def} a-b == rec(b, a, \%u v. rec(v, 0, \%x y. x))
+\tdx{absdiff_def} a|-|b == (a-b) #+ (b-a)
+\tdx{mult_def} a#*b == rec(a, 0, \%u v. b #+ v)
+
+\tdx{mod_def} a mod b ==
+ rec(a, 0, \%u v. rec(succ(v) |-| b, 0, \%x y. succ(v)))
+
+\tdx{div_def} a div b ==
+ rec(a, 0, \%u v. rec(succ(u) mod b, succ(v), \%x y. v))
+
+\tdx{add_typing} [| a:N; b:N |] ==> a #+ b : N
+\tdx{addC0} b:N ==> 0 #+ b = b : N
+\tdx{addC_succ} [| a:N; b:N |] ==> succ(a) #+ b = succ(a #+ b) : N
+
+\tdx{add_assoc} [| a:N; b:N; c:N |] ==>
+ (a #+ b) #+ c = a #+ (b #+ c) : N
+
+\tdx{add_commute} [| a:N; b:N |] ==> a #+ b = b #+ a : N
+
+\tdx{mult_typing} [| a:N; b:N |] ==> a #* b : N
+\tdx{multC0} b:N ==> 0 #* b = 0 : N
+\tdx{multC_succ} [| a:N; b:N |] ==> succ(a) #* b = b #+ (a#*b) : N
+\tdx{mult_commute} [| a:N; b:N |] ==> a #* b = b #* a : N
+
+\tdx{add_mult_dist} [| a:N; b:N; c:N |] ==>
+ (a #+ b) #* c = (a #* c) #+ (b #* c) : N
+
+\tdx{mult_assoc} [| a:N; b:N; c:N |] ==>
+ (a #* b) #* c = a #* (b #* c) : N
+
+\tdx{diff_typing} [| a:N; b:N |] ==> a - b : N
+\tdx{diffC0} a:N ==> a - 0 = a : N
+\tdx{diff_0_eq_0} b:N ==> 0 - b = 0 : N
+\tdx{diff_succ_succ} [| a:N; b:N |] ==> succ(a) - succ(b) = a - b : N
+\tdx{diff_self_eq_0} a:N ==> a - a = 0 : N
+\tdx{add_inverse_diff} [| a:N; b:N; b-a=0 : N |] ==> b #+ (a-b) = a : N
+\end{ttbox}
+\caption{The theory of arithmetic} \label{ctt_arith}
+\end{figure}
+
+
+\section{A theory of arithmetic}
+\thydx{Arith} is a theory of elementary arithmetic. It proves the
+properties of addition, multiplication, subtraction, division, and
+remainder, culminating in the theorem
+\[ a \bmod b + (a/b)\times b = a. \]
+Figure~\ref{ctt_arith} presents the definitions and some of the key
+theorems, including commutative, distributive, and associative laws.
+
+The operators~\verb'#+', \verb'-', \verb'|-|', \verb'#*', \verb'mod'
+and~\verb'div' stand for sum, difference, absolute difference, product,
+remainder and quotient, respectively. Since Type Theory has only primitive
+recursion, some of their definitions may be obscure.
+
+The difference~$a-b$ is computed by taking $b$ predecessors of~$a$, where
+the predecessor function is $\lambda v. {\tt rec}(v, 0, \lambda x\,y. x)$.
+
+The remainder $a\bmod b$ counts up to~$a$ in a cyclic fashion, using 0
+as the successor of~$b-1$. Absolute difference is used to test the
+equality $succ(v)=b$.
+
+The quotient $a/b$ is computed by adding one for every number $x$
+such that $0\leq x \leq a$ and $x\bmod b = 0$.
+
+
+
+\section{The examples directory}
+This directory contains examples and experimental proofs in CTT.
+\begin{ttdescription}
+\item[CTT/ex/typechk.ML]
+contains simple examples of type-checking and type deduction.
+
+\item[CTT/ex/elim.ML]
+contains some examples from Martin-L\"of~\cite{martinlof84}, proved using
+{\tt pc_tac}.
+
+\item[CTT/ex/equal.ML]
+contains simple examples of rewriting.
+
+\item[CTT/ex/synth.ML]
+demonstrates the use of unknowns with some trivial examples of program
+synthesis.
+\end{ttdescription}
+
+
+\section{Example: type inference}
+Type inference involves proving a goal of the form $a\in\Var{A}$, where $a$
+is a term and $\Var{A}$ is an unknown standing for its type. The type,
+initially
+unknown, takes shape in the course of the proof. Our example is the
+predecessor function on the natural numbers.
+\begin{ttbox}
+Goal "lam n. rec(n, 0, \%x y. x) : ?A";
+{\out Level 0}
+{\out lam n. rec(n,0,\%x y. x) : ?A}
+{\out 1. lam n. rec(n,0,\%x y. x) : ?A}
+\end{ttbox}
+Since the term is a Constructive Type Theory $\lambda$-abstraction (not to
+be confused with a meta-level abstraction), we apply the rule
+\tdx{ProdI}, for $\Pi$-introduction. This instantiates~$\Var{A}$ to a
+product type of unknown domain and range.
+\begin{ttbox}
+by (resolve_tac [ProdI] 1);
+{\out Level 1}
+{\out lam n. rec(n,0,\%x y. x) : PROD x:?A1. ?B1(x)}
+{\out 1. ?A1 type}
+{\out 2. !!n. n : ?A1 ==> rec(n,0,\%x y. x) : ?B1(n)}
+\end{ttbox}
+Subgoal~1 is too flexible. It can be solved by instantiating~$\Var{A@1}$
+to any type, but most instantiations will invalidate subgoal~2. We
+therefore tackle the latter subgoal. It asks the type of a term beginning
+with {\tt rec}, which can be found by $N$-elimination.%
+\index{*NE theorem}
+\begin{ttbox}
+by (eresolve_tac [NE] 2);
+{\out Level 2}
+{\out lam n. rec(n,0,\%x y. x) : PROD x:N. ?C2(x,x)}
+{\out 1. N type}
+{\out 2. !!n. 0 : ?C2(n,0)}
+{\out 3. !!n x y. [| x : N; y : ?C2(n,x) |] ==> x : ?C2(n,succ(x))}
+\end{ttbox}
+Subgoal~1 is no longer flexible: we now know~$\Var{A@1}$ is the type of
+natural numbers. However, let us continue proving nontrivial subgoals.
+Subgoal~2 asks, what is the type of~0?\index{*NIO theorem}
+\begin{ttbox}
+by (resolve_tac [NI0] 2);
+{\out Level 3}
+{\out lam n. rec(n,0,\%x y. x) : N --> N}
+{\out 1. N type}
+{\out 2. !!n x y. [| x : N; y : N |] ==> x : N}
+\end{ttbox}
+The type~$\Var{A}$ is now fully determined. It is the product type
+$\prod@{x\in N}N$, which is shown as the function type $N\to N$ because
+there is no dependence on~$x$. But we must prove all the subgoals to show
+that the original term is validly typed. Subgoal~2 is provable by
+assumption and the remaining subgoal falls by $N$-formation.%
+\index{*NF theorem}
+\begin{ttbox}
+by (assume_tac 2);
+{\out Level 4}
+{\out lam n. rec(n,0,\%x y. x) : N --> N}
+{\out 1. N type}
+\ttbreak
+by (resolve_tac [NF] 1);
+{\out Level 5}
+{\out lam n. rec(n,0,\%x y. x) : N --> N}
+{\out No subgoals!}
+\end{ttbox}
+Calling \ttindex{typechk_tac} can prove this theorem in one step.
+
+Even if the original term is ill-typed, one can infer a type for it, but
+unprovable subgoals will be left. As an exercise, try to prove the
+following invalid goal:
+\begin{ttbox}
+Goal "lam n. rec(n, 0, \%x y. tt) : ?A";
+\end{ttbox}
+
+
+
+\section{An example of logical reasoning}
+Logical reasoning in Type Theory involves proving a goal of the form
+$\Var{a}\in A$, where type $A$ expresses a proposition and $\Var{a}$ stands
+for its proof term, a value of type $A$. The proof term is initially
+unknown and takes shape during the proof.
+
+Our example expresses a theorem about quantifiers in a sorted logic:
+\[ \infer{(\ex{x\in A}P(x)) \disj (\ex{x\in A}Q(x))}
+ {\ex{x\in A}P(x)\disj Q(x)}
+\]
+By the propositions-as-types principle, this is encoded
+using~$\Sigma$ and~$+$ types. A special case of it expresses a
+distributive law of Type Theory:
+\[ \infer{(A\times B) + (A\times C)}{A\times(B+C)} \]
+Generalizing this from $\times$ to $\Sigma$, and making the typing
+conditions explicit, yields the rule we must derive:
+\[ \infer{\Var{a} \in (\sum@{x\in A} B(x)) + (\sum@{x\in A} C(x))}
+ {\hbox{$A$ type} &
+ \infer*{\hbox{$B(x)$ type}}{[x\in A]} &
+ \infer*{\hbox{$C(x)$ type}}{[x\in A]} &
+ p\in \sum@{x\in A} B(x)+C(x)}
+\]
+To begin, we bind the rule's premises --- returned by the~{\tt goal}
+command --- to the {\ML} variable~{\tt prems}.
+\begin{ttbox}
+val prems = Goal
+ "[| A type; \ttback
+\ttback !!x. x:A ==> B(x) type; \ttback
+\ttback !!x. x:A ==> C(x) type; \ttback
+\ttback p: SUM x:A. B(x) + C(x) \ttback
+\ttback |] ==> ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))";
+{\out Level 0}
+{\out ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. ?a : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
+{\out val prems = ["A type [A type]",}
+{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
+{\out "?x : A ==> C(?x) type [!!x. x : A ==> C(x) type]",}
+{\out "p : SUM x:A. B(x) + C(x) [p : SUM x:A. B(x) + C(x)]"]}
+{\out : thm list}
+\end{ttbox}
+The last premise involves the sum type~$\Sigma$. Since it is a premise
+rather than the assumption of a goal, it cannot be found by {\tt
+ eresolve_tac}. We could insert it (and the other atomic premise) by
+calling
+\begin{ttbox}
+cut_facts_tac prems 1;
+\end{ttbox}
+A forward proof step is more straightforward here. Let us resolve the
+$\Sigma$-elimination rule with the premises using~\ttindex{RL}. This
+inference yields one result, which we supply to {\tt
+ resolve_tac}.\index{*SumE theorem}
+\begin{ttbox}
+by (resolve_tac (prems RL [SumE]) 1);
+{\out Level 1}
+{\out split(p,?c1) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y.}
+{\out [| x : A; y : B(x) + C(x) |] ==>}
+{\out ?c1(x,y) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+The subgoal has two new parameters, $x$ and~$y$. In the main goal,
+$\Var{a}$ has been instantiated with a \cdx{split} term. The
+assumption $y\in B(x) + C(x)$ is eliminated next, causing a case split and
+creating the parameter~$xa$. This inference also inserts~\cdx{when}
+into the main goal.\index{*PlusE theorem}
+\begin{ttbox}
+by (eresolve_tac [PlusE] 1);
+{\out Level 2}
+{\out split(p,\%x y. when(y,?c2(x,y),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y xa.}
+{\out [| x : A; xa : B(x) |] ==>}
+{\out ?c2(x,y,xa) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
+{\out 2. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+To complete the proof object for the main goal, we need to instantiate the
+terms $\Var{c@2}(x,y,xa)$ and $\Var{d@2}(x,y,xa)$. We attack subgoal~1 by
+a~$+$-introduction rule; since the goal assumes $xa\in B(x)$, we take the left
+injection~(\cdx{inl}).
+\index{*PlusI_inl theorem}
+\begin{ttbox}
+by (resolve_tac [PlusI_inl] 1);
+{\out Level 3}
+{\out split(p,\%x y. when(y,\%xa. inl(?a3(x,y,xa)),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a3(x,y,xa) : SUM x:A. B(x)}
+{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+\ttbreak
+{\out 3. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+A new subgoal~2 has appeared, to verify that $\sum@{x\in A}C(x)$ is a type.
+Continuing to work on subgoal~1, we apply the $\Sigma$-introduction rule.
+This instantiates the term $\Var{a@3}(x,y,xa)$; the main goal now contains
+an ordered pair, whose components are two new unknowns.%
+\index{*SumI theorem}
+\begin{ttbox}
+by (resolve_tac [SumI] 1);
+{\out Level 4}
+{\out split(p,\%x y. when(y,\%xa. inl(<?a4(x,y,xa),?b4(x,y,xa)>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?a4(x,y,xa) : A}
+{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(?a4(x,y,xa))}
+{\out 3. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out 4. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+The two new subgoals both hold by assumption. Observe how the unknowns
+$\Var{a@4}$ and $\Var{b@4}$ are instantiated throughout the proof state.
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 5}
+{\out split(p,\%x y. when(y,\%xa. inl(<x,?b4(x,y,xa)>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
+{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> ?b4(x,y,xa) : B(x)}
+{\out 2. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out 3. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\ttbreak
+by (assume_tac 1);
+{\out Level 6}
+{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y xa. [| x : A; xa : B(x) |] ==> SUM x:A. C(x) type}
+{\out 2. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+Subgoal~1 is an example of a well-formedness subgoal~\cite{constable86}.
+Such subgoals are usually trivial; this one yields to
+\ttindex{typechk_tac}, given the current list of premises.
+\begin{ttbox}
+by (typechk_tac prems);
+{\out Level 7}
+{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),?d2(x,y)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out 1. !!x y ya.}
+{\out [| x : A; ya : C(x) |] ==>}
+{\out ?d2(x,y,ya) : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+\end{ttbox}
+This subgoal is the other case from the $+$-elimination above, and can be
+proved similarly. Quicker is to apply \ttindex{pc_tac}. The main goal
+finally gets a fully instantiated proof object.
+\begin{ttbox}
+by (pc_tac prems 1);
+{\out Level 8}
+{\out split(p,\%x y. when(y,\%xa. inl(<x,xa>),\%y. inr(<x,y>)))}
+{\out : (SUM x:A. B(x)) + (SUM x:A. C(x))}
+{\out No subgoals!}
+\end{ttbox}
+Calling \ttindex{pc_tac} after the first $\Sigma$-elimination above also
+proves this theorem.
+
+
+\section{Example: deriving a currying functional}
+In simply-typed languages such as {\ML}, a currying functional has the type
+\[ (A\times B \to C) \to (A\to (B\to C)). \]
+Let us generalize this to the dependent types~$\Sigma$ and~$\Pi$.
+The functional takes a function~$f$ that maps $z:\Sigma(A,B)$
+to~$C(z)$; the resulting function maps $x\in A$ and $y\in B(x)$ to
+$C(\langle x,y\rangle)$.
+
+Formally, there are three typing premises. $A$ is a type; $B$ is an
+$A$-indexed family of types; $C$ is a family of types indexed by
+$\Sigma(A,B)$. The goal is expressed using \hbox{\tt PROD f} to ensure
+that the parameter corresponding to the functional's argument is really
+called~$f$; Isabelle echoes the type using \verb|-->| because there is no
+explicit dependence upon~$f$.
+\begin{ttbox}
+val prems = Goal
+ "[| A type; !!x. x:A ==> B(x) type; \ttback
+\ttback !!z. z: (SUM x:A. B(x)) ==> C(z) type \ttback
+\ttback |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ttback
+\ttback (PROD x:A . PROD y:B(x) . C(<x,y>))";
+\ttbreak
+{\out Level 0}
+{\out ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
+{\out (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out 1. ?a : (PROD z:SUM x:A. B(x). C(z)) -->}
+{\out (PROD x:A. PROD y:B(x). C(<x,y>))}
+\ttbreak
+{\out val prems = ["A type [A type]",}
+{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
+{\out "?z : SUM x:A. B(x) ==> C(?z) type}
+{\out [!!z. z : SUM x:A. B(x) ==> C(z) type]"] : thm list}
+\end{ttbox}
+This is a chance to demonstrate \ttindex{intr_tac}. Here, the tactic
+repeatedly applies $\Pi$-introduction and proves the rather
+tiresome typing conditions.
+
+Note that $\Var{a}$ becomes instantiated to three nested
+$\lambda$-abstractions. It would be easier to read if the bound variable
+names agreed with the parameters in the subgoal. Isabelle attempts to give
+parameters the same names as corresponding bound variables in the goal, but
+this does not always work. In any event, the goal is logically correct.
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 1}
+{\out lam x xa xb. ?b7(x,xa,xb)}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out 1. !!f x y.}
+{\out [| f : PROD z:SUM x:A. B(x). C(z); x : A; y : B(x) |] ==>}
+{\out ?b7(f,x,y) : C(<x,y>)}
+\end{ttbox}
+Using $\Pi$-elimination, we solve subgoal~1 by applying the function~$f$.
+\index{*ProdE theorem}
+\begin{ttbox}
+by (eresolve_tac [ProdE] 1);
+{\out Level 2}
+{\out lam x xa xb. x ` <xa,xb>}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out 1. !!f x y. [| x : A; y : B(x) |] ==> <x,y> : SUM x:A. B(x)}
+\end{ttbox}
+Finally, we verify that the argument's type is suitable for the function
+application. This is straightforward using introduction rules.
+\index{*intr_tac}
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 3}
+{\out lam x xa xb. x ` <xa,xb>}
+{\out : (PROD z:SUM x:A. B(x). C(z)) --> (PROD x:A. PROD y:B(x). C(<x,y>))}
+{\out No subgoals!}
+\end{ttbox}
+Calling~\ttindex{pc_tac} would have proved this theorem in one step; it can
+also prove an example by Martin-L\"of, related to $\disj$-elimination
+\cite[page~58]{martinlof84}.
+
+
+\section{Example: proving the Axiom of Choice} \label{ctt-choice}
+Suppose we have a function $h\in \prod@{x\in A}\sum@{y\in B(x)} C(x,y)$,
+which takes $x\in A$ to some $y\in B(x)$ paired with some $z\in C(x,y)$.
+Interpreting propositions as types, this asserts that for all $x\in A$
+there exists $y\in B(x)$ such that $C(x,y)$. The Axiom of Choice asserts
+that we can construct a function $f\in \prod@{x\in A}B(x)$ such that
+$C(x,f{\tt`}x)$ for all $x\in A$, where the latter property is witnessed by a
+function $g\in \prod@{x\in A}C(x,f{\tt`}x)$.
+
+In principle, the Axiom of Choice is simple to derive in Constructive Type
+Theory. The following definitions work:
+\begin{eqnarray*}
+ f & \equiv & {\tt fst} \circ h \\
+ g & \equiv & {\tt snd} \circ h
+\end{eqnarray*}
+But a completely formal proof is hard to find. The rules can be applied in
+countless ways, yielding many higher-order unifiers. The proof can get
+bogged down in the details. But with a careful selection of derived rules
+(recall Fig.\ts\ref{ctt-derived}) and the type-checking tactics, we can
+prove the theorem in nine steps.
+\begin{ttbox}
+val prems = Goal
+ "[| A type; !!x. x:A ==> B(x) type; \ttback
+\ttback !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ttback
+\ttback |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ttback
+\ttback (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
+{\out Level 0}
+{\out ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out 1. ?a : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out val prems = ["A type [A type]",}
+{\out "?x : A ==> B(?x) type [!!x. x : A ==> B(x) type]",}
+{\out "[| ?x : A; ?y : B(?x) |] ==> C(?x, ?y) type}
+{\out [!!x y. [| x : A; y : B(x) |] ==> C(x, y) type]"]}
+{\out : thm list}
+\end{ttbox}
+First, \ttindex{intr_tac} applies introduction rules and performs routine
+type-checking. This instantiates~$\Var{a}$ to a construction involving
+a $\lambda$-abstraction and an ordered pair. The pair's components are
+themselves $\lambda$-abstractions and there is a subgoal for each.
+\begin{ttbox}
+by (intr_tac prems);
+{\out Level 1}
+{\out lam x. <lam xa. ?b7(x,xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b7(h,x) : B(x)}
+\ttbreak
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. ?b7(h,x)) ` x)}
+\end{ttbox}
+Subgoal~1 asks to find the choice function itself, taking $x\in A$ to some
+$\Var{b@7}(h,x)\in B(x)$. Subgoal~2 asks, given $x\in A$, for a proof
+object $\Var{b@8}(h,x)$ to witness that the choice function's argument and
+result lie in the relation~$C$. This latter task will take up most of the
+proof.
+\index{*ProdE theorem}\index{*SumE_fst theorem}\index{*RS}
+\begin{ttbox}
+by (eresolve_tac [ProdE RS SumE_fst] 1);
+{\out Level 2}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x. x : A ==> x : A}
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
+\end{ttbox}
+Above, we have composed {\tt fst} with the function~$h$. Unification
+has deduced that the function must be applied to $x\in A$. We have our
+choice function.
+\begin{ttbox}
+by (assume_tac 1);
+{\out Level 3}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,(lam x. fst(h ` x)) ` x)}
+\end{ttbox}
+Before we can compose {\tt snd} with~$h$, the arguments of $C$ must be
+simplified. The derived rule \tdx{replace_type} lets us replace a type
+by any equivalent type, shown below as the schematic term $\Var{A@{13}}(h,x)$:
+\begin{ttbox}
+by (resolve_tac [replace_type] 1);
+{\out Level 4}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out C(x,(lam x. fst(h ` x)) ` x) = ?A13(h,x)}
+\ttbreak
+{\out 2. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : ?A13(h,x)}
+\end{ttbox}
+The derived rule \tdx{subst_eqtyparg} lets us simplify a type's
+argument (by currying, $C(x)$ is a unary type operator):
+\begin{ttbox}
+by (resolve_tac [subst_eqtyparg] 1);
+{\out Level 5}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out (lam x. fst(h ` x)) ` x = ?c14(h,x) : ?A14(h,x)}
+\ttbreak
+{\out 2. !!h x z.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out z : ?A14(h,x) |] ==>}
+{\out C(x,z) type}
+\ttbreak
+{\out 3. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,?c14(h,x))}
+\end{ttbox}
+Subgoal~1 requires simply $\beta$-contraction, which is the rule
+\tdx{ProdC}. The term $\Var{c@{14}}(h,x)$ in the last subgoal
+receives the contracted result.
+\begin{ttbox}
+by (resolve_tac [ProdC] 1);
+{\out Level 6}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out x : ?A15(h,x)}
+\ttbreak
+{\out 2. !!h x xa.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out xa : ?A15(h,x) |] ==>}
+{\out fst(h ` xa) : ?B15(h,x,xa)}
+\ttbreak
+{\out 3. !!h x z.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A;}
+{\out z : ?B15(h,x,x) |] ==>}
+{\out C(x,z) type}
+\ttbreak
+{\out 4. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,fst(h ` x))}
+\end{ttbox}
+Routine type-checking goals proliferate in Constructive Type Theory, but
+\ttindex{typechk_tac} quickly solves them. Note the inclusion of
+\tdx{SumE_fst} along with the premises.
+\begin{ttbox}
+by (typechk_tac (SumE_fst::prems));
+{\out Level 7}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. ?b8(x,xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x.}
+{\out [| h : PROD x:A. SUM y:B(x). C(x,y); x : A |] ==>}
+{\out ?b8(h,x) : C(x,fst(h ` x))}
+\end{ttbox}
+We are finally ready to compose {\tt snd} with~$h$.
+\index{*ProdE theorem}\index{*SumE_snd theorem}\index{*RS}
+\begin{ttbox}
+by (eresolve_tac [ProdE RS SumE_snd] 1);
+{\out Level 8}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+\ttbreak
+{\out 1. !!h x. x : A ==> x : A}
+{\out 2. !!h x. x : A ==> B(x) type}
+{\out 3. !!h x xa. [| x : A; xa : B(x) |] ==> C(x,xa) type}
+\end{ttbox}
+The proof object has reached its final form. We call \ttindex{typechk_tac}
+to finish the type-checking.
+\begin{ttbox}
+by (typechk_tac prems);
+{\out Level 9}
+{\out lam x. <lam xa. fst(x ` xa),lam xa. snd(x ` xa)>}
+{\out : (PROD x:A. SUM y:B(x). C(x,y)) -->}
+{\out (SUM f:PROD x:A. B(x). PROD x:A. C(x,f ` x))}
+{\out No subgoals!}
+\end{ttbox}
+It might be instructive to compare this proof with Martin-L\"of's forward
+proof of the Axiom of Choice \cite[page~50]{martinlof84}.
+
+\index{Constructive Type Theory|)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/LK.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,711 @@
+\chapter{First-Order Sequent Calculus}
+\index{sequent calculus|(}
+
+The theory~\thydx{LK} implements classical first-order logic through Gentzen's
+sequent calculus (see Gallier~\cite{gallier86} or Takeuti~\cite{takeuti87}).
+Resembling the method of semantic tableaux, the calculus is well suited for
+backwards proof. Assertions have the form \(\Gamma\turn \Delta\), where
+\(\Gamma\) and \(\Delta\) are lists of formulae. Associative unification,
+simulated by higher-order unification, handles lists
+(\S\ref{sec:assoc-unification} presents details, if you are interested).
+
+The logic is many-sorted, using Isabelle's type classes. The class of
+first-order terms is called \cldx{term}. No types of individuals are
+provided, but extensions can define types such as {\tt nat::term} and type
+constructors such as {\tt list::(term)term}. Below, the type variable
+$\alpha$ ranges over class {\tt term}; the equality symbol and quantifiers
+are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which
+belongs to class {\tt logic}.
+
+LK implements a classical logic theorem prover that is nearly as powerful as
+the generic classical reasoner. The simplifier is now available too.
+
+To work in LK, start up Isabelle specifying \texttt{Sequents} as the
+object-logic. Once in Isabelle, change the context to theory \texttt{LK.thy}:
+\begin{ttbox}
+isabelle Sequents
+context LK.thy;
+\end{ttbox}
+Modal logic and linear logic are also available, but unfortunately they are
+not documented.
+
+
+\begin{figure}
+\begin{center}
+\begin{tabular}{rrr}
+ \it name &\it meta-type & \it description \\
+ \cdx{Trueprop}& $[sobj\To sobj, sobj\To sobj]\To prop$ & coercion to $prop$\\
+ \cdx{Seqof} & $[o,sobj]\To sobj$ & singleton sequence \\
+ \cdx{Not} & $o\To o$ & negation ($\neg$) \\
+ \cdx{True} & $o$ & tautology ($\top$) \\
+ \cdx{False} & $o$ & absurdity ($\bot$)
+\end{tabular}
+\end{center}
+\subcaption{Constants}
+
+\begin{center}
+\begin{tabular}{llrrr}
+ \it symbol &\it name &\it meta-type & \it priority & \it description \\
+ \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 &
+ universal quantifier ($\forall$) \\
+ \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 &
+ existential quantifier ($\exists$) \\
+ \sdx{THE} & \cdx{The} & $(\alpha\To o)\To \alpha$ & 10 &
+ definite description ($\iota$)
+\end{tabular}
+\end{center}
+\subcaption{Binders}
+
+\begin{center}
+\index{*"= symbol}
+\index{&@{\tt\&} symbol}
+\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working
+\index{*"-"-"> symbol}
+\index{*"<"-"> symbol}
+\begin{tabular}{rrrr}
+ \it symbol & \it meta-type & \it priority & \it description \\
+ \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
+ \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\
+ \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\
+ \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\
+ \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$)
+\end{tabular}
+\end{center}
+\subcaption{Infixes}
+
+\begin{center}
+\begin{tabular}{rrr}
+ \it external & \it internal & \it description \\
+ \tt $\Gamma$ |- $\Delta$ & \tt Trueprop($\Gamma$, $\Delta$) &
+ sequent $\Gamma\turn \Delta$
+\end{tabular}
+\end{center}
+\subcaption{Translations}
+\caption{Syntax of {\tt LK}} \label{lk-syntax}
+\end{figure}
+
+
+\begin{figure}
+\dquotes
+\[\begin{array}{rcl}
+ prop & = & sequence " |- " sequence
+\\[2ex]
+sequence & = & elem \quad (", " elem)^* \\
+ & | & empty
+\\[2ex]
+ elem & = & "\$ " term \\
+ & | & formula \\
+ & | & "<<" sequence ">>"
+\\[2ex]
+ formula & = & \hbox{expression of type~$o$} \\
+ & | & term " = " term \\
+ & | & "\ttilde\ " formula \\
+ & | & formula " \& " formula \\
+ & | & formula " | " formula \\
+ & | & formula " --> " formula \\
+ & | & formula " <-> " formula \\
+ & | & "ALL~" id~id^* " . " formula \\
+ & | & "EX~~" id~id^* " . " formula \\
+ & | & "THE~" id~ " . " formula
+ \end{array}
+\]
+\caption{Grammar of {\tt LK}} \label{lk-grammar}
+\end{figure}
+
+
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{basic} $H, P, $G |- $E, P, $F
+
+\tdx{contRS} $H |- $E, $S, $S, $F ==> $H |- $E, $S, $F
+\tdx{contLS} $H, $S, $S, $G |- $E ==> $H, $S, $G |- $E
+
+\tdx{thinRS} $H |- $E, $F ==> $H |- $E, $S, $F
+\tdx{thinLS} $H, $G |- $E ==> $H, $S, $G |- $E
+
+\tdx{cut} [| $H |- $E, P; $H, P |- $E |] ==> $H |- $E
+\subcaption{Structural rules}
+
+\tdx{refl} $H |- $E, a=a, $F
+\tdx{subst} $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)
+\subcaption{Equality rules}
+\end{ttbox}
+
+\caption{Basic Rules of {\tt LK}} \label{lk-basic-rules}
+\end{figure}
+
+\begin{figure}
+\begin{ttbox}
+\tdx{True_def} True == False-->False
+\tdx{iff_def} P<->Q == (P-->Q) & (Q-->P)
+
+\tdx{conjR} [| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F
+\tdx{conjL} $H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E
+
+\tdx{disjR} $H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F
+\tdx{disjL} [| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E
+
+\tdx{impR} $H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F
+\tdx{impL} [| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E
+
+\tdx{notR} $H, P |- $E, $F ==> $H |- $E, ~P, $F
+\tdx{notL} $H, $G |- $E, P ==> $H, ~P, $G |- $E
+
+\tdx{FalseL} $H, False, $G |- $E
+
+\tdx{allR} (!!x. $H|- $E, P(x), $F) ==> $H|- $E, ALL x. P(x), $F
+\tdx{allL} $H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G|- $E
+
+\tdx{exR} $H|- $E, P(x), $F, EX x. P(x) ==> $H|- $E, EX x. P(x), $F
+\tdx{exL} (!!x. $H, P(x), $G|- $E) ==> $H, EX x. P(x), $G|- $E
+
+\tdx{The} [| $H |- $E, P(a), $F; !!x. $H, P(x) |- $E, x=a, $F |] ==>
+ $H |- $E, P(THE x. P(x)), $F
+\subcaption{Logical rules}
+\end{ttbox}
+
+\caption{Rules of {\tt LK}} \label{lk-rules}
+\end{figure}
+
+
+\section{Syntax and rules of inference}
+\index{*sobj type}
+
+Figure~\ref{lk-syntax} gives the syntax for {\tt LK}, which is complicated
+by the representation of sequents. Type $sobj\To sobj$ represents a list
+of formulae.
+
+The \textbf{definite description} operator~$\iota x. P[x]$ stands for some~$a$
+satisfying~$P[a]$, if one exists and is unique. Since all terms in LK denote
+something, a description is always meaningful, but we do not know its value
+unless $P[x]$ defines it uniquely. The Isabelle notation is \hbox{\tt THE
+ $x$.\ $P[x]$}. The corresponding rule (Fig.\ts\ref{lk-rules}) does not
+entail the Axiom of Choice because it requires uniqueness.
+
+Conditional expressions are available with the notation
+\[ \dquotes
+ "if"~formula~"then"~term~"else"~term. \]
+
+Figure~\ref{lk-grammar} presents the grammar of LK. Traditionally,
+\(\Gamma\) and \(\Delta\) are meta-variables for sequences. In Isabelle's
+notation, the prefix~\verb|$| on a term makes it range over sequences.
+In a sequent, anything not prefixed by \verb|$| is taken as a formula.
+
+The notation \texttt{<<$sequence$>>} stands for a sequence of formul\ae{}.
+For example, you can declare the constant \texttt{imps} to consist of two
+implications:
+\begin{ttbox}
+consts P,Q,R :: o
+constdefs imps :: seq'=>seq'
+ "imps == <<P --> Q, Q --> R>>"
+\end{ttbox}
+Then you can use it in axioms and goals, for example
+\begin{ttbox}
+Goalw [imps_def] "P, $imps |- R";
+{\out Level 0}
+{\out P, $imps |- R}
+{\out 1. P, P --> Q, Q --> R |- R}
+by (Fast_tac 1);
+{\out Level 1}
+{\out P, $imps |- R}
+{\out No subgoals!}
+\end{ttbox}
+
+Figures~\ref{lk-basic-rules} and~\ref{lk-rules} present the rules of theory
+\thydx{LK}. The connective $\bimp$ is defined using $\conj$ and $\imp$. The
+axiom for basic sequents is expressed in a form that provides automatic
+thinning: redundant formulae are simply ignored. The other rules are
+expressed in the form most suitable for backward proof; exchange and
+contraction rules are not normally required, although they are provided
+anyway.
+
+
+\begin{figure}
+\begin{ttbox}
+\tdx{thinR} $H |- $E, $F ==> $H |- $E, P, $F
+\tdx{thinL} $H, $G |- $E ==> $H, P, $G |- $E
+
+\tdx{contR} $H |- $E, P, P, $F ==> $H |- $E, P, $F
+\tdx{contL} $H, P, P, $G |- $E ==> $H, P, $G |- $E
+
+\tdx{symR} $H |- $E, $F, a=b ==> $H |- $E, b=a, $F
+\tdx{symL} $H, $G, b=a |- $E ==> $H, a=b, $G |- $E
+
+\tdx{transR} [| $H|- $E, $F, a=b; $H|- $E, $F, b=c |]
+ ==> $H|- $E, a=c, $F
+
+\tdx{TrueR} $H |- $E, True, $F
+
+\tdx{iffR} [| $H, P |- $E, Q, $F; $H, Q |- $E, P, $F |]
+ ==> $H |- $E, P<->Q, $F
+
+\tdx{iffL} [| $H, $G |- $E, P, Q; $H, Q, P, $G |- $E |]
+ ==> $H, P<->Q, $G |- $E
+
+\tdx{allL_thin} $H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E
+\tdx{exR_thin} $H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F
+
+\tdx{the_equality} [| $H |- $E, P(a), $F;
+ !!x. $H, P(x) |- $E, x=a, $F |]
+ ==> $H |- $E, (THE x. P(x)) = a, $F
+\end{ttbox}
+
+\caption{Derived rules for {\tt LK}} \label{lk-derived}
+\end{figure}
+
+Figure~\ref{lk-derived} presents derived rules, including rules for
+$\bimp$. The weakened quantifier rules discard each quantification after a
+single use; in an automatic proof procedure, they guarantee termination,
+but are incomplete. Multiple use of a quantifier can be obtained by a
+contraction rule, which in backward proof duplicates a formula. The tactic
+{\tt res_inst_tac} can instantiate the variable~{\tt?P} in these rules,
+specifying the formula to duplicate.
+See theory {\tt Sequents/LK0} in the sources for complete listings of
+the rules and derived rules.
+
+To support the simplifier, hundreds of equivalences are proved for
+the logical connectives and for if-then-else expressions. See the file
+\texttt{Sequents/simpdata.ML}.
+
+\section{Automatic Proof}
+
+LK instantiates Isabelle's simplifier. Both equality ($=$) and the
+biconditional ($\bimp$) may be used for rewriting. The tactic
+\texttt{Simp_tac} refers to the default simpset (\texttt{simpset()}). With
+sequents, the \texttt{full_} and \texttt{asm_} forms of the simplifier are not
+required; all the formulae{} in the sequent will be simplified. The left-hand
+formulae{} are taken as rewrite rules. (Thus, the behaviour is what you would
+normally expect from calling \texttt{Asm_full_simp_tac}.)
+
+For classical reasoning, several tactics are available:
+\begin{ttbox}
+Safe_tac : int -> tactic
+Step_tac : int -> tactic
+Fast_tac : int -> tactic
+Best_tac : int -> tactic
+Pc_tac : int -> tactic
+\end{ttbox}
+These refer not to the standard classical reasoner but to a separate one
+provided for the sequent calculus. Two commands are available for adding new
+sequent calculus rules, safe or unsafe, to the default ``theorem pack'':
+\begin{ttbox}
+Add_safes : thm list -> unit
+Add_unsafes : thm list -> unit
+\end{ttbox}
+To control the set of rules for individual invocations, lower-case versions of
+all these primitives are available. Sections~\ref{sec:thm-pack}
+and~\ref{sec:sequent-provers} give full details.
+
+
+\section{Tactics for the cut rule}
+
+According to the cut-elimination theorem, the cut rule can be eliminated
+from proofs of sequents. But the rule is still essential. It can be used
+to structure a proof into lemmas, avoiding repeated proofs of the same
+formula. More importantly, the cut rule cannot be eliminated from
+derivations of rules. For example, there is a trivial cut-free proof of
+the sequent \(P\conj Q\turn Q\conj P\).
+Noting this, we might want to derive a rule for swapping the conjuncts
+in a right-hand formula:
+\[ \Gamma\turn \Delta, P\conj Q\over \Gamma\turn \Delta, Q\conj P \]
+The cut rule must be used, for $P\conj Q$ is not a subformula of $Q\conj
+P$. Most cuts directly involve a premise of the rule being derived (a
+meta-assumption). In a few cases, the cut formula is not part of any
+premise, but serves as a bridge between the premises and the conclusion.
+In such proofs, the cut formula is specified by calling an appropriate
+tactic.
+
+\begin{ttbox}
+cutR_tac : string -> int -> tactic
+cutL_tac : string -> int -> tactic
+\end{ttbox}
+These tactics refine a subgoal into two by applying the cut rule. The cut
+formula is given as a string, and replaces some other formula in the sequent.
+\begin{ttdescription}
+\item[\ttindexbold{cutR_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
+ applies the cut rule to subgoal~$i$. It then deletes some formula from the
+ right side of subgoal~$i$, replacing that formula by~$P$.
+
+\item[\ttindexbold{cutL_tac} {\it P\/} {\it i}] reads an LK formula~$P$, and
+ applies the cut rule to subgoal~$i$. It then deletes some formula from the
+ left side of the new subgoal $i+1$, replacing that formula by~$P$.
+\end{ttdescription}
+All the structural rules --- cut, contraction, and thinning --- can be
+applied to particular formulae using {\tt res_inst_tac}.
+
+
+\section{Tactics for sequents}
+\begin{ttbox}
+forms_of_seq : term -> term list
+could_res : term * term -> bool
+could_resolve_seq : term * term -> bool
+filseq_resolve_tac : thm list -> int -> int -> tactic
+\end{ttbox}
+Associative unification is not as efficient as it might be, in part because
+the representation of lists defeats some of Isabelle's internal
+optimisations. The following operations implement faster rule application,
+and may have other uses.
+\begin{ttdescription}
+\item[\ttindexbold{forms_of_seq} {\it t}]
+returns the list of all formulae in the sequent~$t$, removing sequence
+variables.
+
+\item[\ttindexbold{could_res} ($t$,$u$)]
+tests whether two formula lists could be resolved. List $t$ is from a
+premise or subgoal, while $u$ is from the conclusion of an object-rule.
+Assuming that each formula in $u$ is surrounded by sequence variables, it
+checks that each conclusion formula is unifiable (using {\tt could_unify})
+with some subgoal formula.
+
+\item[\ttindexbold{could_resolve_seq} ($t$,$u$)]
+ tests whether two sequents could be resolved. Sequent $t$ is a premise
+ or subgoal, while $u$ is the conclusion of an object-rule. It simply
+ calls {\tt could_res} twice to check that both the left and the right
+ sides of the sequents are compatible.
+
+\item[\ttindexbold{filseq_resolve_tac} {\it thms} {\it maxr} {\it i}]
+uses {\tt filter_thms could_resolve} to extract the {\it thms} that are
+applicable to subgoal~$i$. If more than {\it maxr\/} theorems are
+applicable then the tactic fails. Otherwise it calls {\tt resolve_tac}.
+Thus, it is the sequent calculus analogue of \ttindex{filt_resolve_tac}.
+\end{ttdescription}
+
+
+\section{A simple example of classical reasoning}
+The theorem $\turn\ex{y}\all{x}P(y)\imp P(x)$ is a standard example of the
+classical treatment of the existential quantifier. Classical reasoning is
+easy using~LK, as you can see by comparing this proof with the one given in
+the FOL manual~\cite{isabelle-ZF}. From a logical point of view, the proofs
+are essentially the same; the key step here is to use \tdx{exR} rather than
+the weaker~\tdx{exR_thin}.
+\begin{ttbox}
+Goal "|- EX y. ALL x. P(y)-->P(x)";
+{\out Level 0}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. |- EX y. ALL x. P(y) --> P(x)}
+by (resolve_tac [exR] 1);
+{\out Level 1}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. |- ALL x. P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
+\end{ttbox}
+There are now two formulae on the right side. Keeping the existential one
+in reserve, we break down the universal one.
+\begin{ttbox}
+by (resolve_tac [allR] 1);
+{\out Level 2}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. !!x. |- P(?x) --> P(x), EX x. ALL xa. P(x) --> P(xa)}
+by (resolve_tac [impR] 1);
+{\out Level 3}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. !!x. P(?x) |- P(x), EX x. ALL xa. P(x) --> P(xa)}
+\end{ttbox}
+Because LK is a sequent calculus, the formula~$P(\Var{x})$ does not become an
+assumption; instead, it moves to the left side. The resulting subgoal cannot
+be instantiated to a basic sequent: the bound variable~$x$ is not unifiable
+with the unknown~$\Var{x}$.
+\begin{ttbox}
+by (resolve_tac [basic] 1);
+{\out by: tactic failed}
+\end{ttbox}
+We reuse the existential formula using~\tdx{exR_thin}, which discards
+it; we shall not need it a third time. We again break down the resulting
+formula.
+\begin{ttbox}
+by (resolve_tac [exR_thin] 1);
+{\out Level 4}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. !!x. P(?x) |- P(x), ALL xa. P(?x7(x)) --> P(xa)}
+by (resolve_tac [allR] 1);
+{\out Level 5}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. !!x xa. P(?x) |- P(x), P(?x7(x)) --> P(xa)}
+by (resolve_tac [impR] 1);
+{\out Level 6}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. !!x xa. P(?x), P(?x7(x)) |- P(x), P(xa)}
+\end{ttbox}
+Subgoal~1 seems to offer lots of possibilities. Actually the only useful
+step is instantiating~$\Var{x@7}$ to $\lambda x. x$,
+transforming~$\Var{x@7}(x)$ into~$x$.
+\begin{ttbox}
+by (resolve_tac [basic] 1);
+{\out Level 7}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out No subgoals!}
+\end{ttbox}
+This theorem can be proved automatically. Because it involves quantifier
+duplication, we employ best-first search:
+\begin{ttbox}
+Goal "|- EX y. ALL x. P(y)-->P(x)";
+{\out Level 0}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out 1. |- EX y. ALL x. P(y) --> P(x)}
+by (best_tac LK_dup_pack 1);
+{\out Level 1}
+{\out |- EX y. ALL x. P(y) --> P(x)}
+{\out No subgoals!}
+\end{ttbox}
+
+
+
+\section{A more complex proof}
+Many of Pelletier's test problems for theorem provers \cite{pelletier86}
+can be solved automatically. Problem~39 concerns set theory, asserting
+that there is no Russell set --- a set consisting of those sets that are
+not members of themselves:
+\[ \turn \neg (\exists x. \forall y. y\in x \bimp y\not\in y) \]
+This does not require special properties of membership; we may generalize
+$x\in y$ to an arbitrary predicate~$F(x,y)$. The theorem, which is trivial
+for \texttt{Fast_tac}, has a short manual proof. See the directory {\tt
+ Sequents/LK} for many more examples.
+
+We set the main goal and move the negated formula to the left.
+\begin{ttbox}
+Goal "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
+{\out Level 0}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+by (resolve_tac [notR] 1);
+{\out Level 1}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. EX x. ALL y. F(y,x) <-> ~ F(y,y) |-}
+\end{ttbox}
+The right side is empty; we strip both quantifiers from the formula on the
+left.
+\begin{ttbox}
+by (resolve_tac [exL] 1);
+{\out Level 2}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. ALL y. F(y,x) <-> ~ F(y,y) |-}
+by (resolve_tac [allL_thin] 1);
+{\out Level 3}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. F(?x2(x),x) <-> ~ F(?x2(x),?x2(x)) |-}
+\end{ttbox}
+The rule \tdx{iffL} says, if $P\bimp Q$ then $P$ and~$Q$ are either
+both true or both false. It yields two subgoals.
+\begin{ttbox}
+by (resolve_tac [iffL] 1);
+{\out Level 4}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
+{\out 2. !!x. ~ F(?x2(x),?x2(x)), F(?x2(x),x) |-}
+\end{ttbox}
+We must instantiate~$\Var{x@2}$, the shared unknown, to satisfy both
+subgoals. Beginning with subgoal~2, we move a negated formula to the left
+and create a basic sequent.
+\begin{ttbox}
+by (resolve_tac [notL] 2);
+{\out Level 5}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. |- F(?x2(x),x), ~ F(?x2(x),?x2(x))}
+{\out 2. !!x. F(?x2(x),x) |- F(?x2(x),?x2(x))}
+by (resolve_tac [basic] 2);
+{\out Level 6}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. |- F(x,x), ~ F(x,x)}
+\end{ttbox}
+Thanks to the instantiation of~$\Var{x@2}$, subgoal~1 is obviously true.
+\begin{ttbox}
+by (resolve_tac [notR] 1);
+{\out Level 7}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out 1. !!x. F(x,x) |- F(x,x)}
+by (resolve_tac [basic] 1);
+{\out Level 8}
+{\out |- ~ (EX x. ALL y. F(y,x) <-> ~ F(y,y))}
+{\out No subgoals!}
+\end{ttbox}
+
+\section{*Unification for lists}\label{sec:assoc-unification}
+
+Higher-order unification includes associative unification as a special
+case, by an encoding that involves function composition
+\cite[page~37]{huet78}. To represent lists, let $C$ be a new constant.
+The empty list is $\lambda x. x$, while $[t@1,t@2,\ldots,t@n]$ is
+represented by
+\[ \lambda x. C(t@1,C(t@2,\ldots,C(t@n,x))). \]
+The unifiers of this with $\lambda x.\Var{f}(\Var{g}(x))$ give all the ways
+of expressing $[t@1,t@2,\ldots,t@n]$ as the concatenation of two lists.
+
+Unlike orthodox associative unification, this technique can represent certain
+infinite sets of unifiers by flex-flex equations. But note that the term
+$\lambda x. C(t,\Var{a})$ does not represent any list. Flex-flex constraints
+containing such garbage terms may accumulate during a proof.
+\index{flex-flex constraints}
+
+This technique lets Isabelle formalize sequent calculus rules,
+where the comma is the associative operator:
+\[ \infer[(\conj\hbox{-left})]
+ {\Gamma,P\conj Q,\Delta \turn \Theta}
+ {\Gamma,P,Q,\Delta \turn \Theta} \]
+Multiple unifiers occur whenever this is resolved against a goal containing
+more than one conjunction on the left.
+
+LK exploits this representation of lists. As an alternative, the sequent
+calculus can be formalized using an ordinary representation of lists, with a
+logic program for removing a formula from a list. Amy Felty has applied this
+technique using the language $\lambda$Prolog~\cite{felty91a}.
+
+Explicit formalization of sequents can be tiresome. But it gives precise
+control over contraction and weakening, and is essential to handle relevant
+and linear logics.
+
+
+\section{*Packaging sequent rules}\label{sec:thm-pack}
+
+The sequent calculi come with simple proof procedures. These are incomplete
+but are reasonably powerful for interactive use. They expect rules to be
+classified as \textbf{safe} or \textbf{unsafe}. A rule is safe if applying it to a
+provable goal always yields provable subgoals. If a rule is safe then it can
+be applied automatically to a goal without destroying our chances of finding a
+proof. For instance, all the standard rules of the classical sequent calculus
+{\sc lk} are safe. An unsafe rule may render the goal unprovable; typical
+examples are the weakened quantifier rules {\tt allL_thin} and {\tt exR_thin}.
+
+Proof procedures use safe rules whenever possible, using an unsafe rule as a
+last resort. Those safe rules are preferred that generate the fewest
+subgoals. Safe rules are (by definition) deterministic, while the unsafe
+rules require a search strategy, such as backtracking.
+
+A \textbf{pack} is a pair whose first component is a list of safe rules and
+whose second is a list of unsafe rules. Packs can be extended in an obvious
+way to allow reasoning with various collections of rules. For clarity, LK
+declares \mltydx{pack} as an \ML{} datatype, although is essentially a type
+synonym:
+\begin{ttbox}
+datatype pack = Pack of thm list * thm list;
+\end{ttbox}
+Pattern-matching using constructor {\tt Pack} can inspect a pack's
+contents. Packs support the following operations:
+\begin{ttbox}
+pack : unit -> pack
+pack_of : theory -> pack
+empty_pack : pack
+prop_pack : pack
+LK_pack : pack
+LK_dup_pack : pack
+add_safes : pack * thm list -> pack \hfill\textbf{infix 4}
+add_unsafes : pack * thm list -> pack \hfill\textbf{infix 4}
+\end{ttbox}
+\begin{ttdescription}
+\item[\ttindexbold{pack}] returns the pack attached to the current theory.
+
+\item[\ttindexbold{pack_of $thy$}] returns the pack attached to theory $thy$.
+
+\item[\ttindexbold{empty_pack}] is the empty pack.
+
+\item[\ttindexbold{prop_pack}] contains the propositional rules, namely
+those for $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$, along with the
+rules {\tt basic} and {\tt refl}. These are all safe.
+
+\item[\ttindexbold{LK_pack}]
+extends {\tt prop_pack} with the safe rules {\tt allR}
+and~{\tt exL} and the unsafe rules {\tt allL_thin} and
+{\tt exR_thin}. Search using this is incomplete since quantified
+formulae are used at most once.
+
+\item[\ttindexbold{LK_dup_pack}]
+extends {\tt prop_pack} with the safe rules {\tt allR}
+and~{\tt exL} and the unsafe rules \tdx{allL} and~\tdx{exR}.
+Search using this is complete, since quantified formulae may be reused, but
+frequently fails to terminate. It is generally unsuitable for depth-first
+search.
+
+\item[$pack$ \ttindexbold{add_safes} $rules$]
+adds some safe~$rules$ to the pack~$pack$.
+
+\item[$pack$ \ttindexbold{add_unsafes} $rules$]
+adds some unsafe~$rules$ to the pack~$pack$.
+\end{ttdescription}
+
+
+\section{*Proof procedures}\label{sec:sequent-provers}
+
+The LK proof procedure is similar to the classical reasoner described in
+\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+ {Chap.\ts\ref{chap:classical}}.
+%
+In fact it is simpler, since it works directly with sequents rather than
+simulating them. There is no need to distinguish introduction rules from
+elimination rules, and of course there is no swap rule. As always,
+Isabelle's classical proof procedures are less powerful than resolution
+theorem provers. But they are more natural and flexible, working with an
+open-ended set of rules.
+
+Backtracking over the choice of a safe rule accomplishes nothing: applying
+them in any order leads to essentially the same result. Backtracking may
+be necessary over basic sequents when they perform unification. Suppose
+that~0, 1, 2,~3 are constants in the subgoals
+\[ \begin{array}{c}
+ P(0), P(1), P(2) \turn P(\Var{a}) \\
+ P(0), P(2), P(3) \turn P(\Var{a}) \\
+ P(1), P(3), P(2) \turn P(\Var{a})
+ \end{array}
+\]
+The only assignment that satisfies all three subgoals is $\Var{a}\mapsto 2$,
+and this can only be discovered by search. The tactics given below permit
+backtracking only over axioms, such as {\tt basic} and {\tt refl};
+otherwise they are deterministic.
+
+
+\subsection{Method A}
+\begin{ttbox}
+reresolve_tac : thm list -> int -> tactic
+repeat_goal_tac : pack -> int -> tactic
+pc_tac : pack -> int -> tactic
+\end{ttbox}
+These tactics use a method developed by Philippe de Groote. A subgoal is
+refined and the resulting subgoals are attempted in reverse order. For
+some reason, this is much faster than attempting the subgoals in order.
+The method is inherently depth-first.
+
+At present, these tactics only work for rules that have no more than two
+premises. They fail --- return no next state --- if they can do nothing.
+\begin{ttdescription}
+\item[\ttindexbold{reresolve_tac} $thms$ $i$]
+repeatedly applies the $thms$ to subgoal $i$ and the resulting subgoals.
+
+\item[\ttindexbold{repeat_goal_tac} $pack$ $i$]
+applies the safe rules in the pack to a goal and the resulting subgoals.
+If no safe rule is applicable then it applies an unsafe rule and continues.
+
+\item[\ttindexbold{pc_tac} $pack$ $i$]
+applies {\tt repeat_goal_tac} using depth-first search to solve subgoal~$i$.
+\end{ttdescription}
+
+
+\subsection{Method B}
+\begin{ttbox}
+safe_tac : pack -> int -> tactic
+step_tac : pack -> int -> tactic
+fast_tac : pack -> int -> tactic
+best_tac : pack -> int -> tactic
+\end{ttbox}
+These tactics are analogous to those of the generic classical
+reasoner. They use `Method~A' only on safe rules. They fail if they
+can do nothing.
+\begin{ttdescription}
+\item[\ttindexbold{safe_goal_tac} $pack$ $i$]
+applies the safe rules in the pack to a goal and the resulting subgoals.
+It ignores the unsafe rules.
+
+\item[\ttindexbold{step_tac} $pack$ $i$]
+either applies safe rules (using {\tt safe_goal_tac}) or applies one unsafe
+rule.
+
+\item[\ttindexbold{fast_tac} $pack$ $i$]
+applies {\tt step_tac} using depth-first search to solve subgoal~$i$.
+Despite its name, it is frequently slower than {\tt pc_tac}.
+
+\item[\ttindexbold{best_tac} $pack$ $i$]
+applies {\tt step_tac} using best-first search to solve subgoal~$i$. It is
+particularly useful for quantifier duplication (using \ttindex{LK_dup_pack}).
+\end{ttdescription}
+
+
+
+\index{sequent calculus|)}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/Sequents.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,200 @@
+\chapter{Defining A Sequent-Based Logic}
+\label{chap:sequents}
+
+\underscoreon %this file contains the @ character
+
+The Isabelle theory \texttt{Sequents.thy} provides facilities for using
+sequent notation in users' object logics. This theory allows users to
+easily interface the surface syntax of sequences with an underlying
+representation suitable for higher-order unification.
+
+\section{Concrete syntax of sequences}
+
+Mathematicians and logicians have used sequences in an informal way
+much before proof systems such as Isabelle were created. It seems
+sensible to allow people using Isabelle to express sequents and
+perform proofs in this same informal way, and without requiring the
+theory developer to spend a lot of time in \ML{} programming.
+
+By using {\tt Sequents.thy}
+appropriately, a logic developer can allow users to refer to sequences
+in several ways:
+%
+\begin{itemize}
+\item A sequence variable is any alphanumeric string with the first
+ character being a \verb%$% sign.
+So, consider the sequent \verb%$A |- B%, where \verb%$A%
+is intended to match a sequence of zero or more items.
+
+\item A sequence with unspecified sub-sequences and unspecified or
+individual items is written as a comma-separated list of regular
+variables (representing items), particular items, and
+sequence variables, as in
+\begin{ttbox}
+$A, B, C, $D(x) |- E
+\end{ttbox}
+Here both \verb%$A% and \verb%$D(x)%
+are allowed to match any subsequences of items on either side of the
+two items that match $B$ and $C$. Moreover, the sequence matching
+\verb%$D(x)% may contain occurrences of~$x$.
+
+\item An empty sequence can be represented by a blank space, as in
+\verb? |- true?.
+\end{itemize}
+
+These syntactic constructs need to be assimilated into the object
+theory being developed. The type that we use for these visible objects
+is given the name {\tt seq}.
+A {\tt seq} is created either by the empty space, a {\tt seqobj} or a
+{\tt seqobj} followed by a {\tt seq}, with a comma between them. A
+{\tt seqobj} is either an item or a variable representing a
+sequence. Thus, a theory designer can specify a function that takes
+two sequences and returns a meta-level proposition by giving it the
+Isabelle type \verb|[seq, seq] => prop|.
+
+This is all part of the concrete syntax, but one may wish to
+exploit Isabelle's higher-order abstract syntax by actually having a
+different, more powerful {\em internal} syntax.
+
+
+
+\section{ Basis}
+
+One could opt to represent sequences as first-order objects (such as
+simple lists), but this would not allow us to use many facilities
+Isabelle provides for matching. By using a slightly more complex
+representation, users of the logic can reap many benefits in
+facilities for proofs and ease of reading logical terms.
+
+A sequence can be represented as a function --- a constructor for
+further sequences --- by defining a binary {\em abstract} function
+\verb|Seq0'| with type \verb|[o,seq']=>seq'|, and translating a
+sequence such as \verb|A, B, C| into
+\begin{ttbox}
+\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))
+\end{ttbox}
+This sequence can therefore be seen as a constructor
+for further sequences. The constructor \verb|Seq0'| is never given a
+value, and therefore it is not possible to evaluate this expression
+into a basic value.
+
+Furthermore, if we want to represent the sequence \verb|A, $B, C|,
+we note that \verb|$B| already represents a sequence, so we can use
+\verb|B| itself to refer to the function, and therefore the sequence
+can be mapped to the internal form:
+\verb|%s. SeqO'(A, B(SeqO'(C, s)))|.
+
+So, while we wish to continue with the standard, well-liked {\em
+external} representation of sequences, we can represent them {\em
+internally} as functions of type \verb|seq'=>seq'|.
+
+
+\section{Object logics}
+
+Recall that object logics are defined by mapping elements of
+particular types to the Isabelle type \verb|prop|, usually with a
+function called {\tt Trueprop}. So, an object
+logic proposition {\tt P} is matched to the Isabelle proposition
+{\tt Trueprop(P)}\@. The name of the function is often hidden, so the
+user just sees {\tt P}\@. Isabelle is eager to make types match, so it
+inserts {\tt Trueprop} automatically when an object of type {\tt prop}
+is expected. This mechanism can be observed in most of the object
+logics which are direct descendants of {\tt Pure}.
+
+In order to provide the desired syntactic facilities for sequent
+calculi, rather than use just one function that maps object-level
+propositions to meta-level propositions, we use two functions, and
+separate internal from the external representation.
+
+These functions need to be given a type that is appropriate for the particular
+form of sequents required: single or multiple conclusions. So
+multiple-conclusion sequents (used in the LK logic) can be
+specified by the following two definitions, which are lifted from the inbuilt
+{\tt Sequents/LK.thy}:
+\begin{ttbox}
+ Trueprop :: two_seqi
+ "@Trueprop" :: two_seqe ("((_)/ |- (_))" [6,6] 5)
+\end{ttbox}
+%
+where the types used are defined in {\tt Sequents.thy} as
+abbreviations:
+\begin{ttbox}
+ two_seqi = [seq'=>seq', seq'=>seq'] => prop
+ two_seqe = [seq, seq] => prop
+\end{ttbox}
+
+The next step is to actually create links into the low-level parsing
+and pretty-printing mechanisms, which map external and internal
+representations. These functions go below the user level and capture
+the underlying structure of Isabelle terms in \ML{}\@. Fortunately the
+theory developer need not delve in this level; {\tt Sequents.thy}
+provides the necessary facilities. All the theory developer needs to
+add in the \ML{} section is a specification of the two translation
+functions:
+\begin{ttbox}
+ML
+val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
+val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
+\end{ttbox}
+
+In summary: in the logic theory being developed, the developer needs
+to specify the types for the internal and external representation of
+the sequences, and use the appropriate parsing and pretty-printing
+functions.
+
+\section{What's in \texttt{Sequents.thy}}
+
+Theory \texttt{Sequents.thy} makes many declarations that you need to know
+about:
+\begin{enumerate}
+\item The Isabelle types given below, which can be used for the
+constants that map object-level sequents and meta-level propositions:
+%
+\begin{ttbox}
+ single_seqe = [seq,seqobj] => prop
+ single_seqi = [seq'=>seq',seq'=>seq'] => prop
+ two_seqi = [seq'=>seq', seq'=>seq'] => prop
+ two_seqe = [seq, seq] => prop
+ three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop
+ three_seqe = [seq, seq, seq] => prop
+ four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop
+ four_seqe = [seq, seq, seq, seq] => prop
+\end{ttbox}
+
+The \verb|single_| and \verb|two_| sets of mappings for internal and
+external representations are the ones used for, say single and
+multiple conclusion sequents. The other functions are provided to
+allow rules that manipulate more than two functions, as can be seen in
+the inbuilt object logics.
+
+\item An auxiliary syntactic constant has been
+defined that directly maps a sequence to its internal representation:
+\begin{ttbox}
+"@Side" :: seq=>(seq'=>seq') ("<<(_)>>")
+\end{ttbox}
+Whenever a sequence (such as \verb|<< A, $B, $C>>|) is entered using this
+syntax, it is translated into the appropriate internal representation. This
+form can be used only where a sequence is expected.
+
+\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},
+ \texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the
+ translation from external to internal form. Analogously there are
+ \texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},
+ \texttt{four\_seq\_tr'} for pretty-printing, that is, the translation from
+ internal to external form. These functions can be used in the \ML{} section
+ of a theory file to specify the translations to be used. As an example of
+ use, note that in {\tt LK.thy} we declare two identifiers:
+\begin{ttbox}
+val parse_translation =
+ [("@Trueprop",Sequents.two_seq_tr "Trueprop")];
+val print_translation =
+ [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];
+\end{ttbox}
+The given parse translation will be applied whenever a \verb|@Trueprop|
+constant is found, translating using \verb|two_seq_tr| and inserting the
+constant \verb|Trueprop|. The pretty-printing translation is applied
+analogously; a term that contains \verb|Trueprop| is printed as a
+\verb|@Trueprop|.
+\end{enumerate}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/build Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" logo -o isabelle.pdf ""
+"$ISABELLE_TOOL" logo -o isabelle.eps ""
+
+cp "$ISABELLE_HOME/doc-src/iman.sty" .
+cp "$ISABELLE_HOME/doc-src/extra.sty" .
+cp "$ISABELLE_HOME/doc-src/ttbox.sty" .
+cp "$ISABELLE_HOME/doc-src/proof.sty" .
+cp "$ISABELLE_HOME/doc-src/manual.bib" .
+
+"$ISABELLE_TOOL" latex -o sty
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o bbl
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_HOME/doc-src/sedindex" root
+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/preface.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,75 @@
+\chapter*{Preface}
+Several logics come with Isabelle. Many of them are sufficiently developed
+to serve as comfortable reasoning environments. They are also good
+starting points for defining new logics. Each logic is distributed with
+sample proofs, some of which are described in this document.
+
+\texttt{HOL} is currently the best developed Isabelle object-logic, including
+an extensive library of (concrete) mathematics, and various packages for
+advanced definitional concepts (like (co-)inductive sets and types,
+well-founded recursion etc.). The distribution also includes some large
+applications. See the separate manual \emph{Isabelle's Logics: HOL}. There
+is also a comprehensive tutorial on Isabelle/HOL available.
+
+\texttt{ZF} provides another starting point for applications, with a slightly
+less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages
+are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
+more advanced constructions for sets than simply-typed \texttt{HOL}.
+\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
+in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
+
+\medskip There are some further logics distributed with Isabelle:
+\begin{ttdescription}
+\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
+ which is the basis of a preliminary method for deriving programs from
+ proofs~\cite{coen92}. It is built upon classical~FOL.
+
+\item[\thydx{LCF}] is a version of Scott's Logic for Computable
+ Functions, which is also implemented by the~{\sc lcf}
+ system~\cite{paulson87}. It is built upon classical~FOL.
+
+\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
+ \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
+
+\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
+Theory~\cite{nordstrom90}, with extensional equality. Universes are not
+included.
+
+\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
+ \end{ttdescription}
+
+The directory \texttt{Sequents} contains several logics based
+ upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn
+B@1,\ldots,B@n$; rules are applied using associative matching.
+\begin{ttdescription}
+\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
+
+\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.
+
+\item[\thydx{ILL}] implements intuitionistic linear logic.
+\end{ttdescription}
+
+The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
+ Cube} are undocumented. All object-logics' sources are distributed with
+Isabelle (see the directory \texttt{src}). They are also available for
+browsing on the WWW at
+
+\begin{center}\small
+ \begin{tabular}{l}
+ \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
+ \url{http://isabelle.in.tum.de/library/} \\
+ \end{tabular}
+\end{center}
+
+Note that this is not necessarily consistent with your local sources!
+
+\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
+\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
+performing some Isabelle proofs. Consult the {\em Reference Manual} for more
+information on tactics, packages, etc.
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "logics"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/root.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,51 @@
+\documentclass[12pt,a4paper]{report}
+\usepackage{graphicx,iman,extra,ttbox,proof,latexsym,pdfsetup}
+
+%%%STILL NEEDS MODAL, LCF
+%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
+%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
+%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
+%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
+%% run ../sedindex logics to prepare index file
+\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
+
+\author{{\em Lawrence C. Paulson}\\
+ Computer Laboratory \\ University of Cambridge \\
+ \texttt{lcp@cl.cam.ac.uk}\\[3ex]
+ With Contributions by Tobias Nipkow and Markus Wenzel%
+ \thanks{Markus Wenzel made numerous improvements. Sara Kalvala
+ contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote
+ wrote the first version of the logic~LK. Tobias Nipkow developed
+ LCF and~Cube. Martin Coen developed~Modal with assistance
+ from Rajeev Gor\'e. The research has been funded by the EPSRC
+ (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
+ (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
+ Schwerpunktprogramm \emph{Deduktion}.} }
+
+\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
+ \hrule\bigskip}
+\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
+
+\makeindex
+
+\underscoreoff
+
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
+
+\pagestyle{headings}
+\sloppy
+\binperiod %%%treat . like a binary operator
+
+\begin{document}
+\maketitle
+\pagenumbering{roman} \tableofcontents \clearfirst
+\include{preface}
+\include{syntax}
+\include{LK}
+\include{Sequents}
+%%\include{Modal}
+\include{CTT}
+\bibliographystyle{plain}
+\bibliography{manual}
+\printindex
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Logics/document/syntax.tex Mon Aug 27 21:04:37 2012 +0200
@@ -0,0 +1,60 @@
+%% THIS FILE IS COMMON TO ALL LOGIC MANUALS
+
+\chapter{Syntax definitions}
+The syntax of each logic is presented using a context-free grammar.
+These grammars obey the following conventions:
+\begin{itemize}
+\item identifiers denote nonterminal symbols
+\item \texttt{typewriter} font denotes terminal symbols
+\item parentheses $(\ldots)$ express grouping
+\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$
+can be repeated~0 or more times
+\item alternatives are separated by a vertical bar,~$|$
+\item the symbol for alphanumeric identifiers is~{\it id\/}
+\item the symbol for scheme variables is~{\it var}
+\end{itemize}
+To reduce the number of nonterminals and grammar rules required, Isabelle's
+syntax module employs {\bf priorities},\index{priorities} or precedences.
+Each grammar rule is given by a mixfix declaration, which has a priority,
+and each argument place has a priority. This general approach handles
+infix operators that associate either to the left or to the right, as well
+as prefix and binding operators.
+
+In a syntactically valid expression, an operator's arguments never involve
+an operator of lower priority unless brackets are used. Consider
+first-order logic, where $\exists$ has lower priority than $\disj$,
+which has lower priority than $\conj$. There, $P\conj Q \disj R$
+abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also,
+$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than
+$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$
+becomes syntactically invalid if the brackets are removed.
+
+A {\bf binder} is a symbol associated with a constant of type
+$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder
+for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the
+syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall
+x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is
+possible for any constant provided that $\tau$ and $\tau'$ are the same type.
+The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To
+bool)\To\alpha$ and normally binds only one variable.
+ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
+binder because it has type $[i, i\To o]\To o$. The syntax for binders allows
+type constraints on bound variables, as in
+\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
+
+To avoid excess detail, the logic descriptions adopt a semi-formal style.
+Infix operators and binding operators are listed in separate tables, which
+include their priorities. Grammar descriptions do not include numeric
+priorities; instead, the rules appear in order of decreasing priority.
+This should suffice for most purposes; for full details, please consult the
+actual syntax definitions in the {\tt.thy} files.
+
+Each nonterminal symbol is associated with some Isabelle type. For
+example, the formulae of first-order logic have type~$o$. Every
+Isabelle expression of type~$o$ is therefore a formula. These include
+atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
+generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
+suitable types. Therefore, `expression of type~$o$' is listed as a
+separate possibility in the grammar for formulae.
+
+
--- a/doc-src/Logics/logics.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-\documentclass[12pt,a4paper]{report}
-\usepackage{graphicx,../iman,../extra,../ttbox,../proof,latexsym,../pdfsetup}
-
-%%%STILL NEEDS MODAL, LCF
-%%% to index derived rls: ^\([a-zA-Z0-9][a-zA-Z0-9_]*\) \\tdx{\1}
-%%% to index rulenames: ^ *(\([a-zA-Z0-9][a-zA-Z0-9_]*\), \\tdx{\1}
-%%% to index constants: \\tt \([a-zA-Z0-9][a-zA-Z0-9_]*\) \\cdx{\1}
-%%% to deverbify: \\verb|\([^|]*\)| \\ttindex{\1}
-%% run ../sedindex logics to prepare index file
-\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Isabelle's Logics}
-
-\author{{\em Lawrence C. Paulson}\\
- Computer Laboratory \\ University of Cambridge \\
- \texttt{lcp@cl.cam.ac.uk}\\[3ex]
- With Contributions by Tobias Nipkow and Markus Wenzel%
- \thanks{Markus Wenzel made numerous improvements. Sara Kalvala
- contributed Chap.\ts\ref{chap:sequents}. Philippe de Groote
- wrote the first version of the logic~LK. Tobias Nipkow developed
- LCF and~Cube. Martin Coen developed~Modal with assistance
- from Rajeev Gor\'e. The research has been funded by the EPSRC
- (grants GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT
- (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG
- Schwerpunktprogramm \emph{Deduktion}.} }
-
-\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip
- \hrule\bigskip}
-\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}}
-
-\makeindex
-
-\underscoreoff
-
-\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} %% {secnumdepth}{2}???
-
-\pagestyle{headings}
-\sloppy
-\binperiod %%%treat . like a binary operator
-
-\begin{document}
-\maketitle
-\pagenumbering{roman} \tableofcontents \clearfirst
-\include{preface}
-\include{syntax}
-\include{LK}
-\include{Sequents}
-%%\include{Modal}
-\include{CTT}
-\bibliographystyle{plain}
-\bibliography{../manual}
-\printindex
-\end{document}
--- a/doc-src/Logics/preface.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-\chapter*{Preface}
-Several logics come with Isabelle. Many of them are sufficiently developed
-to serve as comfortable reasoning environments. They are also good
-starting points for defining new logics. Each logic is distributed with
-sample proofs, some of which are described in this document.
-
-\texttt{HOL} is currently the best developed Isabelle object-logic, including
-an extensive library of (concrete) mathematics, and various packages for
-advanced definitional concepts (like (co-)inductive sets and types,
-well-founded recursion etc.). The distribution also includes some large
-applications. See the separate manual \emph{Isabelle's Logics: HOL}. There
-is also a comprehensive tutorial on Isabelle/HOL available.
-
-\texttt{ZF} provides another starting point for applications, with a slightly
-less developed library than \texttt{HOL}. \texttt{ZF}'s definitional packages
-are similar to those of \texttt{HOL}. Untyped \texttt{ZF} set theory provides
-more advanced constructions for sets than simply-typed \texttt{HOL}.
-\texttt{ZF} is built on \texttt{FOL} (first-order logic), both are described
-in a separate manual \emph{Isabelle's Logics: FOL and ZF}~\cite{isabelle-ZF}.
-
-\medskip There are some further logics distributed with Isabelle:
-\begin{ttdescription}
-\item[\thydx{CCL}] is Martin Coen's Classical Computational Logic,
- which is the basis of a preliminary method for deriving programs from
- proofs~\cite{coen92}. It is built upon classical~FOL.
-
-\item[\thydx{LCF}] is a version of Scott's Logic for Computable
- Functions, which is also implemented by the~{\sc lcf}
- system~\cite{paulson87}. It is built upon classical~FOL.
-
-\item[\thydx{HOLCF}] is a version of {\sc lcf}, defined as an extension of
- \texttt{HOL}\@. See \cite{MuellerNvOS99} for more details on \texttt{HOLCF}.
-
-\item[\thydx{CTT}] is a version of Martin-L\"of's Constructive Type
-Theory~\cite{nordstrom90}, with extensional equality. Universes are not
-included.
-
-\item[\thydx{Cube}] is Barendregt's $\lambda$-cube.
- \end{ttdescription}
-
-The directory \texttt{Sequents} contains several logics based
- upon the sequent calculus. Sequents have the form $A@1,\ldots,A@m\turn
-B@1,\ldots,B@n$; rules are applied using associative matching.
-\begin{ttdescription}
-\item[\thydx{LK}] is classical first-order logic as a sequent calculus.
-
-\item[\thydx{Modal}] implements the modal logics $T$, $S4$, and~$S43$.
-
-\item[\thydx{ILL}] implements intuitionistic linear logic.
-\end{ttdescription}
-
-The logics \texttt{CCL}, \texttt{LCF}, \texttt{Modal}, \texttt{ILL} and {\tt
- Cube} are undocumented. All object-logics' sources are distributed with
-Isabelle (see the directory \texttt{src}). They are also available for
-browsing on the WWW at
-
-\begin{center}\small
- \begin{tabular}{l}
- \url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/library/} \\
- \url{http://isabelle.in.tum.de/library/} \\
- \end{tabular}
-\end{center}
-
-Note that this is not necessarily consistent with your local sources!
-
-\medskip Do not read the \emph{Isabelle's Logics} manuals before reading
-\emph{Isabelle/HOL --- The Tutorial} or \emph{Introduction to Isabelle}, and
-performing some Isabelle proofs. Consult the {\em Reference Manual} for more
-information on tactics, packages, etc.
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "logics"
-%%% End:
--- a/doc-src/Logics/syntax.tex Mon Aug 27 20:50:10 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-%% THIS FILE IS COMMON TO ALL LOGIC MANUALS
-
-\chapter{Syntax definitions}
-The syntax of each logic is presented using a context-free grammar.
-These grammars obey the following conventions:
-\begin{itemize}
-\item identifiers denote nonterminal symbols
-\item \texttt{typewriter} font denotes terminal symbols
-\item parentheses $(\ldots)$ express grouping
-\item constructs followed by a Kleene star, such as $id^*$ and $(\ldots)^*$
-can be repeated~0 or more times
-\item alternatives are separated by a vertical bar,~$|$
-\item the symbol for alphanumeric identifiers is~{\it id\/}
-\item the symbol for scheme variables is~{\it var}
-\end{itemize}
-To reduce the number of nonterminals and grammar rules required, Isabelle's
-syntax module employs {\bf priorities},\index{priorities} or precedences.
-Each grammar rule is given by a mixfix declaration, which has a priority,
-and each argument place has a priority. This general approach handles
-infix operators that associate either to the left or to the right, as well
-as prefix and binding operators.
-
-In a syntactically valid expression, an operator's arguments never involve
-an operator of lower priority unless brackets are used. Consider
-first-order logic, where $\exists$ has lower priority than $\disj$,
-which has lower priority than $\conj$. There, $P\conj Q \disj R$
-abbreviates $(P\conj Q) \disj R$ rather than $P\conj (Q\disj R)$. Also,
-$\exists x.P\disj Q$ abbreviates $\exists x.(P\disj Q)$ rather than
-$(\exists x.P)\disj Q$. Note especially that $P\disj(\exists x.Q)$
-becomes syntactically invalid if the brackets are removed.
-
-A {\bf binder} is a symbol associated with a constant of type
-$(\sigma\To\tau)\To\tau'$. For instance, we may declare~$\forall$ as a binder
-for the constant~$All$, which has type $(\alpha\To o)\To o$. This defines the
-syntax $\forall x.t$ to mean $All(\lambda x.t)$. We can also write $\forall
-x@1\ldots x@m.t$ to abbreviate $\forall x@1. \ldots \forall x@m.t$; this is
-possible for any constant provided that $\tau$ and $\tau'$ are the same type.
-The Hilbert description operator $\varepsilon x.P\,x$ has type $(\alpha\To
-bool)\To\alpha$ and normally binds only one variable.
-ZF's bounded quantifier $\forall x\in A.P(x)$ cannot be declared as a
-binder because it has type $[i, i\To o]\To o$. The syntax for binders allows
-type constraints on bound variables, as in
-\[ \forall (x{::}\alpha) \; (y{::}\beta) \; z{::}\gamma. Q(x,y,z) \]
-
-To avoid excess detail, the logic descriptions adopt a semi-formal style.
-Infix operators and binding operators are listed in separate tables, which
-include their priorities. Grammar descriptions do not include numeric
-priorities; instead, the rules appear in order of decreasing priority.
-This should suffice for most purposes; for full details, please consult the
-actual syntax definitions in the {\tt.thy} files.
-
-Each nonterminal symbol is associated with some Isabelle type. For
-example, the formulae of first-order logic have type~$o$. Every
-Isabelle expression of type~$o$ is therefore a formula. These include
-atomic formulae such as $P$, where $P$ is a variable of type~$o$, and more
-generally expressions such as $P(t,u)$, where $P$, $t$ and~$u$ have
-suitable types. Therefore, `expression of type~$o$' is listed as a
-separate possibility in the grammar for formulae.
-
-
--- a/doc-src/ROOT Mon Aug 27 20:50:10 2012 +0200
+++ b/doc-src/ROOT Mon Aug 27 21:04:37 2012 +0200
@@ -109,6 +109,18 @@
Examples2
Examples3
+session Logics (doc) in "Logics" = Pure +
+ options [document_variants = "logics"]
+ theories
+ files
+ "../iman.sty"
+ "../extra.sty"
+ "../ttbox.sty"
+ "../proof.sty"
+ "../manual.bib"
+ "document/build"
+ "document/root.tex"
+
session Main (doc) in "Main/Docs" = HOL +
options [browser_info = false, document = false,
document_dump = document, document_dump_mode = "tex"]