Re: [isabelle] Two questions of a beginner



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
> > 
> > 
> 







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.