(*  Title:      CTT/ex/elim
    ID:         $Id: elim.ML,v 1.7 2005/04/07 07:25:34 wenzelm Exp $
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1991  University of Cambridge

Some examples taken from P. Martin-L\"of, Intuitionistic type theory
        (Bibliopolis, 1984).

by (safe_tac prems 1);
by (step_tac prems 1);
by (pc_tac prems 1);
*)

writeln"Examples with elimination rules";


writeln"This finds the functions fst and snd!"; 
Goal "A type ==> ?a : (A*A) --> A";
by (pc_tac [] 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
result();
writeln"first solution is fst;  backtracking gives snd";
back(); 
back() handle ERROR => writeln"And there are indeed no others";  


writeln"Double negation of the Excluded Middle";
Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
by (intr_tac []);
by (rtac ProdE 1);
by (assume_tac 1);
by (pc_tac [] 1);
result();

Goal "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
by (pc_tac [] 1);
result();
(*The sequent version (ITT) could produce an interesting alternative
  by backtracking.  No longer.*)

writeln"Binary sums and products";
Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
by (pc_tac [] 1);
result();

(*A distributive law*)
Goal "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
by (pc_tac [] 1);
result();

(*more general version, same proof*)
val prems = Goal
   "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
\      ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
by (pc_tac prems 1);
result();

writeln"Construction of the currying functional";
Goal "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
by (pc_tac [] 1);
result();

(*more general goal with same proof*)
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 (pc_tac prems 1);
result();

writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
Goal "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
by (pc_tac [] 1);
result();

(*more general goal with same proof*)
val prems = Goal 
 "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \
\  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
\       --> (PROD z : (SUM x:A . B(x)) . C(z))";
by (pc_tac prems 1);
result();

writeln"Function application";
Goal "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
by (pc_tac [] 1);
result();

writeln"Basic test of quantifier reasoning";
val prems = Goal  
    "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
\    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
\         --> (PROD x:A . SUM y:B . C(x,y))";
by (pc_tac prems 1);
result();

(*faulty proof attempt, stripping the quantifiers in wrong sequence
by (intr_tac[]);
by (pc_tac prems 1);        ...fails!!  *)

writeln"Martin-Lof (1984) pages 36-7: the combinator S";
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. PROD y:B(x). C(x,y)) \
\            --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
by (pc_tac prems 1);
result();

writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
val prems = Goal
    "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
\    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
\         --> (PROD z: A+B. C(z))";
by (pc_tac prems 1);
result();

(*towards AXIOM OF CHOICE*)
Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
by (pc_tac [] 1);
by (fold_tac basic_defs);   (*puts in fst and snd*)
result();

(*Martin-Lof (1984) page 50*)
writeln"AXIOM OF CHOICE!  Delicate use of elimination rules";
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 (add_mp_tac 2);
by (add_mp_tac 1);
by (etac SumE_fst 1);
by (rtac replace_type 1);
by (rtac subst_eqtyparg 1);
by (resolve_tac comp_rls 1);
by (rtac SumE_snd 4);
by (typechk_tac (SumE_fst::prems));
result();

writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
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);
(*Must not use add_mp_tac as subst_prodE hides the construction.*)
by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);
by (TRYALL assume_tac);
by (rtac replace_type 1);
by (rtac subst_eqtyparg 1);
by (resolve_tac comp_rls 1);
by (etac (ProdE RS SumE) 4);
by (typechk_tac prems);
by (rtac replace_type 1);
by (rtac subst_eqtyparg 1);
by (resolve_tac comp_rls 1);
by (typechk_tac prems);
by (assume_tac 1);
by (fold_tac basic_defs);  (*puts in fst and snd*)
result();

writeln"Example of sequent_style deduction"; 
(*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
    lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
val prems = Goal   
    "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
\    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
by (resolve_tac intr_rls 1);
by (biresolve_tac safe_brls 2);
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
by (res_inst_tac [ ("a","y") ] ProdE 2);
by (typechk_tac prems);
by (rtac SumE 1  THEN  assume_tac 1);
by (intr_tac[]);
by (TRYALL assume_tac);
by (typechk_tac prems);
result();

writeln"Reached end of file.";