[isabelle-dev] ctxt --?--> simplifier

[Makarius]

On Thu, 14 Apr 2011, Walther Neuper wrote:

> searching for how Isabelle/Isar handles contexts, for instance, in
>
> lemma ctxt:
>  assumes asm1: "a = 1" and asm2: "b = -2"
>  shows "2 * a + b = (0::int)"
> using asm1 asm2 by (simp)
>
> I got stuck in reading the code somewhere at Expression.read_statement and 
> Element.activate.
>
> Who quickly has a precise pointer into the code ?

ML structures Expression and Element are high up in the hierarchy of 
modules that make up the full locality of logical entities and their 
interpretation in different contexts.  It would take a long way down until 
you reach the primitive thm.ML with its hyps field for internal 
representation of local facts.  But this is also more directly explained 
in the "implementation" manual, the technical term to look for is 
"hypotheses".

Assuming as usual that user code refrains from poking in internal things, 
like the thm hyps field or the main conclusion of a goal state, there is 
nothing special about the above situation.  The Simplifier gets a theorem, 
no more no less.


Here is your example again:

lemma ctxt:
   assumes asm1: "a = 1" and asm2: "b = -2"
   shows "2 * a + b = (0::int)"

   ML_val {* @{thm asm1}; @{thm asm2} *}

   using asm1 asm2 by (simp)

The printed "[.]" indicates that there are hidden hyps, but you never 
should look there or depend on that implementation detail of the kernel.


 	Makarius