src/ZF/ex/Contract0.ML
changeset 0 a5a9c433f639
child 16 0b033d50ca1c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/Contract0.ML	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,117 @@
     1.4 +(*  Title: 	ZF/ex/contract.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Tobias Nipkow & Lawrence C Paulson
     1.7 +    Copyright   1992  University of Cambridge
     1.8 +
     1.9 +For ex/contract.thy.
    1.10 +*)
    1.11 +
    1.12 +open Contract0;
    1.13 +
    1.14 +structure Contract = Inductive_Fun
    1.15 + (val thy = Contract0.thy;
    1.16 +  val rec_doms = [("contract","comb*comb")];
    1.17 +  val sintrs = 
    1.18 +      ["[| p:comb;  q:comb |] ==> K#p#q -1-> p",
    1.19 +       "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)",
    1.20 +       "[| p-1->q;  r:comb |] ==> p#r -1-> q#r",
    1.21 +       "[| p-1->q;  r:comb |] ==> r#p -1-> r#q"];
    1.22 +  val monos = [];
    1.23 +  val con_defs = [];
    1.24 +  val type_intrs = Comb.intrs@[SigmaI];
    1.25 +  val type_elims = [SigmaE2]);
    1.26 +
    1.27 +val [K_contract,S_contract,Ap_contract1,Ap_contract2] = Contract.intrs;
    1.28 +
    1.29 +val contract_induct = standard
    1.30 +    (Contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
    1.31 +
    1.32 +(*For type checking: replaces a-1->b by a,b:comb *)
    1.33 +val contract_combE2 = Contract.dom_subset RS subsetD RS SigmaE2;
    1.34 +val contract_combD1 = Contract.dom_subset RS subsetD RS SigmaD1;
    1.35 +val contract_combD2 = Contract.dom_subset RS subsetD RS SigmaD2;
    1.36 +
    1.37 +goal Contract.thy "field(contract) = comb";
    1.38 +by (fast_tac (ZF_cs addIs [equalityI,K_contract] addSEs [contract_combE2]) 1);
    1.39 +val field_contract_eq = result();
    1.40 +
    1.41 +val reduction_refl = standard
    1.42 +    (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
    1.43 +
    1.44 +val rtrancl_into_rtrancl2 = standard
    1.45 +    (r_into_rtrancl RS (trans_rtrancl RS transD));
    1.46 +
    1.47 +val reduction_rls = [reduction_refl, K_contract, S_contract, 
    1.48 +		     K_contract RS rtrancl_into_rtrancl2,
    1.49 +		     S_contract RS rtrancl_into_rtrancl2,
    1.50 +		     Ap_contract1 RS rtrancl_into_rtrancl2,
    1.51 +		     Ap_contract2 RS rtrancl_into_rtrancl2];
    1.52 +
    1.53 +goalw Contract.thy [I_def] "!!p. p:comb ==> I#p ---> p";
    1.54 +by (REPEAT (ares_tac (Comb.intrs @ reduction_rls) 1));
    1.55 +val I_reduce = result();
    1.56 +
    1.57 +goalw Contract.thy [I_def] "I: comb";
    1.58 +by (REPEAT (ares_tac Comb.intrs 1));
    1.59 +val I_comb = result();
    1.60 +
    1.61 +(** Non-contraction results **)
    1.62 +
    1.63 +(*Derive a case for each combinator constructor*)
    1.64 +val K_contract_case = Contract.mk_cases Comb.con_defs "K -1-> r";
    1.65 +val S_contract_case = Contract.mk_cases Comb.con_defs "S -1-> r";
    1.66 +val Ap_contract_case = Contract.mk_cases Comb.con_defs "p#q -1-> r";
    1.67 +
    1.68 +val contract_cs =
    1.69 +    ZF_cs addSIs Comb.intrs
    1.70 +	  addIs  Contract.intrs
    1.71 +	  addSEs [contract_combD1,contract_combD2]     (*type checking*)
    1.72 +	  addSEs [K_contract_case, S_contract_case, Ap_contract_case]
    1.73 +	  addSEs Comb.free_SEs;
    1.74 +
    1.75 +goalw Contract.thy [I_def] "!!r. I -1-> r ==> P";
    1.76 +by (fast_tac contract_cs 1);
    1.77 +val I_contract_case = result();
    1.78 +
    1.79 +goal Contract.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
    1.80 +by (fast_tac contract_cs 1);
    1.81 +val K1_contractD = result();
    1.82 +
    1.83 +goal Contract.thy "!!p r. [| p ---> q;  r: comb |] ==> p#r ---> q#r";
    1.84 +by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    1.85 +by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    1.86 +by (etac rtrancl_induct 1);
    1.87 +by (fast_tac (contract_cs addIs reduction_rls) 1);
    1.88 +by (etac (trans_rtrancl RS transD) 1);
    1.89 +by (fast_tac (contract_cs addIs reduction_rls) 1);
    1.90 +val Ap_reduce1 = result();
    1.91 +
    1.92 +goal Contract.thy "!!p r. [| p ---> q;  r: comb |] ==> r#p ---> r#q";
    1.93 +by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    1.94 +by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    1.95 +by (etac rtrancl_induct 1);
    1.96 +by (fast_tac (contract_cs addIs reduction_rls) 1);
    1.97 +by (etac (trans_rtrancl RS transD) 1);
    1.98 +by (fast_tac (contract_cs addIs reduction_rls) 1);
    1.99 +val Ap_reduce2 = result();
   1.100 +
   1.101 +(** Counterexample to the diamond property for -1-> **)
   1.102 +
   1.103 +goal Contract.thy "K#I#(I#I) -1-> I";
   1.104 +by (REPEAT (ares_tac [K_contract, I_comb, Ap_comb] 1));
   1.105 +val KIII_contract1 = result();
   1.106 +
   1.107 +goalw Contract.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
   1.108 +by (DEPTH_SOLVE (resolve_tac (Comb.intrs @ Contract.intrs) 1));
   1.109 +val KIII_contract2 = result();
   1.110 +
   1.111 +goal Contract.thy "K#I#((K#I)#(K#I)) -1-> I";
   1.112 +by (REPEAT (ares_tac (Comb.intrs @ [K_contract, I_comb]) 1));
   1.113 +val KIII_contract3 = result();
   1.114 +
   1.115 +goalw Contract.thy [diamond_def] "~ diamond(contract)";
   1.116 +by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
   1.117 +                    addSEs [I_contract_case]) 1);
   1.118 +val not_diamond_contract = result();
   1.119 +
   1.120 +writeln"Reached end of file.";