Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
IntEx.thy
changeset 529 6348c2a57ec2
parent 506 91c374abde06
child 536 44fa9df44e6f 
--- a/IntEx.thy	Fri Dec 04 15:04:05 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:18:33 2009 +0100
@@ -9,13 +9,13 @@
   "intrel (x, y) (u, v) = (x + v = u + y)"
 
 quotient my_int = "nat \<times> nat" / intrel
-  apply(unfold EQUIV_def)
+  apply(unfold equivp_def)
   apply(auto simp add: mem_def expand_fun_eq)
   done
 
 thm quotient_thm
 
-thm my_int_equiv
+thm my_int_equivp
 
 print_theorems
 print_quotients
@@ -198,30 +198,30 @@
 
 
 lemma foldr_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
 apply (induct l)
-apply (simp add: QUOTIENT_ABS_REP[OF b])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 lemma foldl_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
 apply (induct l arbitrary:e)
-apply (simp add: QUOTIENT_ABS_REP[OF a])
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 lemma map_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
-  and     b: "QUOTIENT R2 abs2 rep2"
+  assumes a: "Quotient R1 abs1 rep1"
+  and     b: "Quotient R2 abs2 rep2"
   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
 apply (induct l)
 apply (simp)
-apply (simp add: QUOTIENT_ABS_REP[OF a] QUOTIENT_ABS_REP[OF b])
+apply (simp add: Quotient_ABS_REP[OF a] Quotient_ABS_REP[OF b])
 done
 
 
@@ -231,10 +231,10 @@
 by simp
 
 lemma cons_prs:
-  assumes a: "QUOTIENT R1 abs1 rep1"
+  assumes a: "Quotient R1 abs1 rep1"
   shows "(map abs1) ((rep1 h) # (map rep1 t)) = h # t"
   apply (induct t)
-by (simp_all add: QUOTIENT_ABS_REP[OF a])
+by (simp_all add: Quotient_ABS_REP[OF a])
 
 lemma cons_rsp[quotient_rsp]:
   "(op \<approx> ===> LIST_REL op \<approx> ===> LIST_REL op \<approx>) op # op #"
@@ -264,7 +264,7 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: nil_prs)
 apply(tactic {* clean_tac @{context} 1 *})
 done
@@ -276,8 +276,8 @@
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
 apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
-apply(simp only: foldl_prs[OF QUOTIENT_my_int QUOTIENT_my_int])
-apply(simp only: cons_prs[OF QUOTIENT_my_int])
+apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int])
+apply(simp only: cons_prs[OF Quotient_my_int])
 apply(tactic {* clean_tac @{context} 1 *})
 done
nominal2