*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Two questions of a beginner*From*: Peter Lammich <lammich at in.tum.de>*Date*: Fri, 18 Jan 2013 14:19:27 +0100*Cc*: Not Sure <kuerzn at googlemail.com>, Cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <52BA9A34-0C1E-4497-AD4D-757A6B398852@cam.ac.uk>*References*: <50F8ADCC.3080003@gmail.com> <52BA9A34-0C1E-4497-AD4D-757A6B398852@cam.ac.uk>

Hi, On Fr, 2013-01-18 at 12:19 +0000, Lawrence Paulson wrote: > The answer to your second question is to use a structured proof. Non-atomic premises are all but useless in the apply style. In a structured proof, you can use such a thing exactly like an inference rule. > Not an answer for a beginner: I'm frequently using the following code, that gives you a method rprems, that does exactly the requested thing (see examples below the code). We already discussed several times whether we should integrate this method into Isabelle (see separate post on devel-list) .. Peter ------------------------------- ML {* (* Resolve with premises. Copied and adjusted from Goal.assume_rule_tac. *) fun rprems_tac ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => let fun non_atomic (Const ("==>", _) $ _ $ _) = true | non_atomic (Const ("all", _) $ _) = true | non_atomic _ = false; val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal''); val ethms = Rs |> map (fn R => (Raw_Simplifier.norm_hhf (Thm.trivial R))); in eresolve_tac ethms i end ); (* Resolve with premise. Copied and adjusted from Goal.assume_rule_tac. *) fun rprem_tac n ctxt = Goal.norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) => let val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt; val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal'; val R = nth (Drule.strip_imp_prems goal'') (n - 1) val rl = Raw_Simplifier.norm_hhf (Thm.trivial R) in etac rl i end ); val setup = Method.setup @{binding rprems} (Scan.lift (Scan.option Parse.nat) >> (fn i => fn ctxt => SIMPLE_METHOD' ( case i of NONE => rprems_tac ctxt | SOME i => rprem_tac i ctxt )) ) "Resolve with premises" *} setup "setup" (* EXAMPLES: *) lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk> \<Longrightarrow> C" apply (rprems 2) -- "Explicitely specify number of premise" apply (rprems 1) . lemma "\<lbrakk> A\<Longrightarrow>B; B\<Longrightarrow>C; A \<rbrakk> \<Longrightarrow> C" apply (rprems) -- "Resolve with any matching premise, first to last, backtracking" apply (rprems) . -------------------------- > You will find plenty of Isabelle documentation here: http://isabelle.in.tum.de/documentation.html > > Larry Paulson > > > On 18 Jan 2013, at 02:05, Not Sure <kuerzn at googlemail.com> wrote: > > > > > > > Hi! > > > > I have two (plus one) questions: > > > > 1. blast, auto, ... are all GREAT! > > But is there a way (in ProofGeneral) to see the proofs found by these > > tools more detail? > > > > 2. If I have a non-atomic premise like: > > > > [| A ==> B ; ... |] ==> C > > > > how can I "use" it as a rule? > > > > I am looking for somethink like: > > > > apply (rule premise1) > > > > 3. Where could I have found answers to these questions? > > > > > > Thanks! > > > > > > Johannes > > > > >

**Follow-Ups**:**Re: [isabelle] Two questions of a beginner***From:*Makarius

**References**:**[isabelle] Two questions of a beginner***From:*Not Sure

**Re: [isabelle] Two questions of a beginner***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Two questions of a beginner
- Next by Date: Re: [isabelle] Trying to use "datatype" to restrict types of formulas used, getting error
- Previous by Thread: Re: [isabelle] Two questions of a beginner
- Next by Thread: Re: [isabelle] Two questions of a beginner
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list