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