src/ZF/ex/Commutation.ML
changeset 11042 bb566dd3f927
child 11316 b4e71bd751e4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/ex/Commutation.ML	Sat Feb 03 12:41:38 2001 +0100
     1.3 @@ -0,0 +1,131 @@
     1.4 +(*  Title:      HOL/Lambda/Commutation.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Tobias Nipkow & Sidi Ould Ehmety
     1.7 +    Copyright   1995  TU Muenchen
     1.8 +
     1.9 +Commutation theory for proving the Church Rosser theorem
    1.10 +	ported from Isabelle/HOL  by Sidi Ould Ehmety
    1.11 +*)
    1.12 +
    1.13 +Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
    1.14 +by (Blast_tac 1);
    1.15 +qed "square_sym";                
    1.16 +
    1.17 +
    1.18 +Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)";
    1.19 +by (Blast_tac 1);
    1.20 +qed "square_subset"; 
    1.21 +
    1.22 +
    1.23 +Goalw [square_def]
    1.24 + "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
    1.25 +by (Clarify_tac 1);
    1.26 +by (etac rtrancl_induct 1);
    1.27 +by (blast_tac (claset()  addIs [rtrancl_refl]) 1);
    1.28 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    1.29 +qed_spec_mp "square_rtrancl";                 
    1.30 +
    1.31 +(* A special case of square_rtrancl_on *)
    1.32 +Goalw [diamond_def, commute_def, strip_def]
    1.33 + "diamond(r) ==> strip(r)";
    1.34 +by (resolve_tac [square_rtrancl] 1);
    1.35 +by (ALLGOALS(Asm_simp_tac));
    1.36 +qed "diamond_strip";
    1.37 +
    1.38 +(*** commute ***)
    1.39 +
    1.40 +Goalw [commute_def] 
    1.41 +    "commute(r,s) ==> commute(s,r)";
    1.42 +by (blast_tac (claset() addIs [square_sym]) 1);
    1.43 +qed "commute_sym";
    1.44 +
    1.45 +Goalw [commute_def] 
    1.46 +"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
    1.47 +by (Clarify_tac 1);
    1.48 +by (rtac square_rtrancl 1);
    1.49 +by (rtac square_sym  2);
    1.50 +by (rtac square_rtrancl 2);
    1.51 +by (rtac square_sym  3);
    1.52 +by (ALLGOALS(asm_simp_tac 
    1.53 +        (simpset() addsimps [rtrancl_field])));
    1.54 +qed_spec_mp "commute_rtrancl";
    1.55 +
    1.56 +
    1.57 +Goalw [strip_def,confluent_def, diamond_def]
    1.58 +"strip(r) ==> confluent(r)";
    1.59 +by (dtac commute_rtrancl 1);
    1.60 +by (ALLGOALS(asm_full_simp_tac (simpset() 
    1.61 +   addsimps [rtrancl_field])));
    1.62 +qed "strip_confluent";
    1.63 +
    1.64 +
    1.65 +Goalw [commute_def,square_def]
    1.66 +  "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
    1.67 +by (Blast_tac 1);
    1.68 +qed "commute_Un";
    1.69 +
    1.70 +
    1.71 +Goalw [diamond_def]
    1.72 +  "[| diamond(r); diamond(s); commute(r, s) |] \
    1.73 +\ ==> diamond(r Un s)";
    1.74 +by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
    1.75 +qed "diamond_Un";                                           
    1.76 +
    1.77 +
    1.78 +Goalw [diamond_def,confluent_def] 
    1.79 +    "diamond(r) ==> confluent(r)";
    1.80 +by (etac commute_rtrancl 1);
    1.81 +by (Simp_tac 1);
    1.82 +qed "diamond_confluent";            
    1.83 +
    1.84 +
    1.85 +Goalw [confluent_def]
    1.86 + "[| confluent(r); confluent(s); commute(r^*, s^*); \
    1.87 +\           r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)";
    1.88 +by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    1.89 +by (blast_tac (claset() addDs [diamond_Un] 
    1.90 +     addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
    1.91 +by Auto_tac;
    1.92 +qed "confluent_Un";
    1.93 +
    1.94 +
    1.95 +Goal
    1.96 + "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)";
    1.97 +by (dresolve_tac [rtrancl_subset RS sym] 1);
    1.98 +by (assume_tac 1);
    1.99 +by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
   1.100 +by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
   1.101 +by (Asm_simp_tac 1);
   1.102 +qed "diamond_to_confluence";               
   1.103 +
   1.104 +(*** Church_Rosser ***)
   1.105 +
   1.106 +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
   1.107 +  "Church_Rosser(r) ==> confluent(r)";
   1.108 +by Auto_tac;
   1.109 +by (dtac converseI 1);
   1.110 +by (full_simp_tac (simpset() 
   1.111 +                   addsimps [rtrancl_converse RS sym]) 1);
   1.112 +by (dres_inst_tac [("x", "b")] spec 1);
   1.113 +by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
   1.114 +by (res_inst_tac [("b", "a")] rtrancl_trans 1);
   1.115 +by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
   1.116 +qed "Church_Rosser1";
   1.117 +
   1.118 +
   1.119 +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
   1.120 +"confluent(r) ==> Church_Rosser(r)";
   1.121 +by Auto_tac;
   1.122 +by (forward_tac [fieldI1] 1);
   1.123 +by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
   1.124 +by (etac rtrancl_induct 1);
   1.125 +by (ALLGOALS(Clarify_tac));
   1.126 +by (blast_tac (claset() addIs [rtrancl_refl]) 1);
   1.127 +by (blast_tac (claset() delrules [rtrancl_refl] 
   1.128 +                        addIs [r_into_rtrancl, rtrancl_trans]) 1);
   1.129 +qed "Church_Rosser2";
   1.130 +
   1.131 +
   1.132 +Goal "Church_Rosser(r) <-> confluent(r)";
   1.133 +by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
   1.134 +qed "Church_Rosser";
   1.135 \ No newline at end of file