src/ZF/ex/ParContract.ML
author lcp
Tue Aug 16 18:58:42 1994 +0200 (1994-08-16)
changeset 532 851df239ac8b
parent 496 3fc829fa81d2
permissions -rw-r--r--
ZF/Makefile,ROOT.ML, ZF/ex/Integ.thy: updated for EquivClass
     1 (*  Title: 	ZF/ex/parcontract.ML
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson
     4     Copyright   1993  University of Cambridge
     5 
     6 Parallel contraction
     7 
     8 HOL system proofs may be found in
     9 /usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    10 *)
    11 
    12 structure ParContract = Inductive_Fun
    13  (val thy	 = Contract.thy;
    14   val thy_name	 = "ParContract";
    15   val rec_doms	 = [("parcontract","comb*comb")];
    16   val sintrs	 = 
    17       ["[| p:comb |] ==> p =1=> p",
    18        "[| p:comb;  q:comb |] ==> K#p#q =1=> p",
    19        "[| p:comb;  q:comb;  r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)",
    20        "[| p=1=>q;  r=1=>s |] ==> p#r =1=> q#s"];
    21   val monos	 = [];
    22   val con_defs	 = [];
    23   val type_intrs = Comb.intrs;
    24   val type_elims = []);
    25 
    26 val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = 
    27     ParContract.intrs;
    28 
    29 val parcontract_induct = standard
    30     (ParContract.mutual_induct RS spec RS spec RSN (2,rev_mp));
    31 
    32 (*For type checking: replaces a=1=>b by a,b:comb *)
    33 val parcontract_combE2 = ParContract.dom_subset RS subsetD RS SigmaE2;
    34 val parcontract_combD1 = ParContract.dom_subset RS subsetD RS SigmaD1;
    35 val parcontract_combD2 = ParContract.dom_subset RS subsetD RS SigmaD2;
    36 
    37 goal ParContract.thy "field(parcontract) = comb";
    38 by (fast_tac (ZF_cs addIs [equalityI,K_parcontract] 
    39 	            addSEs [parcontract_combE2]) 1);
    40 val field_parcontract_eq = result();
    41 
    42 val parcontract_caseE = standard
    43      (ParContract.unfold RS equalityD1 RS subsetD RS CollectE);
    44 
    45 (*Derive a case for each combinator constructor*)
    46 val K_parcontract_case = ParContract.mk_cases Comb.con_defs "K =1=> r";
    47 val S_parcontract_case = ParContract.mk_cases Comb.con_defs "S =1=> r";
    48 val Ap_parcontract_case = ParContract.mk_cases Comb.con_defs "p#q =1=> r";
    49 
    50 val parcontract_cs =
    51     ZF_cs addSIs Comb.intrs
    52 	  addIs  ParContract.intrs
    53 	  addSEs [Ap_E, K_parcontract_case, S_parcontract_case, 
    54 		  Ap_parcontract_case]
    55 	  addSEs [parcontract_combD1, parcontract_combD2]     (*type checking*)
    56           addSEs Comb.free_SEs;
    57 
    58 (*** Basic properties of parallel contraction ***)
    59 
    60 goal ParContract.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
    61 by (fast_tac parcontract_cs 1);
    62 val K1_parcontractD = result();
    63 
    64 goal ParContract.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
    65 by (fast_tac parcontract_cs 1);
    66 val S1_parcontractD = result();
    67 
    68 goal ParContract.thy
    69  "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
    70 by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
    71 val S2_parcontractD = result();
    72 
    73 (*Church-Rosser property for parallel contraction*)
    74 goalw ParContract.thy [diamond_def] "diamond(parcontract)";
    75 by (rtac (impI RS allI RS allI) 1);
    76 by (etac parcontract_induct 1);
    77 by (ALLGOALS 
    78     (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
    79 val diamond_parcontract = result();
    80 
    81 (*** Transitive closure preserves the Church-Rosser property ***)
    82 
    83 goalw ParContract.thy [diamond_def]
    84     "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
    85 \    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
    86 by (etac trancl_induct 1);
    87 by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
    88 by (slow_best_tac (ZF_cs addSDs [spec RS mp]
    89 		         addIs  [r_into_trancl, trans_trancl RS transD]) 1);
    90 val diamond_trancl_lemma = result();
    91 
    92 val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
    93 
    94 val [major] = goal ParContract.thy "diamond(r) ==> diamond(r^+)";
    95 bw diamond_def;  (*unfold only in goal, not in premise!*)
    96 by (rtac (impI RS allI RS allI) 1);
    97 by (etac trancl_induct 1);
    98 by (ALLGOALS
    99     (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
   100 		          addEs [major RS diamond_lemmaE])));
   101 val diamond_trancl = result();
   102 
   103 
   104 (*** Equivalence of p--->q and p===>q ***)
   105 
   106 goal ParContract.thy "!!p q. p-1->q ==> p=1=>q";
   107 by (etac contract_induct 1);
   108 by (ALLGOALS (fast_tac (parcontract_cs)));
   109 val contract_imp_parcontract = result();
   110 
   111 goal ParContract.thy "!!p q. p--->q ==> p===>q";
   112 by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
   113 by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
   114 by (etac rtrancl_induct 1);
   115 by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
   116 by (fast_tac (ZF_cs addIs [contract_imp_parcontract, 
   117 			   r_into_trancl, trans_trancl RS transD]) 1);
   118 val reduce_imp_parreduce = result();
   119 
   120 
   121 goal ParContract.thy "!!p q. p=1=>q ==> p--->q";
   122 by (etac parcontract_induct 1);
   123 by (fast_tac (contract_cs addIs reduction_rls) 1);
   124 by (fast_tac (contract_cs addIs reduction_rls) 1);
   125 by (fast_tac (contract_cs addIs reduction_rls) 1);
   126 by (rtac (trans_rtrancl RS transD) 1);
   127 by (ALLGOALS 
   128     (fast_tac 
   129      (contract_cs addIs [Ap_reduce1, Ap_reduce2]
   130                   addSEs [parcontract_combD1,parcontract_combD2])));
   131 val parcontract_imp_reduce = result();
   132 
   133 goal ParContract.thy "!!p q. p===>q ==> p--->q";
   134 by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
   135 by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
   136 by (etac trancl_induct 1);
   137 by (etac parcontract_imp_reduce 1);
   138 by (etac (trans_rtrancl RS transD) 1);
   139 by (etac parcontract_imp_reduce 1);
   140 val parreduce_imp_reduce = result();
   141 
   142 goal ParContract.thy "p===>q <-> p--->q";
   143 by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
   144 val parreduce_iff_reduce = result();
   145 
   146 writeln"Reached end of file.";