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.
Even more name changes and cleaning
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 04 Dec 2009 15:50:57 +0100
changeset 537 57073b0b8fac
parent 536 44fa9df44e6f
child 538 bce41bea3de2
Even more name changes and cleaning
IntEx.thy file | annotate | diff | comparison | revisions
QuotList.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions
QuotScript.thy file | annotate | diff | comparison | revisions 
--- a/IntEx.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/IntEx.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -1,7 +1,6 @@
 theory IntEx
 imports QuotMain
 begin
-  
 
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infix "\<approx>" 50)
@@ -237,12 +236,12 @@
 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 #"
+  "(op \<approx> ===> list_rel op \<approx> ===> list_rel op \<approx>) op # op #"
 by simp
 
 (* I believe it's true. *)
 lemma foldl_rsp[quotient_rsp]:
-  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> LIST_REL op \<approx> ===> op \<approx>) foldl foldl"
+  "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> list_rel op \<approx> ===> op \<approx>) foldl foldl"
 apply (simp only: fun_rel.simps)
 apply (rule allI)
 apply (rule allI)
@@ -257,7 +256,7 @@
 sorry
 
 lemma nil_listrel_rsp[quotient_rsp]:
-  "(LIST_REL R) [] []"
+  "(list_rel R) [] []"
 by simp
 
 lemma "foldl PLUS x [] = x"
--- a/QuotList.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -7,15 +7,15 @@
   by simp
 
 fun
-  LIST_REL
+  list_rel
 where
-  "LIST_REL R [] [] = True"
-| "LIST_REL R (x#xs) [] = False"
-| "LIST_REL R [] (x#xs) = False"
-| "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
+  "list_rel R [] [] = True"
+| "list_rel R (x#xs) [] = False"
+| "list_rel R [] (x#xs) = False"
+| "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
 
-lemma LIST_REL_EQ:
-  shows "LIST_REL (op =) \<equiv> (op =)"
+lemma list_rel_EQ:
+  shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
 apply(rule allI)+
@@ -23,22 +23,22 @@
 apply(simp_all)
 done
 
-lemma LIST_REL_REFL:
+lemma list_rel_REFL:
   assumes a: "\<And>x y. R x y = (R x = R y)"
-  shows "LIST_REL R x x"
+  shows "list_rel R x x"
 by (induct x) (auto simp add: a)
 
 lemma LIST_equivp:
   assumes a: "equivp R"
-  shows "equivp (LIST_REL R)"
+  shows "equivp (list_rel R)"
 unfolding equivp_def
 apply(rule allI)+
 apply(induct_tac x y rule: list_induct2')
 apply(simp)
 apply(simp add: expand_fun_eq)
-apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(metis list_rel.simps(1) list_rel.simps(2))
 apply(simp add: expand_fun_eq)
-apply(metis LIST_REL.simps(1) LIST_REL.simps(2))
+apply(metis list_rel.simps(1) list_rel.simps(2))
 apply(simp add: expand_fun_eq)
 apply(rule iffI)
 apply(rule allI)
@@ -48,21 +48,21 @@
 using a
 apply(unfold equivp_def)
 apply(auto)[1]
-apply(metis LIST_REL.simps(4))
+apply(metis list_rel.simps(4))
 done
 
-lemma LIST_REL_REL: 
+lemma list_rel_REL: 
   assumes q: "Quotient R Abs Rep"
-  shows "LIST_REL R r s = (LIST_REL R r r \<and> LIST_REL R s s \<and> (map Abs r = map Abs s))"
+  shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
 apply(induct r s rule: list_induct2')
 apply(simp_all)
 using Quotient_REL[OF q]
 apply(metis)
 done
 
-lemma LIST_Quotient:
+lemma list_quotient:
   assumes q: "Quotient R Abs Rep"
-  shows "Quotient (LIST_REL R) (map Abs) (map Rep)"
+  shows "Quotient (list_rel R) (map Abs) (map Rep)"
 unfolding Quotient_def
 apply(rule conjI)
 apply(rule allI)
@@ -76,7 +76,7 @@
 apply(simp)
 apply(simp add: Quotient_REP_reflp[OF q])
 apply(rule allI)+
-apply(rule LIST_REL_REL[OF q])
+apply(rule list_rel_REL[OF q])
 done
 
 lemma CONS_PRS:
@@ -86,8 +86,8 @@
 
 lemma CONS_RSP:
   assumes q: "Quotient R Abs Rep"
-  and     a: "R h1 h2" "LIST_REL R t1 t2"
-  shows "LIST_REL R (h1#t1) (h2#t2)"
+  and     a: "R h1 h2" "list_rel R t1 t2"
+  shows "list_rel R (h1#t1) (h2#t2)"
 using a by (auto)
 
 lemma NIL_PRS:
@@ -97,7 +97,7 @@
 
 lemma NIL_RSP:
   assumes q: "Quotient R Abs Rep"
-  shows "LIST_REL R [] []"
+  shows "list_rel R [] []"
 by simp
 
 lemma MAP_PRS:
@@ -110,9 +110,9 @@
 lemma MAP_RSP:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
-  and     a: "(R1 ===> R2) f1 f2" 
-  and     b: "LIST_REL R1 l1 l2"
-  shows "LIST_REL R2 (map f1 l1) (map f2 l2)"
+  and     a: "(R1 ===> R2) f1 f2"
+  and     b: "list_rel R1 l1 l2"
+  shows "list_rel R2 (map f1 l1) (map f2 l2)"
 using b a
 by (induct l1 l2 rule: list_induct2')
    (simp_all)
--- a/QuotMain.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -141,12 +141,12 @@
 (* the auxiliary data for the quotient types *)
 use "quotient_info.ML"
 
-declare [[map list = (map, LIST_REL)]]
+declare [[map list = (map, list_rel)]]
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
 
-lemmas [quotient_thm] = 
-  FUN_Quotient LIST_Quotient
+lemmas [quotient_thm] =
+  fun_quotient list_quotient
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}
@@ -214,7 +214,7 @@
   done
 
 lemmas id_simps =
-  FUN_MAP_I[THEN eq_reflection]
+  fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
   prod_fun_id map_id
@@ -610,7 +610,7 @@
     val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc rel_eqvs))
     val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc rel_eqvs))
     val simp_ctxt = (Simplifier.context ctxt empty_ss) addsimprocs [simproc1, simproc2, simproc3, simproc4]
-    (* TODO: Make sure that there are no LIST_REL, PAIR_REL etc involved *)
+    (* TODO: Make sure that there are no list_rel, pair_rel etc involved *)
     val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) rel_eqvs
   in
   ObjectLogic.full_atomize_tac THEN'
--- a/QuotScript.thy	Fri Dec 04 15:41:09 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 15:50:57 2009 +0100
@@ -121,11 +121,12 @@
 where
   "f ---> g \<equiv> fun_map f g"
 
-lemma FUN_MAP_I:
+lemma fun_map_id:
   shows "(id ---> id) = id"
 by (simp add: expand_fun_eq id_def)
 
-lemma IN_FUN:
+(* Not used *)
+lemma in_fun:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
 by (simp add: mem_def)
 
@@ -143,7 +144,7 @@
   "(op =) ===> (op =) \<equiv> (op =)"
 by (rule eq_reflection) (simp add: expand_fun_eq)
 
-lemma FUN_Quotient:
+lemma fun_quotient:
   assumes q1: "Quotient R1 abs1 rep1"
   and     q2: "Quotient R2 abs2 rep2"
   shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
@@ -224,7 +225,7 @@
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) 
                              \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
-using FUN_Quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
+using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
 by blast
 
 (* TODO: it is the same as APPLY_RSP *)
@@ -246,7 +247,7 @@
   and     r2: "Respects (R1 ===> R2) g" 
   shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
 apply(rule_tac iffI)
-using FUN_Quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
+using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))
nominal2