# HG changeset patch # User wenzelm # Date 1386939541 -3600 # Node ID ba66830fae4c64fb058b9bfa28e0dd4b2fbe0bb9 # Parent b91afc3aa3e6d58e3fee6847a44b5a8c26b60edb tuned whitespace; diff -r b91afc3aa3e6 -r ba66830fae4c src/HOL/Tools/Function/function_elims.ML --- a/src/HOL/Tools/Function/function_elims.ML Fri Dec 13 12:31:45 2013 +0100 +++ b/src/HOL/Tools/Function/function_elims.ML Fri Dec 13 13:59:01 2013 +0100 @@ -34,117 +34,122 @@ local fun propagate_tac i thm = - let fun inspect eq = case eq of - Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) => - if Logic.occs (Free x, t) then raise Match else true - | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => - if Logic.occs (Free x, t) then raise Match else false - | _ => raise Match; - fun mk_eq thm = (if inspect (prop_of thm) then - [thm RS eq_reflection] - else - [Thm.symmetric (thm RS eq_reflection)]) - handle Match => []; - val ss = Simplifier.global_context (Thm.theory_of_thm thm) empty_ss - |> Simplifier.set_mksimps (K mk_eq) + let + fun inspect eq = + (case eq of + Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ Free x $ t) => + if Logic.occs (Free x, t) then raise Match else true + | Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ t $ Free x) => + if Logic.occs (Free x, t) then raise Match else false + | _ => raise Match); + fun mk_eq thm = + (if inspect (prop_of thm) then [thm RS eq_reflection] + else [Thm.symmetric (thm RS eq_reflection)]) + handle Match => []; + val ss = + Simplifier.global_context (Thm.theory_of_thm thm) empty_ss + |> Simplifier.set_mksimps (K mk_eq); in asm_lr_simp_tac ss i thm end; -val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+} -val boolE = @{thms HOL.TrueE HOL.FalseE} -val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+} -val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False} +val eqBoolI = @{lemma "!!P. P ==> P = True" "!!P. ~P ==> P = False" by iprover+}; +val boolE = @{thms HOL.TrueE HOL.FalseE}; +val boolD = @{lemma "!!P. True = P ==> P" "!!P. False = P ==> ~P" by iprover+}; +val eqBool = @{thms HOL.eq_True HOL.eq_False HOL.not_False_eq_True HOL.not_True_eq_False}; fun bool_subst_tac ctxt i = - REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i) - THEN REPEAT (dresolve_tac boolD i) - THEN REPEAT (eresolve_tac boolE i) + REPEAT (EqSubst.eqsubst_asm_tac ctxt [1] eqBool i) + THEN REPEAT (dresolve_tac boolD i) + THEN REPEAT (eresolve_tac boolE i) fun mk_bool_elims ctxt elim = - let val tac = ALLGOALS (bool_subst_tac ctxt) - fun mk_bool_elim b = - elim - |> Thm.forall_elim b - |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1)) - |> Tactic.rule_by_tactic ctxt tac + let + val tac = ALLGOALS (bool_subst_tac ctxt); + fun mk_bool_elim b = + elim + |> Thm.forall_elim b + |> Tactic.rule_by_tactic ctxt (TRY (resolve_tac eqBoolI 1)) + |> Tactic.rule_by_tactic ctxt tac; in - map mk_bool_elim [@{cterm True}, @{cterm False}] + map mk_bool_elim [@{cterm True}, @{cterm False}] end; in fun mk_partial_elim_rules ctxt result = let - val thy = Proof_Context.theory_of ctxt; + val thy = Proof_Context.theory_of ctxt; - val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, - termination, domintros, ...} = result; - val n_fs = length fs; + val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, + termination, domintros, ...} = result; + val n_fs = length fs; - fun mk_partial_elim_rule (idx,f) = - let fun mk_funeq 0 T (acc_vars, acc_lhs) = - let val y = Free("y",T) in - (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) - end - | mk_funeq n (Type(@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) = - let val xn = Free ("x" ^ Int.toString n,S) in - mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) - end - | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f])) + fun mk_partial_elim_rule (idx, f) = + let + fun mk_funeq 0 T (acc_vars, acc_lhs) = + let val y = Free("y", T) + in (y :: acc_vars, (HOLogic.mk_Trueprop (HOLogic.mk_eq (acc_lhs, y))), T) end + | mk_funeq n (Type (@{type_name "fun"}, [S, T])) (acc_vars, acc_lhs) = + let val xn = Free ("x" ^ Int.toString n, S) + in mk_funeq (n - 1) T (xn :: acc_vars, acc_lhs $ xn) end + | mk_funeq _ _ _ = raise (TERM ("Not a function.", [f])); - val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl - |> HOLogic.dest_Trueprop - |> dest_funprop |> fst |> fst) = f) - psimps + val f_simps = + filter (fn r => + (prop_of r |> Logic.strip_assums_concl + |> HOLogic.dest_Trueprop + |> dest_funprop |> fst |> fst) = f) + psimps; - val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl - |> HOLogic.dest_Trueprop - |> snd o fst o dest_funprop |> length; - val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([],f) - val (rhs_var, arg_vars) = case free_vars of x::xs => (x, rev xs) - val args = HOLogic.mk_tuple arg_vars; - val domT = R |> dest_Free |> snd |> hd o snd o dest_Type - - val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; - - val cprop = cterm_of thy prop + val arity = + hd f_simps + |> prop_of + |> Logic.strip_assums_concl + |> HOLogic.dest_Trueprop + |> snd o fst o dest_funprop + |> length; + val (free_vars,prop,ranT) = mk_funeq arity (fastype_of f) ([], f); + val (rhs_var, arg_vars) = (case free_vars of x :: xs => (x, rev xs)); + val args = HOLogic.mk_tuple arg_vars; + val domT = R |> dest_Free |> snd |> hd o snd o dest_Type; - val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; - val asms_thms = map Thm.assume asms; + val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args; + + val cprop = cterm_of thy prop; + + val asms = [cprop, cterm_of thy (HOLogic.mk_Trueprop (dom $ sumtree_inj))]; + val asms_thms = map Thm.assume asms; - fun prep_subgoal i = - REPEAT (eresolve_tac @{thms Pair_inject} i) - THEN Method.insert_tac (case asms_thms of - thm::thms => (thm RS sym) :: thms) i - THEN propagate_tac i - THEN TRY - ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i) - THEN bool_subst_tac ctxt i; + fun prep_subgoal i = + REPEAT (eresolve_tac @{thms Pair_inject} i) + THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i + THEN propagate_tac i + THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN atac i) + THEN bool_subst_tac ctxt i; - val tac = ALLGOALS prep_subgoal; + val tac = ALLGOALS prep_subgoal; - val elim_stripped = - nth cases idx - |> Thm.forall_elim @{cterm "P::bool"} - |> Thm.forall_elim (cterm_of thy args) - |> Tactic.rule_by_tactic ctxt tac - |> fold_rev Thm.implies_intr asms - |> Thm.forall_intr (cterm_of thy rhs_var) + val elim_stripped = + nth cases idx + |> Thm.forall_elim @{cterm "P::bool"} + |> Thm.forall_elim (cterm_of thy args) + |> Tactic.rule_by_tactic ctxt tac + |> fold_rev Thm.implies_intr asms + |> Thm.forall_intr (cterm_of thy rhs_var); - val bool_elims = (case ranT of - Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped - | _ => []); + val bool_elims = + (case ranT of + Type (@{type_name bool}, []) => mk_bool_elims ctxt elim_stripped + | _ => []); - fun unstrip rl = - rl |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm - (map (cterm_of thy) arg_vars)) - |> Thm.forall_intr @{cterm "P::bool"} - - in - map unstrip (elim_stripped :: bool_elims) - end; - + fun unstrip rl = + rl + |> (fn thm => List.foldr (uncurry Thm.forall_intr) thm (map (cterm_of thy) arg_vars)) + |> Thm.forall_intr @{cterm "P::bool"}; + in + map unstrip (elim_stripped :: bool_elims) + end; in map_index mk_partial_elim_rule fs end;