1 (*  Title:      Quotient_List.thy

     2     Author:     Cezary Kaliszyk and Christian Urban

     3 *)

     4 theory Quotient_List

     5 imports Quotient Quotient_Syntax List

     6 begin

     7 

     8 section {* Quotient infrastructure for the list type. *}

     9 

    10 fun

    11   list_rel

    12 where

    13   "list_rel R [] [] = True"

    14 | "list_rel R (x#xs) [] = False"

    15 | "list_rel R [] (x#xs) = False"

    16 | "list_rel R (x#xs) (y#ys) = (R x y \<and> list_rel R xs ys)"

    17 

    18 declare [[map list = (map, list_rel)]]

    19 

    20 lemma split_list_all:

    21   shows "(\<forall>x. P x) \<longleftrightarrow> P [] \<and> (\<forall>x xs. P (x#xs))"

    22   apply(auto)

    23   apply(case_tac x)

    24   apply(simp_all)

    25   done

    26 

    27 lemma map_id[id_simps]:

    28   shows "map id = id"

    29   apply(simp add: expand_fun_eq)

    30   apply(rule allI)

    31   apply(induct_tac x)

    32   apply(simp_all)

    33   done

    34 

    35 

    36 lemma list_rel_reflp:

    37   shows "equivp R \<Longrightarrow> list_rel R xs xs"

    38   apply(induct xs)

    39   apply(simp_all add: equivp_reflp)

    40   done

    41 

    42 lemma list_rel_symp:

    43   assumes a: "equivp R"

    44   shows "list_rel R xs ys \<Longrightarrow> list_rel R ys xs"

    45   apply(induct xs ys rule: list_induct2')

    46   apply(simp_all)

    47   apply(rule equivp_symp[OF a])

    48   apply(simp)

    49   done

    50 

    51 lemma list_rel_transp:

    52   assumes a: "equivp R"

    53   shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"

    54   apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')

    55   apply(simp_all)

    56   apply(case_tac xs3)

    57   apply(simp_all)

    58   apply(rule equivp_transp[OF a])

    59   apply(auto)

    60   done

    61 

    62 lemma list_equivp[quot_equiv]:

    63   assumes a: "equivp R"

    64   shows "equivp (list_rel R)"

    65   apply(rule equivpI)

    66   unfolding reflp_def symp_def transp_def

    67   apply(subst split_list_all)

    68   apply(simp add: equivp_reflp[OF a] list_rel_reflp[OF a])

    69   apply(blast intro: list_rel_symp[OF a])

    70   apply(blast intro: list_rel_transp[OF a])

    71   done

    72 

    73 lemma list_rel_rel:

    74   assumes q: "Quotient R Abs Rep"

    75   shows "list_rel R r s = (list_rel R r r \<and> list_rel R s s \<and> (map Abs r = map Abs s))"

    76   apply(induct r s rule: list_induct2')

    77   apply(simp_all)

    78   using Quotient_rel[OF q]

    79   apply(metis)

    80   done

    81 

    82 lemma list_quotient[quot_thm]:

    83   assumes q: "Quotient R Abs Rep"

    84   shows "Quotient (list_rel R) (map Abs) (map Rep)"

    85   unfolding Quotient_def

    86   apply(subst split_list_all)

    87   apply(simp add: Quotient_abs_rep[OF q] abs_o_rep[OF q] map_id)

    88   apply(rule conjI)

    89   apply(rule allI)

    90   apply(induct_tac a)

    91   apply(simp)

    92   apply(simp)

    93   apply(simp add: Quotient_rep_reflp[OF q])

    94   apply(rule allI)+

    95   apply(rule list_rel_rel[OF q])

    96   done

    97 

    98 

    99 lemma cons_prs_aux:

   100   assumes q: "Quotient R Abs Rep"

   101   shows "(map Abs) ((Rep h) # (map Rep t)) = h # t"

   102   by (induct t) (simp_all add: Quotient_abs_rep[OF q])

   103 

   104 lemma cons_prs[quot_preserve]:

   105   assumes q: "Quotient R Abs Rep"

   106   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"

   107   by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])

   108      (simp)

   109 

   110 lemma cons_rsp[quot_respect]:

   111   assumes q: "Quotient R Abs Rep"

   112   shows "(R ===> list_rel R ===> list_rel R) (op #) (op #)"

   113   by (auto)

   114 

   115 lemma nil_prs[quot_preserve]:

   116   assumes q: "Quotient R Abs Rep"

   117   shows "map Abs [] = []"

   118   by simp

   119 

   120 lemma nil_rsp[quot_respect]:

   121   assumes q: "Quotient R Abs Rep"

   122   shows "list_rel R [] []"

   123   by simp

   124 

   125 lemma map_prs_aux:

   126   assumes a: "Quotient R1 abs1 rep1"

   127   and     b: "Quotient R2 abs2 rep2"

   128   shows "(map abs2) (map ((abs1 ---> rep2) f) (map rep1 l)) = map f l"

   129   by (induct l)

   130      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])

   131 

   132 

   133 lemma map_prs[quot_preserve]:

   134   assumes a: "Quotient R1 abs1 rep1"

   135   and     b: "Quotient R2 abs2 rep2"

   136   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"

   137   by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])

   138      (simp)

   139 

   140 

   141 lemma map_rsp[quot_respect]:

   142   assumes q1: "Quotient R1 Abs1 Rep1"

   143   and     q2: "Quotient R2 Abs2 Rep2"

   144   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"

   145   apply(simp)

   146   apply(rule allI)+

   147   apply(rule impI)

   148   apply(rule allI)+

   149   apply (induct_tac xa ya rule: list_induct2')

   150   apply simp_all

   151   done

   152 

   153 lemma foldr_prs_aux:

   154   assumes a: "Quotient R1 abs1 rep1"

   155   and     b: "Quotient R2 abs2 rep2"

   156   shows "abs2 (foldr ((abs1 ---> abs2 ---> rep2) f) (map rep1 l) (rep2 e)) = foldr f l e"

   157   by (induct l) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])

   158 

   159 lemma foldr_prs[quot_preserve]:

   160   assumes a: "Quotient R1 abs1 rep1"

   161   and     b: "Quotient R2 abs2 rep2"

   162   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"

   163   by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])

   164      (simp)

   165 

   166 lemma foldl_prs_aux:

   167   assumes a: "Quotient R1 abs1 rep1"

   168   and     b: "Quotient R2 abs2 rep2"

   169   shows "abs1 (foldl ((abs1 ---> abs2 ---> rep1) f) (rep1 e) (map rep2 l)) = foldl f e l"

   170   by (induct l arbitrary:e) (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])

   171 

   172 

   173 lemma foldl_prs[quot_preserve]:

   174   assumes a: "Quotient R1 abs1 rep1"

   175   and     b: "Quotient R2 abs2 rep2"

   176   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"

   177   by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])

   178      (simp)

   179 

   180 lemma list_rel_empty:

   181   shows "list_rel R [] b \<Longrightarrow> length b = 0"

   182   by (induct b) (simp_all)

   183 

   184 lemma list_rel_len:

   185   shows "list_rel R a b \<Longrightarrow> length a = length b"

   186   apply (induct a arbitrary: b)

   187   apply (simp add: list_rel_empty)

   188   apply (case_tac b)

   189   apply simp_all

   190   done

   191 

   192 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)

   193 lemma foldl_rsp[quot_respect]:

   194   assumes q1: "Quotient R1 Abs1 Rep1"

   195   and     q2: "Quotient R2 Abs2 Rep2"

   196   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"

   197   apply(auto)

   198   apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")

   199   apply simp

   200   apply (rule_tac x="xa" in spec)

   201   apply (rule_tac x="ya" in spec)

   202   apply (rule_tac xs="xb" and ys="yb" in list_induct2)

   203   apply (rule list_rel_len)

   204   apply (simp_all)

   205   done

   206 

   207 lemma foldr_rsp[quot_respect]:

   208   assumes q1: "Quotient R1 Abs1 Rep1"

   209   and     q2: "Quotient R2 Abs2 Rep2"

   210   shows "((R1 ===> R2 ===> R2) ===> list_rel R1 ===> R2 ===> R2) foldr foldr"

   211   apply auto

   212   apply(subgoal_tac "R2 xb yb \<longrightarrow> list_rel R1 xa ya \<longrightarrow> R2 (foldr x xa xb) (foldr y ya yb)")

   213   apply simp

   214   apply (rule_tac xs="xa" and ys="ya" in list_induct2)

   215   apply (rule list_rel_len)

   216   apply (simp_all)

   217   done

   218 

   219 lemma list_rel_eq[id_simps]:

   220   shows "(list_rel (op =)) = (op =)"

   221   unfolding expand_fun_eq

   222   apply(rule allI)+

   223   apply(induct_tac x xa rule: list_induct2')

   224   apply(simp_all)

   225   done

   226 

   227 lemma list_rel_refl:

   228   assumes a: "\<And>x y. R x y = (R x = R y)"

   229   shows "list_rel R x x"

   230   by (induct x) (auto simp add: a)

   231 

   232 end