Modified proofs due to added triv_forall_equality.
authornipkow
Fri Feb 07 14:15:35 1997 +0100 (1997-02-07)
changeset 25978b523426e1a4
parent 2596 3b4ad6c7726f
child 2598 c49dfe47675e
Modified proofs due to added triv_forall_equality.
TFL/examples/Subst/Unify.ML
     1.1 --- a/TFL/examples/Subst/Unify.ML	Fri Feb 07 14:13:58 1997 +0100
     1.2 +++ b/TFL/examples/Subst/Unify.ML	Fri Feb 07 14:15:35 1997 +0100
     1.3 @@ -357,14 +357,13 @@
     1.4  by (REPEAT (rtac allI 1));
     1.5  by (rtac impI 1);
     1.6  by (etac conjE 1);
     1.7 -by (rename_tac "foo bar M1 N1 M2 N2" 1);
     1.8  by (Subst_case_tac [("v","Unify(M1, M2)")]);
     1.9 -by (rename_tac "foo bar M1 N1 M2 N2 theta" 1);
    1.10 +by (rename_tac "theta" 1);
    1.11  
    1.12  by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]);
    1.13 -by (rename_tac "foo bar M1 N1 M2 N2 theta sigma" 1);
    1.14 +by (rename_tac "sigma" 1);
    1.15  by (REPEAT (rtac allI 1));
    1.16 -by (rename_tac "foo bar M1 N1 M2 N2 theta sigma P Q" 1); 
    1.17 +by (rename_tac "P Q" 1); 
    1.18  by (simp_tac (HOL_ss addsimps [subst_comp]) 1);
    1.19  by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1);
    1.20  by (fast_tac HOL_cs 1);
    1.21 @@ -477,22 +476,21 @@
    1.22  by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1);
    1.23  by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*)
    1.24  
    1.25 -by (prune_params_tac);
    1.26  by (safe_tac HOL_cs);
    1.27 -by (rename_tac "M1 N1 M2 N2 theta sigma gamma" 1);
    1.28 +by (rename_tac "theta sigma gamma" 1);
    1.29  
    1.30  by (rewrite_tac [MoreGeneral_def]);
    1.31  by (rotate_tac ~3 1);
    1.32  by (eres_inst_tac [("x","gamma")] allE 1);
    1.33  by (Asm_full_simp_tac 1);
    1.34  by (etac exE 1);
    1.35 -by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta" 1);
    1.36 +by (rename_tac "delta" 1);
    1.37  by (eres_inst_tac [("x","delta")] allE 1);
    1.38  by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
    1.39  by (dtac mp 1);
    1.40  by (atac 1);
    1.41  by (etac exE 1);
    1.42 -by (rename_tac "M1 N1 M2 N2 theta sigma gamma delta rho" 1);
    1.43 +by (rename_tac "rho" 1);
    1.44  
    1.45  by (rtac exI 1);
    1.46  by (rtac subst_trans 1);
    1.47 @@ -527,7 +525,7 @@
    1.48  by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]);
    1.49  by (hyp_subst_tac 1);
    1.50  by prune_params_tac;
    1.51 -by (rename_tac "M1 N1 M2 N2 theta sigma" 1);
    1.52 +by (rename_tac "theta sigma" 1);
    1.53  
    1.54  by (dtac Unify_gives_MGU 1);
    1.55  by (dtac Unify_gives_MGU 1);