Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic
--- 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 \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
| "\<not> x < y \<Longrightarrow> 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 {*
--- 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)"
--- 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 *}
--- 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)
--- 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