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 ML {* |
5 |
6 fun quotient_lift_consts_export qtys spec ctxt = |
|
7 let |
|
8 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
|
9 val (ts_loc, defs_loc) = split_list result; |
|
10 val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
11 val ts = map (Morphism.term morphism) ts_loc |
|
12 val defs = Morphism.fact morphism defs_loc |
|
13 in |
|
14 (ts, defs, ctxt') |
|
15 end |
|
16 *} |
|
17 |
6 |
18 ML {* |
7 ML {* |
19 fun prove_perm_zero lthy induct perm_def perm_frees = |
8 fun prove_perm_zero lthy induct perm_def perm_frees = |
20 let |
9 let |
21 val perm_types = map fastype_of perm_frees; |
10 val perm_types = map fastype_of perm_frees; |
130 |
119 |
131 val ((perm_frees, perm_ldef), lthy') = |
120 val ((perm_frees, perm_ldef), lthy') = |
132 Primrec.add_primrec |
121 Primrec.add_primrec |
133 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
122 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
134 |
123 |
135 val perm_zero_thms = List.take (prove_perm_zero lthy' induct perm_ldef perm_frees, dt_nos); |
124 val perm_zero_thms = prove_perm_zero lthy' induct perm_ldef perm_frees |
136 val perm_plus_thms = List.take (prove_perm_plus lthy' induct perm_ldef perm_frees, dt_nos) |
125 val perm_plus_thms = prove_perm_plus lthy' induct perm_ldef perm_frees |
|
126 val perm_zero_thms' = List.take (perm_zero_thms, dt_nos); |
|
127 val perm_plus_thms' = List.take (perm_plus_thms, dt_nos) |
137 val perms_name = space_implode "_" perm_fn_names |
128 val perms_name = space_implode "_" perm_fn_names |
138 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
129 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
139 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
130 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
|
131 |
140 fun tac _ (_, simps, _) = |
132 fun tac _ (_, simps, _) = |
141 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
133 (Class.intro_classes_tac []) THEN ALLGOALS (resolve_tac simps); |
|
134 |
142 fun morphism phi (dfs, simps, fvs) = |
135 fun morphism phi (dfs, simps, fvs) = |
143 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
136 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
144 in |
137 in |
145 lthy' |
138 lthy' |
146 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms)) |
139 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
147 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms)) |
140 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
148 |> Class_Target.prove_instantiation_exit_result morphism tac |
141 |> Class_Target.prove_instantiation_exit_result morphism tac |
149 (perm_ldef, (perm_zero_thms @ perm_plus_thms), perm_frees) |
142 (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_frees) |
150 end |
143 end |
151 *} |
144 *} |
152 |
145 |
153 (* Test *) |
146 (* Test *) |
154 (*atom_decl name |
147 (*atom_decl name |
173 |
166 |
174 print_theorems |
167 print_theorems |
175 *) |
168 *) |
176 |
169 |
177 ML {* |
170 ML {* |
|
171 fun quotient_lift_consts_export qtys spec ctxt = |
|
172 let |
|
173 val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt; |
|
174 val (ts_loc, defs_loc) = split_list result; |
|
175 val morphism = ProofContext.export_morphism ctxt' ctxt; |
|
176 val ts = map (Morphism.term morphism) ts_loc |
|
177 val defs = Morphism.fact morphism defs_loc |
|
178 in |
|
179 (ts, defs, ctxt') |
|
180 end |
|
181 *} |
|
182 |
|
183 ML {* |
178 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
184 fun define_lifted_perms qtys full_tnames name_term_pairs thms thy = |
179 let |
185 let |
180 val lthy = |
186 val lthy = |
181 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
187 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
182 val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy; |
188 val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy; |