
diff -r 6fd072d3acd2 -r a228acf2907e Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Thu Feb 18 15:03:09 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Thu Feb 18 18:33:53 2010 +0100
@@ -1,5 +1,5 @@
 theory Fv
-imports "Nominal2_Atoms"
+imports "Nominal2_Atoms" "Abs"
 begin
 
 (* Bindings are given as a list which has a length being equal
@@ -80,12 +80,19 @@
   (* Copy from Term *)
   fun is_funtype (Type ("fun", [_, _])) = true
     | is_funtype _ = false;
+  (* Similar to one in USyntax *)
+  fun mk_pair (fst, snd) =
+    let val ty1 = fastype_of fst
+      val ty2 = fastype_of snd
+      val c = HOLogic.pair_const ty1 ty2
+    in c $ fst $ snd
+    end;
+
 *}
 
-
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
-fun define_raw_fv full_tname bindsall lthy =
+fun define_fv_alpha full_tname bindsall lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr, ...} = Datatype.the_info thy full_tname;
@@ -95,19 +102,26 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
-  fun fv_eq_constr i (cname, dts) bindcs =
+  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 fv_alpha_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 args = map Free (names ~~ Ts);
+      val names2 = Name.variant_list ("pi" :: names) (Datatype_Prop.make_tnames Ts);
+      val args2 = map Free (names2 ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
       val fv_c = nth fv_frees i;
-      fun fv_bind (NONE, i) =
+      val alpha = nth alpha_frees i;
+      fun fv_bind args (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' *)
             if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
             mk_single_atom (nth args i)
-        | fv_bind (SOME f, i) = f $ (nth args i);
+        | fv_bind args (SOME f, i) = f $ (nth args i);
       fun fv_arg ((dt, x), bindxs) =
         let
           val arg =
@@ -115,70 +129,64 @@
             (* TODO: we just assume everything can be 'atomized' *)
             if (is_funtype o fastype_of) x then mk_atoms x else
             HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
-          val sub = mk_union (map fv_bind bindxs)
+          val sub = mk_union (map (fv_bind args) bindxs)
         in
           mk_diff arg sub
         end;
-        val _ = tracing ("d" ^ string_of_int (length dts));
-        val _ = tracing (string_of_int (length args));
-        val _ = tracing (string_of_int (length bindcs));
+      val fv_eq = HOLogic.mk_Trueprop (HOLogic.mk_eq
+        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs))))
+      val alpha_rhs =
+        HOLogic.mk_Trueprop (alpha $ (list_comb (c, args)) $ (list_comb (c, args2)));
+      fun alpha_arg ((dt, bindxs), (arg, arg2)) =
+        if bindxs = [] then (
+          if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
+          else (HOLogic.mk_eq (arg, arg2)))
+        else
+          if is_rec_type dt then let
+            (* THE HARD CASE *)
+            val lhs_binds = mk_union (map (fv_bind args) bindxs);
+            val lhs = mk_pair (lhs_binds, arg);
+            val rhs_binds = mk_union (map (fv_bind args2) bindxs);
+            val rhs = mk_pair (rhs_binds, arg2);
+            val alpha = nth alpha_frees (body_index dt);
+            val fv = nth fv_frees (body_index dt);
+            val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ (Free ("pi", @{typ perm})) $ rhs;
+            val alpha_gen_t = Syntax.check_term lthy alpha_gen_pre
+          in
+            HOLogic.mk_exists ("pi", @{typ perm}, alpha_gen_t)
+          (* TODO Add some test that is makes sense *)
+          end else @{term "True"}
+      val alpha_lhss = map (HOLogic.mk_Trueprop o alpha_arg) (dts ~~ bindcs ~~ (args ~~ args2))
+      val alpha_eq = Logic.list_implies (alpha_lhss, alpha_rhs)
     in
-      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))
+      (fv_eq, alpha_eq)
     end;
-  fun fv_eq (i, (_, _, constrs)) binds = map2 (fv_eq_constr i) constrs binds;
-  val fv_eqs = flat (map2 fv_eq descr bindsall)
+  fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
+  val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+  val add_binds = map (fn x => (Attrib.empty_binding, x))
+  val (fvs, lthy') = (Primrec.add_primrec
+    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
+  val (alphas, lthy'') = (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) []
+     (add_binds alpha_eqs) [] lthy')
 in
-  (* The snd will be removed later *)
-  snd (Primrec.add_primrec
-    (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) fv_eqs lthy)
+  ((fvs, alphas), lthy'')
 end
 *}
 
-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
-*}
-
+(* tests
 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" [[[[]]]] *}
+local_setup {* define_fv_alpha "Fv.ty" [[[[]]]] *}
 print_theorems
-*)
+
 
 datatype rtrm1 =
   rVr1 "name"
@@ -199,15 +207,12 @@
 | "bv1 (BVr x) = {atom x}"
 | "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp1)"
 
-local_setup {* define_raw_fv "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
+setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Fv.rtrm1", "Fv.bp"] *}
+
+local_setup {* define_fv_alpha "Fv.rtrm1"
+  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(SOME @{term bv1}, 0)], [], [(SOME @{term bv1}, 0)]]],
    [[], [[]], [[], []]]] *}
 print_theorems
-
-local_setup {* define_alpha "Fv.rtrm1"
-  [[[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
-   [[], [[]], [[], []]]] *}
-print_theorems
-
+*)
 
 end




