# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308825039 -3600
# Node ID eda5aeb056a64f91ddf5aaad67b17bdfaa5cd9be
# Parent  4e04f38329e57211288b4f59e5225bf31e8a2ce1
fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package

diff -r 4e04f38329e5 -r eda5aeb056a6 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/Ex/TypeVarsTest.thy	Thu Jun 23 11:30:39 2011 +0100
@@ -38,11 +38,10 @@
 thm lam.fv_bn_eqvt
 thm lam.size_eqvt
 
-(* FIXME: only works for type variables 'a 'b 'c *)
 
-nominal_datatype ('a, 'b, 'c) psi =
+nominal_datatype ('alpha, 'beta, 'gamma) psi =
   PsiNil
-| Output "'a" "'a" "('a, 'b, 'c) psi" 
+| Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
 
 end
diff -r 4e04f38329e5 -r eda5aeb056a6 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/Nominal2.thy	Thu Jun 23 11:30:39 2011 +0100
@@ -239,7 +239,7 @@
 
   val _ = trace_msg (K "Proving distinct theorems...")
   val alpha_distincts = 
-    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_tys
+    mk_alpha_distincts lthy4 alpha_cases raw_distinct_thms alpha_trms raw_dt_names
 
   val _ = trace_msg (K "Proving eq-iff theorems...")
   val alpha_eq_iff = 
@@ -287,7 +287,7 @@
   val _ = trace_msg (K "Proving alpha implies bn...")
   val alpha_bn_imp_thms = 
     raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy5 
-  
+
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
     raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
diff -r 4e04f38329e5 -r eda5aeb056a6 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 23 11:30:39 2011 +0100
@@ -14,7 +14,7 @@
     term list * term list * thm list * thm list * thm * local_theory
 
   val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
-    term list -> typ list -> thm list
+    term list -> string list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> thm list
@@ -262,14 +262,15 @@
     val alpha_intros_loc = #intrs alphas;
     val alpha_cases_loc = #elims alphas;
     val phi = ProofContext.export_morphism lthy' lthy;
-
-    val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc
-    val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy  
-    val alpha_induct = Morphism.thm phi alpha_induct_loc;
+    
+    val all_alpha_trms = all_alpha_trms_loc
+      |> map (Morphism.term phi) 
+      |> map Type.legacy_freeze 
+    val alpha_induct = Morphism.thm phi alpha_induct_loc
     val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
     val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
 
-    val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms'
+    val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
   in
     (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
   end
@@ -279,17 +280,14 @@
 (** produces the distinctness theorems **)
 
 (* transforms the distinctness theorems of the constructors 
-   to "not-alphas" of the constructors *)
+   into "not-alphas" of the constructors *)
 fun mk_distinct_goal ty_trm_assoc neq =
   let
-    val (lhs, rhs) = 
-      neq
-      |> HOLogic.dest_Trueprop
-      |> HOLogic.dest_not
-      |> HOLogic.dest_eq
-    val ty = fastype_of lhs
+    val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = 
+      HOLogic.dest_not (HOLogic.dest_Trueprop neq)
+    val ty_str = fst (dest_Type (domain_type ty_eq))
   in
-    (lookup ty_trm_assoc ty) $ lhs $ rhs
+    Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs
     |> HOLogic.mk_not
     |> HOLogic.mk_Trueprop
   end
@@ -299,27 +297,19 @@
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
 
-fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
+fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
   let
-    (* proper import of type-variables does not work,
-       since then they are replaced by new variables, messing
-       up the ty_trm assoc list *)
-    val distinct_thms' = map Thm.legacy_freezeT distinct_thms
-    val ty_trm_assoc = alpha_tys ~~ alpha_trms
+    val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) alpha_trms)
 
     fun mk_alpha_distinct distinct_trm =
       let
-        val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt
         val goal = mk_distinct_goal ty_trm_assoc distinct_trm
     in
-      Goal.prove ctxt' [] [] goal 
+      Goal.prove ctxt [] [] goal 
         (K (distinct_tac cases_thms distinct_thms 1))
-      |> singleton (Variable.export ctxt' ctxt)
     end
-    
   in
-    map (mk_alpha_distinct o prop_of) distinct_thms'
-    |> map Thm.varifyT_global
+    map (mk_alpha_distinct o prop_of) distinct_thms
   end
 
 
@@ -657,17 +647,16 @@
 
 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
   let
-    val arg_ty = domain_type o fastype_of 
+    val arg_ty = fst o dest_Type o domain_type o fastype_of 
     val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
     fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 
     val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
     val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
     val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
-  
+
     val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
       @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
-
   in
     alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
       (K (asm_full_simp_tac ss)) ctxt
@@ -708,7 +697,6 @@
     THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
   end
 
-
 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
   let
     val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
@@ -718,15 +706,15 @@
         NONE => HOLogic.eq_const ty
       | SOME alpha => alpha 
   
-    fun fun_rel_app t1 t2 = 
+    fun fun_rel_app (t1, t2) = 
       Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
 
     fun prep_goal trm =
       trm
       |> strip_type o fastype_of
-      |>> map lookup
-      ||> lookup
-      |> uncurry (fold_rev fun_rel_app)
+      |> (fn (tys, ty) => tys @ [ty])
+      |> map lookup
+      |> foldr1 fun_rel_app
       |> (fn t => t $ trm $ trm)
       |> Syntax.check_term ctxt
       |> HOLogic.mk_Trueprop
diff -r 4e04f38329e5 -r eda5aeb056a6 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Jun 23 11:30:39 2011 +0100
@@ -281,15 +281,19 @@
 
     val (info, lthy'') = prove_termination_fun size_simps (Local_Theory.restore lthy')
  
-    val {fs, simps, inducts, ...} = info;
+    val {fs, simps, inducts, ...} = info; 
 
     val morphism = ProofContext.export_morphism lthy'' lthy
     val simps_exp = map (Morphism.thm morphism) (the simps)
     val inducts_exp = map (Morphism.thm morphism) (the inducts)
-
+    
     val (fvs', fv_bns') = chop (length fv_frees) fs
+
+    (* grafting the types so that they coincide with the input into the function package *)
+    val fvs'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fvs' fv_tys
+    val fv_bns'' = map2 (fn t => fn ty => Const (fst (dest_Const t), ty) ) fv_bns' fv_bn_tys
   in
-    (fvs', fv_bns', simps_exp, inducts_exp, lthy'')
+    (fvs'', fv_bns'', simps_exp, inducts_exp, lthy'')
   end