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>
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>
diff
changeset
|
3 |
"../Nominal-General/Nominal2_Base"
|
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>
diff
changeset
|
4 |
"../Nominal-General/Nominal2_Atoms"
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
begin
|
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
|
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>
diff
changeset
|
7 |
|
|
1910
|
8 |
(* permutations for quotient types *)
|
|
1899
|
9 |
|
|
2144
|
10 |
ML {* Class_Target.prove_instantiation_exit_result *}
|
|
|
11 |
|
|
1253
|
12 |
ML {*
|
|
1903
|
13 |
fun quotient_lift_consts_export qtys spec ctxt =
|
|
|
14 |
let
|
|
|
15 |
val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
|
|
|
16 |
val (ts_loc, defs_loc) = split_list result;
|
|
|
17 |
val morphism = ProofContext.export_morphism ctxt' ctxt;
|
|
|
18 |
val ts = map (Morphism.term morphism) ts_loc
|
|
|
19 |
val defs = Morphism.fact morphism defs_loc
|
|
|
20 |
in
|
|
|
21 |
(ts, defs, ctxt')
|
|
|
22 |
end
|
|
|
23 |
*}
|
|
|
24 |
|
|
|
25 |
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
|
26 |
fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
|
|
1253
|
27 |
let
|
|
|
28 |
val lthy =
|
|
|
29 |
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
|
30 |
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
|
31 |
val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
|
|
1253
|
32 |
fun tac _ =
|
|
|
33 |
Class.intro_classes_tac [] THEN
|
|
|
34 |
(ALLGOALS (resolve_tac lifted_thms))
|
|
|
35 |
val lthy'' = Class.prove_instantiation_instance tac lthy'
|
|
|
36 |
in
|
|
|
37 |
Local_Theory.exit_global lthy''
|
|
|
38 |
end
|
|
|
39 |
*}
|
|
|
40 |
|
|
1342
|
41 |
ML {*
|
|
|
42 |
fun neq_to_rel r neq =
|
|
|
43 |
let
|
|
|
44 |
val neq = HOLogic.dest_Trueprop (prop_of neq)
|
|
|
45 |
val eq = HOLogic.dest_not neq
|
|
|
46 |
val (lhs, rhs) = HOLogic.dest_eq eq
|
|
|
47 |
val rel = r $ lhs $ rhs
|
|
|
48 |
val nrel = HOLogic.mk_not rel
|
|
|
49 |
in
|
|
|
50 |
HOLogic.mk_Trueprop nrel
|
|
|
51 |
end
|
|
|
52 |
*}
|
|
|
53 |
|
|
|
54 |
ML {*
|
|
|
55 |
fun neq_to_rel_tac cases distinct =
|
|
|
56 |
rtac notI THEN' eresolve_tac cases THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct)
|
|
|
57 |
*}
|
|
|
58 |
|
|
|
59 |
ML {*
|
|
|
60 |
fun distinct_rel ctxt cases (dists, rel) =
|
|
|
61 |
let
|
|
|
62 |
val ((_, thms), ctxt') = Variable.import false dists ctxt
|
|
|
63 |
val terms = map (neq_to_rel rel) thms
|
|
|
64 |
val nrels = map (fn t => Goal.prove ctxt' [] [] t (fn _ => neq_to_rel_tac cases dists 1)) terms
|
|
|
65 |
in
|
|
|
66 |
Variable.export ctxt' ctxt nrels
|
|
|
67 |
end
|
|
|
68 |
*}
|
|
|
69 |
|
|
|
70 |
|
|
|
71 |
|
|
1899
|
72 |
(* Test *)
|
|
1910
|
73 |
(*
|
|
|
74 |
atom_decl name
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
75 |
|
1896
996d4411e95e
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
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
|
77 |
Var "name"
|
|
1910
|
78 |
| 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
|
79 |
| 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
|
80 |
| Let "bp" "trm" "trm"
|
|
1170
|
81 |
and bp =
|
|
|
82 |
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
|
83 |
| 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
|
84 |
| BPair "bp" "bp"
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
85 |
|
|
1899
|
86 |
setup {* fn thy =>
|
|
|
87 |
let
|
|
1910
|
88 |
val info = Datatype.the_info thy "Perm.trm"
|
|
1899
|
89 |
in
|
|
1910
|
90 |
define_raw_perms info 2 thy |> snd
|
|
1899
|
91 |
end
|
|
|
92 |
*}
|
|
1170
|
93 |
|
|
|
94 |
print_theorems
|
|
|
95 |
*)
|
|
|
96 |
|
1159
3c6bee89d826
Ported Stefan's permutation code, still needs some localizing.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
97 |
end
|