Re: [isabelle] Using Simplifier.asm_rewrite

On Wed, 3 Feb 2016, Viorel Preoteasa wrote:

If I define in ML

val pair_a = @{term "(term for p, term for f)"};

and I apply the procedure described above all works well,
however if instead I define the pair as the right hand
side of a definition that contains the same term for the
pair, the simplification does not work. The "if" term stays

val pair_b =  Thm.term_of (Thm.rhs_of ( @{thm Test_Pair_def}));

The only difference between pair_a and pair_b seems to be the types. In pair_a there are simple type variables, while in pair_b there are schematic type variables.

Schematic type variables in goal states or terms that should be simplified are notorious for surprises. The quickest way to avoid that in the given example is to use Logic.unvarify_global on pair_b, but note that "global" operations don't work in local contexts, and locale contexts are the rule and not the exception.

Attached is the theory with the ML function implementing this simplification.

Some more notes after reading through this for 10min:

- always use formal antiquotation instead of literal string constants,
  e.g. @{const_name Trueprop}, @{type_name fun};

- observe maximum line length of 80-100 chars;

- never use hardwired Free variables like "Aux_Var", "u", "v", "w" in production code;

- see "implementation" manual ch. 0 about Isabelle/ML usage;

The manual provides general background information and a few examples, with important functions mentioned in the text as entry points to the sources. E.g. Variable.import, Variable.export, may help to get a feeling how the context discipline with locally fixed and exported schematic variables works.


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