src/ZF/ex/Comb.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 515 abcc438e7c27
child 760 f0200e91b272
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
clasohm@0
     1
(*  Title: 	ZF/ex/comb.ML
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author: 	Lawrence C Paulson
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
lcp@515
     6
Combinatory Logic example: the Church-Rosser Theorem
lcp@515
     7
Curiously, combinators do not include free variables.
lcp@515
     8
lcp@515
     9
Example taken from
lcp@515
    10
    J. Camilleri and T. F. Melham.
lcp@515
    11
    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
lcp@515
    12
    Report 265, University of Cambridge Computer Laboratory, 1992.
lcp@515
    13
lcp@515
    14
HOL system proofs may be found in
lcp@515
    15
/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
lcp@515
    16
*)
lcp@515
    17
lcp@515
    18
open Comb;
lcp@515
    19
lcp@515
    20
val [_,_,comb_Ap] = comb.intrs;
lcp@515
    21
val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
lcp@515
    22
lcp@515
    23
lcp@515
    24
(*** Results about Contraction ***)
lcp@515
    25
lcp@515
    26
val contract_induct = standard
lcp@515
    27
    (contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
lcp@515
    28
lcp@515
    29
(*For type checking: replaces a-1->b by a,b:comb *)
lcp@515
    30
val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
lcp@515
    31
val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
lcp@515
    32
val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
lcp@515
    33
lcp@515
    34
goal Comb.thy "field(contract) = comb";
lcp@515
    35
by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
lcp@515
    36
val field_contract_eq = result();
lcp@515
    37
lcp@515
    38
val reduction_refl = standard
lcp@515
    39
    (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
lcp@515
    40
lcp@515
    41
val rtrancl_into_rtrancl2 = standard
lcp@515
    42
    (r_into_rtrancl RS (trans_rtrancl RS transD));
lcp@515
    43
lcp@515
    44
val reduction_rls = [reduction_refl, contract.K, contract.S, 
lcp@515
    45
		     contract.K RS rtrancl_into_rtrancl2,
lcp@515
    46
		     contract.S RS rtrancl_into_rtrancl2,
lcp@515
    47
		     contract.Ap1 RS rtrancl_into_rtrancl2,
lcp@515
    48
		     contract.Ap2 RS rtrancl_into_rtrancl2];
lcp@515
    49
lcp@515
    50
(*Example only: not used*)
lcp@515
    51
goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
lcp@515
    52
by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
lcp@515
    53
val reduce_I = result();
lcp@515
    54
lcp@515
    55
goalw Comb.thy [I_def] "I: comb";
lcp@515
    56
by (REPEAT (ares_tac comb.intrs 1));
lcp@515
    57
val comb_I = result();
lcp@515
    58
lcp@515
    59
(** Non-contraction results **)
clasohm@0
    60
lcp@515
    61
(*Derive a case for each combinator constructor*)
lcp@515
    62
val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
lcp@515
    63
val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
lcp@515
    64
val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
lcp@515
    65
lcp@515
    66
val contract_cs =
lcp@515
    67
    ZF_cs addSIs comb.intrs
lcp@515
    68
	  addIs  contract.intrs
lcp@515
    69
	  addSEs [contract_combD1,contract_combD2]     (*type checking*)
lcp@515
    70
	  addSEs [K_contractE, S_contractE, Ap_contractE]
lcp@515
    71
	  addSEs comb.free_SEs;
lcp@515
    72
lcp@515
    73
goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
lcp@515
    74
by (fast_tac contract_cs 1);
lcp@515
    75
val I_contract_E = result();
lcp@515
    76
lcp@515
    77
goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
lcp@515
    78
by (fast_tac contract_cs 1);
lcp@515
    79
val K1_contractD = result();
lcp@515
    80
lcp@515
    81
goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> p#r ---> q#r";
lcp@515
    82
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
lcp@515
    83
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
lcp@515
    84
by (etac rtrancl_induct 1);
lcp@515
    85
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
    86
by (etac (trans_rtrancl RS transD) 1);
lcp@515
    87
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
    88
val Ap_reduce1 = result();
lcp@515
    89
lcp@515
    90
goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> r#p ---> r#q";
lcp@515
    91
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
lcp@515
    92
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
lcp@515
    93
by (etac rtrancl_induct 1);
lcp@515
    94
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
    95
by (etac (trans_rtrancl RS transD) 1);
lcp@515
    96
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
    97
val Ap_reduce2 = result();
lcp@515
    98
lcp@515
    99
(** Counterexample to the diamond property for -1-> **)
lcp@515
   100
lcp@515
   101
goal Comb.thy "K#I#(I#I) -1-> I";
lcp@515
   102
by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
lcp@515
   103
val KIII_contract1 = result();
lcp@515
   104
lcp@515
   105
goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
lcp@515
   106
by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
lcp@515
   107
val KIII_contract2 = result();
lcp@515
   108
lcp@515
   109
goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
lcp@515
   110
by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
lcp@515
   111
val KIII_contract3 = result();
lcp@515
   112
lcp@515
   113
goalw Comb.thy [diamond_def] "~ diamond(contract)";
lcp@515
   114
by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
lcp@515
   115
                    addSEs [I_contract_E]) 1);
lcp@515
   116
val not_diamond_contract = result();
lcp@515
   117
clasohm@0
   118
clasohm@0
   119
lcp@515
   120
(*** Results about Parallel Contraction ***)
lcp@515
   121
lcp@515
   122
val parcontract_induct = standard
lcp@515
   123
    (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
lcp@515
   124
lcp@515
   125
(*For type checking: replaces a=1=>b by a,b:comb *)
lcp@515
   126
val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
lcp@515
   127
val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
lcp@515
   128
val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
lcp@515
   129
lcp@515
   130
goal Comb.thy "field(parcontract) = comb";
lcp@515
   131
by (fast_tac (ZF_cs addIs [equalityI, parcontract.K] 
lcp@515
   132
	            addSEs [parcontract_combE2]) 1);
lcp@515
   133
val field_parcontract_eq = result();
lcp@515
   134
lcp@515
   135
(*Derive a case for each combinator constructor*)
lcp@515
   136
val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
lcp@515
   137
val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
lcp@515
   138
val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
lcp@515
   139
lcp@515
   140
val parcontract_cs =
lcp@515
   141
    ZF_cs addSIs comb.intrs
lcp@515
   142
	  addIs  parcontract.intrs
lcp@515
   143
	  addSEs [Ap_E, K_parcontractE, S_parcontractE, 
lcp@515
   144
		  Ap_parcontractE]
lcp@515
   145
	  addSEs [parcontract_combD1, parcontract_combD2]     (*type checking*)
lcp@515
   146
          addSEs comb.free_SEs;
lcp@515
   147
lcp@515
   148
(*** Basic properties of parallel contraction ***)
lcp@515
   149
lcp@515
   150
goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
lcp@515
   151
by (fast_tac parcontract_cs 1);
lcp@515
   152
val K1_parcontractD = result();
lcp@515
   153
lcp@515
   154
goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
lcp@515
   155
by (fast_tac parcontract_cs 1);
lcp@515
   156
val S1_parcontractD = result();
lcp@515
   157
lcp@515
   158
goal Comb.thy
lcp@515
   159
 "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
lcp@515
   160
by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
lcp@515
   161
val S2_parcontractD = result();
lcp@515
   162
lcp@515
   163
(*Church-Rosser property for parallel contraction*)
lcp@515
   164
goalw Comb.thy [diamond_def] "diamond(parcontract)";
lcp@515
   165
by (rtac (impI RS allI RS allI) 1);
lcp@515
   166
by (etac parcontract_induct 1);
lcp@515
   167
by (ALLGOALS 
lcp@515
   168
    (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
lcp@515
   169
val diamond_parcontract = result();
lcp@515
   170
lcp@515
   171
(*** Transitive closure preserves the Church-Rosser property ***)
clasohm@0
   172
lcp@515
   173
goalw Comb.thy [diamond_def]
lcp@515
   174
    "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
lcp@515
   175
\    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
lcp@515
   176
by (etac trancl_induct 1);
lcp@515
   177
by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
lcp@515
   178
by (slow_best_tac (ZF_cs addSDs [spec RS mp]
lcp@515
   179
		         addIs  [r_into_trancl, trans_trancl RS transD]) 1);
lcp@515
   180
val diamond_trancl_lemma = result();
lcp@515
   181
lcp@515
   182
val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
lcp@515
   183
lcp@515
   184
val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
lcp@515
   185
bw diamond_def;  (*unfold only in goal, not in premise!*)
lcp@515
   186
by (rtac (impI RS allI RS allI) 1);
lcp@515
   187
by (etac trancl_induct 1);
lcp@515
   188
by (ALLGOALS
lcp@515
   189
    (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
lcp@515
   190
		          addEs [major RS diamond_lemmaE])));
lcp@515
   191
val diamond_trancl = result();
lcp@515
   192
lcp@515
   193
lcp@515
   194
(*** Equivalence of p--->q and p===>q ***)
lcp@515
   195
lcp@515
   196
goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
lcp@515
   197
by (etac contract_induct 1);
lcp@515
   198
by (ALLGOALS (fast_tac (parcontract_cs)));
lcp@515
   199
val contract_imp_parcontract = result();
clasohm@0
   200
lcp@515
   201
goal Comb.thy "!!p q. p--->q ==> p===>q";
lcp@515
   202
by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
lcp@515
   203
by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
lcp@515
   204
by (etac rtrancl_induct 1);
lcp@515
   205
by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
lcp@515
   206
by (fast_tac (ZF_cs addIs [contract_imp_parcontract, 
lcp@515
   207
			   r_into_trancl, trans_trancl RS transD]) 1);
lcp@515
   208
val reduce_imp_parreduce = result();
lcp@515
   209
clasohm@0
   210
lcp@515
   211
goal Comb.thy "!!p q. p=1=>q ==> p--->q";
lcp@515
   212
by (etac parcontract_induct 1);
lcp@515
   213
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
   214
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
   215
by (fast_tac (contract_cs addIs reduction_rls) 1);
lcp@515
   216
by (rtac (trans_rtrancl RS transD) 1);
lcp@515
   217
by (ALLGOALS 
lcp@515
   218
    (fast_tac 
lcp@515
   219
     (contract_cs addIs [Ap_reduce1, Ap_reduce2]
lcp@515
   220
                  addSEs [parcontract_combD1,parcontract_combD2])));
lcp@515
   221
val parcontract_imp_reduce = result();
lcp@515
   222
lcp@515
   223
goal Comb.thy "!!p q. p===>q ==> p--->q";
lcp@515
   224
by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
lcp@515
   225
by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
lcp@515
   226
by (etac trancl_induct 1);
lcp@515
   227
by (etac parcontract_imp_reduce 1);
lcp@515
   228
by (etac (trans_rtrancl RS transD) 1);
lcp@515
   229
by (etac parcontract_imp_reduce 1);
lcp@515
   230
val parreduce_imp_reduce = result();
lcp@515
   231
lcp@515
   232
goal Comb.thy "p===>q <-> p--->q";
lcp@515
   233
by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
lcp@515
   234
val parreduce_iff_reduce = result();
lcp@515
   235
lcp@515
   236
writeln"Reached end of file.";