New example Comb: Church-Rosser for combinators, ported from ZF
authorpaulson
Thu Apr 04 10:24:38 1996 +0200 (1996-04-04)
changeset 1639d3484e841d1e
parent 1638 69c094639823
child 1640 581165679095
New example Comb: Church-Rosser for combinators, ported from ZF
src/HOL/Makefile
src/HOL/ex/Comb.ML
src/HOL/ex/Comb.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/Makefile	Wed Apr 03 20:08:27 1996 +0200
     1.2 +++ b/src/HOL/Makefile	Thu Apr 04 10:24:38 1996 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4  
     1.5  ##Miscellaneous examples
     1.6  EX_NAMES = LexProd MT Acc PropLog Puzzle Mutil Qsort LList Rec Simult Term \
     1.7 -	   String BT Perm
     1.8 +	   String BT Perm Comb
     1.9  
    1.10  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.11             ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/ex/Comb.ML	Thu Apr 04 10:24:38 1996 +0200
     2.3 @@ -0,0 +1,188 @@
     2.4 +(*  Title:      HOL/ex/comb.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson
     2.7 +    Copyright   1996  University of Cambridge
     2.8 +
     2.9 +Combinatory Logic example: the Church-Rosser Theorem
    2.10 +Curiously, combinators do not include free variables.
    2.11 +
    2.12 +Example taken from
    2.13 +    J. Camilleri and T. F. Melham.
    2.14 +    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    2.15 +    Report 265, University of Cambridge Computer Laboratory, 1992.
    2.16 +
    2.17 +HOL system proofs may be found in
    2.18 +/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    2.19 +*)
    2.20 +
    2.21 +open Comb;
    2.22 +
    2.23 +
    2.24 +(*** Reflexive/Transitive closure preserves the Church-Rosser property 
    2.25 +     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
    2.26 +***)
    2.27 +
    2.28 +val [_, spec_mp] = [spec] RL [mp];
    2.29 +
    2.30 +(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
    2.31 +goalw Comb.thy [diamond_def]
    2.32 +    "!!x y r. [| diamond(r);  (x,y):r^* |] ==> \
    2.33 +\    ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
    2.34 +by (etac rtrancl_induct 1);
    2.35 +by (fast_tac (HOL_cs addIs [rtrancl_refl]) 1);
    2.36 +by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    2.37 +                          addSDs [spec_mp]) 1);
    2.38 +val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
    2.39 +
    2.40 +val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
    2.41 +by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
    2.42 +by (rtac (impI RS allI RS allI) 1);
    2.43 +by (etac rtrancl_induct 1);
    2.44 +by (fast_tac (set_cs addIs [rtrancl_refl]) 1);
    2.45 +by (ALLGOALS
    2.46 +    (slow_best_tac (set_cs addIs [r_into_rtrancl, rtrancl_trans]
    2.47 +                           addEs [major RS diamond_strip_lemmaE])));
    2.48 +qed "diamond_rtrancl";
    2.49 +
    2.50 +
    2.51 +(*** Results about Contraction ***)
    2.52 +
    2.53 +bind_thm ("contract_induct",
    2.54 +    (contract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
    2.55 +
    2.56 +(** Non-contraction results **)
    2.57 +
    2.58 +(*Derive a case for each combinator constructor*)
    2.59 +val K_contractE = contract.mk_cases comb.simps "K -1-> z";
    2.60 +val S_contractE = contract.mk_cases comb.simps "S -1-> z";
    2.61 +val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
    2.62 +
    2.63 +val contract_cs =
    2.64 +    HOL_cs addIs  contract.intrs
    2.65 +	   addSEs [K_contractE, S_contractE, Ap_contractE]
    2.66 +	   addss  (HOL_ss addsimps comb.simps);
    2.67 +
    2.68 +goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
    2.69 +by (fast_tac contract_cs 1);
    2.70 +qed "I_contract_E";
    2.71 +
    2.72 +(*Unused*)
    2.73 +goal Comb.thy "!!x z. K#x -1-> z ==> (EX y. z = K#y & x -1-> y)";
    2.74 +by (fast_tac contract_cs 1);
    2.75 +qed "K1_contractD";
    2.76 +
    2.77 +goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
    2.78 +by (etac rtrancl_induct 1);
    2.79 +by (rtac rtrancl_refl 1);
    2.80 +by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
    2.81 +qed "Ap_reduce1";
    2.82 +
    2.83 +goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
    2.84 +by (etac rtrancl_induct 1);
    2.85 +by (rtac rtrancl_refl 1);
    2.86 +by (fast_tac (contract_cs addIs [r_into_rtrancl, rtrancl_trans]) 1);
    2.87 +qed "Ap_reduce2";
    2.88 +
    2.89 +(** Counterexample to the diamond property for -1-> **)
    2.90 +
    2.91 +goal Comb.thy "K#I#(I#I) -1-> I";
    2.92 +by (rtac contract.K 1);
    2.93 +qed "KIII_contract1";
    2.94 +
    2.95 +goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
    2.96 +by (fast_tac contract_cs 1);
    2.97 +qed "KIII_contract2";
    2.98 +
    2.99 +goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
   2.100 +by (fast_tac contract_cs 1);
   2.101 +qed "KIII_contract3";
   2.102 +
   2.103 +goalw Comb.thy [diamond_def] "~ diamond(contract)";
   2.104 +by (fast_tac (HOL_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
   2.105 +                     addSEs [I_contract_E]) 1);
   2.106 +qed "not_diamond_contract";
   2.107 +
   2.108 +
   2.109 +
   2.110 +(*** Results about Parallel Contraction ***)
   2.111 +
   2.112 +bind_thm ("parcontract_induct",
   2.113 +    (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp)));
   2.114 +
   2.115 +(*Derive a case for each combinator constructor*)
   2.116 +val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
   2.117 +val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
   2.118 +val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
   2.119 +
   2.120 +val parcontract_cs =
   2.121 +    HOL_cs addIs  parcontract.intrs
   2.122 +	   addSEs [K_parcontractE, S_parcontractE, 
   2.123 +		   Ap_parcontractE]
   2.124 +	   addss  (HOL_ss addsimps comb.simps);
   2.125 +
   2.126 +(*** Basic properties of parallel contraction ***)
   2.127 +
   2.128 +goal Comb.thy "!!x z. K#x =1=> z ==> (EX p'. z = K#p' & x =1=> p')";
   2.129 +by (fast_tac parcontract_cs 1);
   2.130 +qed "K1_parcontractD";
   2.131 +
   2.132 +goal Comb.thy "!!x z. S#x =1=> z ==> (EX p'. z = S#p' & x =1=> p')";
   2.133 +by (fast_tac parcontract_cs 1);
   2.134 +qed "S1_parcontractD";
   2.135 +
   2.136 +goal Comb.thy
   2.137 + "!!x y z. S#x#y =1=> z ==> (EX p' q'. z = S#p'#q' & x =1=> p' & y =1=> q')";
   2.138 +by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
   2.139 +     (*the extra rule makes the proof more than twice as fast*)
   2.140 +qed "S2_parcontractD";
   2.141 +
   2.142 +(*Church-Rosser property for parallel contraction*)
   2.143 +goalw Comb.thy [diamond_def] "diamond(parcontract)";
   2.144 +by (rtac (impI RS allI RS allI) 1);
   2.145 +by (etac parcontract_induct 1);
   2.146 +by (ALLGOALS 
   2.147 +    (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
   2.148 +qed "diamond_parcontract";
   2.149 +
   2.150 +
   2.151 +(*** Equivalence of x--->y and x===>y ***)
   2.152 +
   2.153 +goal Comb.thy "contract <= parcontract";
   2.154 +by (rtac subsetI 1);
   2.155 +by (etac contract.induct 1);
   2.156 +by (ALLGOALS (fast_tac (parcontract_cs)));
   2.157 +qed "contract_subset_parcontract";
   2.158 +
   2.159 +(*Reductions: simply throw together reflexivity, transitivity and
   2.160 +  the one-step reductions*)
   2.161 +val reduce_cs = contract_cs
   2.162 +                addIs [rtrancl_refl, r_into_rtrancl,
   2.163 +		       contract.K, contract.S, Ap_reduce1, Ap_reduce2,
   2.164 +		       rtrancl_trans];
   2.165 +
   2.166 +(*Example only: not used*)
   2.167 +goalw Comb.thy [I_def] "I#x ---> x";
   2.168 +by (best_tac reduce_cs 1);
   2.169 +qed "reduce_I";
   2.170 +
   2.171 +goal Comb.thy "parcontract <= contract^*";
   2.172 +by (rtac subsetI 1);
   2.173 +by (etac parcontract.induct 1);
   2.174 +by (ALLGOALS (deepen_tac reduce_cs 0));
   2.175 +qed "parcontract_subset_reduce";
   2.176 +
   2.177 +goal Comb.thy "contract^* = parcontract^*";
   2.178 +by (REPEAT 
   2.179 +    (resolve_tac [equalityI, 
   2.180 +		  contract_subset_parcontract RS rtrancl_mono, 
   2.181 +		  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
   2.182 +qed "reduce_eq_parreduce";
   2.183 +
   2.184 +goal Comb.thy "diamond(contract^*)";
   2.185 +by (simp_tac (HOL_ss addsimps [reduce_eq_parreduce, diamond_rtrancl, 
   2.186 +			       diamond_parcontract]) 1);
   2.187 +
   2.188 +qed "diamond_reduce";
   2.189 +
   2.190 +
   2.191 +writeln"Reached end of file.";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/ex/Comb.thy	Thu Apr 04 10:24:38 1996 +0200
     3.3 @@ -0,0 +1,74 @@
     3.4 +(*  Title:      HOL/ex/Comb.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson
     3.7 +    Copyright   1996  University of Cambridge
     3.8 +
     3.9 +Combinatory Logic example: the Church-Rosser Theorem
    3.10 +Curiously, combinators do not include free variables.
    3.11 +
    3.12 +Example taken from
    3.13 +    J. Camilleri and T. F. Melham.
    3.14 +    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    3.15 +    Report 265, University of Cambridge Computer Laboratory, 1992.
    3.16 +*)
    3.17 +
    3.18 +
    3.19 +Comb = Trancl +
    3.20 +
    3.21 +(** Datatype definition of combinators S and K, with infixed application **)
    3.22 +datatype comb = K
    3.23 +              | S
    3.24 +              | "#" comb comb (infixl 90)
    3.25 +
    3.26 +(** Inductive definition of contractions, -1->
    3.27 +             and (multi-step) reductions, --->
    3.28 +**)
    3.29 +consts
    3.30 +  contract  :: "(comb*comb) set"
    3.31 +  "-1->"    :: [comb,comb] => bool   (infixl 50)
    3.32 +  "--->"    :: [comb,comb] => bool   (infixl 50)
    3.33 +
    3.34 +translations
    3.35 +  "x -1-> y" == "(x,y) : contract"
    3.36 +  "x ---> y" == "(x,y) : contract^*"
    3.37 +
    3.38 +inductive "contract"
    3.39 +  intrs
    3.40 +    K     "K#x#y -1-> x"
    3.41 +    S     "S#x#y#z -1-> (x#z)#(y#z)"
    3.42 +    Ap1   "x-1->y ==> x#z -1-> y#z"
    3.43 +    Ap2   "x-1->y ==> z#x -1-> z#y"
    3.44 +
    3.45 +
    3.46 +(** Inductive definition of parallel contractions, =1=>
    3.47 +             and (multi-step) parallel reductions, ===>
    3.48 +**)
    3.49 +consts
    3.50 +  parcontract :: "(comb*comb) set"
    3.51 +  "=1=>"    :: [comb,comb] => bool   (infixl 50)
    3.52 +  "===>"    :: [comb,comb] => bool   (infixl 50)
    3.53 +
    3.54 +translations
    3.55 +  "x =1=> y" == "(x,y) : parcontract"
    3.56 +  "x ===> y" == "(x,y) : parcontract^*"
    3.57 +
    3.58 +inductive "parcontract"
    3.59 +  intrs
    3.60 +    refl  "x =1=> x"
    3.61 +    K     "K#x#y =1=> x"
    3.62 +    S     "S#x#y#z =1=> (x#z)#(y#z)"
    3.63 +    Ap    "[| x=1=>y;  z=1=>s |] ==> x#z =1=> y#s"
    3.64 +
    3.65 +
    3.66 +(*Misc definitions*)
    3.67 +constdefs
    3.68 +  I :: comb
    3.69 +  "I == S#K#K"
    3.70 +
    3.71 +  (*confluence; Lambda/Commutation treats this more abstractly*)
    3.72 +  diamond   :: "('a * 'a)set => bool"	
    3.73 +  "diamond(r) == ALL x y. (x,y):r --> 
    3.74 +                  (ALL y'. (x,y'):r --> 
    3.75 +                    (EX z. (y,z):r & (y',z) : r))"
    3.76 +
    3.77 +end
     4.1 --- a/src/HOL/ex/ROOT.ML	Wed Apr 03 20:08:27 1996 +0200
     4.2 +++ b/src/HOL/ex/ROOT.ML	Thu Apr 04 10:24:38 1996 +0200
     4.3 @@ -16,6 +16,7 @@
     4.4  time_use_thy "String";
     4.5  time_use_thy "BT";
     4.6  time_use_thy "Perm";
     4.7 +time_use_thy "Comb";
     4.8  time_use_thy "InSort";
     4.9  time_use_thy "Qsort";
    4.10  time_use_thy "LexProd";