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.
Cleaning & Renaming coming from QuotList
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 04 Dec 2009 16:12:40 +0100
changeset 539 8287fb5b8d7a
parent 538 bce41bea3de2
child 540 c0b13fb70d6d
Cleaning & Renaming coming from QuotList
QuotList.thy file | annotate | diff | comparison | revisions
QuotMain.thy file | annotate | diff | comparison | revisions
QuotScript.thy file | annotate | diff | comparison | revisions 
--- a/QuotList.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -2,10 +2,6 @@
 imports QuotScript List
 begin
 
-lemma LIST_map_id:
-  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
-  by simp
-
 fun
   list_rel
 where
@@ -14,70 +10,60 @@
 | "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 =)"
-apply(rule eq_reflection)
-unfolding expand_fun_eq
-apply(rule allI)+
-apply(induct_tac x xa rule: list_induct2')
-apply(simp_all)
-done
-
-lemma list_rel_REFL:
-  assumes a: "\<And>x y. R x y = (R x = R y)"
-  shows "list_rel R x x"
-by (induct x) (auto simp add: a)
-
-lemma LIST_equivp:
+lemma list_equivp:
   assumes a: "equivp 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(simp add: expand_fun_eq)
-apply(metis list_rel.simps(1) list_rel.simps(2))
-apply(simp add: expand_fun_eq)
-apply(rule iffI)
-apply(rule allI)
-apply(case_tac x)
-apply(simp)
-apply(simp)
-using a
-apply(unfold equivp_def)
-apply(auto)[1]
-apply(metis list_rel.simps(4))
-done
+  unfolding equivp_def
+  apply(rule allI)+
+  apply(induct_tac x y rule: list_induct2')
+  apply(simp_all 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(rule iffI)
+  apply(rule allI)
+  apply(case_tac x)
+  apply(simp_all)
+  using a
+  apply(unfold equivp_def)
+  apply(auto)[1]
+  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))"
-apply(induct r s rule: list_induct2')
-apply(simp_all)
-using Quotient_REL[OF q]
-apply(metis)
-done
+  apply(induct r s rule: list_induct2')
+  apply(simp_all)
+  using Quotient_rel[OF q]
+  apply(metis)
+  done
 
 lemma list_quotient:
   assumes q: "Quotient R Abs Rep"
   shows "Quotient (list_rel R) (map Abs) (map Rep)"
-unfolding Quotient_def
-apply(rule conjI)
-apply(rule allI)
-apply(induct_tac a)
-apply(simp)
-apply(simp add: Quotient_ABS_REP[OF q])
-apply(rule conjI)
-apply(rule allI)
-apply(induct_tac a)
-apply(simp)
-apply(simp)
-apply(simp add: Quotient_REP_reflp[OF q])
-apply(rule allI)+
-apply(rule list_rel_REL[OF q])
-done
+  unfolding Quotient_def
+  apply(rule conjI)
+  apply(rule allI)
+  apply(induct_tac a)
+  apply(simp)
+  apply(simp add: Quotient_ABS_REP[OF q])
+  apply(rule conjI)
+  apply(rule allI)
+  apply(induct_tac a)
+  apply(simp)
+  apply(simp)
+  apply(simp add: Quotient_REP_reflp[OF q])
+  apply(rule allI)+
+  apply(rule list_rel_rel[OF q])
+  done
+
+
+
+
+
+
+(* Rest is not used *)
+
 
 lemma CONS_PRS:
   assumes q: "Quotient R Abs Rep"
@@ -118,138 +104,24 @@
    (simp_all)
 
 
-end
 
-(*
-val LENGTH_PRS = store_thm
-   ("LENGTH_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l. LENGTH l = LENGTH (MAP rep l)--),
-
-val LENGTH_RSP = store_thm
-   ("LENGTH_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2.
-          (LIST_REL R) l1 l2 ==>
-          (LENGTH l1 = LENGTH l2)--),
-val APPEND_PRS = store_thm
-   ("APPEND_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l m. APPEND l m = MAP abs (APPEND (MAP rep l) (MAP rep m))--),
-
-val APPEND_RSP = store_thm
-   ("APPEND_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2 m1 m2.
-          (LIST_REL R) l1 l2 /\ (LIST_REL R) m1 m2 ==>
-          (LIST_REL R) (APPEND l1 m1) (APPEND l2 m2)--),
-val FLAT_PRS = store_thm
-   ("FLAT_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l. FLAT l = MAP abs (FLAT (MAP (MAP rep) l))--),
-
-val FLAT_RSP = store_thm
-   ("FLAT_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2.
-          LIST_REL (LIST_REL R) l1 l2 ==>
-          (LIST_REL R) (FLAT l1) (FLAT l2)--),
-
-val REVERSE_PRS = store_thm
-   ("REVERSE_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l. REVERSE l = MAP abs (REVERSE (MAP rep l))--),
-
-val REVERSE_RSP = store_thm
-   ("REVERSE_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2.
-          LIST_REL R l1 l2 ==>
-          (LIST_REL R) (REVERSE l1) (REVERSE l2)--),
-
-val FILTER_PRS = store_thm
-   ("FILTER_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !P l. FILTER P l = (MAP abs) (FILTER ((abs --> I) P) (MAP rep l))
-       --),
-
-val FILTER_RSP = store_thm
-   ("FILTER_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !P1 P2 l1 l2.
-          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
-          (LIST_REL R) (FILTER P1 l1) (FILTER P2 l2)--),
-
-val NULL_PRS = store_thm
-   ("NULL_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l. NULL l = NULL (MAP rep l)--),
+lemma LIST_map_id:
+  shows "map (\<lambda>x. x) = (\<lambda>x. x)"
+  by simp
 
-val NULL_RSP = store_thm
-   ("NULL_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2.
-          LIST_REL R l1 l2 ==>
-          (NULL l1 = NULL l2)--),
-
-val SOME_EL_PRS = store_thm
-   ("SOME_EL_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l P. SOME_EL P l = SOME_EL ((abs --> I) P) (MAP rep l)--),
-
-val SOME_EL_RSP = store_thm
-   ("SOME_EL_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2 P1 P2.
-          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
-          (SOME_EL P1 l1 = SOME_EL P2 l2)--),
-
-val ALL_EL_PRS = store_thm
-   ("ALL_EL_PRS",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l P. ALL_EL P l = ALL_EL ((abs --> I) P) (MAP rep l)--),
-
-val ALL_EL_RSP = store_thm
-   ("ALL_EL_RSP",
-    (--!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==>
-         !l1 l2 P1 P2.
-          (R ===> $=) P1 P2 /\ (LIST_REL R) l1 l2 ==>
-          (ALL_EL P1 l1 = ALL_EL P2 l2)--),
+lemma list_rel_EQ:
+  shows "list_rel (op =) \<equiv> (op =)"
+apply(rule eq_reflection)
+unfolding expand_fun_eq
+apply(rule allI)+
+apply(induct_tac x xa rule: list_induct2')
+apply(simp_all)
+done
 
-val FOLDL_PRS = store_thm
-   ("FOLDL_PRS",
-    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
-        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
-         !l f e. FOLDL f e l =
-                 abs1 (FOLDL ((abs1 --> abs2 --> rep1) f)
-                      (rep1 e)
-                      (MAP rep2 l))--),
-
-val FOLDL_RSP = store_thm
-   ("FOLDL_RSP",
-    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
-        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
-         !l1 l2 f1 f2 e1 e2.
-          (R1 ===> R2 ===> R1) f1 f2 /\
-             R1 e1 e2 /\ (LIST_REL R2) l1 l2 ==>
-          R1 (FOLDL f1 e1 l1) (FOLDL f2 e2 l2)--),
+lemma list_rel_REFL:
+  assumes a: "\<And>x y. R x y = (R x = R y)"
+  shows "list_rel R x x"
+by (induct x) (auto simp add: a)
 
-val FOLDR_PRS = store_thm
-   ("FOLDR_PRS",
-    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
-        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
-         !l f e. FOLDR f e l =
-                 abs2 (FOLDR ((abs1 --> abs2 --> rep2) f)
-                      (rep2 e)
-                      (MAP rep1 l))--),
 
-val FOLDR_RSP = store_thm
-   ("FOLDR_RSP",
-    (--!R1 (abs1:'a -> 'c) rep1. QUOTIENT R1 abs1 rep1 ==>
-        !R2 (abs2:'b -> 'd) rep2. QUOTIENT R2 abs2 rep2 ==>
-         !l1 l2 f1 f2 e1 e2.
-          (R1 ===> R2 ===> R2) f1 f2 /\
-             R2 e1 e2 /\ (LIST_REL R1) l1 l2 ==>
-          R2 (FOLDR f1 e1 l1) (FOLDR f2 e2 l2)--),
-*)
-
+end
--- a/QuotMain.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -461,7 +461,7 @@
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
      rtac @{thm IDENTITY_equivp},
-     rtac @{thm LIST_equivp}])
+     rtac @{thm list_equivp}])
 *}
 
 ML {*
--- a/QuotScript.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -53,7 +53,7 @@
 using a unfolding Quotient_def
 by blast
 
-lemma Quotient_REL:
+lemma Quotient_rel:
   assumes a: "Quotient E Abs Rep"
   shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))"
 using a unfolding Quotient_def
@@ -251,7 +251,7 @@
 apply(metis fun_rel_IMP)
 using r1 unfolding Respects_def expand_fun_eq
 apply(simp (no_asm_use))
-apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1])
+apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1])
 done
 
 (* ask Peter: fun_rel_IMP used twice *) 
@@ -328,14 +328,14 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
 (* Not used *)
 lemma REP_ABS_RSP_LEFT:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using q a by (metis Quotient_REL[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
+using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q])
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)
nominal2