|
1 (* Title: nominal_dt_rawperm.ML |
|
2 Author: Cezary Kaliszyk |
|
3 Author: Christian Urban |
|
4 |
|
5 Definitions of the raw permutations and |
|
6 proof that the raw datatypes are in the |
|
7 pt-class. |
|
8 *) |
|
9 |
|
10 signature NOMINAL_DT_RAWPERM = |
|
11 sig |
|
12 val define_raw_perms: Datatype.descr -> (string * sort) list -> thm -> int -> theory -> |
|
13 (term list * thm list * thm list) * theory |
|
14 end |
|
15 |
|
16 |
|
17 structure Nominal_Dt_RawPerm: NOMINAL_DT_RAWPERM = |
|
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 *) |
|
32 fun perm_arg permute_fn_frees p (arg_dty, arg) = |
|
33 if Datatype_Aux.is_rec_type arg_dty |
|
34 then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg |
|
35 else mk_perm p arg |
|
36 |
|
37 |
|
38 (* generates the equation for the permutation function for one constructor; |
|
39 i is the index of the corresponding datatype *) |
|
40 fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) = |
|
41 let |
|
42 val p = Free ("p", @{typ perm}) |
|
43 val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts |
|
44 val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys) |
|
45 val args = map Free (arg_names ~~ arg_tys) |
|
46 val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i)) |
|
47 val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args) |
|
48 val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args)) |
|
49 val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) |
|
50 in |
|
51 (Attrib.empty_binding, eq) |
|
52 end |
|
53 |
|
54 |
|
55 (** proves the two pt-type class properties **) |
|
56 |
|
57 fun prove_permute_zero lthy induct perm_defs perm_fns = |
|
58 let |
|
59 val perm_types = map (body_type o fastype_of) perm_fns |
|
60 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
61 |
|
62 fun single_goal ((perm_fn, T), x) = |
|
63 HOLogic.mk_eq (perm_fn $ @{term "0::perm"} $ Free (x, T), Free (x, T)) |
|
64 |
|
65 val goals = |
|
66 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
67 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
68 |
|
69 val simps = HOL_basic_ss addsimps (@{thm permute_zero} :: perm_defs) |
|
70 |
|
71 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
72 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
73 in |
|
74 Goal.prove lthy perm_indnames [] goals (K tac) |
|
75 |> Datatype_Aux.split_conj_thm |
|
76 end |
|
77 |
|
78 |
|
79 fun prove_permute_plus lthy induct perm_defs perm_fns = |
|
80 let |
|
81 val p = Free ("p", @{typ perm}) |
|
82 val q = Free ("q", @{typ perm}) |
|
83 val perm_types = map (body_type o fastype_of) perm_fns |
|
84 val perm_indnames = Datatype_Prop.make_tnames perm_types |
|
85 |
|
86 fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq |
|
87 (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T))) |
|
88 |
|
89 val goals = |
|
90 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
91 (map single_goal (perm_fns ~~ perm_types ~~ perm_indnames))) |
|
92 |
|
93 val simps = HOL_basic_ss addsimps (@{thm permute_plus} :: perm_defs) |
|
94 |
|
95 val tac = (Datatype_Aux.indtac induct perm_indnames |
|
96 THEN_ALL_NEW asm_simp_tac simps) 1 |
|
97 in |
|
98 Goal.prove lthy ("p" :: "q" :: perm_indnames) [] goals (K tac) |
|
99 |> Datatype_Aux.split_conj_thm |
|
100 end |
|
101 |
|
102 |
|
103 (* user_dt_nos refers to the number of "un-unfolded" datatypes |
|
104 given by the user |
|
105 *) |
|
106 fun define_raw_perms (dt_descr:Datatype.descr) sorts induct_thm user_dt_nos thy = |
|
107 let |
|
108 val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr; |
|
109 val user_full_tnames = List.take (all_full_tnames, user_dt_nos); |
|
110 |
|
111 val perm_fn_names = prefix_dt_names dt_descr sorts "permute_" |
|
112 val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr |
|
113 val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types) |
|
114 |
|
115 fun perm_eq (i, (_, _, constrs)) = |
|
116 map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs; |
|
117 |
|
118 val perm_eqs = maps perm_eq dt_descr; |
|
119 |
|
120 val lthy = |
|
121 Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy; |
|
122 |
|
123 val ((perm_funs, perm_eq_thms), lthy') = |
|
124 Primrec.add_primrec |
|
125 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy; |
|
126 |
|
127 val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs |
|
128 val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs |
|
129 val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos); |
|
130 val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos) |
|
131 val perms_name = space_implode "_" perm_fn_names |
|
132 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
|
133 val perms_plus_bind = Binding.name (perms_name ^ "_plus") |
|
134 |
|
135 fun tac _ (_, _, simps) = |
|
136 Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac simps) |
|
137 |
|
138 fun morphism phi (fvs, dfs, simps) = |
|
139 (map (Morphism.term phi) fvs, map (Morphism.thm phi) dfs, map (Morphism.thm phi) simps); |
|
140 in |
|
141 lthy' |
|
142 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms')) |
|
143 |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms')) |
|
144 |> Class_Target.prove_instantiation_exit_result morphism tac |
|
145 (perm_funs, perm_eq_thms, perm_zero_thms' @ perm_plus_thms') |
|
146 end |
|
147 |
|
148 |
|
149 end (* structure *) |
|
150 |