# HG changeset patch # User desharna # Date 1418984338 -3600 # Node ID c448752e8b9d4103713b9a071da2d7e42ab92826 # Parent d1def4b100edf5334eda68645ddd7843658bcf35 generate 'disc_eq_case' for Ctr_Sugars diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 19 11:18:58 2014 +0100 @@ -66,8 +66,6 @@ val mk_nthN: int -> term -> int -> term (*parameterized thms*) - val eqTrueI: thm - val eqFalseI: thm val prod_injectD: thm val prod_injectI: thm val ctrans: thm @@ -345,8 +343,6 @@ fun mk_sym thm = thm RS sym; (*TODO: antiquote heavily used theorems once*) -val eqTrueI = @{thm iffD2[OF eq_True]}; -val eqFalseI = @{thm iffD2[OF eq_False]}; val prod_injectD = @{thm iffD1[OF prod.inject]}; val prod_injectI = @{thm iffD2[OF prod.inject]}; val ctrans = @{thm ordLeq_transitive}; diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 19 11:18:58 2014 +0100 @@ -30,6 +30,7 @@ disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, + disc_eq_cases: thm list, sel_defs: thm list, sel_thmss: thm list list, distinct_discsss: thm list list list, @@ -119,6 +120,7 @@ disc_defs: thm list, disc_thmss: thm list list, discIs: thm list, + disc_eq_cases: thm list, sel_defs: thm list, sel_thmss: thm list list, distinct_discsss: thm list list list, @@ -132,8 +134,8 @@ fun morph_ctr_sugar phi ({kind, T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts, case_thms, case_cong, case_cong_weak, case_distribs, split, split_asm, disc_defs, disc_thmss, - discIs, sel_defs, sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, - split_sels, split_sel_asms, case_eq_ifs} : ctr_sugar) = + discIs, disc_eq_cases, sel_defs, sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, + collapses, expands, split_sels, split_sel_asms, case_eq_ifs} : ctr_sugar) = {kind = kind, T = Morphism.typ phi T, ctrs = map (Morphism.term phi) ctrs, @@ -153,6 +155,7 @@ disc_defs = map (Morphism.thm phi) disc_defs, disc_thmss = map (map (Morphism.thm phi)) disc_thmss, discIs = map (Morphism.thm phi) discIs, + disc_eq_cases = map (Morphism.thm phi) disc_eq_cases, sel_defs = map (Morphism.thm phi) sel_defs, sel_thmss = map (map (Morphism.thm phi)) sel_thmss, distinct_discsss = map (map (map (Morphism.thm phi))) distinct_discsss, @@ -232,6 +235,7 @@ val collapseN = "collapse"; val discN = "disc"; val discIN = "discI"; +val disc_eq_caseN = "disc_eq_case"; val distinctN = "distinct"; val distinct_discN = "distinct_disc"; val exhaustN = "exhaust"; @@ -505,6 +509,7 @@ val case0 = Morphism.term phi raw_case; val casex = mk_case As B case0; val casexC = mk_case As C case0; + val casexBool = mk_case As HOLogic.boolT case0; val fcase = Term.list_comb (casex, fs); @@ -770,9 +775,9 @@ val (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, exhaust_disc_thms, exhaust_sel_thms, all_collapse_thms, safe_collapse_thms, - expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms) = + expand_thms, split_sel_thms, split_sel_asm_thms, case_eq_if_thms, disc_eq_case_thms) = if no_discs_sels then - ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []) else let val udiscs = map (rapp u) discs; @@ -982,11 +987,28 @@ |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation end; + + val disc_eq_case_thms = + let + fun term_of_bool b = if b then @{term True} else @{term False}; + fun mk_case_args n = map_index (fn (k, argTs) => + fold_rev Term.absdummy argTs (term_of_bool (n = k))) ctr_Tss; + val goals = map_index (fn (n, udisc) => + mk_Trueprop_eq (udisc, list_comb (casexBool, mk_case_args n) $ u)) udiscs; + in + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, ...} => mk_disc_eq_case_tac ctxt (certify ctxt u) + exhaust_thm (flat nontriv_disc_thmss) distinct_thms case_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation + end; in (sel_defs, all_sel_thms, sel_thmss, disc_defs, disc_thmss, nontriv_disc_thmss, discI_thms, nontriv_discI_thms, distinct_disc_thms, distinct_disc_thmsss, [exhaust_disc_thm], [exhaust_sel_thm], all_collapse_thms, safe_collapse_thms, - [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm]) + [expand_thm], [split_sel_thm], [split_sel_asm_thm], [case_eq_if_thm], + disc_eq_case_thms) end; val case_distrib_thm = @@ -1026,6 +1048,7 @@ (collapseN, safe_collapse_thms, if ms = [0] then [] else simp_attrs), (discN, flat nontriv_disc_thmss, simp_attrs), (discIN, nontriv_discI_thms, []), + (disc_eq_caseN, disc_eq_case_thms, []), (distinctN, distinct_thms, simp_attrs @ inductsimp_attrs), (distinct_discN, distinct_disc_thms, dest_attrs), (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]), @@ -1073,11 +1096,11 @@ distincts = distinct_thms, case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm, case_distribs = [case_distrib_thm], split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs, - disc_thmss = disc_thmss, discIs = discI_thms, sel_defs = sel_defs, sel_thmss = sel_thmss, - distinct_discsss = distinct_disc_thmsss, exhaust_discs = exhaust_disc_thms, - exhaust_sels = exhaust_sel_thms, collapses = all_collapse_thms, expands = expand_thms, - split_sels = split_sel_thms, split_sel_asms = split_sel_asm_thms, - case_eq_ifs = case_eq_if_thms} + disc_thmss = disc_thmss, discIs = discI_thms, disc_eq_cases = disc_eq_case_thms, + sel_defs = sel_defs, sel_thmss = sel_thmss, distinct_discsss = distinct_disc_thmsss, + exhaust_discs = exhaust_disc_thms, exhaust_sels = exhaust_sel_thms, + collapses = all_collapse_thms, expands = expand_thms, split_sels = split_sel_thms, + split_sel_asms = split_sel_asm_thms, case_eq_ifs = case_eq_if_thms} |> morph_ctr_sugar (substitute_noted_thm noted); in (ctr_sugar, lthy' |> register_ctr_sugar plugins ctr_sugar) diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Fri Dec 19 11:18:58 2014 +0100 @@ -23,6 +23,8 @@ 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_eq_case_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> + tactic val mk_exhaust_disc_tac: int -> thm -> thm list -> tactic val mk_exhaust_sel_tac: int -> thm -> thm list -> tactic val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list -> @@ -93,6 +95,14 @@ REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN' SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)); +fun mk_disc_eq_case_tac ctxt ct exhaust discs distincts cases = + HEADGOAL Goal.conjunction_tac THEN + ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW + (hyp_subst_tac ctxt THEN' + SELECT_GOAL (unfold_thms_tac ctxt (@{thms not_True_eq_False not_False_eq_True} @ cases @ + ((refl :: discs @ distincts) RL [eqTrueI, eqFalseI]))) THEN' + resolve_tac @{thms TrueI True_not_False False_not_True})); + fun mk_expand_tac ctxt n ms uexhaust_disc vexhaust_disc uncollapses distinct_discsss distinct_discsss' = if ms = [0] then diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Fri Dec 19 11:18:58 2014 +0100 @@ -74,6 +74,10 @@ val ss_only: thm list -> Proof.context -> Proof.context + (*parameterized thms*) + val eqTrueI: thm + val eqFalseI: thm + val WRAP: ('a -> tactic) -> ('a -> tactic) -> 'a list -> tactic -> tactic val WRAP': ('a -> int -> tactic) -> ('a -> int -> tactic) -> 'a list -> (int -> tactic) -> int -> tactic @@ -251,6 +255,9 @@ fun ss_only thms ctxt = clear_simpset (put_simpset HOL_basic_ss ctxt) addsimps thms; +val eqTrueI = @{thm iffD2[OF eq_True]}; +val eqFalseI = @{thm iffD2[OF eq_False]}; + (*Tactical WRAP surrounds a static given tactic (core) with two deterministic chains of tactics*) fun WRAP gen_before gen_after xs core_tac = fold_rev (fn x => fn tac => gen_before x THEN tac THEN gen_after x) xs core_tac; diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/Old_Datatype/old_datatype_data.ML --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Dec 19 11:18:58 2014 +0100 @@ -116,6 +116,7 @@ disc_defs = [], disc_thmss = [], discIs = [], + disc_eq_cases = [], sel_defs = [], sel_thmss = [], distinct_discsss = [], diff -r d1def4b100ed -r c448752e8b9d src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Mon Jan 05 06:56:15 2015 +0100 +++ b/src/HOL/Tools/record.ML Fri Dec 19 11:18:58 2014 +0100 @@ -1787,9 +1787,9 @@ discs = [], selss = [], exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, case_distribs = [], split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], - disc_thmss = [], discIs = [], sel_defs = [], sel_thmss = [sel_thms], distinct_discsss = [], - exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [], - split_sel_asms = [], case_eq_ifs = []}; + disc_thmss = [], discIs = [], disc_eq_cases = [], sel_defs = [], sel_thmss = [sel_thms], + distinct_discsss = [], exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], + split_sels = [], split_sel_asms = [], case_eq_ifs = []}; (* definition *)