Re: [isabelle] Equivalent to schematic_lemma inside proof blocks

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

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.


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