1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Perm
|
1774
|
2 |
imports "../Nominal-General/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 |
|
1910
|
5 |
(* definitions of the permute function for raw nominal datatypes *)
|
1903
|
6 |
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
7 |
|
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
8 |
ML {*
|
1910
|
9 |
(* returns the type of the nth datatype *)
|
1899
|
10 |
fun nth_dtyp dt_descr sorts i =
|
|
11 |
Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i);
|
|
12 |
*}
|
|
13 |
|
|
14 |
ML {*
|
1966
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
15 |
(* generates for every datatype a name str ^ dt_name *)
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
16 |
fun prefix_dt_names dt_descr sorts str =
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
17 |
let
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
18 |
fun get_nth_name (i, _) =
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
19 |
Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
20 |
in
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
21 |
Datatype_Prop.indexify_names
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
22 |
(map (prefix str o get_nth_name) dt_descr)
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
23 |
end
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
24 |
*}
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
25 |
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
26 |
|
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
27 |
ML {*
|
1900
|
28 |
(* permutation function for one argument
|
|
29 |
|
1901
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
30 |
- in case the argument is recursive it returns
|
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
31 |
|
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
permute_fn p arg
|
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
33 |
|
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
34 |
- in case the argument is non-recursive it will build
|
1900
|
35 |
|
|
36 |
p o arg
|
|
37 |
|
|
38 |
*)
|
1899
|
39 |
fun perm_arg permute_fns pi (arg_dty, arg) =
|
|
40 |
if Datatype_Aux.is_rec_type arg_dty
|
1901
93dfd5a10e92
removed dead code (nominal cannot deal with argument types of constructors that are functions)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
41 |
then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
|
1900
|
42 |
else mk_perm pi arg
|
1899
|
43 |
*}
|
|
44 |
|
|
45 |
ML {*
|
1902
|
46 |
(* equation for permutation function for one constructor;
|
|
47 |
i is the index of the correspodning datatype *)
|
|
48 |
fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
|
1899
|
49 |
let
|
|
50 |
val pi = Free ("p", @{typ perm})
|
|
51 |
val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
|
|
52 |
val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
|
|
53 |
val args = map Free (arg_names ~~ arg_tys)
|
|
54 |
val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
|
|
55 |
val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)
|
|
56 |
val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))
|
|
57 |
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
|
|
58 |
in
|
|
59 |
(Attrib.empty_binding, eq)
|
|
60 |
end
|
|
61 |
*}
|
|
62 |
|
|
63 |
ML {*
|
1910
|
64 |
fun prove_permute_zero lthy induct perm_defs perm_fns =
|
|
65 |
let
|
|
66 |
val perm_types = map (body_type o fastype_of) perm_fns
|
|
67 |
val perm_indnames = Datatype_Prop.make_tnames perm_types
|
|
68 |
|
|
69 |
fun single_goal ((perm_fn, T), x) =
|
|
70 |
HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T))
|
|
71 |
|
|
72 |
val goals =
|
|
73 |
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
|
74 |
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
|
|
75 |
|
|
76 |
val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs)
|
|
77 |
|
|
78 |
val tac = (Datatype_Aux.indtac induct perm_indnames
|
|
79 |
THEN_ALL_NEW asm_simp_tac simps) 1
|
|
80 |
in
|
|
81 |
Goal.prove lthy perm_indnames [] goals (K tac)
|
|
82 |
|> Datatype_Aux.split_conj_thm
|
|
83 |
end
|
|
84 |
*}
|
|
85 |
|
|
86 |
ML {*
|
|
87 |
fun prove_permute_plus lthy induct perm_defs perm_fns =
|
|
88 |
let
|
|
89 |
val pi1 = Free ("p", @{typ perm})
|
|
90 |
val pi2 = Free ("q", @{typ perm})
|
|
91 |
val perm_types = map (body_type o fastype_of) perm_fns
|
|
92 |
val perm_indnames = Datatype_Prop.make_tnames perm_types
|
|
93 |
|
|
94 |
fun single_goal ((perm, T), x) = HOLogic.mk_eq
|
|
95 |
(perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
|
|
96 |
|
|
97 |
val goals =
|
|
98 |
HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
|
|
99 |
(map single_goal (perm_fns ~~ perm_types ~~ perm_indnames)))
|
|
100 |
|
|
101 |
val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs)
|
|
102 |
|
|
103 |
val tac = (Datatype_Aux.indtac induct perm_indnames
|
|
104 |
THEN_ALL_NEW asm_simp_tac simps) 1
|
|
105 |
in
|
|
106 |
Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac)
|
|
107 |
|> Datatype_Aux.split_conj_thm
|
|
108 |
end
|
|
109 |
*}
|
|
110 |
|
|
111 |
ML {*
|
1899
|
112 |
(* defines the permutation functions for raw datatypes and
|
|
113 |
proves that they are instances of pt
|
1910
|
114 |
|
|
115 |
dt_nos refers to the number of "un-unfolded" datatypes
|
|
116 |
given by the user
|
1899
|
117 |
*)
|
|
118 |
fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
|
1170
|
119 |
let
|
1899
|
120 |
val {descr as dt_descr, induct, sorts, ...} = dt_info;
|
|
121 |
val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
|
|
122 |
val full_tnames = List.take (all_full_tnames, dt_nos);
|
|
123 |
|
1966
b6b3374a402d
factured out common functionality of prefixing the dt-names with a string
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
|
1899
|
125 |
|
|
126 |
val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
|
|
127 |
|
|
128 |
val permute_fns = perm_fn_names ~~ perm_types
|
|
129 |
|
|
130 |
fun perm_eq (i, (_, _, constrs)) =
|
1902
|
131 |
map (perm_eq_constr dt_descr sorts permute_fns i) constrs;
|
1899
|
132 |
|
|
133 |
val perm_eqs = maps perm_eq dt_descr;
|
|
134 |
|
|
135 |
val lthy =
|
|
136 |
Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
|
|
137 |
|
1910
|
138 |
val ((perm_fns, perm_ldef), lthy') =
|
1899
|
139 |
Primrec.add_primrec
|
|
140 |
(map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
|
|
141 |
|
1910
|
142 |
val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
|
|
143 |
val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
|
1903
|
144 |
val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
|
|
145 |
val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
|
1899
|
146 |
val perms_name = space_implode "_" perm_fn_names
|
|
147 |
val perms_zero_bind = Binding.name (perms_name ^ "_zero")
|
1902
|
148 |
val perms_plus_bind = Binding.name (perms_name ^ "_plus")
|
1903
|
149 |
|
1899
|
150 |
fun tac _ (_, simps, _) =
|
1910
|
151 |
Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps)
|
1903
|
152 |
|
1899
|
153 |
fun morphism phi (dfs, simps, fvs) =
|
|
154 |
(map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs);
|
|
155 |
in
|
1910
|
156 |
lthy'
|
|
157 |
|> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
|
|
158 |
|> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
|
|
159 |
|> Class_Target.prove_instantiation_exit_result morphism tac
|
|
160 |
(perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
|
1899
|
161 |
end
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
162 |
*}
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
163 |
|
1910
|
164 |
(* permutations for quotient types *)
|
1899
|
165 |
|
1253
|
166 |
ML {*
|
1903
|
167 |
fun quotient_lift_consts_export qtys spec ctxt =
|
|
168 |
let
|
|
169 |
val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
|
|
170 |
val (ts_loc, defs_loc) = split_list result;
|
|
171 |
val morphism = ProofContext.export_morphism ctxt' ctxt;
|
|
172 |
val ts = map (Morphism.term morphism) ts_loc
|
|
173 |
val defs = Morphism.fact morphism defs_loc
|
|
174 |
in
|
|
175 |
(ts, defs, ctxt')
|
|
176 |
end
|
|
177 |
*}
|
|
178 |
|
|
179 |
ML {*
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
180 |
fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
|
1253
|
181 |
let
|
|
182 |
val lthy =
|
|
183 |
Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
184 |
val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
|
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
185 |
val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
|
1253
|
186 |
fun tac _ =
|
|
187 |
Class.intro_classes_tac [] THEN
|
|
188 |
(ALLGOALS (resolve_tac lifted_thms))
|
|
189 |
val lthy'' = Class.prove_instantiation_instance tac lthy'
|
|
190 |
in
|
|
191 |
Local_Theory.exit_global lthy''
|
|
192 |
end
|
|
193 |
*}
|
|
194 |
|
1342
|
195 |
ML {*
|
|
196 |
fun neq_to_rel r neq =
|
|
197 |
let
|
|
198 |
val neq = HOLogic.dest_Trueprop (prop_of neq)
|
|
199 |
val eq = HOLogic.dest_not neq
|
|
200 |
val (lhs, rhs) = HOLogic.dest_eq eq
|
|
201 |
val rel = r $ lhs $ rhs
|
|
202 |
val nrel = HOLogic.mk_not rel
|
|
203 |
in
|
|
204 |
HOLogic.mk_Trueprop nrel
|
|
205 |
end
|
|
206 |
*}
|
|
207 |
|
|
208 |
ML {*
|
|
209 |
fun neq_to_rel_tac cases distinct =
|
|
210 |
rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
|
|
211 |
*}
|
|
212 |
|
|
213 |
ML {*
|
|
214 |
fun distinct_rel ctxt cases (dists, rel) =
|
|
215 |
let
|
|
216 |
val ((_, thms), ctxt') = Variable.import false dists ctxt
|
|
217 |
val terms = map (neq_to_rel rel) thms
|
|
218 |
val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
|
|
219 |
in
|
|
220 |
Variable.export ctxt' ctxt nrels
|
|
221 |
end
|
|
222 |
*}
|
|
223 |
|
|
224 |
|
|
225 |
|
1899
|
226 |
(* Test *)
|
1910
|
227 |
(*
|
|
228 |
atom_decl name
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
229 |
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
230 |
datatype trm =
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
231 |
Var "name"
|
1910
|
232 |
| App "trm" "(trm list) list"
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
233 |
| Lam "name" "trm"
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
234 |
| Let "bp" "trm" "trm"
|
1170
|
235 |
and bp =
|
|
236 |
BUnit
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
237 |
| BVar "name"
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
238 |
| BPair "bp" "bp"
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
239 |
|
1899
|
240 |
setup {* fn thy =>
|
|
241 |
let
|
1910
|
242 |
val info = Datatype.the_info thy "Perm.trm"
|
1899
|
243 |
in
|
1910
|
244 |
define_raw_perms info 2 thy |> snd
|
1899
|
245 |
end
|
|
246 |
*}
|
1170
|
247 |
|
|
248 |
print_theorems
|
|
249 |
*)
|
|
250 |
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
251 |
end
|