src/CTT/ex/elim.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1446 a8387e934fa7
child 3837 d7f033c74b38
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     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;                         \
    69 \               !!z. z: (SUM x:A. B(x)) ==> C(z) type           \
    70 \    |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).    \
    71 \                     (PROD x:A . PROD y:B(x) . C(<x,y>))";
    72 by (pc_tac prems 1);
    73 result();
    74 
    75 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)";
    76 val prems = goal CTT.thy 
    77     "[| A type;  B type;  C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)";
    78 by (pc_tac prems 1);
    79 result();
    80 
    81 (*more general goal with same proof*)
    82 val prems = goal CTT.thy 
    83   "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \
    84 \  ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \
    85 \       --> (PROD z : (SUM x:A . B(x)) . C(z))";
    86 by (pc_tac prems 1);
    87 result();
    88 
    89 writeln"Function application";
    90 val prems = goal CTT.thy  
    91     "[| A type;  B type |] ==> ?a : ((A --> B) * A) --> B";
    92 by (pc_tac prems 1);
    93 result();
    94 
    95 writeln"Basic test of quantifier reasoning";
    96 val prems = goal CTT.thy  
    97     "[| A type;  B type;  !!x y.[| x:A;  y:B |] ==> C(x,y) type |] ==> \
    98 \    ?a :     (SUM y:B . PROD x:A . C(x,y))  \
    99 \         --> (PROD x:A . SUM y:B . C(x,y))";
   100 by (pc_tac prems 1);
   101 result();
   102 
   103 (*faulty proof attempt, stripping the quantifiers in wrong sequence
   104 by (intr_tac[]);
   105 by (pc_tac prems 1);        ...fails!!  *)
   106 
   107 writeln"Martin-Lof (1984) pages 36-7: the combinator S";
   108 val prems = goal CTT.thy  
   109     "[| A type;  !!x. x:A ==> B(x) type;  \
   110 \       !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \
   111 \    ==> ?a :    (PROD x:A. PROD y:B(x). C(x,y)) \
   112 \            --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   113 by (pc_tac prems 1);
   114 result();
   115 
   116 writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination";
   117 val prems = goal CTT.thy
   118     "[| A type;  B type;  !!z. z: A+B ==> C(z) type|] ==> \
   119 \    ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))  \
   120 \         --> (PROD z: A+B. C(z))";
   121 by (pc_tac prems 1);
   122 result();
   123 
   124 (*towards AXIOM OF CHOICE*)
   125 val prems = goal CTT.thy  
   126   "[| A type;  B type;  C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)";
   127 by (pc_tac prems 1);
   128 by (fold_tac basic_defs);   (*puts in fst and snd*)
   129 result();
   130 
   131 (*Martin-Lof (1984) page 50*)
   132 writeln"AXIOM OF CHOICE!!!  Delicate use of elimination rules";
   133 val prems = goal CTT.thy   
   134     "[| A type;  !!x. x:A ==> B(x) type;                        \
   135 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
   136 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
   137 \                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   138 by (intr_tac prems);
   139 by (add_mp_tac 2);
   140 by (add_mp_tac 1);
   141 by (etac SumE_fst 1);
   142 by (rtac replace_type 1);
   143 by (rtac subst_eqtyparg 1);
   144 by (resolve_tac comp_rls 1);
   145 by (rtac SumE_snd 4);
   146 by (typechk_tac (SumE_fst::prems));
   147 result();
   148 
   149 writeln"Axiom of choice.  Proof without fst, snd.  Harder still!"; 
   150 val prems = goal CTT.thy   
   151     "[| A type;  !!x.x:A ==> B(x) type;                         \
   152 \       !!x y.[| x:A;  y:B(x) |] ==> C(x,y) type                \
   153 \    |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).        \
   154 \                        (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))";
   155 by (intr_tac prems);
   156 (*Must not use add_mp_tac as subst_prodE hides the construction.*)
   157 by (resolve_tac [ProdE RS SumE] 1  THEN  assume_tac 1);
   158 by (TRYALL assume_tac);
   159 by (rtac replace_type 1);
   160 by (rtac subst_eqtyparg 1);
   161 by (resolve_tac comp_rls 1);
   162 by (etac (ProdE RS SumE) 4);
   163 by (typechk_tac prems);
   164 by (rtac replace_type 1);
   165 by (rtac subst_eqtyparg 1);
   166 by (resolve_tac comp_rls 1);
   167 by (typechk_tac prems);
   168 by (assume_tac 1);
   169 by (fold_tac basic_defs);  (*puts in fst and snd*)
   170 result();
   171 
   172 writeln"Example of sequent_style deduction"; 
   173 (*When splitting z:A*B, the assumption C(z) is affected;  ?a becomes
   174     lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w)     *)
   175 val prems = goal CTT.thy   
   176     "[| A type;  B type;  !!z. z:A*B ==> C(z) type |] ==>  \
   177 \    ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))";
   178 by (resolve_tac intr_rls 1);
   179 by (biresolve_tac safe_brls 2);
   180 (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
   181 by (res_inst_tac [ ("a","y") ] ProdE 2);
   182 by (typechk_tac prems);
   183 by (rtac SumE 1  THEN  assume_tac 1);
   184 by (intr_tac[]);
   185 by (TRYALL assume_tac);
   186 by (typechk_tac prems);
   187 result();
   188 
   189 writeln"Reached end of file.";