# HG changeset patch # User blanchet # Date 1376313917 -7200 # Node ID 2b430bbb5a1af34bf7326f4090ce29a06801951d # Parent 5e25877c51d4500f6b1327b1fbae71e5a28f635b define case constant from other 'free constructor' axioms diff -r 5e25877c51d4 -r 2b430bbb5a1a src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Aug 12 15:25:16 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Aug 12 15:25:17 2013 +0200 @@ -39,7 +39,7 @@ val name_of_disc: term -> string val wrap_free_constructors: ({prems: thm list, context: Proof.context} -> tactic) list list -> - (((bool * bool) * term list) * term) * + (((bool * bool) * term list) * binding) * (binding list * (binding list list * (binding * term) list list)) -> local_theory -> ctr_sugar * local_theory val parse_wrap_free_constructors_options: (bool * bool) parser @@ -177,8 +177,8 @@ fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs; -fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), raw_case), - (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = +fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs), + raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy = let (* TODO: sanity checks on arguments *) @@ -188,13 +188,10 @@ val _ = if n > 0 then () else error "No constructors specified"; val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs; - val case0 = prep_term no_defs_lthy raw_case; val sel_defaultss = pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss); - val case0T = fastype_of case0; - val Type (dataT_name, As0) = - domain_type (snd (strip_typeN (num_binder_types case0T - 1) case0T)); + val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0)); val data_b = Binding.qualified_name dataT_name; val data_b_name = Binding.name_of data_b; @@ -256,15 +253,15 @@ else sel)) (1 upto m) o pad_list Binding.empty m) ctrs0 ms; - val casex = mk_case As B case0; val case_Ts = map (fn Ts => Ts ---> B) ctr_Tss; - val (((((((xss, xss'), yss), fs), gs), [u', v']), (p, p')), names_lthy) = no_defs_lthy |> + val ((((((((xss, xss'), yss), fs), gs), [u', v']), [w]), (p, p')), names_lthy) = no_defs_lthy |> mk_Freess' "x" ctr_Tss ||>> mk_Freess "y" ctr_Tss ||>> mk_Frees "f" case_Ts ||>> mk_Frees "g" case_Ts ||>> (apfst (map (rpair dataT)) oo Variable.variant_fixes) [data_b_name, data_b_name ^ "'"] + ||>> mk_Frees "z" [B] ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "P") HOLogic.boolT; val u = Free u'; @@ -277,16 +274,43 @@ val xfs = map2 (curry Term.list_comb) fs xss; val xgs = map2 (curry Term.list_comb) gs xss; + (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides + nicer names). Consider removing. *) + val eta_fs = map2 eta_expand_arg xss xfs; + val eta_gs = map2 eta_expand_arg xss xgs; + + val case_binding = + qualify false + (if Binding.is_empty raw_case_binding orelse + Binding.eq_name (raw_case_binding, standard_binding) then + Binding.suffix_name ("_" ^ caseN) data_b + else + raw_case_binding); + + fun mk_case_disj xctr xf xs = + list_exists_free xs (HOLogic.mk_conj (HOLogic.mk_eq (u, xctr), HOLogic.mk_eq (w, xf))); + + val case_rhs = + fold_rev (fold_rev Term.lambda) [fs, [u]] + (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $ + Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss))); + + val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy + |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs)) + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy lthy'; + + val case_def = Morphism.thm phi raw_case_def; + + val case0 = Morphism.term phi raw_case; + val casex = mk_case As B case0; + val fcase = Term.list_comb (casex, fs); val ufcase = fcase $ u; val vfcase = fcase $ v; - (* TODO: Eta-expension is for compatibility with the old datatype package (but it also provides - nicer names). Consider removing. *) - val eta_fs = map2 eta_expand_arg xss xfs; - val eta_gs = map2 eta_expand_arg xss xgs; - val eta_fcase = Term.list_comb (casex, eta_fs); val eta_gcase = Term.list_comb (casex, eta_gs); @@ -312,7 +336,7 @@ val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs, sel_defss, lthy') = if no_dests then - (true, [], [], [], [], [], [], [], [], [], no_defs_lthy) + (true, [], [], [], [], [], [], [], [], [], lthy) else let fun disc_free b = Free (Binding.name_of b, mk_pred1T dataT); @@ -328,7 +352,7 @@ NONE => (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T) - | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy) + | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term lthy) | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks; fun sel_spec b proto_sels = @@ -337,14 +361,14 @@ (case duplicates (op =) (map fst proto_sels) of k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^ " for constructor " ^ - quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1)))) + quote (Syntax.string_of_term lthy (nth ctrs (k - 1)))) | [] => ()) val T = (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of [T] => T | T :: T' :: _ => error ("Inconsistent range type for selector " ^ - quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^ - " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T'))); + quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ lthy T) ^ " vs. " + ^ quote (Syntax.string_of_typ lthy T'))); in mk_Trueprop_eq (Free (Binding.name_of b, dataT --> T) $ u, Term.list_comb (mk_case As T case0, mk_sel_case_args b proto_sels T) $ u) @@ -368,7 +392,7 @@ fun unflat_selss xs = unflat_lookup Binding.eq_name sel_bindings xs sel_bindingss; val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) = - no_defs_lthy + lthy |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b => if Binding.is_empty b then if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def) @@ -432,16 +456,11 @@ map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs))) end; - val cases_goal = - map3 (fn xs => fn xctr => fn xf => - fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xss xctrs xfs; - - val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss @ [cases_goal]; + val goalss = [exhaust_goal] :: inject_goalss @ half_distinct_goalss; fun after_qed thmss lthy = let - val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) = - (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss))); + val ([exhaust_thm], (inject_thmss, half_distinct_thmss)) = (hd thmss, chop n (tl thmss)); val inject_thms = flat inject_thmss; @@ -470,6 +489,19 @@ |> Thm.close_derivation end; + val case_thms = + let + val goals = + map3 (fn xctr => fn xf => fn xs => + fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss; + in + map4 (fn k => fn goal => fn injects => fn distinctss => + Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => + mk_case_tac ctxt n k case_def injects distinctss) + |> Thm.close_derivation) + ks goals inject_thmss distinct_thmsss + end; + val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) = if no_dests then @@ -767,7 +799,7 @@ "wrap an existing freely generated type's constructors" ((parse_wrap_free_constructors_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- - Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss -- + parse_binding -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss -- Scan.optional parse_bound_termss []) ([], [])) ([], ([], []))) >> wrap_free_constructors_cmd); diff -r 5e25877c51d4 -r 2b430bbb5a1a src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML Mon Aug 12 15:25:17 2013 +0200 @@ -8,6 +8,7 @@ signature BNF_CTR_SUGAR_TACTICS = sig val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic + val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic val mk_case_conv_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> tactic @@ -108,10 +109,14 @@ fun mk_case_distinct_ctrs_tac ctxt distincts = REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt); -fun mk_case_tac ctxt n k def injects distinctss = - let val ks = 1 upto n in - HEADGOAL (rtac (def RS trans) THEN' rtac @{thm the_equality} THEN' rtac (mk_disjIN n k) THEN' - REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' rtac refl THEN' +fun mk_case_tac ctxt n k case_def injects distinctss = + let + val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq); + val ks = 1 upto n; + in + HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN' + rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN' + rtac refl THEN' EVERY' (map2 (fn k' => fn distincts => (if k' < n then etac disjE else K all_tac) THEN' (if k' = k then mk_case_same_ctr_tac ctxt injects diff -r 5e25877c51d4 -r 2b430bbb5a1a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:16 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Aug 12 15:25:17 2013 +0200 @@ -65,10 +65,9 @@ val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list -> string * term list * term list list * ((term list list * term list list list) * (typ list * typ list list)) list -> - thm list -> thm list -> thm list list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> - typ list -> typ list -> int list list -> int list list -> int list -> thm list list -> - BNF_Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) -> - local_theory -> + thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list -> typ list -> + int list list -> int list list -> int list -> thm list list -> BNF_Ctr_Sugar.ctr_sugar list -> + term list list -> thm list list -> (thm list -> thm list) -> local_theory -> ((thm list * thm) list * Args.src list) * (thm list list * thm list list * Args.src list) * (thm list list * thm list list) * (thm list list * thm list list * Args.src list) @@ -201,7 +200,6 @@ p :: flat_corec_predss_getterss qss fss @ flat_corec_preds_predsss_gettersss ps qsss fsss; fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs)); -fun mk_uncurried_fun f xs = mk_tupled_fun (HOLogic.mk_tuple xs) f xs; fun mk_uncurried2_fun f xss = mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat_rec_arg_args xss); @@ -689,8 +687,8 @@ fun derive_coinduct_coiters_thms_for_types pre_bnfs (z, cs, cpss, coiters_args_types as [((pgss, crgsss), _), ((phss, cshsss), _)]) - dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns - ctr_defss ctr_sugars coiterss coiter_defss export_args lthy = + dtor_coinducts dtor_ctors dtor_coiter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss + ctr_sugars coiterss coiter_defss export_args lthy = let val coiterss' = transpose coiterss; val coiter_defss' = transpose coiter_defss; @@ -703,8 +701,6 @@ val pre_rel_defs = map rel_def_of_bnf pre_bnfs; val nesting_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nesting_bnfs; val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs; - val nested_map_comp's = map map_comp'_of_bnf nested_bnfs; - val nested_map_ids'' = map (unfold_thms lthy [id_def] o map_id_of_bnf) nested_bnfs; val fp_b_names = map base_name_of_typ fpTs; @@ -839,7 +835,7 @@ let val T = fastype_of cqf in if exists_subtype_in Cs T then let val U = mk_U maybe_mk_sumT T in - build_map lthy (indexify snd fpTs (fn kk => fn TU => + build_map lthy (indexify snd fpTs (fn kk => fn _ => maybe_tack (nth cs kk, nth us kk) (nth fcoiters kk))) (T, U) $ cqf end else @@ -853,20 +849,6 @@ val unfold_goalss = map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss'; val corec_goalss = map8 (map4 oooo mk_goal phss) cs cpss hcorecs ns kss ctrss mss cshsss'; - fun mk_map_if_distrib bnf = - let - val mapx = map_of_bnf bnf; - val live = live_of_bnf bnf; - val ((Ts, T), U) = strip_typeN (live + 1) (fastype_of mapx) |>> split_last; - val fs = Variable.variant_frees lthy [mapx] (map (pair "f") Ts); - val t = Term.list_comb (mapx, map (Var o apfst (rpair 0)) fs); - in - Drule.instantiate' (map (SOME o certifyT lthy) [U, T]) [SOME (certify lthy t)] - @{thm if_distrib} - end; - - val nested_map_if_distribs = map mk_map_if_distrib nested_bnfs; - val unfold_tacss = map3 (map oo mk_coiter_tac unfold_defs nesting_map_ids'') (map un_fold_of dtor_coiter_thmss) pre_map_defs ctr_defss; @@ -1139,7 +1121,7 @@ val ((xtor_co_iterss, iters_args_types, coiters_args_types), lthy') = mk_co_iters_prelims fp fpTs Cs ns mss xtor_co_iterss0 lthy; - fun define_ctrs_case_for_type ((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), + fun define_ctrs_dtrs_for_type (((((((((((((((((((((((fp_bnf, fp_b), fpT), ctor), dtor), xtor_co_iters), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs), pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy = @@ -1149,12 +1131,10 @@ val dtorT = domain_type (fastype_of ctor); val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss; val ctr_sum_prod_T = mk_sumTN_balanced ctr_prod_Ts; - val case_Ts = map (fn Ts => Ts ---> C) ctr_Tss; - val (((((w, fs), xss), yss), u'), names_lthy) = + val ((((w, xss), yss), u'), names_lthy) = no_defs_lthy |> yield_singleton (mk_Frees "w") dtorT - ||>> mk_Frees "f" case_Ts ||>> mk_Freess "x" ctr_Tss ||>> mk_Freess "y" (map (map B_ify) ctr_Tss) ||>> yield_singleton Variable.variant_fixes fp_b_name; @@ -1168,16 +1148,10 @@ map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $ mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs; - val case_binding = qualify false fp_b_name (Binding.suffix_name ("_" ^ caseN) fp_b); - - val case_rhs = - fold_rev Term.lambda (fs @ [u]) - (mk_sum_caseN_balanced (map2 mk_uncurried_fun fs xss) $ (dtor $ u)); - - val ((raw_case :: raw_ctrs, raw_case_def :: raw_ctr_defs), (lthy', lthy)) = no_defs_lthy + val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs => Local_Theory.define ((b, mx), ((Thm.def_binding b, []), rhs)) #>> apsnd snd) - (case_binding :: ctr_bindings) (NoSyn :: ctr_mixfixes) (case_rhs :: ctr_rhss) + ctr_bindings ctr_mixfixes ctr_rhss ||> `Local_Theory.restore; val phi = Proof_Context.export_morphism lthy lthy'; @@ -1185,11 +1159,8 @@ val ctr_defs = map (Morphism.thm phi) raw_ctr_defs; val ctr_defs' = map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs; - val case_def = Morphism.thm phi raw_case_def; val ctrs0 = map (Morphism.term phi) raw_ctrs; - val casex0 = Morphism.term phi raw_case; - val ctrs = map (mk_ctr As) ctrs0; fun wrap_ctrs lthy = @@ -1226,15 +1197,11 @@ map (map (fn (def, def') => fn {context = ctxt, ...} => mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs)); - val case_tacs = - map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} => - mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs; - - val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs]; + val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss; val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in - wrap_free_constructors tacss (((wrap_opts, ctrs0), casex0), (disc_bindings, + wrap_free_constructors tacss (((wrap_opts, ctrs0), standard_binding), (disc_bindings, (sel_bindingss, sel_defaultss))) lthy end; @@ -1391,9 +1358,8 @@ (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs), (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) = derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_inducts - dtor_ctors xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs As kss mss ns ctr_defss - ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) - lthy; + dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs As kss mss ns ctr_defss ctr_sugars + coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1440,7 +1406,7 @@ end; val lthy'' = lthy' - |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ + |> fold_map define_ctrs_dtrs_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ ctors ~~ dtors ~~ xtor_co_iterss ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ diff -r 5e25877c51d4 -r 2b430bbb5a1a src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 15:25:16 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML Mon Aug 12 15:25:17 2013 +0200 @@ -11,7 +11,6 @@ val sum_prod_thms_set: thm list val sum_prod_thms_rel: thm list - val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list -> thm list -> thm list -> thm list list -> thm list list list -> thm list list list -> tactic val mk_coiter_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic @@ -70,12 +69,6 @@ val inst_as_projs_tac = PRIMITIVE oo inst_as_projs; -fun mk_case_tac ctxt n k m case_def ctr_def dtor_ctor = - unfold_thms_tac ctxt [case_def, ctr_def, dtor_ctor] THEN - HEADGOAL (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN' - REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN' - rtac refl); - fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' = unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN unfold_thms_tac ctxt @{thms split_paired_all} THEN