src/HOL/Codatatype/Tools/bnf_sugar.ML
changeset 49027 fc3b9b49c92d
parent 49025 7e89b0520e83
child 49028 487427a02bee
equal deleted inserted replaced
49026:72dcf53c1ee4 49027:fc3b9b49c92d
    19 val case_congN = "case_cong"
    19 val case_congN = "case_cong"
    20 val case_discsN = "case_discs"
    20 val case_discsN = "case_discs"
    21 val casesN = "cases"
    21 val casesN = "cases"
    22 val ctr_selsN = "ctr_sels"
    22 val ctr_selsN = "ctr_sels"
    23 val disc_disjointN = "disc_disjoint"
    23 val disc_disjointN = "disc_disjoint"
       
    24 val disc_exhaustN = "disc_exhaust"
       
    25 val discsN = "discs"
    24 val distinctN = "distinct"
    26 val distinctN = "distinct"
    25 val disc_exhaustN = "disc_exhaust"
       
    26 val selsN = "sels"
    27 val selsN = "sels"
    27 val splitN = "split"
    28 val splitN = "split"
    28 val split_asmN = "split_asm"
    29 val split_asmN = "split_asm"
    29 val weak_case_cong_thmsN = "weak_case_cong"
    30 val weak_case_cong_thmsN = "weak_case_cong"
       
    31 
       
    32 fun index_of_triangle_row _ 0 = 0
       
    33   | index_of_triangle_row n j = index_of_triangle_row n (j - 1) + n - j;
       
    34 
       
    35 fun index_of_triangle_cell n j k = index_of_triangle_row n j + k - (j + 1);
    30 
    36 
    31 fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy =
    37 fun prepare_sugar prep_term (((raw_ctrs, raw_caseof), disc_names), sel_namess) no_defs_lthy =
    32   let
    38   let
    33     (* TODO: sanity checks on arguments *)
    39     (* TODO: sanity checks on arguments *)
    34 
    40 
   192               map3 (mk_thm k xs goal_case case_thm) xs sels sel_defs;
   198               map3 (mk_thm k xs goal_case case_thm) xs sels sel_defs;
   193           in
   199           in
   194             flat (map6 mk_thms ks xss goal_cases case_thms selss sel_defss)
   200             flat (map6 mk_thms ks xss goal_cases case_thms selss sel_defss)
   195           end;
   201           end;
   196 
   202 
   197         val disc_thms = [];
   203         val disc_thms =
       
   204           let
       
   205             fun get_distinct_thm k k' =
       
   206               if k > k' then nth half_distinct_thms (index_of_triangle_cell n (k' - 1) (k - 1))
       
   207               else nth other_half_distinct_thms (index_of_triangle_cell n (k' - 1) (k' - 1))
       
   208             fun mk_thm ((k, m), disc_def) k' =
       
   209               if k = k' then
       
   210                 refl RS (funpow m (fn thm => exI RS thm) (disc_def RS iffD2))
       
   211               else
       
   212                 get_distinct_thm k k' RS (funpow m (fn thm => allI RS thm)
       
   213                   (Local_Defs.unfold lthy @{thms not_ex} (disc_def RS @{thm ssubst[of _ _ Not]})));
       
   214           in
       
   215             map_product mk_thm (ks ~~ map length ctr_Tss ~~ disc_defs) ks
       
   216           end;
   198 
   217 
   199         val disc_disjoint_thms = [];
   218         val disc_disjoint_thms = [];
   200 
   219 
   201         val disc_exhaust_thms = [];
   220         val disc_exhaust_thms = [];
   202 
   221 
   221         lthy
   240         lthy
   222         |> note case_congN [case_cong_thm]
   241         |> note case_congN [case_cong_thm]
   223         |> note case_discsN case_disc_thms
   242         |> note case_discsN case_disc_thms
   224         |> note casesN case_thms
   243         |> note casesN case_thms
   225         |> note ctr_selsN ctr_sel_thms
   244         |> note ctr_selsN ctr_sel_thms
       
   245         |> note discsN disc_thms
   226         |> note disc_disjointN disc_disjoint_thms
   246         |> note disc_disjointN disc_disjoint_thms
   227         |> note disc_exhaustN disc_exhaust_thms
   247         |> note disc_exhaustN disc_exhaust_thms
   228         |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
   248         |> note distinctN (half_distinct_thms @ other_half_distinct_thms)
   229         |> note exhaustN [exhaust_thm]
   249         |> note exhaustN [exhaust_thm]
   230         |> note injectN inject_thms
   250         |> note injectN inject_thms