1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Perm
|
1170
|
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
|
5 |
ML {*
|
|
6 |
open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *)
|
|
7 |
fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty);
|
|
8 |
val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm});
|
|
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 {*
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
|
1170
|
13 |
(* TODO: full_name can be obtained from new_type_names with Datatype *)
|
|
14 |
fun define_raw_perms new_type_names full_tnames thy =
|
|
15 |
let
|
|
16 |
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
|
17 |
(* 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
|
18 |
val sorts = [];
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
"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
|
22 |
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
|
23 |
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
|
24 |
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
|
25 |
val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types);
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
26 |
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
|
27 |
val pi = Free ("pi", @{typ perm});
|
1164
|
28 |
fun perm_eq_constr i (cname, dts) =
|
|
29 |
let
|
|
30 |
val Ts = map (typ_of_dtyp descr sorts) dts;
|
|
31 |
val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts);
|
|
32 |
val args = map Free (names ~~ Ts);
|
|
33 |
val c = Const (cname, Ts ---> (nth_dtyp i));
|
|
34 |
fun perm_arg (dt, x) =
|
|
35 |
let val T = type_of x
|
|
36 |
in
|
|
37 |
if is_rec_type dt then
|
|
38 |
let val (Us, _) = strip_type T
|
|
39 |
in list_abs (map (pair "x") Us,
|
|
40 |
Free (nth perm_names_types' (body_index dt)) $ pi $
|
|
41 |
list_comb (x, map (fn (i, U) =>
|
|
42 |
(permute U) $ (minus_perm $ pi) $ Bound i)
|
|
43 |
((length Us - 1 downto 0) ~~ Us)))
|
|
44 |
end
|
|
45 |
else (permute T) $ pi $ x
|
|
46 |
end;
|
|
47 |
in
|
|
48 |
(Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
|
|
49 |
(Free (nth perm_names_types' i) $
|
|
50 |
Free ("pi", @{typ perm}) $ list_comb (c, args),
|
|
51 |
list_comb (c, map perm_arg (dts ~~ args)))))
|
|
52 |
end;
|
1170
|
53 |
fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs;
|
|
54 |
val perm_eqs = maps perm_eq descr;
|
|
55 |
val lthy =
|
|
56 |
Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
|
|
57 |
(* TODO: Use the version of prmrec that gives the names explicitely. *)
|
|
58 |
val (perm_ldef, lthy') =
|
|
59 |
Primrec.add_primrec
|
|
60 |
(map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy;
|
|
61 |
val perm_frees =
|
|
62 |
(distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef);
|
|
63 |
val perm_empty_thms =
|
|
64 |
let
|
|
65 |
val gl =
|
|
66 |
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
|
67 |
(map (fn ((perm, T), x) => HOLogic.mk_eq
|
|
68 |
(perm $ @{term "0 :: perm"} $ Free (x, T),
|
|
69 |
Free (x, T)))
|
|
70 |
(perm_frees ~~
|
|
71 |
map body_type perm_types ~~ perm_indnames)));
|
|
72 |
fun tac {context = ctxt, ...} =
|
|
73 |
EVERY [
|
|
74 |
indtac induct perm_indnames 1,
|
|
75 |
ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))
|
|
76 |
];
|
|
77 |
in
|
|
78 |
(List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names))
|
|
79 |
end;
|
|
80 |
val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"}
|
|
81 |
val pi1 = Free ("pi1", @{typ perm});
|
|
82 |
val pi2 = Free ("pi2", @{typ perm});
|
|
83 |
val perm_append_thms =
|
|
84 |
List.take ((split_conj_thm
|
|
85 |
(Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) []
|
|
86 |
(HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
|
87 |
(map (fn ((perm, T), x) =>
|
|
88 |
let
|
|
89 |
val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T)
|
|
90 |
val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T))
|
|
91 |
in HOLogic.mk_eq (lhs, rhs)
|
|
92 |
end)
|
|
93 |
(perm_frees ~~
|
|
94 |
map body_type perm_types ~~ perm_indnames))))
|
|
95 |
(fn _ => EVERY [indtac induct perm_indnames 1,
|
|
96 |
ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))),
|
|
97 |
length new_type_names);
|
|
98 |
fun tac ctxt perm_thms =
|
|
99 |
(Class.intro_classes_tac []) THEN (ALLGOALS (
|
|
100 |
simp_tac (@{simpset} addsimps perm_thms
|
|
101 |
)));
|
|
102 |
fun morphism phi = map (Morphism.thm phi);
|
|
103 |
in
|
|
104 |
Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy'
|
|
105 |
end
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
106 |
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
107 |
*}
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
108 |
|
1170
|
109 |
(* Test
|
|
110 |
atom_decl name
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
111 |
|
1170
|
112 |
datatype rtrm1 =
|
|
113 |
rVr1 "name"
|
|
114 |
| rAp1 "rtrm1" "rtrm1 list"
|
|
115 |
| rLm1 "name" "rtrm1"
|
|
116 |
| rLt1 "bp" "rtrm1" "rtrm1"
|
|
117 |
and bp =
|
|
118 |
BUnit
|
|
119 |
| BVr "name"
|
|
120 |
| BPr "bp" "bp"
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
121 |
|
1170
|
122 |
|
|
123 |
setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *}
|
|
124 |
print_theorems
|
|
125 |
*)
|
|
126 |
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
127 |
end
|