src/HOL/Tools/inductive_realizer.ML
changeset 26481 92e901171cc8
parent 26477 ecf06644f6cb
child 26535 66bca8a4079c
equal deleted inserted replaced
26480:544cef16045b 26481:92e901171cc8
   394           [rtac (#raw_induct ind_info) 1,
   394           [rtac (#raw_induct ind_info) 1,
   395            rewrite_goals_tac rews,
   395            rewrite_goals_tac rews,
   396            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   396            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
   397              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
   397              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
   398               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   398               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   399         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   399         val (thm', thy') = PureThy.store_thm (space_implode "_"
   400           (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
   400           (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"]), thm) thy;
   401              ["correctness"]), thm), []) thy;
       
   402         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   401         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
   403           (DatatypeAux.split_conj_thm thm');
   402           (DatatypeAux.split_conj_thm thm');
   404         val ([thms'], thy'') = PureThy.add_thmss
   403         val ([thms'], thy'') = PureThy.add_thmss
   405           [((space_implode "_"
   404           [((space_implode "_"
   406              (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
   405              (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
   455            etac elimR 1,
   454            etac elimR 1,
   456            ALLGOALS (asm_simp_tac HOL_basic_ss),
   455            ALLGOALS (asm_simp_tac HOL_basic_ss),
   457            rewrite_goals_tac rews,
   456            rewrite_goals_tac rews,
   458            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
   457            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
   459              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   458              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   460         val (thm', thy') = PureThy.store_thm ((space_implode "_"
   459         val (thm', thy') = PureThy.store_thm (space_implode "_"
   461           (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
   460           (name_of_thm elim :: vs @ Ps @ ["correctness"]), thm) thy
   462       in
   461       in
   463         Extraction.add_realizers_i
   462         Extraction.add_realizers_i
   464           [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
   463           [mk_realizer thy' (vs @ Ps) (name_of_thm elim, elim, thm', rlz, r)] thy'
   465       end;
   464       end;
   466 
   465