24 fun prove_perm_empty lthy induct perm_def perm_frees = |
19 fun prove_perm_empty lthy induct perm_def perm_frees = |
25 let |
20 let |
26 val perm_types = map fastype_of perm_frees; |
21 val perm_types = map fastype_of perm_frees; |
27 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); |
28 fun glc ((perm, T), x) = |
23 fun glc ((perm, T), x) = |
29 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)) |
30 val gl = |
25 val gl = |
31 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
26 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
32 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); |
27 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames))); |
33 fun tac _ = |
28 fun tac _ = |
34 EVERY [ |
29 EVERY [ |
35 indtac induct perm_indnames 1, |
30 Datatype_Aux.indtac induct perm_indnames 1, |
36 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
31 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
37 ]; |
32 ]; |
38 in |
33 in |
39 split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
34 Datatype_Aux.split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
40 end; |
35 end; |
41 *} |
36 *} |
42 |
37 |
43 ML {* |
38 ML {* |
44 fun prove_perm_append lthy induct perm_def perm_frees = |
39 fun prove_perm_append lthy induct perm_def perm_frees = |
45 let |
40 let |
46 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
|
47 val pi1 = Free ("pi1", @{typ perm}); |
41 val pi1 = Free ("pi1", @{typ perm}); |
48 val pi2 = Free ("pi2", @{typ perm}); |
42 val pi2 = Free ("pi2", @{typ perm}); |
49 val perm_types = map fastype_of perm_frees |
43 val perm_types = map fastype_of perm_frees |
50 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); |
51 fun glc ((perm, T), x) = |
45 fun glc ((perm, T), x) = |
52 HOLogic.mk_eq ( |
46 HOLogic.mk_eq ( |
53 perm $ (add_perm $ pi1 $ pi2) $ Free (x, T), |
47 perm $ (mk_plus pi1 pi2) $ Free (x, T), |
54 perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
48 perm $ pi1 $ (perm $ pi2 $ Free (x, T))) |
55 val gl = |
49 val goal = |
56 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
50 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
57 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
51 (map glc (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
58 fun tac _ = |
52 fun tac _ = |
59 EVERY [ |
53 EVERY [ |
60 indtac induct perm_indnames 1, |
54 Datatype_Aux.indtac induct perm_indnames 1, |
61 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
55 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
62 ] |
56 ] |
63 in |
57 in |
64 split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) |
58 Datatype_Aux.split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] goal tac) |
65 end; |
59 end; |
66 *} |
60 *} |
67 |
61 |
68 ML {* |
62 ML {* |
69 fun define_raw_perms (dt_info : info) number thy = |
63 fun define_raw_perms (dt_info : Datatype_Aux.info) number thy = |
70 let |
64 let |
71 val {descr, induct, sorts, ...} = dt_info; |
65 val {descr, induct, sorts, ...} = dt_info; |
72 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
66 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
73 val full_tnames = List.take (all_full_tnames, number); |
67 val full_tnames = List.take (all_full_tnames, number); |
74 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
68 fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); |
75 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
69 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
76 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
70 "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp i)) descr); |
77 val perm_types = map (fn (i, _) => |
71 val perm_types = map (fn (i, _) => |
78 let val T = nth_dtyp i |
72 let val T = nth_dtyp i |
79 in @{typ perm} --> T --> T end) descr; |
73 in @{typ perm} --> T --> T end) descr; |
80 val perm_names_types' = perm_names' ~~ perm_types; |
74 val perm_names_types' = perm_names' ~~ perm_types; |
81 val pi = Free ("pi", @{typ perm}); |
75 val pi = Free ("pi", @{typ perm}); |
82 fun perm_eq_constr i (cname, dts) = |
76 fun perm_eq_constr i (cname, dts) = |
83 let |
77 let |
84 val Ts = map (typ_of_dtyp descr sorts) dts; |
78 val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts; |
85 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
79 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
86 val args = map Free (names ~~ Ts); |
80 val args = map Free (names ~~ Ts); |
87 val c = Const (cname, Ts ---> (nth_dtyp i)); |
81 val c = Const (cname, Ts ---> (nth_dtyp i)); |
88 fun perm_arg (dt, x) = |
82 fun perm_arg (dt, x) = |
89 let val T = type_of x |
83 let val T = type_of x |
90 in |
84 in |
91 if is_rec_type dt then |
85 if Datatype_Aux.is_rec_type dt then |
92 let val (Us, _) = strip_type T |
86 let val (Us, _) = strip_type T |
93 in list_abs (map (pair "x") Us, |
87 in list_abs (map (pair "x") Us, |
94 Free (nth perm_names_types' (body_index dt)) $ pi $ |
88 Free (nth perm_names_types' (Datatype_Aux.body_index dt)) $ pi $ |
95 list_comb (x, map (fn (i, U) => |
89 list_comb (x, map (fn (i, U) => |
96 (mk_perm_ty U (mk_minus pi) (Bound i))) |
90 (mk_perm_ty U (mk_minus pi) (Bound i))) |
97 ((length Us - 1 downto 0) ~~ Us))) |
91 ((length Us - 1 downto 0) ~~ Us))) |
98 end |
92 end |
99 else (mk_perm_ty T pi x) |
93 else (mk_perm_ty T pi x) |