src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 51551 88d1d19fb74f
parent 51380 cac8c9a636b6
child 51745 a06a3c777add
equal deleted inserted replaced
51550:cec08df2c030 51551:88d1d19fb74f
   472                   let
   472                   let
   473                     val goal =
   473                     val goal =
   474                       fold_rev Logic.all [w, u]
   474                       fold_rev Logic.all [w, u]
   475                         (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
   475                         (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
   476                   in
   476                   in
   477                     Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   477                     Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   478                       mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
   478                       mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
   479                         (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
   479                         (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
   480                     |> Thm.close_derivation
   480                     |> Thm.close_derivation
   481                     |> Morphism.thm phi
   481                     |> Morphism.thm phi
   482                   end;
   482                   end;
   799             val kksss = map (map (map (fst o snd) o #2)) raw_premss;
   799             val kksss = map (map (map (fst o snd) o #2)) raw_premss;
   800 
   800 
   801             val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
   801             val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
   802 
   802 
   803             val thm =
   803             val thm =
   804               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   804               Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   805                 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
   805                 mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
   806                   nested_set_natural's pre_set_defss)
   806                   nested_set_natural's pre_set_defss)
   807               |> singleton (Proof_Context.export names_lthy lthy)
   807               |> singleton (Proof_Context.export names_lthy lthy)
   808               |> Thm.close_derivation;
   808               |> Thm.close_derivation;
   809           in
   809           in
   850             val rec_tacss =
   850             val rec_tacss =
   851               map2 (map o mk_rec_like_tac pre_map_defs nested_map_comp's
   851               map2 (map o mk_rec_like_tac pre_map_defs nested_map_comp's
   852                 (nested_map_ids'' @ nesting_map_ids'') rec_defs) fp_rec_thms ctr_defss;
   852                 (nested_map_ids'' @ nesting_map_ids'') rec_defs) fp_rec_thms ctr_defss;
   853 
   853 
   854             fun prove goal tac =
   854             fun prove goal tac =
   855               Skip_Proof.prove lthy [] [] goal (tac o #context)
   855               Goal.prove_sorry lthy [] [] goal (tac o #context)
   856               |> Thm.close_derivation;
   856               |> Thm.close_derivation;
   857           in
   857           in
   858             (map2 (map2 prove) fold_goalss fold_tacss, map2 (map2 prove) rec_goalss rec_tacss)
   858             (map2 (map2 prove) fold_goalss fold_tacss, map2 (map2 prove) rec_goalss rec_tacss)
   859           end;
   859           end;
   860 
   860 
   953 
   953 
   954             val goal = mk_goal rs;
   954             val goal = mk_goal rs;
   955             val strong_goal = mk_goal strong_rs;
   955             val strong_goal = mk_goal strong_rs;
   956 
   956 
   957             fun prove dtor_coinduct' goal =
   957             fun prove dtor_coinduct' goal =
   958               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
   958               Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   959                 mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
   959                 mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
   960                   exhaust_thms ctr_defss disc_thmsss sel_thmsss)
   960                   exhaust_thms ctr_defss disc_thmsss sel_thmsss)
   961               |> singleton (Proof_Context.export names_lthy lthy)
   961               |> singleton (Proof_Context.export names_lthy lthy)
   962               |> Thm.close_derivation;
   962               |> Thm.close_derivation;
   963 
   963 
  1030               map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
  1030               map3 (map oo mk_corec_like_tac corec_defs nested_map_comps'' nested_map_comp's
  1031                   (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
  1031                   (nested_map_ids'' @ nesting_map_ids'') nested_map_if_distribs)
  1032                 fp_rec_thms pre_map_defs ctr_defss;
  1032                 fp_rec_thms pre_map_defs ctr_defss;
  1033 
  1033 
  1034             fun prove goal tac =
  1034             fun prove goal tac =
  1035               Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation;
  1035               Goal.prove_sorry lthy [] [] goal (tac o #context) |> Thm.close_derivation;
  1036 
  1036 
  1037             val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
  1037             val unfold_thmss = map2 (map2 prove) unfold_goalss unfold_tacss;
  1038             val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
  1038             val corec_thmss = map2 (map2 prove) corec_goalss corec_tacss;
  1039 
  1039 
  1040             val filter_safesss =
  1040             val filter_safesss =
  1066               map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
  1066               map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' unfold_thmss disc_thmsss;
  1067             val corec_tacss =
  1067             val corec_tacss =
  1068               map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
  1068               map3 (map oo mk_disc_corec_like_iff_tac) case_splitss' corec_thmss disc_thmsss;
  1069 
  1069 
  1070             fun prove goal tac =
  1070             fun prove goal tac =
  1071               Skip_Proof.prove lthy [] [] goal (tac o #context)
  1071               Goal.prove_sorry lthy [] [] goal (tac o #context)
  1072               |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
  1072               |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
  1073               |> Thm.close_derivation;
  1073               |> Thm.close_derivation;
  1074 
  1074 
  1075             fun proves [_] [_] = []
  1075             fun proves [_] [_] = []
  1076               | proves goals tacs = map2 prove goals tacs;
  1076               | proves goals tacs = map2 prove goals tacs;