Re: [isabelle] print_cases shows non-existing schematic variable

On Wed, 22 Apr 2015, Lars Noschinski wrote:

After looking at the code a bit I was wondering, how the cases method manages to not declare the term bindings -- the term bindings are present in the cases and I could not find an obvious flag or similar which would hide the term bindings.

Things really happen in ~~/src/Pure/Isar/proof_context.ML at his point:

fun case_result c ctxt =
    val Rule_Cases.Case {fixes, ...} = c;
    val (ts, ctxt') = ctxt |> fold_map fix fixes;
    val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
    |> bind_terms (map drop_schematic binds)
    |> update_cases true (map (apsnd SOME) cases)
    |> pair (assumes, (binds, cases))

val apply_case = apfst fst oo case_result;

Later on in proof.ML, apply_case is turned into Proof.invoke_case, which is the Isabelle/ML definition of the Isar command 'case'.

The drop_schematic above drops term bindings that happen to contain left-over schematic variables, i.e. have not been properly determined by other means (further instantiation by the proof method etc.).

It is a classic Isar principle that proof text (and cases are part of that) cannot be schematic. When implementing these things about 15 years ago, I kept it rather simple by leaving schematic parts for informative purposes until the last moment. Something similar happens for schematic type variables, e.g. due to hidden polymorphism.

So instead of halting and catching fire due to schematic variables somewhere, things only fail late for situations where the user insists to make use of uninstantiated proof context elements. Note that the user may also choose to ignore the debatable case definitions, and proceed by other means.

Today, we have higher ambitions in comfort (also IDE support). I am trying to revisit all this for some years already, but again did not manage for Isabelle2015.


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