src/Tools/induct.ML
changeset 25109 dfa8001e6264
parent 24920 2a45e400fdad
child 25959 9ad285dbc7a4
equal deleted inserted replaced
25108:ca5708210cb8 25109:dfa8001e6264
   306 (* make_cases *)
   306 (* make_cases *)
   307 
   307 
   308 fun make_cases is_open rule =
   308 fun make_cases is_open rule =
   309   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
   309   RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
   310 
   310 
   311 fun warn_open true = legacy_feature "open rule cases in proof method"
   311 fun warn_open ctxt true =
   312   | warn_open false = ();
   312       legacy_feature ("open rule cases in proof method" ^ ContextPosition.str_of ctxt)
       
   313   | warn_open _ false = ();
   313 
   314 
   314 
   315 
   315 
   316 
   316 (** cases method **)
   317 (** cases method **)
   317 
   318 
   333 
   334 
   334 in
   335 in
   335 
   336 
   336 fun cases_tac ctxt is_open insts opt_rule facts =
   337 fun cases_tac ctxt is_open insts opt_rule facts =
   337   let
   338   let
   338     val _ = warn_open is_open;
   339     val _ = warn_open ctxt is_open;
   339     val thy = ProofContext.theory_of ctxt;
   340     val thy = ProofContext.theory_of ctxt;
   340     val cert = Thm.cterm_of thy;
   341     val cert = Thm.cterm_of thy;
   341 
   342 
   342     fun inst_rule r =
   343     fun inst_rule r =
   343       if null insts then `RuleCases.get r
   344       if null insts then `RuleCases.get r
   572 
   573 
   573 in
   574 in
   574 
   575 
   575 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   576 fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
   576   let
   577   let
   577     val _ = warn_open is_open;
   578     val _ = warn_open ctxt is_open;
   578     val thy = ProofContext.theory_of ctxt;
   579     val thy = ProofContext.theory_of ctxt;
   579     val cert = Thm.cterm_of thy;
   580     val cert = Thm.cterm_of thy;
   580 
   581 
   581     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   582     val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
   582     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   583     val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs;
   648 
   649 
   649 in
   650 in
   650 
   651 
   651 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   652 fun coinduct_tac ctxt is_open inst taking opt_rule facts =
   652   let
   653   let
   653     val _ = warn_open is_open;
   654     val _ = warn_open ctxt is_open;
   654     val thy = ProofContext.theory_of ctxt;
   655     val thy = ProofContext.theory_of ctxt;
   655     val cert = Thm.cterm_of thy;
   656     val cert = Thm.cterm_of thy;
   656 
   657 
   657     fun inst_rule r =
   658     fun inst_rule r =
   658       if null inst then `RuleCases.get r
   659       if null inst then `RuleCases.get r