# HG changeset patch # User paulson # Date 981200498 -3600 # Node ID bb566dd3f927b125f239602ad5ca782796cddb69 # Parent e07b601e2b5a465280eb9869747d0e6e3c22b03b commutation theory, ported by Sidi Ehmety diff -r e07b601e2b5a -r bb566dd3f927 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sat Feb 03 00:11:07 2001 +0100 +++ b/src/ZF/IsaMakefile Sat Feb 03 12:41:38 2001 +0100 @@ -110,8 +110,9 @@ $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ - ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Data.ML ex/Data.thy ex/Enum.ML \ - ex/Enum.thy ex/LList.ML ex/LList.thy \ + ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \ + ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ + ex/LList.ML ex/LList.thy \ ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ ex/NatSum.ML ex/NatSum.thy ex/Primrec_defs.ML ex/Primrec_defs.thy \ diff -r e07b601e2b5a -r bb566dd3f927 src/ZF/ex/Commutation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/Commutation.ML Sat Feb 03 12:41:38 2001 +0100 @@ -0,0 +1,131 @@ +(* Title: HOL/Lambda/Commutation.thy + ID: $Id$ + Author: Tobias Nipkow & Sidi Ould Ehmety + Copyright 1995 TU Muenchen + +Commutation theory for proving the Church Rosser theorem + ported from Isabelle/HOL by Sidi Ould Ehmety +*) + +Goalw [square_def] "square(r,s,t,u) ==> square(s,r,u,t)"; +by (Blast_tac 1); +qed "square_sym"; + + +Goalw [square_def] "[| square(r,s,t,u); t <= t' |] ==> square(r,s,t',u)"; +by (Blast_tac 1); +qed "square_subset"; + + +Goalw [square_def] + "field(s)<=field(t)==> square(r,s,s,t) --> square(r^*,s,s,t^*)"; +by (Clarify_tac 1); +by (etac rtrancl_induct 1); +by (blast_tac (claset() addIs [rtrancl_refl]) 1); +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1); +qed_spec_mp "square_rtrancl"; + +(* A special case of square_rtrancl_on *) +Goalw [diamond_def, commute_def, strip_def] + "diamond(r) ==> strip(r)"; +by (resolve_tac [square_rtrancl] 1); +by (ALLGOALS(Asm_simp_tac)); +qed "diamond_strip"; + +(*** commute ***) + +Goalw [commute_def] + "commute(r,s) ==> commute(s,r)"; +by (blast_tac (claset() addIs [square_sym]) 1); +qed "commute_sym"; + +Goalw [commute_def] +"commute(r,s) ==> field(r)=field(s) --> commute(r^*,s^*)"; +by (Clarify_tac 1); +by (rtac square_rtrancl 1); +by (rtac square_sym 2); +by (rtac square_rtrancl 2); +by (rtac square_sym 3); +by (ALLGOALS(asm_simp_tac + (simpset() addsimps [rtrancl_field]))); +qed_spec_mp "commute_rtrancl"; + + +Goalw [strip_def,confluent_def, diamond_def] +"strip(r) ==> confluent(r)"; +by (dtac commute_rtrancl 1); +by (ALLGOALS(asm_full_simp_tac (simpset() + addsimps [rtrancl_field]))); +qed "strip_confluent"; + + +Goalw [commute_def,square_def] + "[| commute(r,t); commute(s,t) |] ==> commute(r Un s, t)"; +by (Blast_tac 1); +qed "commute_Un"; + + +Goalw [diamond_def] + "[| diamond(r); diamond(s); commute(r, s) |] \ +\ ==> diamond(r Un s)"; +by (REPEAT(ares_tac [commute_Un,commute_sym] 1)); +qed "diamond_Un"; + + +Goalw [diamond_def,confluent_def] + "diamond(r) ==> confluent(r)"; +by (etac commute_rtrancl 1); +by (Simp_tac 1); +qed "diamond_confluent"; + + +Goalw [confluent_def] + "[| confluent(r); confluent(s); commute(r^*, s^*); \ +\ r<=Sigma(A,B); s<=Sigma(C,D) |] ==> confluent(r Un s)"; +by (rtac (rtrancl_Un_rtrancl RS subst) 1); +by (blast_tac (claset() addDs [diamond_Un] + addIs [rewrite_rule [confluent_def] diamond_confluent]) 3); +by Auto_tac; +qed "confluent_Un"; + + +Goal + "[| diamond(r); s<=r; r<= s^* |] ==> confluent(s)"; +by (dresolve_tac [rtrancl_subset RS sym] 1); +by (assume_tac 1); +by (ALLGOALS(asm_simp_tac (simpset() addsimps[confluent_def]))); +by (resolve_tac [rewrite_rule [confluent_def] diamond_confluent] 1); +by (Asm_simp_tac 1); +qed "diamond_to_confluence"; + +(*** Church_Rosser ***) + +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def] + "Church_Rosser(r) ==> confluent(r)"; +by Auto_tac; +by (dtac converseI 1); +by (full_simp_tac (simpset() + addsimps [rtrancl_converse RS sym]) 1); +by (dres_inst_tac [("x", "b")] spec 1); +by (dres_inst_tac [("x1", "c")] (spec RS mp) 1); +by (res_inst_tac [("b", "a")] rtrancl_trans 1); +by (REPEAT(blast_tac (claset() addIs [rtrancl_mono RS subsetD]) 1)); +qed "Church_Rosser1"; + + +Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def] +"confluent(r) ==> Church_Rosser(r)"; +by Auto_tac; +by (forward_tac [fieldI1] 1); +by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1); +by (etac rtrancl_induct 1); +by (ALLGOALS(Clarify_tac)); +by (blast_tac (claset() addIs [rtrancl_refl]) 1); +by (blast_tac (claset() delrules [rtrancl_refl] + addIs [r_into_rtrancl, rtrancl_trans]) 1); +qed "Church_Rosser2"; + + +Goal "Church_Rosser(r) <-> confluent(r)"; +by (blast_tac(claset() addIs [Church_Rosser1,Church_Rosser2]) 1); +qed "Church_Rosser"; \ No newline at end of file diff -r e07b601e2b5a -r bb566dd3f927 src/ZF/ex/Commutation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/Commutation.thy Sat Feb 03 12:41:38 2001 +0100 @@ -0,0 +1,32 @@ +(* Title: HOL/Lambda/Commutation.thy + ID: $Id$ + Author: Tobias Nipkow & Sidi Ould Ehmety + Copyright 1995 TU Muenchen + +Commutation theory for proving the Church Rosser theorem + ported from Isabelle/HOL by Sidi Ould Ehmety +*) + +Commutation = Main + + +constdefs + square :: [i, i, i, i] => o + "square(r,s,t,u) == + (ALL a b. :r --> (ALL c. :s + --> (EX x. :t & :u)))" + + commute :: [i, i] => o + "commute(r,s) == square(r,s,s,r)" + + diamond :: i=>o + "diamond(r) == commute(r, r)" + + strip :: i=>o + "strip(r) == commute(r^*, r)" + + Church_Rosser :: i => o + "Church_Rosser(r) == (ALL x y. : (r Un converse(r))^* --> + (EX z. :r^* & :r^*))" + confluent :: i=>o + "confluent(r) == diamond(r^*)" +end diff -r e07b601e2b5a -r bb566dd3f927 src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Sat Feb 03 00:11:07 2001 +0100 +++ b/src/ZF/ex/ROOT.ML Sat Feb 03 12:41:38 2001 +0100 @@ -26,6 +26,7 @@ time_use_thy "Rmap"; (*mapping a relation over a list*) time_use_thy "Mutil"; (*mutilated chess board*) time_use_thy "PropLog"; (*completeness of propositional logic*) +time_use_thy "Commutation"; (*abstract Church-Rosser theory*) (*two Coq examples by Christine Paulin-Mohring*) time_use_thy "ListN"; time_use_thy "Acc";