equal
deleted
inserted
replaced
43 |
43 |
44 |
44 |
45 (*** Results about Contraction ***) |
45 (*** Results about Contraction ***) |
46 |
46 |
47 (*Derive a case for each combinator constructor*) |
47 (*Derive a case for each combinator constructor*) |
48 val K_contractE = contract.mk_cases comb.simps "K -1-> z"; |
48 val K_contractE = contract.mk_cases "K -1-> z"; |
49 val S_contractE = contract.mk_cases comb.simps "S -1-> z"; |
49 val S_contractE = contract.mk_cases "S -1-> z"; |
50 val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z"; |
50 val Ap_contractE = contract.mk_cases "x#y -1-> z"; |
51 |
51 |
52 AddSIs [contract.K, contract.S]; |
52 AddSIs [contract.K, contract.S]; |
53 AddIs [contract.Ap1, contract.Ap2]; |
53 AddIs [contract.Ap1, contract.Ap2]; |
54 AddSEs [K_contractE, S_contractE, Ap_contractE]; |
54 AddSEs [K_contractE, S_contractE, Ap_contractE]; |
55 |
55 |
94 |
94 |
95 |
95 |
96 (*** Results about Parallel Contraction ***) |
96 (*** Results about Parallel Contraction ***) |
97 |
97 |
98 (*Derive a case for each combinator constructor*) |
98 (*Derive a case for each combinator constructor*) |
99 val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z"; |
99 val K_parcontractE = parcontract.mk_cases "K =1=> z"; |
100 val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z"; |
100 val S_parcontractE = parcontract.mk_cases "S =1=> z"; |
101 val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z"; |
101 val Ap_parcontractE = parcontract.mk_cases "x#y =1=> z"; |
102 |
102 |
103 AddSIs [parcontract.refl, parcontract.K, parcontract.S]; |
103 AddSIs [parcontract.refl, parcontract.K, parcontract.S]; |
104 AddIs [parcontract.Ap]; |
104 AddIs [parcontract.Ap]; |
105 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE]; |
105 AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE]; |
106 |
106 |