src/CTT/ex/elim.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 281 f1f96b9e6285
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	CTT/ex/elim
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 
     6 Some examples taken from P. Martin-L\"of, Intuitionistic type theory
     7 	(Bibliopolis, 1984).
     8 
     9 by (safe_tac prems 1);
    10 by (step_tac prems 1);
    11 by (pc_tac prems 1);
    12 *)
    13 
    14 writeln"Examples with elimination rules";
    15 
    16 
    17 writeln"This finds the functions fst and snd!"; 
    18 val prems = goal CTT.thy "A type ==> ?a : (A*A) --> A";
    19 by (pc_tac prems 1  THEN  fold_tac basic_defs);   (*puts in fst and snd*)
    20 result();
    21 writeln"first solution is fst;  backtracking gives snd";
    22 back(); 
    23 back() handle ERROR => writeln"And there are indeed no others";  
    24 
    25 
    26 writeln"Double negation of the Excluded Middle";
    27 val prems = goal CTT.thy "A type ==> ?a : ((A + (A-->F)) --> F) --> F";
    28 by (intr_tac prems);
    29 by (rtac ProdE 1);
    30 by (assume_tac 1);
    31 by (pc_tac prems 1);
    32 result();
    33 
    34 val prems = goal CTT.thy 
    35     "[| A type;  B type |] ==> ?a : (A*B) --> (B*A)";
    36 by (pc_tac prems 1);
    37 result();
    38 (*The sequent version (ITT) could produce an interesting alternative
    39   by backtracking.  No longer.*)
    40 
    41 writeln"Binary sums and products";
    42 val prems = goal CTT.thy
    43    "[| A type;  B type;  C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)";
    44 by (pc_tac prems 1);
    45 result();
    46 
    47 (*A distributive law*)
    48 val prems = goal CTT.thy 
    49     "[| A type;  B type;  C type |] ==> ?a : A * (B+C)  -->  (A*B + A*C)";
    50 by (pc_tac prems 1);
    51 result();
    52 
    53 (*more general version, same proof*)
    54 val prems = goal CTT.thy 
    55     "[| A type;  !!x. x:A ==> B(x) type;  !!x. x:A ==> C(x) type|] ==> \
    56 \    ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))";
    57 by (pc_tac prems 1);
    58 result();
    59 
    60 writeln"Construction of the currying functional";
    61 val prems = goal CTT.thy 
    62     "[| A type;  B type;  C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))";
    63 by (pc_tac prems 1);
    64 result();
    65 
    66 (*more general goal with same proof*)
    67 val prems = goal CTT.thy  
    68     "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A. B(x)) ==> C(z) type|] \
    69 \    ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
    70 \         --> (PROD x:A . PROD y:B(x) . C(<x,y>))";
    71 by (pc_tac prems 1);
    72 result();
    73 
    74 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
    75 val prems = goal CTT.thy 
    76     "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
    77 by (pc_tac prems 1);
    78 result();
    79 
    80 (*more general goal with same proof*)
    81 val prems = goal CTT.thy 
    82   "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \
    83 \  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
    84 \       --> (PROD z : (SUM x:A . B(x)) . C(z))";
    85 by (pc_tac prems 1);
    86 result();
    87 
    88 writeln"Function application";
    89 val prems = goal CTT.thy  
    90     "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
    91 by (pc_tac prems 1);
    92 result();
    93 
    94 writeln"Basic test of quantifier reasoning";
    95 val prems = goal CTT.thy  
    96     "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
    97 \    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
    98 \         --> (PROD x:A . SUM y:B . C(x,y))";
    99 by (pc_tac prems 1);
   100 result();
   101 
   102 (*faulty proof attempt, stripping the quantifiers in wrong sequence
   103 by (intr_tac[]);
   104 by (pc_tac prems 1);        ...fails!!  *)
   105 
   106 writeln"Martin-Lof (1984) pages 36-7: the combinator S";
   107 val prems = goal CTT.thy  
   108     "[| A type;  !!x. x:A ==> B(x) type;  \
   109 \       !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
   110 \    ==> ?a :    (PROD x:A. PROD y:B(x). C(x,y)) \
   111 \            --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   112 by (pc_tac prems 1);
   113 result();
   114 
   115 writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
   116 val prems = goal CTT.thy
   117     "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
   118 \    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
   119 \         --> (PROD z: A+B. C(z))";
   120 by (pc_tac prems 1);
   121 result();
   122 
   123 (*towards AXIOM OF CHOICE*)
   124 val prems = goal CTT.thy  
   125   "[| A type;  B type;  C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
   126 by (pc_tac prems 1);
   127 by (fold_tac basic_defs);   (*puts in fst and snd*)
   128 result();
   129 
   130 (*Martin-Lof (1984) page 50*)
   131 writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
   132 val prems = goal CTT.thy   
   133     "[| A type;  !!x. x:A ==> B(x) type;  \
   134 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|]  \
   135 \    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y))    \
   136 \            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   137 by (intr_tac prems);
   138 by (add_mp_tac 2);
   139 by (add_mp_tac 1);
   140 by (etac SumE_fst 1);
   141 by (rtac replace_type 1);
   142 by (rtac subst_eqtyparg 1);
   143 by (resolve_tac comp_rls 1);
   144 by (rtac SumE_snd 4);
   145 by (typechk_tac (SumE_fst::prems));
   146 result();
   147 
   148 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
   149 val prems = goal CTT.thy   
   150     "[| A type;  !!x.x:A ==> B(x) type;  \
   151 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type|] \
   152 \    ==> ?a :    (PROD x:A. SUM y:B(x). C(x,y)) \
   153 \            --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   154 by (intr_tac prems);
   155 (*Must not use add_mp_tac as subst_prodE hides the construction.*)
   156 by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);
   157 by (TRYALL assume_tac);
   158 by (rtac replace_type 1);
   159 by (rtac subst_eqtyparg 1);
   160 by (resolve_tac comp_rls 1);
   161 by (etac (ProdE RS SumE) 4);
   162 by (typechk_tac prems);
   163 by (rtac replace_type 1);
   164 by (rtac subst_eqtyparg 1);
   165 by (resolve_tac comp_rls 1);
   166 by (typechk_tac prems);
   167 by (assume_tac 1);
   168 by (fold_tac basic_defs);  (*puts in fst and snd*)
   169 result();
   170 
   171 writeln"Example of sequent_style deduction"; 
   172 (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   173     lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
   174 val prems = goal CTT.thy   
   175     "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
   176 \    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
   177 by (resolve_tac intr_rls 1);
   178 by (biresolve_tac safe_brls 2);
   179 (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
   180 by (res_inst_tac [ ("a","y") ] ProdE 2);
   181 by (typechk_tac prems);
   182 by (rtac SumE 1  THEN  assume_tac 1);
   183 by (intr_tac[]);
   184 by (TRYALL assume_tac);
   185 by (typechk_tac prems);
   186 result();
   187 
   188 writeln"Reached end of file.";