1 theory Perm |
1 theory Perm |
2 imports "../Nominal-General/Nominal2_Atoms" |
2 imports "../Nominal-General/Nominal2_Atoms" |
3 begin |
3 begin |
4 |
4 |
5 |
5 (* definitions of the permute function for raw nominal datatypes *) |
6 |
6 |
7 ML {* |
7 |
8 fun prove_perm_zero lthy induct perm_def perm_frees = |
8 ML {* |
9 let |
9 (* returns the type of the nth datatype *) |
10 val perm_types = map fastype_of perm_frees; |
|
11 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
12 fun glc ((perm, T), x) = |
|
13 HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
14 val gl = |
|
15 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
16 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); |
|
17 fun tac _ = |
|
18 EVERY [ |
|
19 Datatype_Aux.indtac induct perm_indnames 1, |
|
20 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
|
21 ]; |
|
22 in |
|
23 Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
|
24 end; |
|
25 *} |
|
26 |
|
27 ML {* |
|
28 fun prove_perm_plus lthy induct perm_def perm_frees = |
|
29 let |
|
30 val pi1 = Free ("pi1", @{typ perm}); |
|
31 val pi2 = Free ("pi2", @{typ perm}); |
|
32 val perm_types = map fastype_of perm_frees |
|
33 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
34 fun glc ((perm, T), x) = |
|
35 HOLogic.mk_eq ( |
|
36 perm $ (mk_plus pi1 pi2) $ Free (x, T), |
|
37 perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
|
38 val goal = |
|
39 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
40 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
|
41 fun tac _ = |
|
42 EVERY [ |
|
43 Datatype_Aux.indtac induct perm_indnames 1, |
|
44 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
|
45 ] |
|
46 in |
|
47 Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac) |
|
48 end; |
|
49 *} |
|
50 |
|
51 |
|
52 (* definitions of the permute function for a raw nominal datatype *) |
|
53 |
|
54 ML {* |
|
55 fun nth_dtyp dt_descr sorts i = |
10 fun nth_dtyp dt_descr sorts i = |
56 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
11 Datatype_Aux.typ_of_dtyp dt_descr sorts (Datatype_Aux.DtRec i); |
57 *} |
12 *} |
58 |
13 |
59 ML {* |
14 ML {* |
91 (Attrib.empty_binding, eq) |
46 (Attrib.empty_binding, eq) |
92 end |
47 end |
93 *} |
48 *} |
94 |
49 |
95 ML {* |
50 ML {* |
|
51 fun prove_permute_zero lthy induct perm_defs perm_fns = |
|
52 let |
|
53 val perm_types = map (body_type o fastype_of) perm_fns |
|
54 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
55 |
|
56 fun single_goal ((perm_fn, T), x) = |
|
57 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
58 |
|
59 val goals = |
|
60 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
61 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
62 |
|
63 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
|
64 |
|
65 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
66 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
67 in |
|
68 Goal.prove lthy perm_indnames [] goals (K tac) |
|
69 |> Datatype_Aux.split_conj_thm |
|
70 end |
|
71 *} |
|
72 |
|
73 ML {* |
|
74 fun prove_permute_plus lthy induct perm_defs perm_fns = |
|
75 let |
|
76 val pi1 = Free ("p", @{typ perm}) |
|
77 val pi2 = Free ("q", @{typ perm}) |
|
78 val perm_types = map (body_type o fastype_of) perm_fns |
|
79 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
80 |
|
81 fun single_goal ((perm, T), x) = HOLogic.mk_eq |
|
82 (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
|
83 |
|
84 val goals = |
|
85 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
86 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
87 |
|
88 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
|
89 |
|
90 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
91 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
92 in |
|
93 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
94 |> Datatype_Aux.split_conj_thm |
|
95 end |
|
96 *} |
|
97 |
|
98 ML {* |
96 (* defines the permutation functions for raw datatypes and |
99 (* defines the permutation functions for raw datatypes and |
97 proves that they are instances of pt |
100 proves that they are instances of pt |
|
101 |
|
102 dt_nos refers to the number of "un-unfolded" datatypes |
|
103 given by the user |
98 *) |
104 *) |
99 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy = |
105 fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy = |
100 let |
106 let |
101 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
107 val {descr as dt_descr, induct, sorts, ...} = dt_info; |
102 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
108 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
115 val perm_eqs = maps perm_eq dt_descr; |
121 val perm_eqs = maps perm_eq dt_descr; |
116 |
122 |
117 val lthy = |
123 val lthy = |
118 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
124 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
119 |
125 |
120 val ((perm_frees, perm_ldef), lthy') = |
126 val ((perm_fns, perm_ldef), lthy') = |
121 Primrec.add_primrec |
127 Primrec.add_primrec |
122 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
128 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
123 |
129 |
124 val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees |
130 val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns |
125 val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees |
131 val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns |
126 val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); |
132 val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); |
127 val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) |
133 val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) |
128 val perms_name = space_implode "_" perm_fn_names |
134 val perms_name = space_implode "_" perm_fn_names |
129 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
135 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
130 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
136 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
131 |
137 |
132 fun tac _ (_, simps, _) = |
138 fun tac _ (_, simps, _) = |
133 (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps); |
139 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
134 |
140 |
135 fun morphism phi (dfs, simps, fvs) = |
141 fun morphism phi (dfs, simps, fvs) = |
136 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
142 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
137 in |
143 in |
138 lthy' |
144 lthy' |
139 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
145 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
140 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
146 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
141 |> Class_Target.prove_instantiation_exit_result morphism tac |
147 |> Class_Target.prove_instantiation_exit_result morphism tac |
142 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees) |
148 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns) |
143 end |
149 end |
144 *} |
150 *} |
145 |
151 |
146 (* Test *) |
152 (* permutations for quotient types *) |
147 (*atom_decl name |
|
148 |
|
149 datatype trm = |
|
150 Var "name" |
|
151 | App "trm" "trm list" |
|
152 | Lam "name" "trm" |
|
153 | Let "bp" "trm" "trm" |
|
154 and bp = |
|
155 BUnit |
|
156 | BVar "name" |
|
157 | BPair "bp" "bp" |
|
158 |
|
159 setup {* fn thy => |
|
160 let |
|
161 val info = Datatype.the_info thy "Perm.trm" |
|
162 in |
|
163 define_raw_perms info 2 thy |> snd |
|
164 end |
|
165 *} |
|
166 |
|
167 print_theorems |
|
168 *) |
|
169 |
153 |
170 ML {* |
154 ML {* |
171 fun quotient_lift_consts_export qtys spec ctxt = |
155 fun quotient_lift_consts_export qtys spec ctxt = |
172 let |
156 let |
173 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
157 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |