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