| author | Christian Urban <urbanc@in.tum.de> |
| Mon, 24 May 2010 20:02:37 +0100 | |
| changeset 2296 | 45a69c9cc4cc |
| parent 2288 | 3b83960f9544 |
| child 2297 | 9ca7b249760e |
| permissions | -rw-r--r-- |
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
theory Perm |
|
2288
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
2163
diff
changeset
|
2 |
imports |
|
3b83960f9544
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
Christian Urban <urbanc@in.tum.de>
parents:
2163
diff
changeset
|
3 |
"../Nominal-General/Nominal2_Base" |
| 2296 | 4 |
"../Nominal-General/Nominal2_Atoms" |
5 |
"Nominal2_FSet" |
|
6 |
uses ("nominal_dt_rawperm.ML")
|
|
7 |
("nominal_dt_rawfuns.ML")
|
|
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
begin |
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
|
| 2296 | 10 |
use "nominal_dt_rawperm.ML" |
11 |
use "nominal_dt_rawfuns.ML" |
|
|
2035
3622cae9b10e
to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1971
diff
changeset
|
12 |
|
| 2296 | 13 |
ML {*
|
14 |
open Nominal_Dt_RawPerm |
|
15 |
open Nominal_Dt_RawFuns |
|
16 |
*} |
|
17 |
||
18 |
ML {*
|
|
19 |
fun is_atom ctxt ty = |
|
20 |
Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
|
|
21 |
||
22 |
fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
|
|
23 |
| is_atom_set _ _ = false; |
|
24 |
||
25 |
fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
|
|
26 |
| is_atom_fset _ _ = false; |
|
27 |
||
28 |
fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
|
|
29 |
| is_atom_list _ _ = false |
|
30 |
||
31 |
||
32 |
(* functions for producing sets, fsets and lists of general atom type |
|
33 |
out from concrete atom types *) |
|
34 |
fun mk_atom_set t = |
|
35 |
let |
|
36 |
val ty = fastype_of t; |
|
37 |
val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
|
|
38 |
val img_ty = atom_ty --> ty --> @{typ "atom set"};
|
|
39 |
in |
|
40 |
Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
|
|
41 |
end |
|
42 |
||
43 |
fun mk_atom_fset t = |
|
44 |
let |
|
45 |
val ty = fastype_of t; |
|
46 |
val atom_ty = dest_fsetT ty --> @{typ "atom"};
|
|
47 |
val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
|
|
48 |
val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
|
|
49 |
in |
|
50 |
fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
|
|
51 |
end |
|
52 |
*} |
|
| 1910 | 53 |
(* permutations for quotient types *) |
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
54 |
|
| 2144 | 55 |
ML {* Class_Target.prove_instantiation_exit_result *}
|
56 |
||
| 1253 | 57 |
ML {*
|
| 1903 | 58 |
fun quotient_lift_consts_export qtys spec ctxt = |
59 |
let |
|
60 |
val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
|
61 |
val (ts_loc, defs_loc) = split_list result; |
|
62 |
val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
63 |
val ts = map (Morphism.term morphism) ts_loc |
|
64 |
val defs = Morphism.fact morphism defs_loc |
|
65 |
in |
|
66 |
(ts, defs, ctxt') |
|
67 |
end |
|
68 |
*} |
|
69 |
||
70 |
ML {*
|
|
|
1683
f78c820f67c3
Automatically lift theorems and constants only using the new quotient types. Requires new Isabelle.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1503
diff
changeset
|
71 |
fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
| 1253 | 72 |
let |
73 |
val lthy = |
|
74 |
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>
parents:
1503
diff
changeset
|
75 |
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>
parents:
1503
diff
changeset
|
76 |
val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms; |
| 1253 | 77 |
fun tac _ = |
78 |
Class.intro_classes_tac [] THEN |
|
79 |
(ALLGOALS (resolve_tac lifted_thms)) |
|
80 |
val lthy'' = Class.prove_instantiation_instance tac lthy' |
|
81 |
in |
|
82 |
Local_Theory.exit_global lthy'' |
|
83 |
end |
|
84 |
*} |
|
85 |
||
| 1342 | 86 |
ML {*
|
87 |
fun neq_to_rel r neq = |
|
88 |
let |
|
89 |
val neq = HOLogic.dest_Trueprop (prop_of neq) |
|
90 |
val eq = HOLogic.dest_not neq |
|
91 |
val (lhs, rhs) = HOLogic.dest_eq eq |
|
92 |
val rel = r $ lhs $ rhs |
|
93 |
val nrel = HOLogic.mk_not rel |
|
94 |
in |
|
95 |
HOLogic.mk_Trueprop nrel |
|
96 |
end |
|
97 |
*} |
|
98 |
||
99 |
ML {*
|
|
100 |
fun neq_to_rel_tac cases distinct = |
|
101 |
rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct) |
|
102 |
*} |
|
103 |
||
104 |
ML {*
|
|
105 |
fun distinct_rel ctxt cases (dists, rel) = |
|
106 |
let |
|
107 |
val ((_, thms), ctxt') = Variable.import false dists ctxt |
|
108 |
val terms = map (neq_to_rel rel) thms |
|
109 |
val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms |
|
110 |
in |
|
111 |
Variable.export ctxt' ctxt nrels |
|
112 |
end |
|
113 |
*} |
|
114 |
||
115 |
||
116 |
||
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
117 |
(* Test *) |
| 1910 | 118 |
(* |
119 |
atom_decl name |
|
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
120 |
|
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
121 |
datatype trm = |
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
122 |
Var "name" |
| 1910 | 123 |
| 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>
parents:
1871
diff
changeset
|
124 |
| Lam "name" "trm" |
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
125 |
| Let "bp" "trm" "trm" |
|
1170
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
126 |
and bp = |
|
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
127 |
BUnit |
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
128 |
| BVar "name" |
|
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
parents:
1871
diff
changeset
|
129 |
| BPair "bp" "bp" |
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
130 |
|
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
131 |
setup {* fn thy =>
|
|
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
132 |
let |
| 1910 | 133 |
val info = Datatype.the_info thy "Perm.trm" |
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
134 |
in |
| 1910 | 135 |
define_raw_perms info 2 thy |> snd |
|
1899
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
136 |
end |
|
8e0bfb14f6bf
optimised the code of define_raw_perm
Christian Urban <urbanc@in.tum.de>
parents:
1896
diff
changeset
|
137 |
*} |
|
1170
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
138 |
|
|
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
139 |
print_theorems |
|
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
140 |
*) |
|
a7b4160ef463
Wrapped the permutation code.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1164
diff
changeset
|
141 |
|
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
142 |
end |