src/HOL/Lambda/Commutation.ML
changeset 8984 b71c460c6f97
parent 5117 7b5efef2ca74
equal deleted inserted replaced
8983:15bd7d568fb2 8984:b71c460c6f97
    76 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    76 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
    77 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
    77 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
    78 qed "confluent_Un";
    78 qed "confluent_Un";
    79 
    79 
    80 Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
    80 Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
    81 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
    81 by (force_tac (claset() addIs [diamond_confluent] 
    82 		       addss simpset()) 1);
    82                         addDs [rtrancl_subset RS sym], simpset()) 1);
    83 qed "diamond_to_confluence";
    83 qed "diamond_to_confluence";
    84 
    84 
    85 (*** Church_Rosser ***)
    85 (*** Church_Rosser ***)
    86 
    86 
    87 Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]
    87 Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]