diff -r 4b0563bc4b03 -r 7d8949da7d99 Quot/Nominal/Perm.thy
--- a/Quot/Nominal/Perm.thy	Wed Feb 24 17:32:43 2010 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,147 +0,0 @@
-theory Perm
-imports "Nominal2_Atoms"
-begin
-
-ML {*
-  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
-  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
-  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
-*}
-
-ML {*
-fun prove_perm_empty lthy induct perm_def perm_frees =
-let
-  val perm_types = map fastype_of perm_frees;
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
-  val gl =
-    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) => HOLogic.mk_eq
-          (perm $ @{term "0 :: perm"} $ Free (x, T),
-           Free (x, T)))
-       (perm_frees ~~
-        map body_type perm_types ~~ perm_indnames)));
-  fun tac _ =
-    EVERY [
-      indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
-    ];
-in
-  split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
-end;
-*}
-
-ML {*
-fun prove_perm_append lthy induct perm_def perm_frees =
-let
-  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
-  val pi1 = Free ("pi1", @{typ perm});
-  val pi2 = Free ("pi2", @{typ perm});
-  val perm_types = map fastype_of perm_frees
-  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
-  val gl =
-    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
-      (map (fn ((perm, T), x) =>
-          let
-            val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
-            val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
-          in HOLogic.mk_eq (lhs, rhs)
-          end)
-        (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
-  fun tac _ =
-    EVERY [
-      indtac induct perm_indnames 1,
-      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
-    ]
-in
-  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
-end;
-*}
-
-ML {*
-(* TODO: full_name can be obtained from new_type_names with Datatype *)
-fun define_raw_perms new_type_names full_tnames thy =
-let
-  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
-  (* TODO: [] should be the sorts that we'll take from the specification *)
-  val sorts = [];
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
-  val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
-    "permute_" ^ name_of_typ (nth_dtyp i)) descr);
-  val perm_types = map (fn (i, _) =>
-    let val T = nth_dtyp i
-    in @{typ perm} --> T --> T end) descr;
-  val perm_names_types' = perm_names' ~~ perm_types;
-  val pi = Free ("pi", @{typ perm});
-  fun perm_eq_constr i (cname, dts) =
-    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 c = Const (cname, Ts ---> (nth_dtyp i));
-      fun perm_arg (dt, x) =
-        let val T = type_of x
-        in
-          if is_rec_type dt then
-            let val (Us, _) = strip_type T
-            in list_abs (map (pair "x") Us,
-              Free (nth perm_names_types' (body_index dt)) $ pi $
-                list_comb (x, map (fn (i, U) =>
-                  (permute U) $ (minus_perm $ pi) $ Bound i)
-                  ((length Us - 1 downto 0) ~~ Us)))
-            end
-          else (permute T) $ pi $ x
-        end;
-    in
-      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (Free (nth perm_names_types' i) $
-           Free ("pi", @{typ perm}) $ list_comb (c, args),
-         list_comb (c, map perm_arg (dts ~~ args)))))
-    end;
-    fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
-    val perm_eqs = maps perm_eq descr;
-    val lthy =
-      Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-    (* TODO: Use the version of prmrec that gives the names explicitely. *)
-    val ((_, perm_ldef), lthy') =
-      Primrec.add_primrec
-        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
-    val perm_frees =
-      (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
-    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
-    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
-    val perms_name = space_implode "_" perm_names'
-    val perms_zero_bind = Binding.name (perms_name ^ "_zero")
-    val perms_append_bind = Binding.name (perms_name ^ "_append")
-    fun tac _ perm_thms =
-      (Class.intro_classes_tac []) THEN (ALLGOALS (
-        simp_tac (HOL_ss addsimps perm_thms
-      )));
-    fun morphism phi = map (Morphism.thm phi);
-  in
-  lthy'
-  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
-  |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
-  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms)
-  end
-
-*}
-
-(* Test
-atom_decl name
-
-datatype rtrm1 =
-  rVr1 "name"
-| rAp1 "rtrm1" "rtrm1 list"
-| rLm1 "name" "rtrm1"
-| rLt1 "bp" "rtrm1" "rtrm1"
-and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
-
-
-setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
-print_theorems
-*)
-
-end