Re: [isabelle] Equivalent to schematic_lemma inside proof blocks



Hi Makarius,

No, this seems to serve my purposes, although I would prefer not having to add the TERM marker manually.

Andreas

On 15/06/15 16:23, Makarius wrote:
On Mon, 18 May 2015, Andreas Lochbihler wrote:

Meanwhile, I found out how to do it in forward-reasoning style with guess inside a proof
block.

lemma start: "[| TERM x; foo x m; foo x m ==> thesis |] ==> thesis" by assumption

notepad begin
  have "TERM a_very_large_expression" by(simp add: term_def)
  then guess by(rule start)(rule syntactic_analysis_rules)+
  then have "foo a_very_large_expression (245 * x + 7 * y + 3)" by(rule
  foo_mono) simp
end

Of course, the computation performed by the syntactic_analysis_rules cannot be written
in Isar, but that's fine. The TERM expression is only needed to instantiate the
expression in the start rule. By slightly changing the start rule, I can even obtain an
abbreviation for the compound term as an equation during the guess step (without ever
having to write it down :-) ).

Does it mean everything works out, or are there pending questions? Almost arbitrary tricks
may be played.  The standard Isar policies merely try to make non-sense hard.

BTW, the canonical proof for "TERM x" is "." -- is is considered vacuous within
Isabelle/Pure.


     Makarius





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