src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55409 b74248961819
parent 55407 81f7e60755c3
child 55410 54b09e82b9e1
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -359,8 +359,10 @@
     1.4  
     1.5      val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss;
     1.6  
     1.7 -    val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |>
     1.8 -      mk_Freess' "x" ctr_Tss
     1.9 +    val (((((((([exh_y], (xss, xss')), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) =
    1.10 +      no_defs_lthy
    1.11 +      |> mk_Frees "y" [fcT] (* for compatibility with "datatype_realizer.ML" *)
    1.12 +      ||>> mk_Freess' "x" ctr_Tss
    1.13        ||>> mk_Freess "y" ctr_Tss
    1.14        ||>> mk_Frees "f" case_Ts
    1.15        ||>> mk_Frees "g" case_Ts
    1.16 @@ -529,8 +531,8 @@
    1.17      fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
    1.18  
    1.19      val exhaust_goal =
    1.20 -      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (u, xctr)]) in
    1.21 -        fold_rev Logic.all [p, u] (mk_imp_p (map2 mk_prem xctrs xss))
    1.22 +      let fun mk_prem xctr xs = fold_rev Logic.all xs (mk_imp_p [mk_Trueprop_eq (exh_y, xctr)]) in
    1.23 +        fold_rev Logic.all [p, exh_y] (mk_imp_p (map2 mk_prem xctrs xss))
    1.24        end;
    1.25  
    1.26      val inject_goalss =
    1.27 @@ -556,7 +558,10 @@
    1.28  
    1.29      fun after_qed thmss lthy =
    1.30        let
    1.31 -        val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    1.32 +        val ([exhaust_thm0], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss));
    1.33 +        (* for "datatype_realizer.ML": *)
    1.34 +        val exhaust_thm =
    1.35 +          Thm.name_derivation (fcT_name ^ Long_Name.separator ^ exhaustN) exhaust_thm0;
    1.36  
    1.37          val inject_thms = flat inject_thmss;
    1.38  
    1.39 @@ -611,7 +616,8 @@
    1.40            in
    1.41              (Goal.prove_sorry lthy [] [] goal (fn _ => mk_case_cong_tac lthy uexhaust_thm case_thms),
    1.42               Goal.prove_sorry lthy [] [] weak_goal (K (etac arg_cong 1)))
    1.43 -            |> pairself (Thm.close_derivation #> singleton (Proof_Context.export names_lthy lthy))
    1.44 +            |> pairself (singleton (Proof_Context.export names_lthy lthy) #>
    1.45 +              Thm.close_derivation)
    1.46            end;
    1.47  
    1.48          val split_lhs = q $ ufcase;
    1.49 @@ -632,14 +638,14 @@
    1.50          fun prove_split selss goal =
    1.51            Goal.prove_sorry lthy [] [] goal (fn _ =>
    1.52              mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
    1.53 -          |> Thm.close_derivation
    1.54 -          |> singleton (Proof_Context.export names_lthy lthy);
    1.55 +          |> singleton (Proof_Context.export names_lthy lthy)
    1.56 +          |> Thm.close_derivation;
    1.57  
    1.58          fun prove_split_asm asm_goal split_thm =
    1.59            Goal.prove_sorry lthy [] [] asm_goal (fn {context = ctxt, ...} =>
    1.60              mk_split_asm_tac ctxt split_thm)
    1.61 -          |> Thm.close_derivation
    1.62 -          |> singleton (Proof_Context.export names_lthy lthy);
    1.63 +          |> singleton (Proof_Context.export names_lthy lthy)
    1.64 +          |> Thm.close_derivation;
    1.65  
    1.66          val (split_thm, split_asm_thm) =
    1.67            let
    1.68 @@ -693,8 +699,8 @@
    1.69                    val goal = mk_Trueprop_eq (mk_uu_eq (), the_single exist_xs_u_eq_ctrs);
    1.70                  in
    1.71                    Goal.prove_sorry lthy [] [] goal (fn _ => mk_unique_disc_def_tac m uexhaust_thm)
    1.72 +                  |> singleton (Proof_Context.export names_lthy lthy)
    1.73                    |> Thm.close_derivation
    1.74 -                  |> singleton (Proof_Context.export names_lthy lthy)
    1.75                  end;
    1.76  
    1.77                fun mk_alternate_disc_def k =
    1.78 @@ -706,8 +712,8 @@
    1.79                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
    1.80                      mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
    1.81                        (nth distinct_thms (2 - k)) uexhaust_thm)
    1.82 +                  |> singleton (Proof_Context.export names_lthy lthy)
    1.83                    |> Thm.close_derivation
    1.84 -                  |> singleton (Proof_Context.export names_lthy lthy)
    1.85                  end;
    1.86  
    1.87                val has_alternate_disc_def =
    1.88 @@ -843,8 +849,8 @@
    1.89                      mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
    1.90                        (inst_thm v disc_exhaust_thm) uncollapse_thms disc_exclude_thmsss
    1.91                        disc_exclude_thmsss')
    1.92 +                  |> singleton (Proof_Context.export names_lthy lthy)
    1.93                    |> Thm.close_derivation
    1.94 -                  |> singleton (Proof_Context.export names_lthy lthy)
    1.95                  end;
    1.96  
    1.97                val (sel_split_thm, sel_split_asm_thm) =
    1.98 @@ -865,8 +871,8 @@
    1.99                  in
   1.100                    Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   1.101                      mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss)
   1.102 +                  |> singleton (Proof_Context.export names_lthy lthy)
   1.103                    |> Thm.close_derivation
   1.104 -                  |> singleton (Proof_Context.export names_lthy lthy)
   1.105                  end;
   1.106              in
   1.107                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,