src/CTT/ex/synth.ML
author paulson
Tue Apr 30 11:08:09 1996 +0200 (1996-04-30)
changeset 1702 4aa538e82f76
parent 1459 d12da312eff4
child 9251 bd57acd44fc1
permissions -rw-r--r--
Cosmetic re-ordering of declarations
     1 (*  Title:      CTT/ex/synth
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 writeln"Synthesis examples, using a crude form of narrowing";
     8 
     9 
    10 writeln"discovery of predecessor function";
    11 goal CTT.thy 
    12  "?a : SUM pred:?A . Eq(N, pred`0, 0)   \
    13 \                 *  (PROD n:N. Eq(N, pred ` succ(n), n))";
    14 by (intr_tac[]);
    15 by eqintr_tac;
    16 by (resolve_tac reduction_rls 3);
    17 by (resolve_tac comp_rls 5);
    18 by (rew_tac[]);
    19 result();
    20 
    21 writeln"the function fst as an element of a function type";
    22 val prems = goal CTT.thy 
    23     "A type ==> ?a: SUM f:?B . PROD i:A. PROD j:A. Eq(A, f ` <i,j>, i)";
    24 by (intr_tac prems);
    25 by eqintr_tac;
    26 by (resolve_tac reduction_rls 2);
    27 by (resolve_tac comp_rls 4);
    28 by (typechk_tac prems);
    29 writeln"now put in A everywhere";
    30 by (REPEAT (resolve_tac prems 1));
    31 by (fold_tac basic_defs);
    32 result();
    33 
    34 writeln"An interesting use of the eliminator, when";
    35 (*The early implementation of unification caused non-rigid path in occur check
    36   See following example.*)
    37 goal CTT.thy 
    38     "?a : PROD i:N. Eq(?A, ?b(inl(i)), <0    ,   i>)  \
    39 \                 * Eq(?A, ?b(inr(i)), <succ(0), i>)";
    40 by (intr_tac[]);
    41 by eqintr_tac;
    42 by (resolve_tac comp_rls 1);
    43 by (rew_tac[]);
    44 uresult();
    45 
    46 (*Here we allow the type to depend on i.  
    47  This prevents the cycle in the first unification (no longer needed).  
    48  Requires flex-flex to preserve the dependence.
    49  Simpler still: make ?A into a constant type N*N.*)
    50 goal CTT.thy 
    51     "?a : PROD i:N. Eq(?A(i), ?b(inl(i)), <0   ,   i>)   \
    52 \                *  Eq(?A(i), ?b(inr(i)), <succ(0),i>)";
    53 
    54 writeln"A tricky combination of when and split";
    55 (*Now handled easily, but caused great problems once*)
    56 goal CTT.thy 
    57     "?a : PROD i:N. PROD j:N. Eq(?A, ?b(inl(<i,j>)), i)   \
    58 \                          *  Eq(?A, ?b(inr(<i,j>)), j)";
    59 by (intr_tac[]); 
    60 by eqintr_tac;
    61 by (resolve_tac [ PlusC_inl RS trans_elem ] 1);
    62 by (resolve_tac comp_rls 4); 
    63 by (resolve_tac reduction_rls 7);
    64 by (resolve_tac comp_rls 10);
    65 by (typechk_tac[]); (*2 secs*)
    66 by (fold_tac basic_defs);
    67 uresult();
    68 
    69 (*similar but allows the type to depend on i and j*)
    70 goal CTT.thy 
    71     "?a : PROD i:N. PROD j:N. Eq(?A(i,j), ?b(inl(<i,j>)), i) \
    72 \                         *   Eq(?A(i,j), ?b(inr(<i,j>)), j)";
    73 
    74 (*similar but specifying the type N simplifies the unification problems*)
    75 goal CTT.thy
    76     "?a : PROD i:N. PROD j:N. Eq(N, ?b(inl(<i,j>)), i)  \
    77 \                         *   Eq(N, ?b(inr(<i,j>)), j)";
    78 
    79 
    80 writeln"Deriving the addition operator";
    81 goal Arith.thy 
    82    "?c : PROD n:N. Eq(N, ?f(0,n), n)  \
    83 \               *  (PROD m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))";
    84 by (intr_tac[]);
    85 by eqintr_tac;
    86 by (resolve_tac comp_rls 1);
    87 by (rew_tac[]);
    88 by (fold_tac arith_defs);
    89 result();
    90 
    91 writeln"The addition function -- using explicit lambdas";
    92 goal Arith.thy 
    93   "?c : SUM plus : ?A .  \
    94 \        PROD x:N. Eq(N, plus`0`x, x)  \
    95 \               *  (PROD y:N. Eq(N, plus`succ(y)`x, succ(plus`y`x)))";
    96 by (intr_tac[]);
    97 by eqintr_tac;
    98 by (resolve_tac [TSimp.split_eqn] 3);
    99 by (SELECT_GOAL (rew_tac[]) 4);
   100 by (resolve_tac [TSimp.split_eqn] 3);
   101 by (SELECT_GOAL (rew_tac[]) 4);
   102 by (res_inst_tac [("p","y")] NC_succ 3);
   103   (**  by (resolve_tac comp_rls 3);  caused excessive branching  **)
   104 by (rew_tac[]); 
   105 by (fold_tac arith_defs);
   106 result();
   107 
   108 writeln"Reached end of file.";