src/HOL/Library/Quotient_List.thy
author Christian Urban <urbanc@in.tum.de>
Tue May 11 07:45:47 2010 +0100 (2010-05-11)
changeset 36812 e090bdb4e1c5
parent 36276 92011cc923f5
child 37492 ab36b1a50ca8
permissions -rw-r--r--
tuned proof so that no simplifier warning is printed
     1 (*  Title:      HOL/Library/Quotient_List.thy
     2     Author:     Cezary Kaliszyk and Christian Urban
     3 *)
     4 
     5 header {* Quotient infrastructure for the list type *}
     6 
     7 theory Quotient_List
     8 imports Main Quotient_Syntax
     9 begin
    10 
    11 fun
    12   list_rel
    13 where
    14   "list_rel R [] [] = True"
    15 | "list_rel R (x#xs) [] = False"
    16 | "list_rel R [] (x#xs) = False"
    17 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"
    18 
    19 declare [[map list = (map, list_rel)]]
    20 
    21 lemma split_list_all:
    22   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"
    23   apply(auto)
    24   apply(case_tac x)
    25   apply(simp_all)
    26   done
    27 
    28 lemma map_id[id_simps]:
    29   shows "map id = id"
    30   apply(simp add: expand_fun_eq)
    31   apply(rule allI)
    32   apply(induct_tac x)
    33   apply(simp_all)
    34   done
    35 
    36 
    37 lemma list_rel_reflp:
    38   shows "equivp R \<Longrightarrow> list_rel R xs xs"
    39   apply(induct xs)
    40   apply(simp_all add: equivp_reflp)
    41   done
    42 
    43 lemma list_rel_symp:
    44   assumes a: "equivp R"
    45   shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs"
    46   apply(induct xs ys rule: list_induct2')
    47   apply(simp_all)
    48   apply(rule equivp_symp[OF a])
    49   apply(simp)
    50   done
    51 
    52 lemma list_rel_transp:
    53   assumes a: "equivp R"
    54   shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
    55   using a
    56   apply(induct R xs1 xs2 arbitrary: xs3 rule: list_rel.induct)
    57   apply(simp)
    58   apply(simp)
    59   apply(simp)
    60   apply(case_tac xs3)
    61   apply(clarify)
    62   apply(simp (no_asm_use))
    63   apply(clarify)
    64   apply(simp (no_asm_use))
    65   apply(auto intro: equivp_transp)
    66   done
    67 
    68 lemma list_equivp[quot_equiv]:
    69   assumes a: "equivp R"
    70   shows "equivp (list_rel R)"
    71   apply(rule equivpI)
    72   unfolding reflp_def symp_def transp_def
    73   apply(subst split_list_all)
    74   apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])
    75   apply(blast intro: list_rel_symp[OF a])
    76   apply(blast intro: list_rel_transp[OF a])
    77   done
    78 
    79 lemma list_rel_rel:
    80   assumes q: "Quotient R Abs Rep"
    81   shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
    82   apply(induct r s rule: list_induct2')
    83   apply(simp_all)
    84   using Quotient_rel[OF q]
    85   apply(metis)
    86   done
    87 
    88 lemma list_quotient[quot_thm]:
    89   assumes q: "Quotient R Abs Rep"
    90   shows "Quotient (list_rel R) (map Abs) (map Rep)"
    91   unfolding Quotient_def
    92   apply(subst split_list_all)
    93   apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
    94   apply(rule conjI)
    95   apply(rule allI)
    96   apply(induct_tac a)
    97   apply(simp)
    98   apply(simp)
    99   apply(simp add: Quotient_rep_reflp[OF q])
   100   apply(rule allI)+
   101   apply(rule list_rel_rel[OF q])
   102   done
   103 
   104 
   105 lemma cons_prs_aux:
   106   assumes q: "Quotient R Abs Rep"
   107   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
   108   by (induct t) (simp_all add: Quotient_abs_rep[OF q])
   109 
   110 lemma cons_prs[quot_preserve]:
   111   assumes q: "Quotient R Abs Rep"
   112   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
   113   by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
   114      (simp)
   115 
   116 lemma cons_rsp[quot_respect]:
   117   assumes q: "Quotient R Abs Rep"
   118   shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"
   119   by (auto)
   120 
   121 lemma nil_prs[quot_preserve]:
   122   assumes q: "Quotient R Abs Rep"
   123   shows "map Abs [] = []"
   124   by simp
   125 
   126 lemma nil_rsp[quot_respect]:
   127   assumes q: "Quotient R Abs Rep"
   128   shows "list_rel R [] []"
   129   by simp
   130 
   131 lemma map_prs_aux:
   132   assumes a: "Quotient R1 abs1 rep1"
   133   and     b: "Quotient R2 abs2 rep2"
   134   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
   135   by (induct l)
   136      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   137 
   138 lemma map_prs[quot_preserve]:
   139   assumes a: "Quotient R1 abs1 rep1"
   140   and     b: "Quotient R2 abs2 rep2"
   141   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
   142   and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
   143   by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
   144      (simp_all add: Quotient_abs_rep[OF a])
   145 
   146 lemma map_rsp[quot_respect]:
   147   assumes q1: "Quotient R1 Abs1 Rep1"
   148   and     q2: "Quotient R2 Abs2 Rep2"
   149   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
   150   and   "((R1 ===> op =) ===> (list_rel R1) ===> op =) map map"
   151   apply simp_all
   152   apply(rule_tac [!] allI)+
   153   apply(rule_tac [!] impI)
   154   apply(rule_tac [!] allI)+
   155   apply (induct_tac [!] xa ya rule: list_induct2')
   156   apply simp_all
   157   done
   158 
   159 lemma foldr_prs_aux:
   160   assumes a: "Quotient R1 abs1 rep1"
   161   and     b: "Quotient R2 abs2 rep2"
   162   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
   163   by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   164 
   165 lemma foldr_prs[quot_preserve]:
   166   assumes a: "Quotient R1 abs1 rep1"
   167   and     b: "Quotient R2 abs2 rep2"
   168   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
   169   by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
   170      (simp)
   171 
   172 lemma foldl_prs_aux:
   173   assumes a: "Quotient R1 abs1 rep1"
   174   and     b: "Quotient R2 abs2 rep2"
   175   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
   176   by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   177 
   178 
   179 lemma foldl_prs[quot_preserve]:
   180   assumes a: "Quotient R1 abs1 rep1"
   181   and     b: "Quotient R2 abs2 rep2"
   182   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   183   by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
   184      (simp)
   185 
   186 lemma list_rel_empty:
   187   shows "list_rel R [] b \<Longrightarrow> length b = 0"
   188   by (induct b) (simp_all)
   189 
   190 lemma list_rel_len:
   191   shows "list_rel R a b \<Longrightarrow> length a = length b"
   192   apply (induct a arbitrary: b)
   193   apply (simp add: list_rel_empty)
   194   apply (case_tac b)
   195   apply simp_all
   196   done
   197 
   198 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   199 lemma foldl_rsp[quot_respect]:
   200   assumes q1: "Quotient R1 Abs1 Rep1"
   201   and     q2: "Quotient R2 Abs2 Rep2"
   202   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
   203   apply(auto)
   204   apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   205   apply simp
   206   apply (rule_tac x="xa" in spec)
   207   apply (rule_tac x="ya" in spec)
   208   apply (rule_tac xs="xb" and ys="yb" in list_induct2)
   209   apply (rule list_rel_len)
   210   apply (simp_all)
   211   done
   212 
   213 lemma foldr_rsp[quot_respect]:
   214   assumes q1: "Quotient R1 Abs1 Rep1"
   215   and     q2: "Quotient R2 Abs2 Rep2"
   216   shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
   217   apply auto
   218   apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
   219   apply simp
   220   apply (rule_tac xs="xa" and ys="ya" in list_induct2)
   221   apply (rule list_rel_len)
   222   apply (simp_all)
   223   done
   224 
   225 lemma list_rel_rsp:
   226   assumes r: "\<forall>x y. R x y \<longrightarrow> (\<forall>a b. R a b \<longrightarrow> S x a = T y b)"
   227   and l1: "list_rel R x y"
   228   and l2: "list_rel R a b"
   229   shows "list_rel S x a = list_rel T y b"
   230   proof -
   231     have a: "length y = length x" by (rule list_rel_len[OF l1, symmetric])
   232     have c: "length a = length b" by (rule list_rel_len[OF l2])
   233     show ?thesis proof (cases "length x = length a")
   234       case True
   235       have b: "length x = length a" by fact
   236       show ?thesis using a b c r l1 l2 proof (induct rule: list_induct4)
   237         case Nil
   238         show ?case using assms by simp
   239       next
   240         case (Cons h t)
   241         then show ?case by auto
   242       qed
   243     next
   244       case False
   245       have d: "length x \<noteq> length a" by fact
   246       then have e: "\<not>list_rel S x a" using list_rel_len by auto
   247       have "length y \<noteq> length b" using d a c by simp
   248       then have "\<not>list_rel T y b" using list_rel_len by auto
   249       then show ?thesis using e by simp
   250     qed
   251   qed
   252 
   253 lemma[quot_respect]:
   254   "((R ===> R ===> op =) ===> list_rel R ===> list_rel R ===> op =) list_rel list_rel"
   255   by (simp add: list_rel_rsp)
   256 
   257 lemma[quot_preserve]:
   258   assumes a: "Quotient R abs1 rep1"
   259   shows "((abs1 ---> abs1 ---> id) ---> map rep1 ---> map rep1 ---> id) list_rel = list_rel"
   260   apply (simp add: expand_fun_eq)
   261   apply clarify
   262   apply (induct_tac xa xb rule: list_induct2')
   263   apply (simp_all add: Quotient_abs_rep[OF a])
   264   done
   265 
   266 lemma[quot_preserve]:
   267   assumes a: "Quotient R abs1 rep1"
   268   shows "(list_rel ((rep1 ---> rep1 ---> id) R) l m) = (l = m)"
   269   by (induct l m rule: list_induct2') (simp_all add: Quotient_rel_rep[OF a])
   270 
   271 lemma list_rel_eq[id_simps]:
   272   shows "(list_rel (op =)) = (op =)"
   273   unfolding expand_fun_eq
   274   apply(rule allI)+
   275   apply(induct_tac x xa rule: list_induct2')
   276   apply(simp_all)
   277   done
   278 
   279 lemma list_rel_find_element:
   280   assumes a: "x \<in> set a"
   281   and b: "list_rel R a b"
   282   shows "\<exists>y. (y \<in> set b \<and> R x y)"
   283 proof -
   284   have "length a = length b" using b by (rule list_rel_len)
   285   then show ?thesis using a b by (induct a b rule: list_induct2) auto
   286 qed
   287 
   288 lemma list_rel_refl:
   289   assumes a: "\<And>x y. R x y = (R x = R y)"
   290   shows "list_rel R x x"
   291   by (induct x) (auto simp add: a)
   292 
   293 end