src/ZF/ex/Commutation.ML
author paulson
Sat Feb 03 12:41:38 2001 +0100 (2001-02-03)
changeset 11042 bb566dd3f927
child 11316 b4e71bd751e4
permissions -rw-r--r--
commutation theory, ported by Sidi Ehmety
     1 (*  Title:      HOL/Lambda/Commutation.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Sidi Ould Ehmety
     4     Copyright   1995  TU Muenchen
     5 
     6 Commutation theory for proving the Church Rosser theorem
     7 	ported from Isabelle/HOL  by Sidi Ould Ehmety
     8 *)
     9 
    10 Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)";
    11 by (Blast_tac 1);
    12 qed "square_sym";                
    13 
    14 
    15 Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)";
    16 by (Blast_tac 1);
    17 qed "square_subset"; 
    18 
    19 
    20 Goalw [square_def]
    21  "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)";
    22 by (Clarify_tac 1);
    23 by (etac rtrancl_induct 1);
    24 by (blast_tac (claset()  addIs [rtrancl_refl]) 1);
    25 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
    26 qed_spec_mp "square_rtrancl";                 
    27 
    28 (* A special case of square_rtrancl_on *)
    29 Goalw [diamond_def, commute_def, strip_def]
    30  "diamond(r) ==> strip(r)";
    31 by (resolve_tac [square_rtrancl] 1);
    32 by (ALLGOALS(Asm_simp_tac));
    33 qed "diamond_strip";
    34 
    35 (*** commute ***)
    36 
    37 Goalw [commute_def] 
    38     "commute(r,s) ==> commute(s,r)";
    39 by (blast_tac (claset() addIs [square_sym]) 1);
    40 qed "commute_sym";
    41 
    42 Goalw [commute_def] 
    43 "commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)";
    44 by (Clarify_tac 1);
    45 by (rtac square_rtrancl 1);
    46 by (rtac square_sym  2);
    47 by (rtac square_rtrancl 2);
    48 by (rtac square_sym  3);
    49 by (ALLGOALS(asm_simp_tac 
    50         (simpset() addsimps [rtrancl_field])));
    51 qed_spec_mp "commute_rtrancl";
    52 
    53 
    54 Goalw [strip_def,confluent_def, diamond_def]
    55 "strip(r) ==> confluent(r)";
    56 by (dtac commute_rtrancl 1);
    57 by (ALLGOALS(asm_full_simp_tac (simpset() 
    58    addsimps [rtrancl_field])));
    59 qed "strip_confluent";
    60 
    61 
    62 Goalw [commute_def,square_def]
    63   "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)";
    64 by (Blast_tac 1);
    65 qed "commute_Un";
    66 
    67 
    68 Goalw [diamond_def]
    69   "[| diamond(r); diamond(s); commute(r, s) |] \
    70 \ ==> diamond(r Un s)";
    71 by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
    72 qed "diamond_Un";                                           
    73 
    74 
    75 Goalw [diamond_def,confluent_def] 
    76     "diamond(r) ==> confluent(r)";
    77 by (etac commute_rtrancl 1);
    78 by (Simp_tac 1);
    79 qed "diamond_confluent";            
    80 
    81 
    82 Goalw [confluent_def]
    83  "[| confluent(r); confluent(s); commute(r^*, s^*); \
    84 \           r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)";
    85 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    86 by (blast_tac (claset() addDs [diamond_Un] 
    87      addIs [rewrite_rule [confluent_def] diamond_confluent]) 3);
    88 by Auto_tac;
    89 qed "confluent_Un";
    90 
    91 
    92 Goal
    93  "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)";
    94 by (dresolve_tac [rtrancl_subset RS sym] 1);
    95 by (assume_tac 1);
    96 by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def])));
    97 by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1);
    98 by (Asm_simp_tac 1);
    99 qed "diamond_to_confluence";               
   100 
   101 (*** Church_Rosser ***)
   102 
   103 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]
   104   "Church_Rosser(r) ==> confluent(r)";
   105 by Auto_tac;
   106 by (dtac converseI 1);
   107 by (full_simp_tac (simpset() 
   108                    addsimps [rtrancl_converse RS sym]) 1);
   109 by (dres_inst_tac [("x", "b")] spec 1);
   110 by (dres_inst_tac [("x1", "c")] (spec RS mp) 1);
   111 by (res_inst_tac [("b", "a")] rtrancl_trans 1);
   112 by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1));
   113 qed "Church_Rosser1";
   114 
   115 
   116 Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def]  
   117 "confluent(r) ==> Church_Rosser(r)";
   118 by Auto_tac;
   119 by (forward_tac [fieldI1] 1);
   120 by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1);
   121 by (etac rtrancl_induct 1);
   122 by (ALLGOALS(Clarify_tac));
   123 by (blast_tac (claset() addIs [rtrancl_refl]) 1);
   124 by (blast_tac (claset() delrules [rtrancl_refl] 
   125                         addIs [r_into_rtrancl, rtrancl_trans]) 1);
   126 qed "Church_Rosser2";
   127 
   128 
   129 Goal "Church_Rosser(r) <-> confluent(r)";
   130 by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1);
   131 qed "Church_Rosser";