src/ZF/ex/Contract0.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	ZF/ex/contract.ML
     2     ID:         $Id$
     3     Author: 	Tobias Nipkow & Lawrence C Paulson
     4     Copyright   1992  University of Cambridge
     5 
     6 For ex/contract.thy.
     7 *)
     8 
     9 open Contract0;
    10 
    11 structure Contract = Inductive_Fun
    12  (val thy = Contract0.thy;
    13   val rec_doms = [("contract","comb*comb")];
    14   val sintrs = 
    15       ["[| p:comb;  q:comb |] ==> K#p#q -1-> p",
    16        "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)",
    17        "[| p-1->q;  r:comb |] ==> p#r -1-> q#r",
    18        "[| p-1->q;  r:comb |] ==> r#p -1-> r#q"];
    19   val monos = [];
    20   val con_defs = [];
    21   val type_intrs = Comb.intrs@[SigmaI];
    22   val type_elims = [SigmaE2]);
    23 
    24 val [K_contract,S_contract,Ap_contract1,Ap_contract2] = Contract.intrs;
    25 
    26 val contract_induct = standard
    27     (Contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
    28 
    29 (*For type checking: replaces a-1->b by a,b:comb *)
    30 val contract_combE2 = Contract.dom_subset RS subsetD RS SigmaE2;
    31 val contract_combD1 = Contract.dom_subset RS subsetD RS SigmaD1;
    32 val contract_combD2 = Contract.dom_subset RS subsetD RS SigmaD2;
    33 
    34 goal Contract.thy "field(contract) = comb";
    35 by (fast_tac (ZF_cs addIs [equalityI,K_contract] addSEs [contract_combE2]) 1);
    36 val field_contract_eq = result();
    37 
    38 val reduction_refl = standard
    39     (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
    40 
    41 val rtrancl_into_rtrancl2 = standard
    42     (r_into_rtrancl RS (trans_rtrancl RS transD));
    43 
    44 val reduction_rls = [reduction_refl, K_contract, S_contract, 
    45 		     K_contract RS rtrancl_into_rtrancl2,
    46 		     S_contract RS rtrancl_into_rtrancl2,
    47 		     Ap_contract1 RS rtrancl_into_rtrancl2,
    48 		     Ap_contract2 RS rtrancl_into_rtrancl2];
    49 
    50 goalw Contract.thy [I_def] "!!p. p:comb ==> I#p ---> p";
    51 by (REPEAT (ares_tac (Comb.intrs @ reduction_rls) 1));
    52 val I_reduce = result();
    53 
    54 goalw Contract.thy [I_def] "I: comb";
    55 by (REPEAT (ares_tac Comb.intrs 1));
    56 val I_comb = result();
    57 
    58 (** Non-contraction results **)
    59 
    60 (*Derive a case for each combinator constructor*)
    61 val K_contract_case = Contract.mk_cases Comb.con_defs "K -1-> r";
    62 val S_contract_case = Contract.mk_cases Comb.con_defs "S -1-> r";
    63 val Ap_contract_case = Contract.mk_cases Comb.con_defs "p#q -1-> r";
    64 
    65 val contract_cs =
    66     ZF_cs addSIs Comb.intrs
    67 	  addIs  Contract.intrs
    68 	  addSEs [contract_combD1,contract_combD2]     (*type checking*)
    69 	  addSEs [K_contract_case, S_contract_case, Ap_contract_case]
    70 	  addSEs Comb.free_SEs;
    71 
    72 goalw Contract.thy [I_def] "!!r. I -1-> r ==> P";
    73 by (fast_tac contract_cs 1);
    74 val I_contract_case = result();
    75 
    76 goal Contract.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
    77 by (fast_tac contract_cs 1);
    78 val K1_contractD = result();
    79 
    80 goal Contract.thy "!!p r. [| p ---> q;  r: comb |] ==> p#r ---> q#r";
    81 by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    82 by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    83 by (etac rtrancl_induct 1);
    84 by (fast_tac (contract_cs addIs reduction_rls) 1);
    85 by (etac (trans_rtrancl RS transD) 1);
    86 by (fast_tac (contract_cs addIs reduction_rls) 1);
    87 val Ap_reduce1 = result();
    88 
    89 goal Contract.thy "!!p r. [| p ---> q;  r: comb |] ==> r#p ---> r#q";
    90 by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    91 by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    92 by (etac rtrancl_induct 1);
    93 by (fast_tac (contract_cs addIs reduction_rls) 1);
    94 by (etac (trans_rtrancl RS transD) 1);
    95 by (fast_tac (contract_cs addIs reduction_rls) 1);
    96 val Ap_reduce2 = result();
    97 
    98 (** Counterexample to the diamond property for -1-> **)
    99 
   100 goal Contract.thy "K#I#(I#I) -1-> I";
   101 by (REPEAT (ares_tac [K_contract, I_comb, Ap_comb] 1));
   102 val KIII_contract1 = result();
   103 
   104 goalw Contract.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
   105 by (DEPTH_SOLVE (resolve_tac (Comb.intrs @ Contract.intrs) 1));
   106 val KIII_contract2 = result();
   107 
   108 goal Contract.thy "K#I#((K#I)#(K#I)) -1-> I";
   109 by (REPEAT (ares_tac (Comb.intrs @ [K_contract, I_comb]) 1));
   110 val KIII_contract3 = result();
   111 
   112 goalw Contract.thy [diamond_def] "~ diamond(contract)";
   113 by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
   114                     addSEs [I_contract_case]) 1);
   115 val not_diamond_contract = result();
   116 
   117 writeln"Reached end of file.";