equal
deleted
inserted
replaced
7 pt-class. |
7 pt-class. |
8 *) |
8 *) |
9 |
9 |
10 signature NOMINAL_DT_RAWPERM = |
10 signature NOMINAL_DT_RAWPERM = |
11 sig |
11 sig |
12 val define_raw_perms: string list -> typ list -> term list -> thm -> local_theory -> |
12 val define_raw_perms: string list -> typ list -> (string * sort) list -> term list -> thm -> |
13 (term list * thm list * thm list) * local_theory |
13 local_theory -> (term list * thm list * thm list) * local_theory |
14 end |
14 end |
15 |
15 |
16 |
16 |
17 structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = |
17 structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = |
18 struct |
18 struct |
88 in |
88 in |
89 (Attrib.empty_binding, eq) |
89 (Attrib.empty_binding, eq) |
90 end |
90 end |
91 |
91 |
92 |
92 |
93 fun define_raw_perms full_ty_names tys constrs induct_thm lthy = |
93 fun define_raw_perms full_ty_names tys tvs constrs induct_thm lthy = |
94 let |
94 let |
95 val perm_fn_names = full_ty_names |
95 val perm_fn_names = full_ty_names |
96 |> map Long_Name.base_name |
96 |> map Long_Name.base_name |
97 |> map (prefix "permute_") |
97 |> map (prefix "permute_") |
98 |
98 |
111 map (Morphism.thm phi) simps); |
111 map (Morphism.thm phi) simps); |
112 |
112 |
113 val ((perm_funs, perm_eq_thms), lthy') = |
113 val ((perm_funs, perm_eq_thms), lthy') = |
114 lthy |
114 lthy |
115 |> Local_Theory.exit_global |
115 |> Local_Theory.exit_global |
116 |> Class.instantiation (full_ty_names, [], @{sort pt}) |
116 |> Class.instantiation (full_ty_names, tvs, @{sort pt}) |
117 |> Primrec.add_primrec perm_fn_binds perm_eqs |
117 |> Primrec.add_primrec perm_fn_binds perm_eqs |
118 |
118 |
119 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
119 val perm_zero_thms = prove_permute_zero induct_thm perm_eq_thms perm_funs lthy' |
120 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
120 val perm_plus_thms = prove_permute_plus induct_thm perm_eq_thms perm_funs lthy' |
121 in |
121 in |