author kuncar Mon Mar 26 15:32:54 2012 +0200 (2012-03-26) changeset 47116 529d2a949bd4 parent 47107 35807a5d8dc2 child 47117 9890d4f0c1db
tuned proof - no smt call
```     1.1 --- a/src/HOL/Quotient_Examples/Lift_Fun.thy	Sat Mar 24 16:27:04 2012 +0100
1.2 +++ b/src/HOL/Quotient_Examples/Lift_Fun.thy	Mon Mar 26 15:32:54 2012 +0200
1.3 @@ -85,7 +85,10 @@
1.4    unfolding endofun_rel_def map_endofun_def map_fun_def o_def map_endofun'_def endofun_rel'_def id_def
1.5      by (metis (mono_tags) Quotient_endofun rep_abs_rsp)
1.6  next
1.7 -  show "\<And>r s. endofun_rel R r s =
1.8 +  have abs_to_eq: "\<And> x y. abs_endofun x = abs_endofun y \<Longrightarrow> x = y"
1.9 +  by (drule arg_cong[where f=rep_endofun]) (simp add: Quotient_rep_abs[OF Quotient_endofun])
1.10 +  fix r s
1.11 +  show "endofun_rel R r s =
1.12            (endofun_rel R r r \<and>
1.13             endofun_rel R s s \<and> map_endofun Abs Rep r = map_endofun Abs Rep s)"
1.14      apply(auto simp add: endofun_rel_def endofun_rel'_def map_endofun_def map_endofun'_def)
1.15 @@ -95,8 +98,7 @@
1.16      apply metis
1.17      using fun_quotient[OF a a, THEN Quotient_rel]
1.18      apply metis
1.19 -    using fun_quotient[OF a a, THEN Quotient_rel]
1.20 -    by (smt Quotient_endofun rep_abs_rsp)
1.21 +    by (auto intro: fun_quotient[OF a a, THEN Quotient_rel, THEN iffD1] simp add: abs_to_eq)
1.22  qed
1.23
1.24  declare [[map endofun = (endofun_rel, endofun_quotient)]]
```