# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1266501789 -3600
# Node ID 6fd072d3acd28f91199710f7ea8e396c6e546aea
# Parent  15362b433d644c22faac98e669020acbf5ade844
First (non-working) version of alpha-equivalence

diff -r 15362b433d64 -r 6fd072d3acd2 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Thu Feb 18 13:36:38 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Thu Feb 18 15:03:09 2010 +0100
@@ -82,6 +82,7 @@
     | is_funtype _ = false;
 *}
 
+
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_raw_fv full_tname bindsall lthy =
@@ -100,7 +101,7 @@
       val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
       val args = map Free (names ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
-      val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
+      val fv_c = nth fv_frees i;
       fun fv_bind (NONE, i) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             (* TODO we assume that all can be 'atomized' *)
@@ -128,22 +129,56 @@
   fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
   val fv_eqs = flat (map2 fv_eq descr bindsall)
 in
+  (* The snd will be removed later *)
   snd (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
 end
 *}
 
-(* tests:
+ML {*
+fun define_alpha full_tname bindsall lthy =
+let
+  val thy = ProofContext.theory_of lthy;
+  val {descr, ...} = Datatype.the_info thy full_tname;
+  val sorts = []; (* TODO *)
+  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  val alpha_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
+    "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
+  val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
+  val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  fun alpha_eq_constr i (cname, dts) bindcs =
+    let
+      val Ts = map (typ_of_dtyp descr sorts) dts;
+      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
+      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+      val args = map Free (names ~~ Ts);
+      val args2 = map Free (names2 ~~ Ts);
+      val c = Const (cname, Ts ---> (nth_dtyp i));
+      val alpha = nth alpha_frees i;
+    in
+      (Attrib.empty_binding, HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2))))
+    end;
+  fun alpha_eq (i, (_, _, constrs)) binds = map2 (alpha_eq_constr i) constrs binds;
+  val alpha_eqs = flat (map2 alpha_eq descr bindsall)
+in
+  (* The snd will be removed later *)
+  snd (Inductive.add_inductive_i
+     {quiet_mode = false, verbose = true, alt_name = Binding.empty,
+      coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
+     (map2 (fn x => fn y => ((Binding.name x, y), NoSyn)) alpha_names alpha_types) [] (alpha_eqs) [] lthy)
+end
+*}
 
 atom_decl name
 
-datatype ty =
+(*datatype ty =
   Var "name set"
 
 ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
 
 local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *}
 print_theorems
+*)
 
 datatype rtrm1 =
   rVr1 "name"
@@ -169,6 +204,10 @@
    [[], [[]], [[], []]]] *}
 print_theorems
 
-*)
+local_setup {* define_alpha "Fv.rtrm1"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+   [[], [[]], [[], []]]] *}
+print_theorems
+
 
 end