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