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