src/HOL/Library/Quotient_List.thy
author wenzelm
Sun Mar 14 14:31:24 2010 +0100 (2010-03-14)
changeset 35788 f1deaca15ca3
parent 35222 4f1fba00f66d
child 36154 11c6106d7787
permissions -rw-r--r--
observe standard header format;
     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   apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
    56   apply(simp_all)
    57   apply(case_tac xs3)
    58   apply(simp_all)
    59   apply(rule equivp_transp[OF a])
    60   apply(auto)
    61   done
    62 
    63 lemma list_equivp[quot_equiv]:
    64   assumes a: "equivp R"
    65   shows "equivp (list_rel R)"
    66   apply(rule equivpI)
    67   unfolding reflp_def symp_def transp_def
    68   apply(subst split_list_all)
    69   apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])
    70   apply(blast intro: list_rel_symp[OF a])
    71   apply(blast intro: list_rel_transp[OF a])
    72   done
    73 
    74 lemma list_rel_rel:
    75   assumes q: "Quotient R Abs Rep"
    76   shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"
    77   apply(induct r s rule: list_induct2')
    78   apply(simp_all)
    79   using Quotient_rel[OF q]
    80   apply(metis)
    81   done
    82 
    83 lemma list_quotient[quot_thm]:
    84   assumes q: "Quotient R Abs Rep"
    85   shows "Quotient (list_rel R) (map Abs) (map Rep)"
    86   unfolding Quotient_def
    87   apply(subst split_list_all)
    88   apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)
    89   apply(rule conjI)
    90   apply(rule allI)
    91   apply(induct_tac a)
    92   apply(simp)
    93   apply(simp)
    94   apply(simp add: Quotient_rep_reflp[OF q])
    95   apply(rule allI)+
    96   apply(rule list_rel_rel[OF q])
    97   done
    98 
    99 
   100 lemma cons_prs_aux:
   101   assumes q: "Quotient R Abs Rep"
   102   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"
   103   by (induct t) (simp_all add: Quotient_abs_rep[OF q])
   104 
   105 lemma cons_prs[quot_preserve]:
   106   assumes q: "Quotient R Abs Rep"
   107   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
   108   by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
   109      (simp)
   110 
   111 lemma cons_rsp[quot_respect]:
   112   assumes q: "Quotient R Abs Rep"
   113   shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"
   114   by (auto)
   115 
   116 lemma nil_prs[quot_preserve]:
   117   assumes q: "Quotient R Abs Rep"
   118   shows "map Abs [] = []"
   119   by simp
   120 
   121 lemma nil_rsp[quot_respect]:
   122   assumes q: "Quotient R Abs Rep"
   123   shows "list_rel R [] []"
   124   by simp
   125 
   126 lemma map_prs_aux:
   127   assumes a: "Quotient R1 abs1 rep1"
   128   and     b: "Quotient R2 abs2 rep2"
   129   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"
   130   by (induct l)
   131      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   132 
   133 
   134 lemma map_prs[quot_preserve]:
   135   assumes a: "Quotient R1 abs1 rep1"
   136   and     b: "Quotient R2 abs2 rep2"
   137   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
   138   by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
   139      (simp)
   140 
   141 
   142 lemma map_rsp[quot_respect]:
   143   assumes q1: "Quotient R1 Abs1 Rep1"
   144   and     q2: "Quotient R2 Abs2 Rep2"
   145   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
   146   apply(simp)
   147   apply(rule allI)+
   148   apply(rule impI)
   149   apply(rule allI)+
   150   apply (induct_tac xa ya rule: list_induct2')
   151   apply simp_all
   152   done
   153 
   154 lemma foldr_prs_aux:
   155   assumes a: "Quotient R1 abs1 rep1"
   156   and     b: "Quotient R2 abs2 rep2"
   157   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"
   158   by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   159 
   160 lemma foldr_prs[quot_preserve]:
   161   assumes a: "Quotient R1 abs1 rep1"
   162   and     b: "Quotient R2 abs2 rep2"
   163   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
   164   by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
   165      (simp)
   166 
   167 lemma foldl_prs_aux:
   168   assumes a: "Quotient R1 abs1 rep1"
   169   and     b: "Quotient R2 abs2 rep2"
   170   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"
   171   by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
   172 
   173 
   174 lemma foldl_prs[quot_preserve]:
   175   assumes a: "Quotient R1 abs1 rep1"
   176   and     b: "Quotient R2 abs2 rep2"
   177   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
   178   by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
   179      (simp)
   180 
   181 lemma list_rel_empty:
   182   shows "list_rel R [] b \<Longrightarrow> length b = 0"
   183   by (induct b) (simp_all)
   184 
   185 lemma list_rel_len:
   186   shows "list_rel R a b \<Longrightarrow> length a = length b"
   187   apply (induct a arbitrary: b)
   188   apply (simp add: list_rel_empty)
   189   apply (case_tac b)
   190   apply simp_all
   191   done
   192 
   193 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   194 lemma foldl_rsp[quot_respect]:
   195   assumes q1: "Quotient R1 Abs1 Rep1"
   196   and     q2: "Quotient R2 Abs2 Rep2"
   197   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
   198   apply(auto)
   199   apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   200   apply simp
   201   apply (rule_tac x="xa" in spec)
   202   apply (rule_tac x="ya" in spec)
   203   apply (rule_tac xs="xb" and ys="yb" in list_induct2)
   204   apply (rule list_rel_len)
   205   apply (simp_all)
   206   done
   207 
   208 lemma foldr_rsp[quot_respect]:
   209   assumes q1: "Quotient R1 Abs1 Rep1"
   210   and     q2: "Quotient R2 Abs2 Rep2"
   211   shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"
   212   apply auto
   213   apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")
   214   apply simp
   215   apply (rule_tac xs="xa" and ys="ya" in list_induct2)
   216   apply (rule list_rel_len)
   217   apply (simp_all)
   218   done
   219 
   220 lemma list_rel_eq[id_simps]:
   221   shows "(list_rel (op =)) = (op =)"
   222   unfolding expand_fun_eq
   223   apply(rule allI)+
   224   apply(induct_tac x xa rule: list_induct2')
   225   apply(simp_all)
   226   done
   227 
   228 lemma list_rel_refl:
   229   assumes a: "\<And>x y. R x y = (R x = R y)"
   230   shows "list_rel R x x"
   231   by (induct x) (auto simp add: a)
   232 
   233 end