improve on #126: workaround loss of qualification for type class assumption names (#127)

Author: dtraytel

ROOT

@@ -45,6 +45,7 @@ session Tests in "tests" = Case_Studies +
   sessions
     System_Fsub
     Operations
+    Infinitary_Lambda_Calculus
   directories
     "fixtures"
   theories

Tools/var_classes.ML

@@ -81,6 +81,10 @@ fun mk_class_for_bound b bound lthy =
     let
       val (class, lthy) = Local_Theory.background_theory_result (fn thy =>
         let
+          (*Work around loss of qualification in "class" axioms by replicating it in the name*)
+          val b' = fold_rev Binding.prefix_name
+            (map (suffix "_" o fst) (filter snd (Binding.path_of b))) b;
+
           fun mk_assumption name term = ((Binding.name name, []), single (term, []));
           val large = mk_assumption "large" (HOLogic.mk_Trueprop (mk_ordLeq
             (mk_card_of (mk_Field bound))
@@ -90,7 +94,7 @@ fun mk_class_for_bound b bound lthy =
             mk_regularCard (mk_card_of (HOLogic.mk_UNIV (Term.aT @{sort type})))
           ))
 
-          val (class, lthy) = Class_Declaration.class b [] [] [
+          val (class, lthy) = Class_Declaration.class b' [] [] [
             Element.Assumes [large, regular]
           ] thy;
         in (class, Local_Theory.exit_global lthy) end

tests/Case_Study_Regression_Tests.thy

@@ -1,10 +1,19 @@
 theory Case_Study_Regression_Tests
-  imports "Binders.MRBNF_Recursor" "System_Fsub.Pattern"
+  imports "Binders.MRBNF_Recursor" "System_Fsub.Pattern" "Infinitary_Lambda_Calculus.ILC"
 begin
 
 (* #72 *)
 binder_datatype (FVars: 'v, FTVars: 'tv) trm2 =
   Var 'v
   | Let "('tv, p::'v) pat" "('v, 'tv) trm2" t::"('v, 'tv) trm2" binds p in t
 
+(* #126 *)
+binder_datatype (FFVars: 'a) iterm2
+  = iVar 'a
+  | iApp "'a iterm2" "'a iterm2 stream"
+  | iLam "(xs::'a) stream" t::"'a iterm2" binds xs in t
+for
+  map: ivvsubst
+  subst: itvsubst
+
 end