author | paulson |
Fri, 26 Apr 1996 13:30:26 +0200 | |
changeset 1691 | fbbd65c89c23 |
parent 1689 | c38d953caedb |
child 1730 | 1c7f793fc374 |
permissions | -rw-r--r-- |
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/ex/comb.ML |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
4 |
Copyright 1996 University of Cambridge |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
5 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
6 |
Combinatory Logic example: the Church-Rosser Theorem |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
7 |
Curiously, combinators do not include free variables. |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
8 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
9 |
Example taken from |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
10 |
J. Camilleri and T. F. Melham. |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
11 |
Reasoning with Inductively Defined Relations in the HOL Theorem Prover. |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
12 |
Report 265, University of Cambridge Computer Laboratory, 1992. |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
13 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
14 |
HOL system proofs may be found in |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
15 |
/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
16 |
*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
17 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
18 |
open Comb; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
19 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
20 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
21 |
(*** Reflexive/Transitive closure preserves the Church-Rosser property |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
22 |
So does the Transitive closure; use r_into_trancl instead of rtrancl_refl |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
23 |
***) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
24 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
25 |
val [_, spec_mp] = [spec] RL [mp]; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
26 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
27 |
(*Strip lemma. The induction hyp is all but the last diamond of the strip.*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
28 |
goalw Comb.thy [diamond_def] |
1691 | 29 |
"!!r. [| diamond(r); (x,y):r^* |] ==> \ |
30 |
\ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)"; |
|
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
31 |
by (etac rtrancl_induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
32 |
by (fast_tac (HOL_cs addIs [rtrancl_refl]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
33 |
by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)] |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
34 |
addSDs [spec_mp]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
35 |
val diamond_strip_lemmaE = result() RS spec RS mp RS exE; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
36 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
37 |
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
38 |
by (rewtac diamond_def); (*unfold only in goal, not in premise!*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
39 |
by (rtac (impI RS allI RS allI) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
40 |
by (etac rtrancl_induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
41 |
by (fast_tac (set_cs addIs [rtrancl_refl]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
42 |
by (ALLGOALS |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
43 |
(slow_best_tac (set_cs addIs [r_into_rtrancl, rtrancl_trans] |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
44 |
addEs [major RS diamond_strip_lemmaE]))); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
45 |
qed "diamond_rtrancl"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
46 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
47 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
48 |
(*** Results about Contraction ***) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
49 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
50 |
(** Non-contraction results **) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
51 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
52 |
(*Derive a case for each combinator constructor*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
53 |
val K_contractE = contract.mk_cases comb.simps "K -1-> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
54 |
val S_contractE = contract.mk_cases comb.simps "S -1-> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
55 |
val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
56 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
57 |
val contract_cs = |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
58 |
HOL_cs addIs contract.intrs |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
59 |
addSEs [K_contractE, S_contractE, Ap_contractE] |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
60 |
addss (HOL_ss addsimps comb.simps); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
61 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
62 |
goalw Comb.thy [I_def] "!!z. I -1-> z ==> P"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
63 |
by (fast_tac contract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
64 |
qed "I_contract_E"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
65 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
66 |
(*Unused*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
67 |
goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
68 |
by (fast_tac contract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
69 |
qed "K1_contractD"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
70 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
71 |
goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
72 |
by (etac rtrancl_induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
73 |
by (rtac rtrancl_refl 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
74 |
by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
75 |
qed "Ap_reduce1"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
76 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
77 |
goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
78 |
by (etac rtrancl_induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
79 |
by (rtac rtrancl_refl 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
80 |
by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
81 |
qed "Ap_reduce2"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
82 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
83 |
(** Counterexample to the diamond property for -1-> **) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
84 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
85 |
goal Comb.thy "K#I#(I#I) -1-> I"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
86 |
by (rtac contract.K 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
87 |
qed "KIII_contract1"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
88 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
89 |
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
90 |
by (fast_tac contract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
91 |
qed "KIII_contract2"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
92 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
93 |
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
94 |
by (fast_tac contract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
95 |
qed "KIII_contract3"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
96 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
97 |
goalw Comb.thy [diamond_def] "~ diamond(contract)"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
98 |
by (fast_tac (HOL_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3] |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
99 |
addSEs [I_contract_E]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
100 |
qed "not_diamond_contract"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
101 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
102 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
103 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
104 |
(*** Results about Parallel Contraction ***) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
105 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
106 |
bind_thm ("parcontract_induct", |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
107 |
(parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp))); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
108 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
109 |
(*Derive a case for each combinator constructor*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
110 |
val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
111 |
val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
112 |
val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
113 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
114 |
val parcontract_cs = |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
115 |
HOL_cs addIs parcontract.intrs |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
116 |
addSEs [K_parcontractE, S_parcontractE, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
117 |
Ap_parcontractE] |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
118 |
addss (HOL_ss addsimps comb.simps); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
119 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
120 |
(*** Basic properties of parallel contraction ***) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
121 |
|
1689 | 122 |
goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')"; |
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
123 |
by (fast_tac parcontract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
124 |
qed "K1_parcontractD"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
125 |
|
1689 | 126 |
goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')"; |
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
127 |
by (fast_tac parcontract_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
128 |
qed "S1_parcontractD"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
129 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
130 |
goal Comb.thy |
1689 | 131 |
"!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')"; |
1639
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
132 |
by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
133 |
(*the extra rule makes the proof more than twice as fast*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
134 |
qed "S2_parcontractD"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
135 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
136 |
(*Church-Rosser property for parallel contraction*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
137 |
goalw Comb.thy [diamond_def] "diamond(parcontract)"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
138 |
by (rtac (impI RS allI RS allI) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
139 |
by (etac parcontract_induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
140 |
by (ALLGOALS |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
141 |
(fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD]))); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
142 |
qed "diamond_parcontract"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
143 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
144 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
145 |
(*** Equivalence of x--->y and x===>y ***) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
146 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
147 |
goal Comb.thy "contract <= parcontract"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
148 |
by (rtac subsetI 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
149 |
by (etac contract.induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
150 |
by (ALLGOALS (fast_tac (parcontract_cs))); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
151 |
qed "contract_subset_parcontract"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
152 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
153 |
(*Reductions: simply throw together reflexivity, transitivity and |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
154 |
the one-step reductions*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
155 |
val reduce_cs = contract_cs |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
156 |
addIs [rtrancl_refl, r_into_rtrancl, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
157 |
contract.K, contract.S, Ap_reduce1, Ap_reduce2, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
158 |
rtrancl_trans]; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
159 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
160 |
(*Example only: not used*) |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
161 |
goalw Comb.thy [I_def] "I#x ---> x"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
162 |
by (best_tac reduce_cs 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
163 |
qed "reduce_I"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
164 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
165 |
goal Comb.thy "parcontract <= contract^*"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
166 |
by (rtac subsetI 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
167 |
by (etac parcontract.induct 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
168 |
by (ALLGOALS (deepen_tac reduce_cs 0)); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
169 |
qed "parcontract_subset_reduce"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
170 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
171 |
goal Comb.thy "contract^* = parcontract^*"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
172 |
by (REPEAT |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
173 |
(resolve_tac [equalityI, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
174 |
contract_subset_parcontract RS rtrancl_mono, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
175 |
parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1)); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
176 |
qed "reduce_eq_parreduce"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
177 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
178 |
goal Comb.thy "diamond(contract^*)"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
179 |
by (simp_tac (HOL_ss addsimps [reduce_eq_parreduce, diamond_rtrancl, |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
180 |
diamond_parcontract]) 1); |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
181 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
182 |
qed "diamond_reduce"; |
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
183 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
184 |
|
d3484e841d1e
New example Comb: Church-Rosser for combinators, ported from ZF
paulson
parents:
diff
changeset
|
185 |
writeln"Reached end of file."; |