src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
changeset 54972 5747fdd4ad3b
parent 54970 891141de5672
child 54973 b35859240103
equal deleted inserted replaced
54971:b4b828025880 54972:5747fdd4ad3b
   987     val nchotomy_goalss =
   987     val nchotomy_goalss =
   988       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
   988       map2 (fn false => K [] | true => single o HOLogic.mk_Trueprop o mk_dnf o map #prems)
   989         de_facto_exhaustives disc_eqnss
   989         de_facto_exhaustives disc_eqnss
   990       |> list_all_fun_args []
   990       |> list_all_fun_args []
   991     val nchotomy_taut_thmss =
   991     val nchotomy_taut_thmss =
   992       map3 (fn {disc_exhausts, ...} => fn false => K []
   992       map3 (fn {disc_exhausts, ...} => fn syntactic_exhaustive =>
   993           | true => map_prove_with_tac (fn {context = ctxt, ...} =>
   993           if syntactic_exhaustive then
   994               mk_primcorec_nchotomy_tac ctxt disc_exhausts))
   994             map_prove_with_tac (fn {context = ctxt, ...} =>
       
   995               mk_primcorec_nchotomy_tac ctxt disc_exhausts)
       
   996           else
       
   997             (case tac_opt of
       
   998               SOME tac => map_prove_with_tac tac
       
   999             | NONE => K []))
   995         corec_specs syntactic_exhaustives nchotomy_goalss;
  1000         corec_specs syntactic_exhaustives nchotomy_goalss;
   996     val goalss = goalss'
  1001     val goalss = goalss'
   997       |> (if is_none tac_opt then
  1002       |> (if is_none tac_opt then
   998           append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives
  1003           append (map2 (fn true => K [] | false => map (rpair [])) syntactic_exhaustives
   999             nchotomy_goalss)
  1004             nchotomy_goalss)
  1002 
  1007 
  1003     fun prove thmss'' def_thms' lthy =
  1008     fun prove thmss'' def_thms' lthy =
  1004       let
  1009       let
  1005         val def_thms = map (snd o snd) def_thms';
  1010         val def_thms = map (snd o snd) def_thms';
  1006 
  1011 
  1007         val nchotomy_thmss = nchotomy_taut_thmss
  1012         val (nchotomy_thmss, exclude_thmss) =
  1008           |> (if is_none tac_opt then map2 append (take actual_nn thmss'') else I);
  1013           if is_none tac_opt then
  1009         val exclude_thmss = thmss'' |> is_none tac_opt ? drop actual_nn;
  1014             (map2 append (take actual_nn thmss'') nchotomy_taut_thmss, drop actual_nn thmss'')
       
  1015           else
       
  1016             (nchotomy_taut_thmss, thmss'');
  1010 
  1017 
  1011         val ps =
  1018         val ps =
  1012           Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
  1019           Variable.variant_frees lthy (maps (maps #fun_args) disc_eqnss) [("P", HOLogic.boolT)];
  1013 
  1020 
  1014         val exhaust_thmss =
  1021         val exhaust_thmss =
  1327   |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
  1334   |> Seq.hd) ooo add_primcorec_ursive_cmd NONE;
  1328 
  1335 
  1329 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
  1336 val add_primcorec_cmd = (fn (goalss, after_qed, lthy) =>
  1330   lthy
  1337   lthy
  1331   |> after_qed (map (fn [] => []
  1338   |> after_qed (map (fn [] => []
  1332       | _ => primcorec_error "need exclusiveness proofs - use primcorecursive instead of primcorec")
  1339       | _ => error "\"auto\" failed -- use \"primcorecursive\" instead of \"primcorec\"")
  1333     goalss)) ooo add_primcorec_ursive_cmd (SOME (auto_tac o #context));
  1340     goalss)) ooo add_primcorec_ursive_cmd (SOME (auto_tac o #context));
  1334 
  1341 
  1335 end;
  1342 end;