|
1 theory Perm |
|
2 imports "Nominal2_Atoms" |
|
3 begin |
|
4 |
|
5 ML {* |
|
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
|
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
|
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
|
9 *} |
|
10 |
|
11 ML {* |
|
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
|
13 let |
|
14 val perm_types = map fastype_of perm_frees; |
|
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
16 val gl = |
|
17 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
18 (map (fn ((perm, T), x) => HOLogic.mk_eq |
|
19 (perm $ @{term "0 :: perm"} $ Free (x, T), |
|
20 Free (x, T))) |
|
21 (perm_frees ~~ |
|
22 map body_type perm_types ~~ perm_indnames))); |
|
23 fun tac _ = |
|
24 EVERY [ |
|
25 indtac induct perm_indnames 1, |
|
26 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_zero} :: perm_def))) |
|
27 ]; |
|
28 in |
|
29 split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
|
30 end; |
|
31 *} |
|
32 |
|
33 ML {* |
|
34 fun prove_perm_append lthy induct perm_def perm_frees = |
|
35 let |
|
36 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
|
37 val pi1 = Free ("pi1", @{typ perm}); |
|
38 val pi2 = Free ("pi2", @{typ perm}); |
|
39 val perm_types = map fastype_of perm_frees |
|
40 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
41 val gl = |
|
42 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
43 (map (fn ((perm, T), x) => |
|
44 let |
|
45 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
46 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
47 in HOLogic.mk_eq (lhs, rhs) |
|
48 end) |
|
49 (perm_frees ~~ map body_type perm_types ~~ perm_indnames)))) |
|
50 fun tac _ = |
|
51 EVERY [ |
|
52 indtac induct perm_indnames 1, |
|
53 ALLGOALS (asm_full_simp_tac (HOL_ss addsimps (@{thm permute_plus} :: perm_def))) |
|
54 ] |
|
55 in |
|
56 split_conj_thm (Goal.prove lthy ("pi1" :: "pi2" :: perm_indnames) [] gl tac) |
|
57 end; |
|
58 *} |
|
59 |
|
60 ML {* |
|
61 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
|
62 fun define_raw_perms new_type_names full_tnames thy = |
|
63 let |
|
64 val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); |
|
65 (* TODO: [] should be the sorts that we'll take from the specification *) |
|
66 val sorts = []; |
|
67 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
|
68 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
|
69 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
|
70 val perm_types = map (fn (i, _) => |
|
71 let val T = nth_dtyp i |
|
72 in @{typ perm} --> T --> T end) descr; |
|
73 val perm_names_types' = perm_names' ~~ perm_types; |
|
74 val pi = Free ("pi", @{typ perm}); |
|
75 fun perm_eq_constr i (cname, dts) = |
|
76 let |
|
77 val Ts = map (typ_of_dtyp descr sorts) dts; |
|
78 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
|
79 val args = map Free (names ~~ Ts); |
|
80 val c = Const (cname, Ts ---> (nth_dtyp i)); |
|
81 fun perm_arg (dt, x) = |
|
82 let val T = type_of x |
|
83 in |
|
84 if is_rec_type dt then |
|
85 let val (Us, _) = strip_type T |
|
86 in list_abs (map (pair "x") Us, |
|
87 Free (nth perm_names_types' (body_index dt)) $ pi $ |
|
88 list_comb (x, map (fn (i, U) => |
|
89 (permute U) $ (minus_perm $ pi) $ Bound i) |
|
90 ((length Us - 1 downto 0) ~~ Us))) |
|
91 end |
|
92 else (permute T) $ pi $ x |
|
93 end; |
|
94 in |
|
95 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
96 (Free (nth perm_names_types' i) $ |
|
97 Free ("pi", @{typ perm}) $ list_comb (c, args), |
|
98 list_comb (c, map perm_arg (dts ~~ args))))) |
|
99 end; |
|
100 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
|
101 val perm_eqs = maps perm_eq descr; |
|
102 val lthy = |
|
103 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
|
104 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
|
105 val ((_, perm_ldef), lthy') = |
|
106 Primrec.add_primrec |
|
107 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
|
108 val perm_frees = |
|
109 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
|
110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
|
111 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
|
112 val perms_name = space_implode "_" perm_names' |
|
113 val perms_zero_bind = Binding.name (perms_name ^ "_zero") |
|
114 val perms_append_bind = Binding.name (perms_name ^ "_append") |
|
115 fun tac _ perm_thms = |
|
116 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
|
117 simp_tac (HOL_ss addsimps perm_thms |
|
118 ))); |
|
119 fun morphism phi = map (Morphism.thm phi); |
|
120 in |
|
121 lthy' |
|
122 |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_empty_thms)) |
|
123 |> snd o (Local_Theory.note ((perms_append_bind, []), perm_append_thms)) |
|
124 |> Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) |
|
125 end |
|
126 |
|
127 *} |
|
128 |
|
129 (* Test |
|
130 atom_decl name |
|
131 |
|
132 datatype rtrm1 = |
|
133 rVr1 "name" |
|
134 | rAp1 "rtrm1" "rtrm1 list" |
|
135 | rLm1 "name" "rtrm1" |
|
136 | rLt1 "bp" "rtrm1" "rtrm1" |
|
137 and bp = |
|
138 BUnit |
|
139 | BVr "name" |
|
140 | BPr "bp" "bp" |
|
141 |
|
142 |
|
143 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *} |
|
144 print_theorems |
|
145 *) |
|
146 |
|
147 end |