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: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> |
12 val define_raw_perms: string list -> typ list -> term list -> thm -> theory -> |
13 (term list * thm list * thm list) * theory |
13 (term list * thm list * thm list) * 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 |
19 |
|
20 |
|
21 (* permutation function for one argument |
|
22 |
|
23 - in case the argument is recursive it returns |
|
24 |
|
25 permute_fn p arg |
|
26 |
|
27 - in case the argument is non-recursive it will return |
|
28 |
|
29 p o arg |
|
30 *) |
|
31 fun perm_arg permute_fn_frees p (arg_dty, arg) = |
|
32 if Datatype_Aux.is_rec_type arg_dty |
|
33 then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg |
|
34 else mk_perm p arg |
|
35 |
|
36 |
|
37 (* generates the equation for the permutation function for one constructor; |
|
38 i is the index of the corresponding datatype *) |
|
39 fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = |
|
40 let |
|
41 val p = Free ("p", @{typ perm}) |
|
42 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
|
43 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
44 val args = map Free (arg_names ~~ arg_tys) |
|
45 val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) |
|
46 val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) |
|
47 val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) |
|
48 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
49 in |
|
50 (Attrib.empty_binding, eq) |
|
51 end |
|
52 |
19 |
53 |
20 |
54 (** proves the two pt-type class properties **) |
21 (** proves the two pt-type class properties **) |
55 |
22 |
56 fun prove_permute_zero lthy induct perm_defs perm_fns = |
23 fun prove_permute_zero lthy induct perm_defs perm_fns = |
97 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
64 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
98 |> Datatype_Aux.split_conj_thm |
65 |> Datatype_Aux.split_conj_thm |
99 end |
66 end |
100 |
67 |
101 |
68 |
102 (* user_dt_nos refers to the number of "un-unfolded" datatypes |
69 fun mk_perm_eq ty_perm_assoc cnstr = |
103 given by the user |
|
104 *) |
|
105 fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy = |
|
106 let |
70 let |
107 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
71 fun lookup_perm p (ty, arg) = |
108 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
72 case (AList.lookup (op=) ty_perm_assoc ty) of |
|
73 SOME perm => perm $ p $ arg |
|
74 | NONE => Const (@{const_name permute}, perm_ty ty) $ p $ arg |
109 |
75 |
110 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
76 val p = Free ("p", @{typ perm}) |
111 val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
77 val (arg_tys, ty) = |
|
78 fastype_of cnstr |
|
79 |> strip_type |
|
80 |
|
81 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
82 val args = map Free (arg_names ~~ arg_tys) |
|
83 |
|
84 val lhs = lookup_perm p (ty, list_comb (cnstr, args)) |
|
85 val rhs = list_comb (cnstr, map (lookup_perm p) (arg_tys ~~ args)) |
|
86 |
|
87 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
88 in |
|
89 (Attrib.empty_binding, eq) |
|
90 end |
|
91 |
|
92 |
|
93 fun define_raw_perms full_ty_names tys constrs induct_thm thy = |
|
94 let |
|
95 val perm_fn_names = full_ty_names |
|
96 |> map Long_Name.base_name |
|
97 |> map (prefix "permute_") |
|
98 |
|
99 val perm_fn_types = map perm_ty tys |
112 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
100 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
|
101 val perm_fn_binds = map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names |
113 |
102 |
114 fun perm_eq (i, (_, _, constrs)) = |
103 val perm_eqs = map (mk_perm_eq (tys ~~ perm_fn_frees)) constrs |
115 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
|
116 |
|
117 val perm_eqs = maps perm_eq dt_descr; |
|
118 |
104 |
119 val lthy = |
105 val lthy = |
120 Class.instantiation (user_full_tnames, [], @{sort pt}) thy; |
106 Class.instantiation (full_ty_names, [], @{sort pt}) thy |
121 |
107 |
122 val ((perm_funs, perm_eq_thms), lthy') = |
108 val ((perm_funs, perm_eq_thms), lthy') = |
123 Primrec.add_primrec |
109 Primrec.add_primrec perm_fn_binds perm_eqs lthy; |
124 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
|
125 |
110 |
126 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
111 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
127 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
112 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
128 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
|
129 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
|
130 val perms_name = space_implode "_" perm_fn_names |
|
131 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
|
132 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
|
133 |
113 |
134 fun tac _ (_, _, simps) = |
114 fun tac _ (_, _, simps) = |
135 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
115 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
136 |
116 |
137 fun morphism phi (fvs, dfs, simps) = |
117 fun morphism phi (fvs, dfs, simps) = |
138 (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
118 (map (Morphism.term phi) fvs, |
|
119 map (Morphism.thm phi) dfs, |
|
120 map (Morphism.thm phi) simps); |
139 in |
121 in |
140 lthy' |
122 lthy' |
141 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
|
142 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
|
143 |> Class.prove_instantiation_exit_result morphism tac |
123 |> Class.prove_instantiation_exit_result morphism tac |
144 (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') |
124 (perm_funs, perm_eq_thms, perm_zero_thms @ perm_plus_thms) |
145 end |
125 end |
146 |
126 |
147 |
127 |
148 end (* structure *) |
128 end (* structure *) |
149 |
129 |