|
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."; |