[isabelle-dev] Spontaneous disappearance of a fixed variable

[Florian Haftmann]

The attached patch (applicable e.g. on top of 5c68d06f97b3) exhibits a
situation (as can be seen from the included example theory) where a
context existing before entering a nested target is lost after existing
that nested target again.

This is the reason for the following paragraph in isar-ref, §5.7:
»Due to a technical limitation, the specific context of a interpretation
given by a for clause can get lost between a defines and rewrites clause
and must then be recovered manually using explicit sort constraints and
quantified term variables.«

I have no idea where this stems from, but maybe in the sandwich
* background theory
* implementing target
* surface context of implementing target
* proof context (fixes / assumes) (x)
* nested target
the layer marked with (x) is just not supposed to be present.

The observable behaviour is of rather minor relevance and definitely no
show stopper for the upcoming release, but I wanted to have it reported
here.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
-------------- next part --------------
# HG changeset patch
# Parent 7751b7054eedde06b214c05f2f45e56794dbe9f7
diagnostic output for fixed variables

diff -r 7751b7054eed src/HOL/Example.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Example.thy	Sat Dec 19 17:17:59 2015 +0100
@@ -0,0 +1,23 @@
+theory Example
+imports HOL
+begin
+
+definition
+  "id x = x"
+
+locale involutory =
+  fixes f :: "'a \<Rightarrow> 'a"
+  assumes involutory: "f (f x) = x"
+
+global_interpretation nonsense: involutory id for x :: 'a
+  defines nonsense = "id x" -- \<open>
+    Fixed before nested target: x 
+    Fixed before definitions: x 
+    Fixed after definitions: x, nonsense 
+    Fixed after nested target: 
+  \<close>
+  by standard (simp add: id_def)
+
+print_theorems
+
+end
\ No newline at end of file
diff -r 7751b7054eed src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Sat Dec 19 17:02:57 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Sat Dec 19 17:17:59 2015 +0100
@@ -65,18 +65,25 @@
       Local_Theory.define ((b, mx), ((Thm.def_binding_optional b name, atts), rhs)) lthy';
   in (def, lthy'') end;
 
+fun diag_fixes s ctxt =
+  writeln ("Fixed " ^ s ^ ": " ^ commas (map fst (Variable.dest_fixes ctxt)));
+
 fun augment_with_defs prep_term [] deps ctxt = ([], ctxt)
       (*quasi-inhomogeneous type: definitions demand local theory rather than bare proof context*)
   | augment_with_defs prep_term raw_defs deps lthy =
       let
+        val _ = diag_fixes "before nested target" lthy;
         val (_, inner_lthy) =
           Local_Theory.open_target lthy
           ||> fold Locale.activate_declarations deps;
+        val _ = diag_fixes "before definitions" inner_lthy;
         val (inner_defs, inner_lthy') =
           fold_map (augment_with_def prep_term deps) raw_defs inner_lthy;
+        val _ = diag_fixes "after definitions" inner_lthy';
         val lthy' =
           inner_lthy'
           |> Local_Theory.close_target;
+        val _ = diag_fixes "after nested target" lthy';
         val def_eqns =
           map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
       in (def_eqns, lthy') end;
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20151222/592d3167/attachment.asc>