src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML
changeset 61424 c3658c18b7bc
parent 61268 abe08fb15a12
child 62121 c8a93680b80d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -35,7 +35,7 @@
     1.4  
     1.5  val HOL_basic_ss' =
     1.6    simpset_of (put_simpset HOL_basic_ss @{context}
     1.7 -    addsimps @{thms simp_thms Pair_eq}
     1.8 +    addsimps @{thms simp_thms prod.inject}
     1.9      setSolver (mk_solver "all_tac_solver" (fn _ => fn _ => all_tac))
    1.10      setSolver (mk_solver "True_solver" (fn ctxt => resolve_tac ctxt @{thms TrueI})))
    1.11  
    1.12 @@ -62,8 +62,8 @@
    1.13        (case f of
    1.14          Const (name, _) => simp_tac (put_simpset HOL_basic_ss ctxt addsimps
    1.15             [@{thm eval_pred}, Core_Data.predfun_definition_of ctxt name mode,
    1.16 -           @{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
    1.17 -           @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
    1.18 +           @{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
    1.19 +           @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
    1.20        | Free _ =>
    1.21          Subgoal.FOCUS_PREMS (fn {context = ctxt', prems, ...} =>
    1.22            let
    1.23 @@ -232,8 +232,8 @@
    1.24                in
    1.25                  trace_tac ctxt options "before prove_neg_expr:"
    1.26                  THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps
    1.27 -                  [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
    1.28 -                   @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
    1.29 +                  [@{thm case_prod_eta}, @{thm case_prod_beta}, @{thm fst_conv},
    1.30 +                   @{thm snd_conv}, @{thm prod.collapse}, @{thm Product_Type.split_conv}]) 1
    1.31                  THEN (if (is_some name) then
    1.32                      trace_tac ctxt options "before applying not introduction rule"
    1.33                      THEN Subgoal.FOCUS_PREMS (fn {prems, ...} =>
    1.34 @@ -392,8 +392,8 @@
    1.35      val (in_ts, _) = split_mode mode ts;
    1.36      val split_simpset =
    1.37        put_simpset HOL_basic_ss' ctxt
    1.38 -      addsimps [@{thm split_eta}, @{thm split_beta},
    1.39 -        @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}]
    1.40 +      addsimps [@{thm case_prod_eta}, @{thm case_prod_beta},
    1.41 +        @{thm fst_conv}, @{thm snd_conv}, @{thm prod.collapse}]
    1.42      fun prove_prems2 out_ts [] =
    1.43        trace_tac ctxt options "before prove_match2 - last call:"
    1.44        THEN prove_match2 options ctxt out_ts