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



On 22.04.2015 14:54, Makarius wrote:
> 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 =
>   let
>     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;
>   in
>     ctxt'
>     |> bind_terms (map drop_schematic binds)
>     |> update_cases true (map (apsnd SOME) cases)
>     |> pair (assumes, (binds, cases))
>   end;
>
> val apply_case = apfst fst oo case_result;
[...]
> 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.).
Oh, so that's indeed done by this mechanism. Thanks for the explanation.
(I was sure I had constructed a situation where "cases" produced
non-schematic bindings before, but was apparently not careful enough).

  -- Lars




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