5 ML {* |
5 ML {* |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
9 *} |
9 *} |
|
10 |
|
11 ML {* |
|
12 fun prove_perm_empty lthy induct perm_def perm_frees perm_indnames = |
|
13 let |
|
14 val perm_types = map fastype_of perm_frees |
|
15 val gl = |
|
16 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
17 (map (fn ((perm, T), x) => HOLogic.mk_eq |
|
18 (perm $ @{term "0 :: perm"} $ Free (x, T), |
|
19 Free (x, T))) |
|
20 (perm_frees ~~ |
|
21 map body_type perm_types ~~ perm_indnames))); |
|
22 fun tac _ = |
|
23 EVERY [ |
|
24 indtac induct perm_indnames 1, |
|
25 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
|
26 ]; |
|
27 in |
|
28 split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
|
29 end; |
|
30 *} |
|
31 |
10 |
32 |
11 ML {* |
33 ML {* |
12 |
34 |
13 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
35 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
14 fun define_raw_perms new_type_names full_tnames thy = |
36 fun define_raw_perms new_type_names full_tnames thy = |
58 val ((_, perm_ldef), lthy') = |
80 val ((_, perm_ldef), lthy') = |
59 Primrec.add_primrec |
81 Primrec.add_primrec |
60 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
82 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
61 val perm_frees = |
83 val perm_frees = |
62 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
84 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
63 val perm_empty_thms = |
85 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees perm_indnames, length new_type_names); |
64 let |
|
65 val gl = |
|
66 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
67 (map (fn ((perm, T), x) => HOLogic.mk_eq |
|
68 (perm $ @{term "0 :: perm"} $ Free (x, T), |
|
69 Free (x, T))) |
|
70 (perm_frees ~~ |
|
71 map body_type perm_types ~~ perm_indnames))); |
|
72 fun tac {context = ctxt, ...} = |
|
73 EVERY [ |
|
74 indtac induct perm_indnames 1, |
|
75 ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef)) |
|
76 ]; |
|
77 in |
|
78 (List.take (split_conj_thm (Goal.prove lthy' perm_indnames [] gl tac), length new_type_names)) |
|
79 end; |
|
80 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
86 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
81 val pi1 = Free ("pi1", @{typ perm}); |
87 val pi1 = Free ("pi1", @{typ perm}); |
82 val pi2 = Free ("pi2", @{typ perm}); |
88 val pi2 = Free ("pi2", @{typ perm}); |
83 val perm_append_thms = |
89 val perm_append_thms = |
84 List.take ((split_conj_thm |
90 List.take ((split_conj_thm |