# HG changeset patch # User krauss # Date 1207672240 -7200 # Node ID c3e597a476fdba38dce01d119e34a720b5b6a4b6 # Parent 13bbc72fda45986736554feec596d70998a689fe Generic conversion and tactic "atomize_elim" to convert elimination rules to the object logic diff -r 13bbc72fda45 -r c3e597a476fd doc-src/IsarAdvanced/Functions/Thy/Functions.thy --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Tue Apr 08 15:47:15 2008 +0200 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy Tue Apr 08 18:30:40 2008 +0200 @@ -595,12 +595,12 @@ This is an arithmetic triviality, but unfortunately the @{text arith} method cannot handle this specific form of an elimination rule. However, we can use the method @{text - "elim_to_cases"} to do an ad-hoc conversion to a disjunction of + "atomize_elim"} to do an ad-hoc conversion to a disjunction of existentials, which can then be soved by the arithmetic decision procedure. Pattern compatibility and termination are automatic as usual. *} (*<*)ML "goals_limit := 10"(*>*) -apply elim_to_cases +apply atomize_elim apply arith apply auto done @@ -616,7 +616,7 @@ where "ev (2 * n) = True" | "ev (2 * n + 1) = False" -apply elim_to_cases +apply atomize_elim by arith+ termination by (relation "{}") simp @@ -649,7 +649,7 @@ | "gcd 0 y = y" | "x < y \ gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)" | "\ x < y \ gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)" -by (elim_to_cases, auto, arith) +by (atomize_elim, auto, arith) termination by lexicographic_order text {* diff -r 13bbc72fda45 -r c3e597a476fd src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Tue Apr 08 15:47:15 2008 +0200 +++ b/src/FOL/IFOL.thy Tue Apr 08 18:30:40 2008 +0200 @@ -17,6 +17,7 @@ "~~/src/Provers/eqsubst.ML" "~~/src/Provers/quantifier1.ML" "~~/src/Provers/project_rule.ML" + "~~/src/Tools/atomize_elim.ML" ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML") @@ -738,6 +739,22 @@ and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff +subsection {* Atomizing elimination rules *} + +setup AtomizeElim.setup + +lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)" +by rule iprover+ + +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" +by rule iprover+ + +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)" +by rule iprover+ + +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" .. + + subsection {* Calculational rules *} lemma forw_subst: "a = b ==> P(b) ==> P(a)" diff -r 13bbc72fda45 -r c3e597a476fd src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Apr 08 15:47:15 2008 +0200 +++ b/src/HOL/HOL.thy Tue Apr 08 18:30:40 2008 +0200 @@ -23,6 +23,7 @@ "~~/src/Provers/quantifier1.ML" ("simpdata.ML") "~~/src/Tools/random_word.ML" + "~~/src/Tools/atomize_elim.ML" "~~/src/Tools/induct.ML" "~~/src/Tools/code/code_name.ML" "~~/src/Tools/code/code_funcgr.ML" @@ -879,6 +880,22 @@ and [symmetric, defn] = atomize_all atomize_imp atomize_eq +subsubsection {* Atomizing elimination rules *} + +setup AtomizeElim.setup + +lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)" + by rule iprover+ + +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)" + by rule iprover+ + +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)" + by rule iprover+ + +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" .. + + subsection {* Package setup *} subsubsection {* Classical Reasoner setup *} diff -r 13bbc72fda45 -r c3e597a476fd src/HOL/Library/Countable.thy --- a/src/HOL/Library/Countable.thy Tue Apr 08 15:47:15 2008 +0200 +++ b/src/HOL/Library/Countable.thy Tue Apr 08 18:30:40 2008 +0200 @@ -121,7 +121,7 @@ obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0" | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n" | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n" -apply elim_to_cases +apply atomize_elim apply (insert int_cases[of z]) apply (auto simp:zsgn_def) apply (rule_tac x="nat (-z)" in exI, simp) diff -r 13bbc72fda45 -r c3e597a476fd src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 08 15:47:15 2008 +0200 +++ b/src/HOL/Tools/function_package/fundef_package.ML Tue Apr 08 18:30:40 2008 +0200 @@ -174,78 +174,6 @@ val setup_case_cong = DatatypePackage.interpretation case_cong - - -(* ad-hoc method to convert elimination-style goals to existential statements *) - -fun insert_int_goal thy subg st = - let - val goal = hd (prems_of st) - val (ps, imp) = dest_all_all goal - val cps = map (cterm_of thy) ps - - val imp_subg = fold (fn p => fn t => betapply (t,p)) ps subg - val new_subg = implies $ imp_subg $ imp - |> fold_rev mk_forall ps - |> cterm_of thy - |> assume - - val sg2 = imp_subg - |> fold_rev mk_forall ps - |> cterm_of thy - |> assume - - val t' = new_subg - |> fold forall_elim cps - |> Thm.elim_implies (fold forall_elim cps sg2) - |> fold_rev forall_intr cps - - val st' = implies_elim st t' - |> implies_intr (cprop_of sg2) - |> implies_intr (cprop_of new_subg) - in - Seq.single st' - end - -fun mk_cases_statement thy t = - let - fun mk_clause t = - let - val (qs, imp) = dest_all_all t - in - Logic.strip_imp_prems imp - |> map (ObjectLogic.atomize_term thy) - |> foldr1 HOLogic.mk_conj - |> fold_rev (fn Free (v,T) => fn t => HOLogic.mk_exists (v,T,t)) qs - end - - val (ps, imp) = dest_all_all t - in - Logic.strip_imp_prems imp - |> map mk_clause - |> foldr1 HOLogic.mk_disj - |> HOLogic.mk_Trueprop - |> fold_rev lambda ps - end - -fun elim_to_cases1 ctxt st = - let - val thy = theory_of_thm st - val [subg] = prems_of st - val cex = mk_cases_statement thy subg - in - (insert_int_goal thy cex - THEN REPEAT_ALL_NEW (Tactic.ematch_tac [disjE, exE, conjE]) 1 - THEN REPEAT (Goal.assume_rule_tac ctxt 1) - (* THEN REPEAT (etac thin_rl 1)*)) st - end - -fun elim_to_cases_tac ctxt = SELECT_GOAL (elim_to_cases1 ctxt) - -val elim_to_cases_setup = Method.add_methods - [("elim_to_cases", Method.ctxt_args (Method.SIMPLE_METHOD' o elim_to_cases_tac), - "convert elimination-style goal to a disjunction of existentials")] - (* setup *) val setup = @@ -254,7 +182,6 @@ "declaration of congruence rule for function definitions")] #> setup_case_cong #> FundefRelation.setup - #> elim_to_cases_setup val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory