commutation theory, ported by Sidi Ehmety
authorpaulson
Sat Feb 03 12:41:38 2001 +0100 (2001-02-03)
changeset 11042bb566dd3f927
parent 11041 e07b601e2b5a
child 11043 2e3bbac8763b
commutation theory, ported by Sidi Ehmety
src/ZF/IsaMakefile
src/ZF/ex/Commutation.ML
src/ZF/ex/Commutation.thy
src/ZF/ex/ROOT.ML
     1.1 --- a/src/ZF/IsaMakefile	Sat Feb 03 00:11:07 2001 +0100
     1.2 +++ b/src/ZF/IsaMakefile	Sat Feb 03 12:41:38 2001 +0100
     1.3 @@ -110,8 +110,9 @@
     1.4  
     1.5  $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \
     1.6    ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
     1.7 -  ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \
     1.8 -  ex/Enum.thy ex/LList.ML ex/LList.thy \
     1.9 +  ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \
    1.10 +  ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
    1.11 +  ex/LList.ML ex/LList.thy \
    1.12    ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
    1.13    ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
    1.14    ex/NatSum.ML ex/NatSum.thy  ex/Primrec_defs.ML ex/Primrec_defs.thy \
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/ex/Commutation.ML	Sat Feb 03 12:41:38 2001 +0100
     2.3 @@ -0,0 +1,131 @@
     2.4 +(*  Title:      HOL/Lambda/Commutation.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Tobias Nipkow & Sidi Ould Ehmety
     2.7 +    Copyright   1995  TU Muenchen
     2.8 +
     2.9 +Commutation theory for proving the Church Rosser theorem
    2.10 +	ported from Isabelle/HOL  by Sidi Ould Ehmety
    2.11 +*)
    2.12 +
    2.13 +Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
    2.14 +by (Blast_tac 1);
    2.15 +qed "square_sym";                
    2.16 +
    2.17 +
    2.18 +Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)";
    2.19 +by (Blast_tac 1);
    2.20 +qed "square_subset"; 
    2.21 +
    2.22 +
    2.23 +Goalw [square_def]
    2.24 + "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
    2.25 +by (Clarify_tac 1);
    2.26 +by (etac rtrancl_induct 1);
    2.27 +by (blast_tac (claset()  addIs [rtrancl_refl]) 1);
    2.28 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    2.29 +qed_spec_mp "square_rtrancl";                 
    2.30 +
    2.31 +(* A special case of square_rtrancl_on *)
    2.32 +Goalw [diamond_def, commute_def, strip_def]
    2.33 + "diamond(r) ==> strip(r)";
    2.34 +by (resolve_tac [square_rtrancl] 1);
    2.35 +by (ALLGOALS(Asm_simp_tac));
    2.36 +qed "diamond_strip";
    2.37 +
    2.38 +(*** commute ***)
    2.39 +
    2.40 +Goalw [commute_def] 
    2.41 +    "commute(r,s) ==> commute(s,r)";
    2.42 +by (blast_tac (claset() addIs [square_sym]) 1);
    2.43 +qed "commute_sym";
    2.44 +
    2.45 +Goalw [commute_def] 
    2.46 +"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
    2.47 +by (Clarify_tac 1);
    2.48 +by (rtac square_rtrancl 1);
    2.49 +by (rtac square_sym  2);
    2.50 +by (rtac square_rtrancl 2);
    2.51 +by (rtac square_sym  3);
    2.52 +by (ALLGOALS(asm_simp_tac 
    2.53 +        (simpset() addsimps [rtrancl_field])));
    2.54 +qed_spec_mp "commute_rtrancl";
    2.55 +
    2.56 +
    2.57 +Goalw [strip_def,confluent_def, diamond_def]
    2.58 +"strip(r) ==> confluent(r)";
    2.59 +by (dtac commute_rtrancl 1);
    2.60 +by (ALLGOALS(asm_full_simp_tac (simpset() 
    2.61 +   addsimps [rtrancl_field])));
    2.62 +qed "strip_confluent";
    2.63 +
    2.64 +
    2.65 +Goalw [commute_def,square_def]
    2.66 +  "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
    2.67 +by (Blast_tac 1);
    2.68 +qed "commute_Un";
    2.69 +
    2.70 +
    2.71 +Goalw [diamond_def]
    2.72 +  "[| diamond(r); diamond(s); commute(r, s) |] \
    2.73 +\ ==> diamond(r Un s)";
    2.74 +by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
    2.75 +qed "diamond_Un";                                           
    2.76 +
    2.77 +
    2.78 +Goalw [diamond_def,confluent_def] 
    2.79 +    "diamond(r) ==> confluent(r)";
    2.80 +by (etac commute_rtrancl 1);
    2.81 +by (Simp_tac 1);
    2.82 +qed "diamond_confluent";            
    2.83 +
    2.84 +
    2.85 +Goalw [confluent_def]
    2.86 + "[| confluent(r); confluent(s); commute(r^*, s^*); \
    2.87 +\           r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)";
    2.88 +by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    2.89 +by (blast_tac (claset() addDs [diamond_Un] 
    2.90 +     addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
    2.91 +by Auto_tac;
    2.92 +qed "confluent_Un";
    2.93 +
    2.94 +
    2.95 +Goal
    2.96 + "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)";
    2.97 +by (dresolve_tac [rtrancl_subset RS sym] 1);
    2.98 +by (assume_tac 1);
    2.99 +by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
   2.100 +by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
   2.101 +by (Asm_simp_tac 1);
   2.102 +qed "diamond_to_confluence";               
   2.103 +
   2.104 +(*** Church_Rosser ***)
   2.105 +
   2.106 +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
   2.107 +  "Church_Rosser(r) ==> confluent(r)";
   2.108 +by Auto_tac;
   2.109 +by (dtac converseI 1);
   2.110 +by (full_simp_tac (simpset() 
   2.111 +                   addsimps [rtrancl_converse RS sym]) 1);
   2.112 +by (dres_inst_tac [("x", "b")] spec 1);
   2.113 +by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
   2.114 +by (res_inst_tac [("b", "a")] rtrancl_trans 1);
   2.115 +by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
   2.116 +qed "Church_Rosser1";
   2.117 +
   2.118 +
   2.119 +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
   2.120 +"confluent(r) ==> Church_Rosser(r)";
   2.121 +by Auto_tac;
   2.122 +by (forward_tac [fieldI1] 1);
   2.123 +by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
   2.124 +by (etac rtrancl_induct 1);
   2.125 +by (ALLGOALS(Clarify_tac));
   2.126 +by (blast_tac (claset() addIs [rtrancl_refl]) 1);
   2.127 +by (blast_tac (claset() delrules [rtrancl_refl] 
   2.128 +                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
   2.129 +qed "Church_Rosser2";
   2.130 +
   2.131 +
   2.132 +Goal "Church_Rosser(r) <-> confluent(r)";
   2.133 +by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
   2.134 +qed "Church_Rosser";
   2.135 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/ex/Commutation.thy	Sat Feb 03 12:41:38 2001 +0100
     3.3 @@ -0,0 +1,32 @@
     3.4 +(*  Title:      HOL/Lambda/Commutation.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow & Sidi Ould Ehmety
     3.7 +    Copyright   1995  TU Muenchen
     3.8 +
     3.9 +Commutation theory for proving the Church Rosser theorem
    3.10 +	ported from Isabelle/HOL  by Sidi Ould Ehmety
    3.11 +*)
    3.12 +
    3.13 +Commutation = Main +    
    3.14 +
    3.15 +constdefs
    3.16 +  square  :: [i, i, i, i] => o
    3.17 +   "square(r,s,t,u) ==
    3.18 +   (ALL a b. <a,b>:r --> (ALL c. <a, c>:s
    3.19 +                          --> (EX x. <b,x>:t & <c,x>:u)))"
    3.20 +
    3.21 +   commute :: [i, i] => o       
    3.22 +   "commute(r,s) == square(r,s,s,r)"
    3.23 +
    3.24 +  diamond :: i=>o
    3.25 +  "diamond(r)   == commute(r, r)"
    3.26 +
    3.27 +  strip :: i=>o  
    3.28 +  "strip(r) == commute(r^*, r)"
    3.29 +
    3.30 +  Church_Rosser :: i => o     
    3.31 +  "Church_Rosser(r) == (ALL x y. <x,y>: (r Un converse(r))^* -->
    3.32 +			(EX z. <x,z>:r^* & <y,z>:r^*))"
    3.33 +  confluent :: i=>o    
    3.34 +  "confluent(r) == diamond(r^*)"
    3.35 +end          
     4.1 --- a/src/ZF/ex/ROOT.ML	Sat Feb 03 00:11:07 2001 +0100
     4.2 +++ b/src/ZF/ex/ROOT.ML	Sat Feb 03 12:41:38 2001 +0100
     4.3 @@ -26,6 +26,7 @@
     4.4  time_use_thy "Rmap";            (*mapping a relation over a list*)
     4.5  time_use_thy "Mutil";           (*mutilated chess board*)
     4.6  time_use_thy "PropLog";         (*completeness of propositional logic*)
     4.7 +time_use_thy "Commutation";     (*abstract Church-Rosser theory*)
     4.8  (*two Coq examples by Christine Paulin-Mohring*)
     4.9  time_use_thy "ListN";
    4.10  time_use_thy "Acc";