src/HOL/Tools/datatype_realizer.ML
changeset 16123 1381e90c2694
parent 15574 b1d1b5bfc464
child 17521 0f1c48de39f5
equal deleted inserted replaced
16122:864fda4a4056 16123:1381e90c2694
   126           ALLGOALS ObjectLogic.atomize_tac,
   126           ALLGOALS ObjectLogic.atomize_tac,
   127           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
   127           rewrite_goals_tac (o_def :: map mk_meta_eq rec_rewrites),
   128           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   128           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   129             REPEAT (etac allE i) THEN atac i)) 1)]);
   129             REPEAT (etac allE i) THEN atac i)) 1)]);
   130 
   130 
   131     val {path, ...} = Sign.rep_sg sg;
       
   132     val ind_name = Thm.name_of_thm induction;
   131     val ind_name = Thm.name_of_thm induction;
   133     val vs = map (fn i => List.nth (pnames, i)) is;
   132     val vs = map (fn i => List.nth (pnames, i)) is;
   134     val (thy', thm') = thy
   133     val (thy', thm') = thy
   135       |> Theory.absolute_path
   134       |> Theory.absolute_path
   136       |> PureThy.store_thm
   135       |> PureThy.store_thm
   137         ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
   136         ((space_implode "_" (ind_name :: vs @ ["correctness"]), thm), [])
   138       |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
   137       |>> Theory.restore_naming thy;
   139 
   138 
   140     val ivs = Drule.vars_of_terms
   139     val ivs = Drule.vars_of_terms
   141       [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
   140       [Logic.varify (DatatypeProp.make_ind [descr] sorts)];
   142     val rvs = Drule.vars_of_terms [prop_of thm'];
   141     val rvs = Drule.vars_of_terms [prop_of thm'];
   143     val ivs1 = map Var (filter_out (fn (_, T) =>
   142     val ivs1 = map Var (filter_out (fn (_, T) =>
   198          [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
   197          [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1,
   199           ALLGOALS (EVERY'
   198           ALLGOALS (EVERY'
   200             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
   199             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
   201              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
   200              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
   202 
   201 
   203     val {path, ...} = Sign.rep_sg sg;
       
   204     val exh_name = Thm.name_of_thm exhaustion;
   202     val exh_name = Thm.name_of_thm exhaustion;
   205     val (thy', thm') = thy
   203     val (thy', thm') = thy
   206       |> Theory.absolute_path
   204       |> Theory.absolute_path
   207       |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
   205       |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])
   208       |>> Theory.add_path (NameSpace.pack (getOpt (path,[])));
   206       |>> Theory.restore_naming thy;
   209 
   207 
   210     val P = Var (("P", 0), rT' --> HOLogic.boolT);
   208     val P = Var (("P", 0), rT' --> HOLogic.boolT);
   211     val prf = forall_intr_prf (y, forall_intr_prf (P,
   209     val prf = forall_intr_prf (y, forall_intr_prf (P,
   212       foldr (fn ((p, r), prf) =>
   210       foldr (fn ((p, r), prf) =>
   213         forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),
   211         forall_intr_prf (Logic.varify r, AbsP ("H", SOME (Logic.varify p),