src/HOL/UNITY/Rename.thy
changeset 15976 44f615d1729b
parent 15481 fc075ae929e4
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/UNITY/Rename.thy	Tue May 17 10:19:46 2005 +0200
     1.2 +++ b/src/HOL/UNITY/Rename.thy	Tue May 17 17:01:19 2005 +0200
     1.3 @@ -110,10 +110,10 @@
     1.4  lemma bij_extend: "bij h ==> bij (extend (%(x,u::'c). h x))"
     1.5  apply (rule bijI)
     1.6  apply (blast intro: Extend.inj_extend)
     1.7 -apply (rule_tac f = "extend (% (x,u) . inv h x) " in surjI) 
     1.8 -apply (simplesubst inv_inv_eq [of h, symmetric], assumption) 
     1.9 -apply (subst extend_inv, simp add: bij_imp_bij_inv) 
    1.10 -apply (simp add: inv_inv_eq) 
    1.11 +apply (rule_tac f = "extend (% (x,u) . inv h x)" in surjI) 
    1.12 +apply (subst (1 2) inv_inv_eq [of h, symmetric], assumption+)
    1.13 +apply (simp add: bij_imp_bij_inv extend_inv [of "inv h"]) 
    1.14 +apply (simp add: inv_inv_eq)
    1.15  apply (rule Extend.extend_inverse) 
    1.16  apply (simp add: bij_imp_bij_inv) 
    1.17  done
    1.18 @@ -146,14 +146,14 @@
    1.19  
    1.20  lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
    1.21  apply (unfold inj_on_def, auto)
    1.22 -apply (drule_tac x = "mk_program ({x}, {}, {}) " in spec)
    1.23 -apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
    1.24 +apply (drule_tac x = "mk_program ({x}, {}, {})" in spec)
    1.25 +apply (drule_tac x = "mk_program ({y}, {}, {})" in spec)
    1.26  apply (auto simp add: program_equality_iff rename_def extend_def)
    1.27  done
    1.28  
    1.29  lemma surj_rename_imp_surj: "surj (rename h) ==> surj h"
    1.30  apply (unfold surj_def, auto)
    1.31 -apply (drule_tac x = "mk_program ({y}, {}, {}) " in spec)
    1.32 +apply (drule_tac x = "mk_program ({y}, {}, {})" in spec)
    1.33  apply (auto simp add: program_equality_iff rename_def extend_def)
    1.34  done
    1.35