Polished proofs.
authornipkow
Tue Jan 02 14:08:04 1996 +0100 (1996-01-02)
changeset 1431be7c6d77e19c
parent 1430 439e1476a7f8
child 1432 2cdb85e5cd90
Polished proofs.
src/HOL/Lambda/Commutation.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/ParRed.ML
     1.1 --- a/src/HOL/Lambda/Commutation.ML	Tue Jan 02 10:46:50 1996 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.ML	Tue Jan 02 14:08:04 1996 +0100
     1.3 @@ -15,6 +15,11 @@
     1.4  qed "square_sym";
     1.5  
     1.6  goalw Commutation.thy [square_def]
     1.7 +  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
     1.8 +by(fast_tac set_cs 1);
     1.9 +qed "square_subset";
    1.10 +
    1.11 +goalw Commutation.thy [square_def]
    1.12    "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
    1.13  by(fast_tac rel_cs 1);
    1.14  qed "square_reflcl";
    1.15 @@ -66,6 +71,12 @@
    1.16  be commute_rtrancl 1;
    1.17  qed "diamond_confluent";
    1.18  
    1.19 +goalw Commutation.thy [diamond_def]
    1.20 +  "!!R. square R R (R^=) (R^=) ==> confluent R";
    1.21 +by(fast_tac (trancl_cs addIs [square_rtrancl_reflcl_commute,r_into_rtrancl]
    1.22 +                       addEs [square_subset]) 1);
    1.23 +qed "square_reflcl_confluent";
    1.24 +
    1.25  goal Commutation.thy
    1.26   "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
    1.27  \      ==> confluent(R Un S)";
     2.1 --- a/src/HOL/Lambda/Eta.ML	Tue Jan 02 10:46:50 1996 +0100
     2.2 +++ b/src/HOL/Lambda/Eta.ML	Tue Jan 02 14:08:04 1996 +0100
     2.3 @@ -118,22 +118,16 @@
     2.4  
     2.5  (*** Confluence of eta ***)
     2.6  
     2.7 -goalw Eta.thy [id_def]
     2.8 -  "!x y. x-e> y --> (!z. x-e>z --> (? u. y -e>= u & z -e>= u))";
     2.9 +goalw Eta.thy [square_def,id_def]  "square eta eta (eta^=) (eta^=)";
    2.10  br eta.mutual_induct 1;
    2.11  by(ALLGOALS(fast_tac (eta_cs addSEs [eta_decr,not_free_eta] addss !simpset)));
    2.12 -val lemma = result() RS spec RS spec RS mp RS spec RS mp;
    2.13 -
    2.14 -goalw Eta.thy [diamond_def,commute_def,square_def] "diamond(eta^=)";
    2.15 -by(fast_tac (eta_cs addEs [lemma]) 1);
    2.16 -qed "diamond_refl_eta";
    2.17 +val lemma = result();
    2.18  
    2.19  goal Eta.thy "confluent(eta)";
    2.20 -by(stac (rtrancl_reflcl RS sym) 1);
    2.21 -by(rtac (diamond_refl_eta RS diamond_confluent) 1);
    2.22 +by(rtac (lemma RS square_reflcl_confluent) 1);
    2.23  qed "eta_confluent";
    2.24  
    2.25 -(*** Congruence rules for ->> ***)
    2.26 +(*** Congruence rules for -e>> ***)
    2.27  
    2.28  goal Eta.thy "!!s. s -e>> s' ==> Fun s -e>> Fun s'";
    2.29  be rtrancl_induct 1;
    2.30 @@ -157,10 +151,10 @@
    2.31  
    2.32  (*** Commutation of beta and eta ***)
    2.33  
    2.34 -goal Eta.thy "!!s. s -> t ==> !i. free t i --> free s i";
    2.35 -be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    2.36 +goal Eta.thy "!s t. s -> t --> (!i. free t i --> free s i)";
    2.37 +br beta.mutual_induct 1;
    2.38  by(ALLGOALS(Asm_full_simp_tac));
    2.39 -bind_thm("free_beta", result() RS spec RS mp);
    2.40 +bind_thm("free_beta", result() RS spec RS spec RS mp RS spec RS mp);
    2.41  
    2.42  goalw Eta.thy [decr_def] "!s t. s -> t --> (!i. decr s i -> decr t i)";
    2.43  br beta.mutual_induct 1;
     3.1 --- a/src/HOL/Lambda/ParRed.ML	Tue Jan 02 10:46:50 1996 +0100
     3.2 +++ b/src/HOL/Lambda/ParRed.ML	Tue Jan 02 14:08:04 1996 +0100
     3.3 @@ -32,16 +32,14 @@
     3.4  
     3.5  goal ParRed.thy "beta <= par_beta";
     3.6  br subsetI 1;
     3.7 -by (res_inst_tac[("p","x")]PairE 1);
     3.8 -by (hyp_subst_tac 1);
     3.9 +by (split_all_tac 1);
    3.10  be (beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    3.11  by (ALLGOALS(fast_tac (parred_cs addSIs [par_beta_refl])));
    3.12  qed "beta_subset_par_beta";
    3.13  
    3.14  goal ParRed.thy "par_beta <= beta^*";
    3.15  br subsetI 1;
    3.16 -by (res_inst_tac[("p","x")]PairE 1);
    3.17 -by (hyp_subst_tac 1);
    3.18 +by (split_all_tac 1);
    3.19  be (par_beta.mutual_induct RS spec RS spec RSN (2,rev_mp)) 1;
    3.20  by (ALLGOALS(fast_tac (parred_cs addIs
    3.21         [rtrancl_beta_Fun,rtrancl_beta_App,rtrancl_refl,