equal
deleted
inserted
replaced
31 val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1; |
31 val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1; |
32 val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2; |
32 val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2; |
33 |
33 |
34 goal Comb.thy "field(contract) = comb"; |
34 goal Comb.thy "field(contract) = comb"; |
35 by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1); |
35 by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1); |
36 val field_contract_eq = result(); |
36 qed "field_contract_eq"; |
37 |
37 |
38 val reduction_refl = standard |
38 val reduction_refl = standard |
39 (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl); |
39 (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl); |
40 |
40 |
41 val rtrancl_into_rtrancl2 = standard |
41 val rtrancl_into_rtrancl2 = standard |
52 by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1)); |
52 by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1)); |
53 val reduce_I = result(); |
53 val reduce_I = result(); |
54 |
54 |
55 goalw Comb.thy [I_def] "I: comb"; |
55 goalw Comb.thy [I_def] "I: comb"; |
56 by (REPEAT (ares_tac comb.intrs 1)); |
56 by (REPEAT (ares_tac comb.intrs 1)); |
57 val comb_I = result(); |
57 qed "comb_I"; |
58 |
58 |
59 (** Non-contraction results **) |
59 (** Non-contraction results **) |
60 |
60 |
61 (*Derive a case for each combinator constructor*) |
61 (*Derive a case for each combinator constructor*) |
62 val K_contractE = contract.mk_cases comb.con_defs "K -1-> r"; |
62 val K_contractE = contract.mk_cases comb.con_defs "K -1-> r"; |
216 by (rtac (trans_rtrancl RS transD) 1); |
216 by (rtac (trans_rtrancl RS transD) 1); |
217 by (ALLGOALS |
217 by (ALLGOALS |
218 (fast_tac |
218 (fast_tac |
219 (contract_cs addIs [Ap_reduce1, Ap_reduce2] |
219 (contract_cs addIs [Ap_reduce1, Ap_reduce2] |
220 addSEs [parcontract_combD1,parcontract_combD2]))); |
220 addSEs [parcontract_combD1,parcontract_combD2]))); |
221 val parcontract_imp_reduce = result(); |
221 qed "parcontract_imp_reduce"; |
222 |
222 |
223 goal Comb.thy "!!p q. p===>q ==> p--->q"; |
223 goal Comb.thy "!!p q. p===>q ==> p--->q"; |
224 by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1); |
224 by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1); |
225 by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1); |
225 by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1); |
226 by (etac trancl_induct 1); |
226 by (etac trancl_induct 1); |