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