# HG changeset patch # User krauss # Date 1378678447 -7200 # Node ID 53bd62921c546f9785821c3f703fbcbf005cb52e # Parent 825b6a41411b2fc2b290d9e92e238e171b683f34 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information; normalized whitespace and indentation diff -r 825b6a41411b -r 53bd62921c54 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Sun Sep 08 23:58:52 2013 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Mon Sep 09 00:14:07 2013 +0200 @@ -248,10 +248,39 @@ fst (fold_map (project induct_inst) parts 0) end -fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof = +fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs, ...}) = + let + val arg_vars = + cargTs + |> map_index (fn (i, T) => Free ("x" ^ string_of_int i, T)) (* FIXME: proper context *) + + val argsT = fastype_of (HOLogic.mk_tuple arg_vars) + val args = Free ("x", argsT) (* FIXME: proper context *) + + val cert = cterm_of (Proof_Context.theory_of ctxt) + + val sumtree_inj = SumTree.mk_inj ST n i args + + val sum_elims = + @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] HOL.notE[OF Sum_Type.sum.distinct(2)]} + + fun prep_subgoal i = + REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format] Inr_inject[elim_format]} i) + THEN REPEAT (Tactic.eresolve_tac sum_elims i) + in + cases_rule + |> Thm.forall_elim @{cterm "P::bool"} + |> Thm.forall_elim (cert sumtree_inj) + |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal) + |> Thm.forall_intr (cert args) + |> Thm.forall_intr @{cterm "P::bool"} + end + + +fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, n, ST, ...}) proof = let val result = inner_cont proof - val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct], + val FunctionResult {G, R, cases=[cases_rule], psimps, simple_pinducts=[simple_pinduct], termination, domintros, dom, pelims, ...} = result val (all_f_defs, fs) = @@ -269,69 +298,18 @@ val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs val mpsimps = map2 mk_mpsimp fqgars psimps val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m + val mcases = map (mutual_cases_rule lthy cases_rule n ST) parts val mtermination = full_simplify rew_simpset termination val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros in FunctionResult { fs=fs, G=G, R=R, dom=dom, psimps=mpsimps, simple_pinducts=minducts, - cases=cases, pelims=pelims, termination=mtermination, + cases=mcases, pelims=pelims, termination=mtermination, domintros=mdomintros} end -fun postprocess_cases_rules ctxt cont proof = - let val result = cont proof; - val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, pelims, - termination, domintros, ...} = result; - val n_fs = length fs; - val domT = R |> dest_Free |> snd |> hd o snd o dest_Type - - fun postprocess_cases_rule (idx,f) = - let val lhs_of = - prop_of #> Logic.strip_assums_concl #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst - - val f_simps = filter (fn r => Term.head_of (lhs_of r) aconv f) psimps - val arity = length (snd (strip_comb (lhs_of (hd f_simps)))) - - val arg_vars = - take arity (binder_types (fastype_of f)) - |> map_index (fn (i, T) => Free ("x" ^ string_of_int i, T)) (* FIXME: proper context *) - - val argsT = fastype_of (HOLogic.mk_tuple arg_vars); - val args = Free ("x", argsT); (* FIXME: proper context *) - - val cert = cterm_of (Proof_Context.theory_of ctxt); - - val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; - - val sum_elims = @{thms HOL.notE[OF Sum_Type.sum.distinct(1)] - HOL.notE[OF Sum_Type.sum.distinct(2)]}; - fun prep_subgoal i = - REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format] - Inr_inject[elim_format]} i) - THEN REPEAT (Tactic.eresolve_tac sum_elims i); - - in - hd cases - |> Thm.forall_elim @{cterm "P::bool"} - |> Thm.forall_elim (cert sumtree_inj) - |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal) - |> Thm.forall_intr (cert args) - |> Thm.forall_intr @{cterm "P::bool"} - - end; - - val cases' = map_index postprocess_cases_rule fs; - -in - FunctionResult {fs=fs, G=G, R=R, dom=dom, psimps=psimps, - simple_pinducts=simple_pinducts, - cases=cases', pelims=pelims, termination=termination, - domintros=domintros} -end; - - fun prepare_function_mutual config defname fixes eqss lthy = let val mutual as Mutual {fsum_var=(n, T), qglrs, ...} = @@ -343,9 +321,8 @@ val (mutual', lthy'') = define_projections fixes mutual fsum lthy' val cont' = mk_partial_rules_mutual lthy'' cont mutual' - val cont'' = postprocess_cases_rules lthy'' cont' in - ((goalstate, cont''), lthy'') + ((goalstate, cont'), lthy'') end end