# HG changeset patch # User haftmann # Date 1254037943 -7200 # Node ID ec5976f4d3d8aeb1a86a233c2a776cdb71ca35b6 # Parent b68f3afdc1370e59519a19a1925d23f345d630d9 registering split rules and projected induction rules; ML identifiers more close to Isar theorem names diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Sun Sep 27 09:52:23 2009 +0200 @@ -189,13 +189,11 @@ (* add_cases_induct *) -fun add_cases_induct infos induction thy = +fun add_cases_induct infos inducts thy = let - val inducts = Project_Rule.projections (ProofContext.init thy) induction; - - fun named_rules (name, {index, exhaustion, ...}: info) = + fun named_rules (name, {index, exhaust, ...}: info) = [((Binding.empty, nth inducts index), [Induct.induct_type name]), - ((Binding.empty, exhaustion), [Induct.cases_type name])]; + ((Binding.empty, exhaust), [Induct.cases_type name])]; fun unnamed_rule i = ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]); in @@ -307,9 +305,9 @@ (**** make datatype info ****) -fun make_dt_info alt_names descr sorts induct reccomb_names rec_thms - (((((((((i, (_, (tname, _, _))), case_name), case_thms), - exhaustion_thm), distinct_thm), inject), nchotomy), case_cong), weak_case_cong) = +fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms + ((((((((((i, (_, (tname, _, _))), case_name), case_thms), + exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) = (tname, {index = i, alt_names = alt_names, @@ -319,10 +317,11 @@ rec_rewrites = rec_thms, case_name = case_name, case_rewrites = case_thms, - induction = induct, - exhaustion = exhaustion_thm, + inducts = inducts, + exhaust = exhaust_thm, distinct = distinct_thm, inject = inject, + splits = splits, nchotomy = nchotomy, case_cong = case_cong, weak_case_cong = weak_case_cong}); @@ -342,6 +341,7 @@ val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |> DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts types_syntax constr_syntax case_names_induct; + val inducts = Project_Rule.projections (ProofContext.init thy2) induct; val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr sorts induct case_names_exhausts thy2; @@ -360,9 +360,9 @@ descr sorts thy9; val dt_infos = map - (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms) + (make_dt_info (SOME new_type_names) (flat descr) sorts (inducts, induct) reccomb_names rec_thms) ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~ - casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); + casedist_thms ~~ simproc_dists ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs); val simps = flat (distinct @ inject @ case_thms) @ rec_thms; val dt_names = map fst dt_infos; @@ -374,7 +374,7 @@ |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs)) |> put_dt_infos dt_infos - |> add_cases_induct dt_infos induct + |> add_cases_induct dt_infos inducts |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeInterpretation.data (config, map fst dt_infos); @@ -427,10 +427,11 @@ ||>> store_thmss "distinct" new_type_names distinct ||> Sign.add_path (space_implode "_" new_type_names) ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])]; + val inducts = Project_Rule.projections (ProofContext.init thy10) induct'; - val dt_infos = map (make_dt_info alt_names descr sorts induct' reccomb_names rec_thms) + val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms) ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ - map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); + map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs); val simps = flat (distinct @ inject @ case_thms) @ rec_thms; val dt_names = map fst dt_infos; @@ -441,7 +442,7 @@ |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs)) |> put_dt_infos dt_infos - |> add_cases_induct dt_infos induct' + |> add_cases_induct dt_infos inducts |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Sun Sep 27 09:52:23 2009 +0200 @@ -195,10 +195,11 @@ rec_rewrites : thm list, case_name : string, case_rewrites : thm list, - induction : thm, - exhaustion : thm, + inducts : thm list * thm, + exhaust : thm, distinct : simproc_dist, inject : thm list, + splits : thm * thm, nchotomy : thm, case_cong : thm, weak_case_cong : thm}; diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Datatype/datatype_realizer.ML --- a/src/HOL/Tools/Datatype/datatype_realizer.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sun Sep 27 09:52:23 2009 +0200 @@ -38,7 +38,7 @@ fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT); -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : info) is thy = +fun make_ind sorts ({descr, rec_names, rec_rewrites, inducts = (_, induct), ...} : info) is thy = let val recTs = get_rec_types descr sorts; val pnames = if length descr = 1 then ["P"] @@ -113,18 +113,18 @@ (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); val cert = cterm_of thy; val inst = map (pairself cert) (map head_of (HOLogic.dest_conj - (HOLogic.dest_Trueprop (concl_of induction))) ~~ ps); + (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps); val thm = OldGoals.simple_prove_goal_cterm (cert (Logic.list_implies (prems, concl))) (fn prems => [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]), - rtac (cterm_instantiate inst induction) 1, + rtac (cterm_instantiate inst induct) 1, ALLGOALS ObjectLogic.atomize_prems_tac, rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites), REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i => REPEAT (etac allE i) THEN atac i)) 1)]); - val ind_name = Thm.get_name induction; + val ind_name = Thm.get_name induct; val vs = map (fn i => List.nth (pnames, i)) is; val (thm', thy') = thy |> Sign.root_path @@ -157,7 +157,7 @@ in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end; -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : info) thy = +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaust, ...} : info) thy = let val cert = cterm_of thy; val rT = TFree ("'P", HOLogic.typeS); @@ -187,12 +187,12 @@ HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ list_comb (r, rs @ [y']))))) (fn prems => - [rtac (cterm_instantiate [(cert y, cert y')] exhaustion) 1, + [rtac (cterm_instantiate [(cert y, cert y')] exhaust) 1, ALLGOALS (EVERY' [asm_simp_tac (HOL_basic_ss addsimps case_rewrites), resolve_tac prems, asm_simp_tac HOL_basic_ss])]); - val exh_name = Thm.get_name exhaustion; + val exh_name = Thm.get_name exhaust; val (thm', thy') = thy |> Sign.root_path |> PureThy.store_thm (Binding.qualified_name (exh_name ^ "_P_correctness"), thm) @@ -210,7 +210,7 @@ in Extraction.add_realizers_i [(exh_name, (["P"], r', prf)), - (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy' + (exh_name, ([], Extraction.nullt, prf_of exhaust))] thy' end; fun add_dt_realizers config names thy = diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Sun Sep 27 09:52:23 2009 +0200 @@ -38,7 +38,7 @@ (** theory context references **) fun exh_thm_of (dt_info : info Symtab.table) tname = - #exhaustion (the (Symtab.lookup dt_info tname)); + #exhaust (the (Symtab.lookup dt_info tname)); (******************************************************************************) @@ -389,7 +389,7 @@ fun prove_iso_thms (ds, (inj_thms, elem_thms)) = let val (_, (tname, _, _)) = hd ds; - val {induction, ...} = the (Symtab.lookup dt_info tname); + val induct = (snd o #inducts o the o Symtab.lookup dt_info) tname; fun mk_ind_concl (i, _) = let @@ -410,7 +410,7 @@ val inj_thm = SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY - [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, + [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, REPEAT (EVERY [rtac allI 1, rtac impI 1, exh_tac (exh_thm_of dt_info) 1, @@ -436,7 +436,7 @@ val elem_thm = SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2)) (fn _ => - EVERY [(indtac induction [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, + EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1, rewrite_goals_tac rewrites, REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]); diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Function/fundef_datatype.ML --- a/src/HOL/Tools/Function/fundef_datatype.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_datatype.ML Sun Sep 27 09:52:23 2009 +0200 @@ -145,7 +145,7 @@ let val T = fastype_of v val (tname, _) = dest_Type T - val {exhaustion=case_thm, ...} = Datatype.the_info thy tname + val {exhaust=case_thm, ...} = Datatype.the_info thy tname val constrs = inst_constrs_of thy T val c_cases = map (constr_case thy P idx (v :: vs) pts) constrs in diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/Function/size.ML Sun Sep 27 09:52:23 2009 +0200 @@ -59,7 +59,7 @@ fun prove_size_thms (info : info) new_type_names thy = let - val {descr, alt_names, sorts, rec_names, rec_rewrites, induction, ...} = info; + val {descr, alt_names, sorts, rec_names, rec_rewrites, inducts = (_, induct), ...} = info; val l = length new_type_names; val alt_names' = (case alt_names of NONE => replicate l NONE | SOME names => map SOME names); @@ -169,7 +169,7 @@ map (mk_unfolded_size_eq (AList.lookup op = (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs) (xs ~~ recTs2 ~~ rec_combs2)))) - (fn _ => (indtac induction xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); + (fn _ => (indtac induct xs THEN_ALL_NEW asm_simp_tac simpset1) 1)); val unfolded_size_eqs1 = prove_unfolded_size_eqs param_size fs; val unfolded_size_eqs2 = prove_unfolded_size_eqs (K NONE) fs'; diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Sun Sep 27 09:52:23 2009 +0200 @@ -96,7 +96,7 @@ | TVar((s,i),_) => error ("Free variable: " ^ s) val dt = Datatype.the_info thy ty_str in - cases_thm_of_induct_thm (#induction dt) + cases_thm_of_induct_thm (snd (#inducts dt)) end; (* diff -r b68f3afdc137 -r ec5976f4d3d8 src/HOL/Tools/old_primrec.ML --- a/src/HOL/Tools/old_primrec.ML Fri Sep 25 10:20:03 2009 +0200 +++ b/src/HOL/Tools/old_primrec.ML Sun Sep 27 09:52:23 2009 +0200 @@ -230,15 +230,15 @@ (tname, dt)::(find_dts dt_info tnames' tnames) else find_dts dt_info tnames' tnames); -fun prepare_induct ({descr, induction, ...}: info) rec_eqns = +fun prepare_induct ({descr, inducts = (_, induct), ...}: info) rec_eqns = let fun constrs_of (_, (_, _, cs)) = map (fn (cname:string, (_, cargs, _, _, _)) => (cname, map fst cargs)) cs; - val params_of = these o AList.lookup (op =) (List.concat (map constrs_of rec_eqns)); + val params_of = these o AList.lookup (op =) (maps constrs_of rec_eqns); in - induction - |> RuleCases.rename_params (map params_of (List.concat (map (map #1 o #3 o #2) descr))) - |> RuleCases.save induction + induct + |> RuleCases.rename_params (map params_of (maps (map #1 o #3 o #2) descr)) + |> RuleCases.save induct end; local