Quot/Nominal/Perm.thy
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Thu, 25 Feb 2010 07:05:52 +0100
changeset 1257 fde1ddadc726
parent 1256 6c938f84880c
permissions -rw-r--r--
Export perm_frees.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
theory Perm
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     2
imports "Nominal2_Atoms"
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
begin
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     5
ML {*
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     6
  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     7
  fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     8
  val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
     9
*}
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
ML {*
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    12
fun prove_perm_empty lthy induct perm_def perm_frees =
1247
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    13
let
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    14
  val perm_types = map fastype_of perm_frees;
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    15
  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
1256
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    16
  fun glc ((perm, T), x) =
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    17
    HOLogic.mk_eq (perm $ @{term "0 :: perm"} $ Free (x, T), Free (x, T))
1247
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    18
  val gl =
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    19
    HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
1256
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    20
      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)));
1247
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    21
  fun tac _ =
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    22
    EVERY [
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    23
      indtac induct perm_indnames 1,
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    24
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def)))
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    25
    ];
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    26
in
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    27
  split_conj_thm (Goal.prove lthy perm_indnames [] gl tac)
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    28
end;
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    29
*}
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    30
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    31
ML {*
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    32
fun prove_perm_append lthy induct perm_def perm_frees =
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    33
let
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    34
  val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    35
  val pi1 = Free ("pi1", @{typ perm});
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    36
  val pi2 = Free ("pi2", @{typ perm});
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    37
  val perm_types = map fastype_of perm_frees
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    38
  val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
1256
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    39
  fun glc ((perm, T), x) =
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    40
    HOLogic.mk_eq (
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    41
      perm $ (add_perm $ pi1 $ pi2) $ Free (x, T),
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    42
      perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    43
  val gl =
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    44
    (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
1256
6c938f84880c Restructuring the code in Perm
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1253
diff changeset
    45
      (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))))
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    46
  fun tac _ =
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    47
    EVERY [
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    48
      indtac induct perm_indnames 1,
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    49
      ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def)))
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    50
    ]
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    51
in
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    52
  split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac)
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    53
end;
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
    54
*}
1247
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    55
a728e199851d Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1189
diff changeset
    56
ML {*
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    57
(* TODO: full_name can be obtained from new_type_names with Datatype *)
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    58
fun define_raw_perms new_type_names full_tnames thy =
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    59
let
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    60
  val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames);
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
  (* TODO: [] should be the sorts that we'll take from the specification *)
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
  val sorts = [];
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
  val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) =>
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
    "permute_" ^ name_of_typ (nth_dtyp i)) descr);
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
  val perm_types = map (fn (i, _) =>
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
    let val T = nth_dtyp i
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
    in @{typ perm} --> T --> T end) descr;
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  val perm_names_types' = perm_names' ~~ perm_types;
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
  val pi = Free ("pi", @{typ perm});
1164
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    71
  fun perm_eq_constr i (cname, dts) =
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    72
    let
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    73
      val Ts = map (typ_of_dtyp descr sorts) dts;
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    74
      val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    75
      val args = map Free (names ~~ Ts);
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    76
      val c = Const (cname, Ts ---> (nth_dtyp i));
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    77
      fun perm_arg (dt, x) =
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    78
        let val T = type_of x
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    79
        in
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    80
          if is_rec_type dt then
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    81
            let val (Us, _) = strip_type T
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    82
            in list_abs (map (pair "x") Us,
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    83
              Free (nth perm_names_types' (body_index dt)) $ pi $
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    84
                list_comb (x, map (fn (i, U) =>
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    85
                  (permute U) $ (minus_perm $ pi) $ Bound i)
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    86
                  ((length Us - 1 downto 0) ~~ Us)))
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    87
            end
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    88
          else (permute T) $ pi $ x
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    89
        end;
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    90
    in
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    91
      (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    92
        (Free (nth perm_names_types' i) $
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    93
           Free ("pi", @{typ perm}) $ list_comb (c, args),
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    94
         list_comb (c, map perm_arg (dts ~~ args)))))
fe0a31cf30a0 Simplifying perm_eq
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1161
diff changeset
    95
    end;
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    96
    fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    97
    val perm_eqs = maps perm_eq descr;
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    98
    val lthy =
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
    99
      Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   100
    (* TODO: Use the version of prmrec that gives the names explicitely. *)
1257
fde1ddadc726 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1256
diff changeset
   101
    val ((perm_frees, perm_ldef), lthy') =
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   102
      Primrec.add_primrec
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   103
        (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
1248
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
   104
    val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names);
705afaaf6fb4 More refactoring and removed references to the global simpset in Perm.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1247
diff changeset
   105
    val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names)
1249
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   106
    val perms_name = space_implode "_" perm_names'
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   107
    val perms_zero_bind = Binding.name (perms_name ^ "_zero")
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   108
    val perms_append_bind = Binding.name (perms_name ^ "_append")
1257
fde1ddadc726 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1256
diff changeset
   109
    fun tac _ (_, simps, _) =
1253
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   110
      (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps));
1257
fde1ddadc726 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1256
diff changeset
   111
    fun morphism phi (dfs, simps, fvs) =
fde1ddadc726 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1256
diff changeset
   112
      (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   113
  in
1249
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   114
  lthy'
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   115
  |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms))
ea6a52a4f5bf Note the instance proofs, since they can be easily lifted.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1248
diff changeset
   116
  |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms))
1257
fde1ddadc726 Export perm_frees.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1256
diff changeset
   117
  |> Class_Target.prove_instantiation_exit_result morphism tac (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees)
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   118
  end
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
*}
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   121
1253
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   122
ML {*
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   123
fun define_lifted_perms full_tnames name_term_pairs thms thy =
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   124
let
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   125
  val lthy =
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   126
    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   127
  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   128
  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   129
  fun tac _ =
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   130
    Class.intro_classes_tac [] THEN
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   131
    (ALLGOALS (resolve_tac lifted_thms))
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   132
  val lthy'' = Class.prove_instantiation_instance tac lthy'
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   133
in
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   134
  Local_Theory.exit_global lthy''
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   135
end
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   136
*}
cff8a67691d2 Define lifted perms.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1249
diff changeset
   137
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   138
(* Test
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   139
atom_decl name
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   141
datatype rtrm1 =
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   142
  rVr1 "name"
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   143
| rAp1 "rtrm1" "rtrm1 list"
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   144
| rLm1 "name" "rtrm1"
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   145
| rLt1 "bp" "rtrm1" "rtrm1"
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   146
and bp =
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   147
  BUnit
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   148
| BVr "name"
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   149
| BPr "bp" "bp"
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
1170
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   151
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   152
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   153
print_theorems
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   154
*)
a7b4160ef463 Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1164
diff changeset
   155
1159
3c6bee89d826 Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
end