src/HOL/Codatatype/Tools/bnf_wrap.ML
changeset 49118 b815fa776b91
parent 49117 000deee4913e
child 49119 1f605c36869c
equal deleted inserted replaced
49117:000deee4913e 49118:b815fa776b91
    23   | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l;
    23   | mk_un_N _ l suf = un_N ^ suf ^ string_of_int l;
    24 
    24 
    25 val case_congN = "case_cong";
    25 val case_congN = "case_cong";
    26 val case_eqN = "case_eq";
    26 val case_eqN = "case_eq";
    27 val casesN = "cases";
    27 val casesN = "cases";
    28 val ctr_selsN = "ctr_sels";
    28 val collapseN = "collapse";
    29 val disc_exclusN = "disc_exclus";
    29 val disc_exclusN = "disc_exclus";
    30 val disc_exhaustN = "disc_exhaust";
    30 val disc_exhaustN = "disc_exhaust";
    31 val discsN = "discs";
    31 val discsN = "discs";
    32 val distinctN = "distinct";
    32 val distinctN = "distinct";
    33 val exhaustN = "exhaust";
    33 val exhaustN = "exhaust";
   348             in
   348             in
   349               [Skip_Proof.prove lthy [] [] goal (fn _ =>
   349               [Skip_Proof.prove lthy [] [] goal (fn _ =>
   350                  mk_disc_exhaust_tac n exhaust_thm discI_thms)]
   350                  mk_disc_exhaust_tac n exhaust_thm discI_thms)]
   351             end;
   351             end;
   352 
   352 
   353         val ctr_sel_thms =
   353         val collapse_thms =
   354           let
   354           let
   355             fun mk_goal ctr disc sels =
   355             fun mk_goal ctr disc sels =
   356               let
   356               let
   357                 val prem = HOLogic.mk_Trueprop (betapply (disc, v));
   357                 val prem = HOLogic.mk_Trueprop (betapply (disc, v));
   358                 val concl =
   358                 val concl =
   364               end;
   364               end;
   365             val goals = map3 mk_goal ctrs discs selss;
   365             val goals = map3 mk_goal ctrs discs selss;
   366           in
   366           in
   367             map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
   367             map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
   368               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   368               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   369                 mk_ctr_sel_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
   369                 mk_collapse_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
   370             |> map_filter I
   370             |> map_filter I
   371           end;
   371           end;
   372 
   372 
   373         val case_eq_thm =
   373         val case_eq_thm =
   374           let
   374           let
   435 
   435 
   436         val notes =
   436         val notes =
   437           [(case_congN, [case_cong_thm]),
   437           [(case_congN, [case_cong_thm]),
   438            (case_eqN, [case_eq_thm]),
   438            (case_eqN, [case_eq_thm]),
   439            (casesN, case_thms),
   439            (casesN, case_thms),
   440            (ctr_selsN, ctr_sel_thms),
   440            (collapseN, collapse_thms),
   441            (discsN, disc_thms),
   441            (discsN, disc_thms),
   442            (disc_exclusN, disc_exclus_thms),
   442            (disc_exclusN, disc_exclus_thms),
   443            (disc_exhaustN, disc_exhaust_thms),
   443            (disc_exhaustN, disc_exhaust_thms),
   444            (distinctN, distinct_thms),
   444            (distinctN, distinct_thms),
   445            (exhaustN, [exhaust_thm]),
   445            (exhaustN, [exhaust_thm]),