# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1308741502 -3600
# Node ID 1264f2a21ea96354de164e022f6d54bf40f676de
# Parent  0599286b1e2a025bdc0bf9245eda548ccdd0df77
some rudimentary infrastructure for storing data about nominal datatypes

diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -3,6 +3,7 @@
 begin
 
 
+
 atom_decl name
 
 nominal_datatype lam =
@@ -10,11 +11,27 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+ML {* Method.SIMPLE_METHOD' *}
+ML {* Sign.intern_const *}
+
+ML {*
+val test:((Proof.context -> Method.method) context_parser) =
+Scan.succeed (fn ctxt =>
+ let
+   val _ = Inductive.the_inductive ctxt "Lambda.frees_lst_graph"
+ in 
+   Method.SIMPLE_METHOD' (K all_tac)
+ end)
+*}
+
+method_setup test = {* test *} {* test *}
 
 section {* free name function *}
 
 text {* first returns an atom list *}
 
+ML Thm.implies_intr
+
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
 where
diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -4,7 +4,14 @@
 
 section {*** Type Schemes ***}
 
-thm Set.set_mp Set.subsetD
+datatype foo =
+  Foo1
+| Foo2 bar
+and bar =
+  Bar
+
+ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *}
+
 
 atom_decl name 
 
@@ -16,10 +23,23 @@
 and tys =
   All xs::"name fset" ty::"ty" bind (set+) xs in ty
 
+ML {*
+get_all_info @{context}
+*}
+
+ML {*
+get_info @{context} "TypeSchemes.ty"
+*}
+
+ML {*
+#strong_exhaust (the_info @{context} "TypeSchemes.tys")
+*}
+
 thm ty_tys.distinct
 thm ty_tys.induct
 thm ty_tys.inducts
-thm ty_tys.exhaust ty_tys.strong_exhaust
+thm ty_tys.exhaust 
+thm ty_tys.strong_exhaust
 thm ty_tys.fv_defs
 thm ty_tys.bn_defs
 thm ty_tys.perm_simps
@@ -83,6 +103,7 @@
 apply (subst test3)
 defer
 apply rule*)
+thm subst_substs_graph.intros
 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)
diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/Nominal2.thy	Wed Jun 22 12:18:22 2011 +0100
@@ -10,8 +10,12 @@
      ("nominal_function_core.ML")
      ("nominal_mutual.ML")
      ("nominal_function.ML")
+     ("nominal_dt_data.ML")
 begin
 
+use "nominal_dt_data.ML"
+ML {* open Nominal_Dt_Data *}
+
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
@@ -139,6 +143,8 @@
 
 
 ML {*
+(* definition of the raw datatype *)
+
 fun define_raw_dts dts bn_funs bn_eqs bclauses lthy =
 let
   val thy = Local_Theory.exit_global lthy
@@ -459,7 +465,10 @@
   fun thms_suffix s = Binding.qualified true s thms_name 
   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
+  val infos = mk_infos qty_full_names qeq_iffs' qdistincts qstrong_exhaust_thms qstrong_induct_thms
+
   val (_, lthy9') = lthyC
+     |> Local_Theory.declaration false (K (fold register_info infos))
      |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
      ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/nominal_eqvt.ML
--- a/Nominal/nominal_eqvt.ML	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/nominal_eqvt.ML	Wed Jun 22 12:18:22 2011 +0100
@@ -109,6 +109,7 @@
       |> map zero_var_indexes
   end
 
+
 fun note_named_thm (name, thm) ctxt = 
   let
     val thm_name = Binding.qualified_name 
@@ -124,7 +125,7 @@
     val thy = ProofContext.theory_of ctxt
     val ({names, ...}, {preds, raw_induct, intrs, ...}) =
       Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
-     val thms = raw_equivariance preds raw_induct intrs ctxt 
+    val thms = raw_equivariance preds raw_induct intrs ctxt 
   in
     fold_map note_named_thm (names ~~ thms) ctxt |> snd
   end
diff -r 0599286b1e2a -r 1264f2a21ea9 Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Wed Jun 22 17:57:15 2011 +0900
+++ b/Nominal/nominal_function_core.ML	Wed Jun 22 12:18:22 2011 +0100
@@ -589,7 +589,7 @@
   let
     val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) =
       lthy
-      |> Local_Theory.conceal 
+      |> Local_Theory.conceal
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,