# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283017507 -28800
# Node ID d2e929f51fa9457dbe37c0e7f1f93a073fb41d05
# Parent  217ef3e4282ed7fe99f14360957ed337bb1f73e2
added fs-instance proofs

diff -r 217ef3e4282e -r d2e929f51fa9 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 01:45:07 2010 +0800
@@ -37,17 +37,6 @@
 
 
 
-instantiation trm and assg :: fs
-begin
-
-instance
-apply(default)
-apply(simp_all add: single_let.fsupp)
-done
-
-end
-
-
 
 
 lemma test: 
diff -r 217ef3e4282e -r d2e929f51fa9 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/Ex/TypeSchemes.thy	Sun Aug 29 01:45:07 2010 +0800
@@ -19,14 +19,6 @@
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-instantiation ty2 :: fs
-begin
-
-instance 
-sorry
-
-end
-
 
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
diff -r 217ef3e4282e -r d2e929f51fa9 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/NewParser.thy	Sun Aug 29 01:45:07 2010 +0800
@@ -540,18 +540,23 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
-  (* Supports lemmas *) 
-
+  (* supports lemmas *) 
   val qsupports_thms =
     if get_STEPS lthy > 28
     then prove_supports lthyB qperm_simps qtrms
     else raise TEST lthyB
 
+  (* finite supp lemmas *)
   val qfsupp_thms =
     if get_STEPS lthy > 29
     then prove_fsupp lthyB qtys qinduct qsupports_thms
     else raise TEST lthyB
 
+  (* fs instances *)
+  val lthyC =
+    if get_STEPS lthy > 30
+    then fs_instance qtys qty_full_names tvs qfsupp_thms lthyB
+    else raise TEST lthyB
 
   (* noting the theorems *)  
 
@@ -560,7 +565,7 @@
     the_default (Binding.name (space_implode "_" qty_names)) opt_thms_name 
   fun thms_suffix s = Binding.qualified true s thms_name 
 
-  val (_, lthy9') = lthyB
+  val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
      ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
diff -r 217ef3e4282e -r d2e929f51fa9 Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Sun Aug 29 01:17:36 2010 +0800
+++ b/Nominal/nominal_dt_supp.ML	Sun Aug 29 01:45:07 2010 +0800
@@ -9,6 +9,9 @@
 sig
   val prove_supports: Proof.context -> thm list -> term list -> thm list  
   val prove_fsupp: Proof.context -> typ list -> thm -> thm list -> thm list
+
+  val fs_instance: typ list -> string list -> (string * sort) list -> thm list ->  
+    local_theory -> local_theory
 end
 
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
@@ -75,5 +78,25 @@
   |> map zero_var_indexes
 end
 
+
+(* finite supp instances *)
+
+fun fs_instance qtys qfull_ty_names tvs qfsupp_thms lthy =
+let
+  val lthy1 = 
+    lthy
+    |> Local_Theory.exit_global
+    |> Class.instantiation (qfull_ty_names, tvs, @{sort fs}) 
+  
+  fun tac _ =
+    Class.intro_classes_tac [] THEN
+      (ALLGOALS (resolve_tac qfsupp_thms))
+in
+  lthy1
+  |> Class.prove_instantiation_exit tac 
+  |> Named_Target.theory_init
+end
+
+
 end (* structure *)