src/HOL/HOL.thy
changeset 61202 9e37178084c5
parent 61169 4de9ff3ea29a
child 61222 05d28dc76e5c
     1.1 --- a/src/HOL/HOL.thy	Sat Sep 19 22:32:26 2015 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 21 11:31:56 2015 +0200
     1.3 @@ -1691,6 +1691,32 @@
     1.4  \<close>
     1.5  
     1.6  
     1.7 +text{* Tagging a premise of a simp rule with ASSUMPTION forces the simplifier
     1.8 +not to simplify the argument and to solve it by an assumption. *}
     1.9 +
    1.10 +definition ASSUMPTION :: "bool \<Rightarrow> bool" where
    1.11 +"ASSUMPTION A \<equiv> A"
    1.12 +
    1.13 +lemma ASSUMPTION_cong[cong]: "ASSUMPTION A = ASSUMPTION A"
    1.14 +by (rule refl)
    1.15 +
    1.16 +lemma ASSUMPTION_I: "A \<Longrightarrow> ASSUMPTION A"
    1.17 +by(simp add: ASSUMPTION_def)
    1.18 +
    1.19 +lemma ASSUMPTION_D: "ASSUMPTION A \<Longrightarrow> A"
    1.20 +by(simp add: ASSUMPTION_def)
    1.21 +
    1.22 +setup {*
    1.23 +let
    1.24 +  val asm_sol = mk_solver "ASSUMPTION" (fn ctxt =>
    1.25 +    resolve_tac ctxt [@{thm ASSUMPTION_I}] THEN'
    1.26 +    resolve_tac ctxt (Simplifier.prems_of ctxt))
    1.27 +in
    1.28 +  map_theory_simpset (fn ctxt => Simplifier.addSolver (ctxt,asm_sol))
    1.29 +end
    1.30 +*}
    1.31 +
    1.32 +
    1.33  subsection \<open>Code generator setup\<close>
    1.34  
    1.35  subsubsection \<open>Generic code generator preprocessor setup\<close>