14 (ts, defs, ctxt') |
14 (ts, defs, ctxt') |
15 end |
15 end |
16 *} |
16 *} |
17 |
17 |
18 ML {* |
18 ML {* |
19 fun prove_perm_empty lthy induct perm_def perm_frees = |
19 fun prove_perm_zero lthy induct perm_def perm_frees = |
20 let |
20 let |
21 val perm_types = map fastype_of perm_frees; |
21 val perm_types = map fastype_of perm_frees; |
22 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
22 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
23 fun glc ((perm, T), x) = |
23 fun glc ((perm, T), x) = |
24 HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
24 HOLogic.mk_eq (perm $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
34 Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
34 Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
35 end; |
35 end; |
36 *} |
36 *} |
37 |
37 |
38 ML {* |
38 ML {* |
39 fun prove_perm_append lthy induct perm_def perm_frees = |
39 fun prove_perm_plus lthy induct perm_def perm_frees = |
40 let |
40 let |
41 val pi1 = Free ("pi1", @{typ perm}); |
41 val pi1 = Free ("pi1", @{typ perm}); |
42 val pi2 = Free ("pi2", @{typ perm}); |
42 val pi2 = Free ("pi2", @{typ perm}); |
43 val perm_types = map fastype_of perm_frees |
43 val perm_types = map fastype_of perm_frees |
44 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
44 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
84 then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg |
84 then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg |
85 else mk_perm pi arg |
85 else mk_perm pi arg |
86 *} |
86 *} |
87 |
87 |
88 ML {* |
88 ML {* |
89 (* equation for permutation function for one constructor *) |
89 (* equation for permutation function for one constructor; |
90 fun perm_eq_constr thy dt_descr sorts permute_fns i (cnstr_name, dts) = |
90 i is the index of the correspodning datatype *) |
|
91 fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) = |
91 let |
92 let |
92 val pi = Free ("p", @{typ perm}) |
93 val pi = Free ("p", @{typ perm}) |
93 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
94 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
94 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
95 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
95 val args = map Free (arg_names ~~ arg_tys) |
96 val args = map Free (arg_names ~~ arg_tys) |
118 val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
119 val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
119 |
120 |
120 val permute_fns = perm_fn_names ~~ perm_types |
121 val permute_fns = perm_fn_names ~~ perm_types |
121 |
122 |
122 fun perm_eq (i, (_, _, constrs)) = |
123 fun perm_eq (i, (_, _, constrs)) = |
123 map (perm_eq_constr thy dt_descr sorts permute_fns i) constrs; |
124 map (perm_eq_constr dt_descr sorts permute_fns i) constrs; |
124 |
125 |
125 val perm_eqs = maps perm_eq dt_descr; |
126 val perm_eqs = maps perm_eq dt_descr; |
126 |
127 |
127 val lthy = |
128 val lthy = |
128 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
129 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
129 |
130 |
130 val ((perm_frees, perm_ldef), lthy') = |
131 val ((perm_frees, perm_ldef), lthy') = |
131 Primrec.add_primrec |
132 Primrec.add_primrec |
132 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
133 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
133 |
134 |
134 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, dt_nos); |
135 val perm_zero_thms = List.take (prove_perm_zero lthy' induct perm_ldef perm_frees, dt_nos); |
135 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, dt_nos) |
136 val perm_plus_thms = List.take (prove_perm_plus lthy' induct perm_ldef perm_frees, dt_nos) |
136 val perms_name = space_implode "_" perm_fn_names |
137 val perms_name = space_implode "_" perm_fn_names |
137 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
138 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
138 val perms_append_bind = Binding.name (perms_name ^ "_append") |
139 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
139 fun tac _ (_, simps, _) = |
140 fun tac _ (_, simps, _) = |
140 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
141 (Class.intro_classes_tac []) THEN (ALLGOALS (resolve_tac simps)); |
141 fun morphism phi (dfs, simps, fvs) = |
142 fun morphism phi (dfs, simps, fvs) = |
142 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
143 (map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps, map (Morphism.term phi) fvs); |
143 in |
144 in |
144 lthy' |
145 lthy' |
145 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
146 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms)) |
146 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
147 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms)) |
147 |> Class_Target.prove_instantiation_exit_result morphism tac |
148 |> Class_Target.prove_instantiation_exit_result morphism tac |
148 (perm_ldef, (perm_empty_thms @ perm_append_thms), perm_frees) |
149 (perm_ldef, (perm_zero_thms @ perm_plus_thms), perm_frees) |
149 end |
150 end |
150 *} |
151 *} |
151 |
152 |
152 (* Test *) |
153 (* Test *) |
153 (*atom_decl name |
154 (*atom_decl name |