Generic conversion and tactic "atomize_elim" to convert elimination rules
authorkrauss
Tue Apr 08 18:30:40 2008 +0200 (2008-04-08)
changeset 26580c3e597a476fd
parent 26579 13bbc72fda45
child 26581 ed7f995b3c97
Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic
doc-src/IsarAdvanced/Functions/Thy/Functions.thy
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/HOL/Library/Countable.thy
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Tue Apr 08 15:47:15 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Tue Apr 08 18:30:40 2008 +0200
     1.3 @@ -595,12 +595,12 @@
     1.4    This is an arithmetic triviality, but unfortunately the
     1.5    @{text arith} method cannot handle this specific form of an
     1.6    elimination rule. However, we can use the method @{text
     1.7 -  "elim_to_cases"} to do an ad-hoc conversion to a disjunction of
     1.8 +  "atomize_elim"} to do an ad-hoc conversion to a disjunction of
     1.9    existentials, which can then be soved by the arithmetic decision procedure.
    1.10    Pattern compatibility and termination are automatic as usual.
    1.11  *}
    1.12  (*<*)ML "goals_limit := 10"(*>*)
    1.13 -apply elim_to_cases
    1.14 +apply atomize_elim
    1.15  apply arith
    1.16  apply auto
    1.17  done
    1.18 @@ -616,7 +616,7 @@
    1.19  where
    1.20    "ev (2 * n) = True"
    1.21  | "ev (2 * n + 1) = False"
    1.22 -apply elim_to_cases
    1.23 +apply atomize_elim
    1.24  by arith+
    1.25  termination by (relation "{}") simp
    1.26  
    1.27 @@ -649,7 +649,7 @@
    1.28  | "gcd 0 y = y"
    1.29  | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"
    1.30  | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"
    1.31 -by (elim_to_cases, auto, arith)
    1.32 +by (atomize_elim, auto, arith)
    1.33  termination by lexicographic_order
    1.34  
    1.35  text {*
     2.1 --- a/src/FOL/IFOL.thy	Tue Apr 08 15:47:15 2008 +0200
     2.2 +++ b/src/FOL/IFOL.thy	Tue Apr 08 18:30:40 2008 +0200
     2.3 @@ -17,6 +17,7 @@
     2.4    "~~/src/Provers/eqsubst.ML"
     2.5    "~~/src/Provers/quantifier1.ML"
     2.6    "~~/src/Provers/project_rule.ML"
     2.7 +  "~~/src/Tools/atomize_elim.ML"
     2.8    ("fologic.ML")
     2.9    ("hypsubstdata.ML")
    2.10    ("intprover.ML")
    2.11 @@ -738,6 +739,22 @@
    2.12    and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
    2.13  
    2.14  
    2.15 +subsection {* Atomizing elimination rules *}
    2.16 +
    2.17 +setup AtomizeElim.setup
    2.18 +
    2.19 +lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
    2.20 +by rule iprover+
    2.21 +
    2.22 +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
    2.23 +by rule iprover+
    2.24 +
    2.25 +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
    2.26 +by rule iprover+
    2.27 +
    2.28 +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
    2.29 +
    2.30 +
    2.31  subsection {* Calculational rules *}
    2.32  
    2.33  lemma forw_subst: "a = b ==> P(b) ==> P(a)"
     3.1 --- a/src/HOL/HOL.thy	Tue Apr 08 15:47:15 2008 +0200
     3.2 +++ b/src/HOL/HOL.thy	Tue Apr 08 18:30:40 2008 +0200
     3.3 @@ -23,6 +23,7 @@
     3.4    "~~/src/Provers/quantifier1.ML"
     3.5    ("simpdata.ML")
     3.6    "~~/src/Tools/random_word.ML"
     3.7 +  "~~/src/Tools/atomize_elim.ML"
     3.8    "~~/src/Tools/induct.ML"
     3.9    "~~/src/Tools/code/code_name.ML"
    3.10    "~~/src/Tools/code/code_funcgr.ML"
    3.11 @@ -879,6 +880,22 @@
    3.12    and [symmetric, defn] = atomize_all atomize_imp atomize_eq
    3.13  
    3.14  
    3.15 +subsubsection {* Atomizing elimination rules *}
    3.16 +
    3.17 +setup AtomizeElim.setup
    3.18 +
    3.19 +lemma atomize_exL[atomize_elim]: "(!!x. P x ==> Q) == ((EX x. P x) ==> Q)"
    3.20 +  by rule iprover+
    3.21 +
    3.22 +lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
    3.23 +  by rule iprover+
    3.24 +
    3.25 +lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
    3.26 +  by rule iprover+
    3.27 +
    3.28 +lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop A" ..
    3.29 +
    3.30 +
    3.31  subsection {* Package setup *}
    3.32  
    3.33  subsubsection {* Classical Reasoner setup *}
     4.1 --- a/src/HOL/Library/Countable.thy	Tue Apr 08 15:47:15 2008 +0200
     4.2 +++ b/src/HOL/Library/Countable.thy	Tue Apr 08 18:30:40 2008 +0200
     4.3 @@ -121,7 +121,7 @@
     4.4    obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
     4.5    | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
     4.6    | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
     4.7 -apply elim_to_cases
     4.8 +apply atomize_elim
     4.9  apply (insert int_cases[of z])
    4.10  apply (auto simp:zsgn_def)
    4.11  apply (rule_tac x="nat (-z)" in exI, simp)
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 08 15:47:15 2008 +0200
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Apr 08 18:30:40 2008 +0200
     5.3 @@ -174,78 +174,6 @@
     5.4  
     5.5  val setup_case_cong = DatatypePackage.interpretation case_cong
     5.6  
     5.7 -
     5.8 -
     5.9 -(* ad-hoc method to convert elimination-style goals to existential statements *)
    5.10 -
    5.11 -fun insert_int_goal thy subg st =
    5.12 -    let
    5.13 -      val goal = hd (prems_of st)
    5.14 -      val (ps, imp) = dest_all_all goal
    5.15 -      val cps = map (cterm_of thy) ps
    5.16 -
    5.17 -      val imp_subg = fold (fn p => fn t => betapply (t,p)) ps subg
    5.18 -      val new_subg = implies $ imp_subg $ imp
    5.19 -                      |> fold_rev mk_forall ps
    5.20 -                      |> cterm_of thy 
    5.21 -                      |> assume 
    5.22 -
    5.23 -      val sg2 = imp_subg
    5.24 -                 |> fold_rev mk_forall ps
    5.25 -                 |> cterm_of thy 
    5.26 -                 |> assume
    5.27 -
    5.28 -      val t' = new_subg
    5.29 -                |> fold forall_elim cps
    5.30 -                |> Thm.elim_implies (fold forall_elim cps sg2)
    5.31 -                |> fold_rev forall_intr cps
    5.32 -
    5.33 -      val st' = implies_elim st t'
    5.34 -                 |> implies_intr (cprop_of sg2)
    5.35 -                 |> implies_intr (cprop_of new_subg)
    5.36 -    in
    5.37 -      Seq.single st'
    5.38 -    end
    5.39 -
    5.40 -fun mk_cases_statement thy t =
    5.41 -    let
    5.42 -      fun mk_clause t = 
    5.43 -          let 
    5.44 -            val (qs, imp) = dest_all_all t
    5.45 -          in 
    5.46 -            Logic.strip_imp_prems imp
    5.47 -             |> map (ObjectLogic.atomize_term thy)
    5.48 -             |> foldr1 HOLogic.mk_conj
    5.49 -             |> fold_rev (fn Free (v,T) => fn t => HOLogic.mk_exists (v,T,t)) qs
    5.50 -          end
    5.51 -
    5.52 -      val (ps, imp) = dest_all_all t
    5.53 -    in 
    5.54 -      Logic.strip_imp_prems imp
    5.55 -       |> map mk_clause
    5.56 -       |> foldr1 HOLogic.mk_disj
    5.57 -       |> HOLogic.mk_Trueprop
    5.58 -       |> fold_rev lambda ps
    5.59 -    end
    5.60 -
    5.61 -fun elim_to_cases1 ctxt st =
    5.62 -    let
    5.63 -      val thy = theory_of_thm st
    5.64 -      val [subg] = prems_of st
    5.65 -      val cex = mk_cases_statement thy subg
    5.66 -    in
    5.67 -      (insert_int_goal thy cex
    5.68 -       THEN REPEAT_ALL_NEW (Tactic.ematch_tac [disjE, exE, conjE]) 1
    5.69 -       THEN REPEAT (Goal.assume_rule_tac ctxt 1)
    5.70 -    (*   THEN REPEAT (etac thin_rl 1)*)) st
    5.71 -    end
    5.72 -
    5.73 -fun elim_to_cases_tac ctxt = SELECT_GOAL (elim_to_cases1 ctxt)
    5.74 -
    5.75 -val elim_to_cases_setup = Method.add_methods
    5.76 -  [("elim_to_cases", Method.ctxt_args (Method.SIMPLE_METHOD' o elim_to_cases_tac),
    5.77 -    "convert elimination-style goal to a disjunction of existentials")]
    5.78 -
    5.79  (* setup *)
    5.80  
    5.81  val setup =
    5.82 @@ -254,7 +182,6 @@
    5.83        "declaration of congruence rule for function definitions")]
    5.84    #> setup_case_cong
    5.85    #> FundefRelation.setup
    5.86 -  #> elim_to_cases_setup
    5.87  
    5.88  val get_congs = FundefCtxTree.get_fundef_congs o Context.Theory
    5.89