src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
changeset 60781 2da59cdf531c
parent 60774 6c28d8ed2488
child 63239 d562c9948dee
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -46,21 +46,24 @@
     1.4            Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
     1.5              Var (("P", 0), HOLogic.boolT));
     1.6          val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
     1.7 -        val insts' = map (Thm.global_cterm_of thy) induct_Ps ~~ map (Thm.global_cterm_of thy) insts;
     1.8 -        val induct' =
     1.9 -          refl RS
    1.10 -            (nth (Old_Datatype_Aux.split_conj_thm (cterm_instantiate insts' induct)) i
    1.11 -             RSN (2, rev_mp));
    1.12        in
    1.13          Goal.prove_sorry_global thy []
    1.14            (Logic.strip_imp_prems t)
    1.15            (Logic.strip_imp_concl t)
    1.16            (fn {context = ctxt, prems, ...} =>
    1.17 -            EVERY
    1.18 -              [resolve_tac ctxt [induct'] 1,
    1.19 -               REPEAT (resolve_tac ctxt [TrueI] 1),
    1.20 -               REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
    1.21 -               REPEAT (resolve_tac ctxt [TrueI] 1)])
    1.22 +            let
    1.23 +              val insts' = map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts;
    1.24 +              val induct' =
    1.25 +                refl RS
    1.26 +                  (nth (Old_Datatype_Aux.split_conj_thm (infer_instantiate ctxt insts' induct)) i
    1.27 +                   RSN (2, rev_mp));
    1.28 +            in
    1.29 +              EVERY
    1.30 +                [resolve_tac ctxt [induct'] 1,
    1.31 +                 REPEAT (resolve_tac ctxt [TrueI] 1),
    1.32 +                 REPEAT ((resolve_tac ctxt [impI] 1) THEN (eresolve_tac ctxt prems 1)),
    1.33 +                 REPEAT (resolve_tac ctxt [TrueI] 1)]
    1.34 +            end)
    1.35        end;
    1.36  
    1.37      val casedist_thms =
    1.38 @@ -206,16 +209,19 @@
    1.39          val insts =
    1.40            map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
    1.41              ((1 upto length recTs) ~~ recTs ~~ rec_unique_ts);
    1.42 -        val induct' = induct
    1.43 -          |> cterm_instantiate
    1.44 -            (map (Thm.global_cterm_of thy1) induct_Ps ~~ map (Thm.global_cterm_of thy1) insts);
    1.45        in
    1.46          Old_Datatype_Aux.split_conj_thm (Goal.prove_sorry_global thy1 [] []
    1.47            (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
    1.48            (fn {context = ctxt, ...} =>
    1.49 -            #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
    1.50 -              (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
    1.51 -                  rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
    1.52 +            let
    1.53 +              val induct' =
    1.54 +                infer_instantiate ctxt
    1.55 +                  (map (#1 o dest_Var) induct_Ps ~~ map (Thm.cterm_of ctxt) insts) induct;
    1.56 +            in
    1.57 +              #1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
    1.58 +                (((resolve_tac ctxt [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
    1.59 +                    rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))
    1.60 +            end))
    1.61        end;
    1.62  
    1.63      val rec_total_thms = map (fn r => r RS @{thm theI'}) rec_unique_thms;
    1.64 @@ -380,15 +386,16 @@
    1.65      fun prove_split_thms ((((((t1, t2), inject), dist_rewrites'), exhaustion), case_thms'), T) =
    1.66        let
    1.67          val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (Thm.prems_of exhaustion)));
    1.68 +        val ctxt = Proof_Context.init_global thy;
    1.69          val exhaustion' = exhaustion
    1.70 -          |> cterm_instantiate [apply2 (Thm.global_cterm_of thy) (lhs, Free ("x", T))];
    1.71 -        fun tac ctxt =
    1.72 +          |> infer_instantiate ctxt [(#1 (dest_Var lhs), Thm.cterm_of ctxt (Free ("x", T)))];
    1.73 +        val tac =
    1.74            EVERY [resolve_tac ctxt [exhaustion'] 1,
    1.75              ALLGOALS (asm_simp_tac
    1.76                (put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
    1.77        in
    1.78 -        (Goal.prove_sorry_global thy [] [] t1 (tac o #context),
    1.79 -         Goal.prove_sorry_global thy [] [] t2 (tac o #context))
    1.80 +        (Goal.prove_sorry_global thy [] [] t1 (K tac),
    1.81 +         Goal.prove_sorry_global thy [] [] t2 (K tac))
    1.82        end;
    1.83  
    1.84      val split_thm_pairs =
    1.85 @@ -451,13 +458,13 @@
    1.86          val Const (@{const_name Pure.imp}, _) $ tm $ _ = t;
    1.87          val Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ Ma) = tm;
    1.88          val nchotomy' = nchotomy RS spec;
    1.89 -        val [v] = Term.add_vars (Thm.concl_of nchotomy') [];
    1.90 -        val nchotomy'' =
    1.91 -          cterm_instantiate [apply2 (Thm.global_cterm_of thy) (Var v, Ma)] nchotomy';
    1.92 +        val [v] = Term.add_var_names (Thm.concl_of nchotomy') [];
    1.93        in
    1.94          Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    1.95            (fn {context = ctxt, prems, ...} =>
    1.96              let
    1.97 +              val nchotomy'' =
    1.98 +                infer_instantiate ctxt [(v, Thm.cterm_of ctxt Ma)] nchotomy';
    1.99                val simplify = asm_simp_tac (put_simpset HOL_ss ctxt addsimps (prems @ case_rewrites))
   1.100              in
   1.101                EVERY [