# HG changeset patch # User blanchet # Date 1384868000 -3600 # Node ID 27966e17d075baa69f777be3137757049ed2b5ea # Parent 930409d4321149246e040c6e4f4b766e700e49fc case_if -> case_eq_if + docs diff -r 930409d43211 -r 27966e17d075 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Nov 19 14:11:26 2013 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Nov 19 14:33:20 2013 +0100 @@ -350,7 +350,7 @@ custom names. In the example below, the familiar names @{text null}, @{text hd}, @{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2}, -@{text list_set}, @{text list_map}, and @{text list_rel}: +@{text set_list}, @{text map_list}, and @{text rel_list}: *} (*<*) @@ -501,7 +501,7 @@ reference manual \cite{isabelle-isar-ref}. The optional names preceding the type variables allow to override the default -names of the set functions (@{text t_set1}, \ldots, @{text t_setM}). +names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Inside a mutually recursive specification, all defined datatypes must mention exactly the same type variables in the same order. @@ -626,7 +626,7 @@ \begin{itemize} \setlength{\itemsep}{0pt} -\item \relax{Case combinator}: @{text t_case} (rendered using the familiar +\item \relax{Case combinator}: @{text t.t_case} (rendered using the familiar @{text case}--@{text of} syntax) \item \relax{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, @@ -638,22 +638,22 @@ \phantom{\relax{Selectors:}} @{text t.un_C\<^sub>n1}$, \ldots, @{text t.un_C\<^sub>nk\<^sub>n}. \item \relax{Set functions} (or \relax{natural transformations}): -@{text t_set1}, \ldots, @{text t_setm} - -\item \relax{Map function} (or \relax{functorial action}): @{text t_map} - -\item \relax{Relator}: @{text t_rel} - -\item \relax{Iterator}: @{text t_fold} - -\item \relax{Recursor}: @{text t_rec} +@{text set1_t}, \ldots, @{text t.setm_t} + +\item \relax{Map function} (or \relax{functorial action}): @{text t.map_t} + +\item \relax{Relator}: @{text t.rel_t} + +\item \relax{Iterator}: @{text t.t_fold} + +\item \relax{Recursor}: @{text t.t_rec} \end{itemize} \noindent The case combinator, discriminators, and selectors are collectively called \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the -name and is normally hidden. +names and is normally hidden. *} @@ -810,8 +810,8 @@ \item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\ @{thm list.sel_split_asm[no_vars]} -\item[@{text "t."}\hthm{case\_if}\rm:] ~ \\ -@{thm list.case_if[no_vars]} +\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\ +@{thm list.case_eq_if[no_vars]} \end{description} \end{indentblock} @@ -1150,13 +1150,13 @@ \noindent The next example features recursion through the @{text option} type. Although @{text option} is not a new-style datatype, it is registered as a BNF with the -map function @{const option_map}: +map function @{const map_option}: *} primrec_new (*<*)(in early) (*>*)sum_btree :: "('a\{zero,plus}) btree \ 'a" where "sum_btree (BNode a lt rt) = - a + the_default 0 (option_map sum_btree lt) + - the_default 0 (option_map sum_btree rt)" + a + the_default 0 (map_option sum_btree lt) + + the_default 0 (map_option sum_btree rt)" text {* \noindent diff -r 930409d43211 -r 27966e17d075 src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Tue Nov 19 14:11:26 2013 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Tue Nov 19 14:33:20 2013 +0100 @@ -118,7 +118,7 @@ expands = [], sel_splits = [], sel_split_asms = [], - case_ifs = []}; + case_eq_ifs = []}; fun register dt_infos = Data.map (fn {types, constrs, cases} => diff -r 930409d43211 -r 27966e17d075 src/HOL/Tools/ctr_sugar.ML --- a/src/HOL/Tools/ctr_sugar.ML Tue Nov 19 14:11:26 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar.ML Tue Nov 19 14:33:20 2013 +0100 @@ -30,7 +30,7 @@ expands: thm list, sel_splits: thm list, sel_split_asms: thm list, - case_ifs: thm list}; + case_eq_ifs: thm list}; val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar val transfer_ctr_sugar: Proof.context -> ctr_sugar -> ctr_sugar @@ -90,7 +90,7 @@ expands: thm list, sel_splits: thm list, sel_split_asms: thm list, - case_ifs: thm list}; + case_eq_ifs: thm list}; fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar, {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) = @@ -98,7 +98,7 @@ fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss, - disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_ifs} = + disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} = {ctrs = map (Morphism.term phi) ctrs, casex = Morphism.term phi casex, discs = map (Morphism.term phi) discs, @@ -121,7 +121,7 @@ expands = map (Morphism.thm phi) expands, sel_splits = map (Morphism.thm phi) sel_splits, sel_split_asms = map (Morphism.thm phi) sel_split_asms, - case_ifs = map (Morphism.thm phi) case_ifs}; + case_eq_ifs = map (Morphism.thm phi) case_eq_ifs}; val transfer_ctr_sugar = morph_ctr_sugar o Morphism.thm_morphism o Thm.transfer o Proof_Context.theory_of; @@ -160,7 +160,7 @@ val caseN = "case"; val case_congN = "case_cong"; -val case_ifN = "case_if"; +val case_eq_ifN = "case_eq_if"; val collapseN = "collapse"; val disc_excludeN = "disc_exclude"; val disc_exhaustN = "disc_exhaust"; @@ -657,7 +657,7 @@ val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms, - safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_if_thms) = + safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) = if no_discs_sels then ([], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else @@ -861,12 +861,12 @@ (thm, asm_thm) end; - val case_if_thm = + val case_eq_if_thm = let val goal = mk_Trueprop_eq (ufcase, mk_IfN B udiscs usel_fs); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => - mk_case_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) + mk_case_eq_if_tac ctxt n uexhaust_thm case_thms disc_thmss' sel_thmss) |> Thm.close_derivation |> singleton (Proof_Context.export names_lthy lthy) end; @@ -874,7 +874,7 @@ (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm], - [sel_split_asm_thm], [case_if_thm]) + [sel_split_asm_thm], [case_eq_if_thm]) end; val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases)); @@ -890,7 +890,7 @@ val notes = [(caseN, case_thms, code_nitpicksimp_simp_attrs), (case_congN, [case_cong_thm], []), - (case_ifN, case_if_thms, []), + (case_eq_ifN, case_eq_if_thms, []), (collapseN, safe_collapse_thms, simp_attrs), (discN, nontriv_disc_thms, simp_attrs), (discIN, nontriv_discI_thms, []), @@ -921,7 +921,7 @@ discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms, - case_ifs = case_if_thms}; + case_eq_ifs = case_eq_if_thms}; in (ctr_sugar, lthy diff -r 930409d43211 -r 27966e17d075 src/HOL/Tools/ctr_sugar_tactics.ML --- a/src/HOL/Tools/ctr_sugar_tactics.ML Tue Nov 19 14:11:26 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_tactics.ML Tue Nov 19 14:33:20 2013 +0100 @@ -18,8 +18,8 @@ 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_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> thm list list -> - tactic + val mk_case_eq_if_tac: Proof.context -> int -> thm -> thm list -> thm list list -> + thm list list -> tactic val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> @@ -28,8 +28,8 @@ val mk_nchotomy_tac: int -> thm -> tactic val mk_other_half_disc_exclude_tac: thm -> tactic val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic - val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list - list list -> tactic + val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> + thm list list list -> tactic val mk_split_asm_tac: Proof.context -> thm -> tactic val mk_unique_disc_def_tac: int -> thm -> tactic end; @@ -143,17 +143,17 @@ else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss)) end; -fun mk_case_if_tac ctxt n uexhaust cases discss' selss = +fun mk_case_cong_tac ctxt uexhaust cases = + HEADGOAL (rtac uexhaust THEN' + EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); + +fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss = HEADGOAL (rtac uexhaust THEN' EVERY' (map3 (fn casex => fn if_discs => fn sels => EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)), rtac casex]) cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss)); -fun mk_case_cong_tac ctxt uexhaust cases = - HEADGOAL (rtac uexhaust THEN' - EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases)); - fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss = HEADGOAL (rtac uexhaust) THEN ALLGOALS (fn k => (hyp_subst_tac ctxt THEN' @@ -169,4 +169,4 @@ end; -structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics; +structure Ctr_Sugar_General_Tactics : CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics; diff -r 930409d43211 -r 27966e17d075 src/HOL/Tools/ctr_sugar_util.ML --- a/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 19 14:11:26 2013 +0100 +++ b/src/HOL/Tools/ctr_sugar_util.ML Tue Nov 19 14:33:20 2013 +0100 @@ -176,9 +176,7 @@ fun rapp u t = betapply (t, u); fun list_quant_free quant_const = - fold_rev (fn free => fn P => - let val (x, T) = Term.dest_Free free; - in quant_const T $ Term.absfree (x, T) P end); + fold_rev (fn Free (xT as (_, T)) => fn P => quant_const T $ Term.absfree xT P); val list_all_free = list_quant_free HOLogic.all_const; val list_exists_free = list_quant_free HOLogic.exists_const;