1.1 --- a/src/HOL/Tools/ctr_sugar.ML Thu Dec 05 13:38:20 2013 +0100
1.2 +++ b/src/HOL/Tools/ctr_sugar.ML Thu Dec 05 14:11:45 2013 +0100
1.3 @@ -448,6 +448,8 @@
1.4 let
1.5 fun disc_free b = Free (Binding.name_of b, mk_pred1T fcT);
1.6
1.7 + fun disc_spec b exist_xs_u_eq_ctr = mk_Trueprop_eq (disc_free b $ u, exist_xs_u_eq_ctr);
1.8 +
1.9 fun alternate_disc k =
1.10 Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
1.11
1.12 @@ -460,7 +462,7 @@
1.13 | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy)
1.14 | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
1.15
1.16 - fun sel_rhs b proto_sels =
1.17 + fun sel_spec b proto_sels =
1.18 let
1.19 val _ =
1.20 (case duplicates (op =) (map fst proto_sels) of
1.21 @@ -475,7 +477,8 @@
1.22 quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. "
1.23 ^ quote (Syntax.string_of_typ lthy T')));
1.24 in
1.25 - Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T)
1.26 + mk_Trueprop_eq (Free (Binding.name_of b, fcT --> T) $ u,
1.27 + Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u)
1.28 end;
1.29
1.30 val sel_bindings = flat sel_bindingss;
1.31 @@ -498,18 +501,18 @@
1.32 val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
1.33 lthy
1.34 |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
1.35 - let val rhs = Term.lambda u exist_xs_u_eq_ctr in
1.36 - if Binding.is_empty b then
1.37 - if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
1.38 - else pair (alternate_disc k, alternate_disc_no_def)
1.39 - else if Binding.eq_name (b, equal_binding) then
1.40 - pair (rhs, Thm.reflexive (certify lthy rhs))
1.41 - else
1.42 - Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), rhs)) #>> apsnd snd
1.43 - end) ks exist_xs_u_eq_ctrs disc_bindings
1.44 + if Binding.is_empty b then
1.45 + if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
1.46 + else pair (alternate_disc k, alternate_disc_no_def)
1.47 + else if Binding.eq_name (b, equal_binding) then
1.48 + pair (Term.lambda u exist_xs_u_eq_ctr, refl)
1.49 + else
1.50 + Specification.definition (SOME (b, NONE, NoSyn),
1.51 + ((Thm.def_binding b, []), disc_spec b exist_xs_u_eq_ctr)) #>> apsnd snd)
1.52 + ks exist_xs_u_eq_ctrs disc_bindings
1.53 ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
1.54 - Local_Theory.define ((b, NoSyn),
1.55 - ((Thm.def_binding b, []), sel_rhs b proto_sels)) #>> apsnd snd) sel_infos
1.56 + Specification.definition (SOME (b, NONE, NoSyn),
1.57 + ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_infos
1.58 ||> `Local_Theory.restore;
1.59
1.60 val phi = Proof_Context.export_morphism lthy lthy';
1.61 @@ -668,11 +671,9 @@
1.62 val vdiscs = map (rapp v) discs;
1.63 val vselss = map (map (rapp v)) selss;
1.64
1.65 - fun massage_dest_def def = def RS meta_eq_to_obj_eq RS fun_cong;
1.66 -
1.67 fun make_sel_thm xs' case_thm sel_def =
1.68 zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
1.69 - (Drule.forall_intr_vars (case_thm RS (massage_dest_def sel_def RS trans)))));
1.70 + (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
1.71
1.72 val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
1.73
1.74 @@ -706,7 +707,7 @@
1.75 nth exist_xs_u_eq_ctrs (k - 1));
1.76 in
1.77 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
1.78 - mk_alternate_disc_def_tac ctxt k (massage_dest_def (nth disc_defs (2 - k)))
1.79 + mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
1.80 (nth distinct_thms (2 - k)) uexhaust_thm)
1.81 |> Thm.close_derivation
1.82 |> singleton (Proof_Context.export names_lthy lthy)
1.83 @@ -719,7 +720,7 @@
1.84 map2 (fn k => fn def =>
1.85 if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
1.86 else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
1.87 - else massage_dest_def def) ks disc_defs;
1.88 + else def) ks disc_defs;
1.89
1.90 val discD_thms = map (fn def => def RS iffD1) disc_defs';
1.91 val discI_thms =