--- a/src/ZF/ex/Comb.ML Wed Dec 14 10:26:30 1994 +0100
+++ b/src/ZF/ex/Comb.ML Wed Dec 14 11:41:49 1994 +0100
@@ -23,8 +23,8 @@
(*** Results about Contraction ***)
-val contract_induct = standard
- (contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+bind_thm ("contract_induct",
+ (contract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
(*For type checking: replaces a-1->b by a,b:comb *)
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
@@ -35,11 +35,11 @@
by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
qed "field_contract_eq";
-val reduction_refl = standard
- (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
+bind_thm ("reduction_refl",
+ (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl));
-val rtrancl_into_rtrancl2 = standard
- (r_into_rtrancl RS (trans_rtrancl RS transD));
+bind_thm ("rtrancl_into_rtrancl2",
+ (r_into_rtrancl RS (trans_rtrancl RS transD)));
val reduction_rls = [reduction_refl, contract.K, contract.S,
contract.K RS rtrancl_into_rtrancl2,
@@ -50,7 +50,7 @@
(*Example only: not used*)
goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
-val reduce_I = result();
+qed "reduce_I";
goalw Comb.thy [I_def] "I: comb";
by (REPEAT (ares_tac comb.intrs 1));
@@ -72,11 +72,11 @@
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
by (fast_tac contract_cs 1);
-val I_contract_E = result();
+qed "I_contract_E";
goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
by (fast_tac contract_cs 1);
-val K1_contractD = result();
+qed "K1_contractD";
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> p#r ---> q#r";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -85,7 +85,7 @@
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (etac (trans_rtrancl RS transD) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
-val Ap_reduce1 = result();
+qed "Ap_reduce1";
goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> r#p ---> r#q";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -94,33 +94,33 @@
by (fast_tac (contract_cs addIs reduction_rls) 1);
by (etac (trans_rtrancl RS transD) 1);
by (fast_tac (contract_cs addIs reduction_rls) 1);
-val Ap_reduce2 = result();
+qed "Ap_reduce2";
(** Counterexample to the diamond property for -1-> **)
goal Comb.thy "K#I#(I#I) -1-> I";
by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
-val KIII_contract1 = result();
+qed "KIII_contract1";
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
-val KIII_contract2 = result();
+qed "KIII_contract2";
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
-val KIII_contract3 = result();
+qed "KIII_contract3";
goalw Comb.thy [diamond_def] "~ diamond(contract)";
by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
addSEs [I_contract_E]) 1);
-val not_diamond_contract = result();
+qed "not_diamond_contract";
(*** Results about Parallel Contraction ***)
-val parcontract_induct = standard
- (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+bind_thm ("parcontract_induct",
+ (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
(*For type checking: replaces a=1=>b by a,b:comb *)
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
@@ -130,7 +130,7 @@
goal Comb.thy "field(parcontract) = comb";
by (fast_tac (ZF_cs addIs [equalityI, parcontract.K]
addSEs [parcontract_combE2]) 1);
-val field_parcontract_eq = result();
+qed "field_parcontract_eq";
(*Derive a case for each combinator constructor*)
val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
@@ -149,16 +149,16 @@
goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
by (fast_tac parcontract_cs 1);
-val K1_parcontractD = result();
+qed "K1_parcontractD";
goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
by (fast_tac parcontract_cs 1);
-val S1_parcontractD = result();
+qed "S1_parcontractD";
goal Comb.thy
"!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
-val S2_parcontractD = result();
+qed "S2_parcontractD";
(*Church-Rosser property for parallel contraction*)
goalw Comb.thy [diamond_def] "diamond(parcontract)";
@@ -166,7 +166,7 @@
by (etac parcontract_induct 1);
by (ALLGOALS
(fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
-val diamond_parcontract = result();
+qed "diamond_parcontract";
(*** Transitive closure preserves the Church-Rosser property ***)
@@ -177,7 +177,7 @@
by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
by (slow_best_tac (ZF_cs addSDs [spec RS mp]
addIs [r_into_trancl, trans_trancl RS transD]) 1);
-val diamond_trancl_lemma = result();
+qed "diamond_trancl_lemma";
val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
@@ -188,7 +188,7 @@
by (ALLGOALS
(slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
addEs [major RS diamond_lemmaE])));
-val diamond_trancl = result();
+qed "diamond_trancl";
(*** Equivalence of p--->q and p===>q ***)
@@ -196,7 +196,7 @@
goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
by (etac contract_induct 1);
by (ALLGOALS (fast_tac (parcontract_cs)));
-val contract_imp_parcontract = result();
+qed "contract_imp_parcontract";
goal Comb.thy "!!p q. p--->q ==> p===>q";
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
@@ -205,7 +205,7 @@
by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
by (fast_tac (ZF_cs addIs [contract_imp_parcontract,
r_into_trancl, trans_trancl RS transD]) 1);
-val reduce_imp_parreduce = result();
+qed "reduce_imp_parreduce";
goal Comb.thy "!!p q. p=1=>q ==> p--->q";
@@ -227,10 +227,10 @@
by (etac parcontract_imp_reduce 1);
by (etac (trans_rtrancl RS transD) 1);
by (etac parcontract_imp_reduce 1);
-val parreduce_imp_reduce = result();
+qed "parreduce_imp_reduce";
goal Comb.thy "p===>q <-> p--->q";
by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
-val parreduce_iff_reduce = result();
+qed "parreduce_iff_reduce";
writeln"Reached end of file.";