Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 21 Aug 2009 13:56:20 +0200
changeset 5 b3d878d19a09
parent 4 0eb89a350f43
child 6 6a1b4c22a386
Fixed
QuotMain.thy file | annotate | diff | comparison | revisions 
--- a/QuotMain.thy	Fri Aug 21 13:36:58 2009 +0200
+++ b/QuotMain.thy	Fri Aug 21 13:56:20 2009 +0200
@@ -70,12 +70,6 @@
 apply(simp add: thm10 thm11)
 done
 
-lemma REP_ABS_rsp:
-  shows "R g g \<Longrightarrow> (REP (ABS g) = g"
-apply(subst thm11)
-apply(simp add: thm10 thm11)
-done
-
 lemma QUOTIENT:
   "QUOTIENT R ABS REP"
 apply(unfold QUOTIENT_def)
@@ -567,7 +561,7 @@
 unfolding IN_def EMPTY_def
 apply(rule_tac f="(op =) False" in arg_cong)
 apply(rule mem_respects)
-apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
         simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
 apply(rule list_eq.intros)
 done
@@ -589,7 +583,7 @@
 apply(rule mem_respects)
 apply(rule list_eq.intros(3))
 apply(unfold REP_fset_def ABS_fset_def)
-apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
+apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset])
 apply(rule list_eq_sym)
 done
 
@@ -602,8 +596,6 @@
   apply(simp add: list_eq_sym)
 done
 
-thm list_eq.intros
-
 lemma yyy :
   shows "
     (
@@ -620,7 +612,7 @@
                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+  apply(simp only:QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                     simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
   apply(simp)
@@ -629,14 +621,14 @@
                   simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule helper)
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
+  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset,
                    simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
   apply(simp only: QUOT_TYPE.thm11[OF QUOT_TYPE_fset, 
                      simplified REP_fset_def[symmetric] ABS_fset_def[symmetric], symmetric])
   apply(rule list_eq.intros(5))
   apply(rule list_eq.intros(3))
-  apply(rule QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
+  apply(simp only: QUOT_TYPE.REP_ABS_rsp[OF QUOT_TYPE_fset, 
                  simplified REP_fset_def[symmetric] ABS_fset_def[symmetric]])
   apply(rule list_eq_sym)
 done
nominal2