1 theory Perm |
1 theory Perm |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" |
2 imports "Nominal2_Atoms" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 ML {* |
6 |
6 open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *) |
7 datatype rtrm1 = |
7 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
8 rVr1 "name" |
8 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
9 | rAp1 "rtrm1" "rtrm1 list" |
9 *} |
10 | rLm1 "name" "rtrm1" |
|
11 | rLt1 "bp" "rtrm1" "rtrm1" |
|
12 and bp = |
|
13 BUnit |
|
14 | BVr "name" |
|
15 | BPr "bp" "bp" |
|
16 |
10 |
17 ML {* |
11 ML {* |
18 open Datatype_Aux (* typ_of_dtyp, DtRec, ... *) |
|
19 *} |
|
20 |
12 |
21 instantiation rtrm1 and bp :: pt |
13 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
22 begin |
14 fun define_raw_perms new_type_names full_tnames thy = |
23 |
15 let |
24 |
16 val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); |
25 ML {* |
|
26 val {descr, induct, ...} = Datatype.the_info @{theory} "Perm.rtrm1"; |
|
27 val new_type_names = ["rtrm1", "bp"]; |
|
28 (* TODO: [] should be the sorts that we'll take from the specification *) |
17 (* TODO: [] should be the sorts that we'll take from the specification *) |
29 val sorts = []; |
18 val sorts = []; |
30 |
|
31 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
19 fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); |
32 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
20 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
33 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
21 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
34 val perm_names = replicate (length new_type_names) @{const_name permute} @ |
|
35 map (Sign.full_bname @{theory}) (List.drop (perm_names', length new_type_names)); |
|
36 val perm_types = map (fn (i, _) => |
22 val perm_types = map (fn (i, _) => |
37 let val T = nth_dtyp i |
23 let val T = nth_dtyp i |
38 in @{typ perm} --> T --> T end) descr; |
24 in @{typ perm} --> T --> T end) descr; |
39 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
25 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
40 (* TODO: Next line only needed after instantiation *) |
|
41 val perm_names_types = perm_names ~~ perm_types; |
|
42 val perm_names_types' = perm_names' ~~ perm_types; |
26 val perm_names_types' = perm_names' ~~ perm_types; |
43 |
|
44 val pi = Free ("pi", @{typ perm}); |
27 val pi = Free ("pi", @{typ perm}); |
45 fun permute ty = Const (@{const_name permute}, @{typ perm} --> ty --> ty); |
|
46 val minus_perm = Const (@{const_name minus}, @{typ perm} --> @{typ perm}); |
|
47 *} |
|
48 ML {* |
|
49 fun perm_eq_constr i (cname, dts) = |
28 fun perm_eq_constr i (cname, dts) = |
50 let |
29 let |
51 val Ts = map (typ_of_dtyp descr sorts) dts; |
30 val Ts = map (typ_of_dtyp descr sorts) dts; |
52 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
31 val names = Name.variant_list ["pi"] (Datatype_Prop.make_tnames Ts); |
53 val args = map Free (names ~~ Ts); |
32 val args = map Free (names ~~ Ts); |
69 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
48 (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq |
70 (Free (nth perm_names_types' i) $ |
49 (Free (nth perm_names_types' i) $ |
71 Free ("pi", @{typ perm}) $ list_comb (c, args), |
50 Free ("pi", @{typ perm}) $ list_comb (c, args), |
72 list_comb (c, map perm_arg (dts ~~ args))))) |
51 list_comb (c, map perm_arg (dts ~~ args))))) |
73 end; |
52 end; |
74 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
53 fun perm_eq (i, (_, _, constrs)) = map (perm_eq_constr i) constrs; |
75 val perm_eqs = maps perm_eq descr; |
54 val perm_eqs = maps perm_eq descr; |
|
55 val lthy = |
|
56 Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy; |
|
57 (* TODO: Use the version of prmrec that gives the names explicitely. *) |
|
58 val (perm_ldef, lthy') = |
|
59 Primrec.add_primrec |
|
60 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
|
61 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); |
|
63 val perm_empty_thms = |
|
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)"} |
|
81 val pi1 = Free ("pi1", @{typ perm}); |
|
82 val pi2 = Free ("pi2", @{typ perm}); |
|
83 val perm_append_thms = |
|
84 List.take ((split_conj_thm |
|
85 (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) [] |
|
86 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
87 (map (fn ((perm, T), x) => |
|
88 let |
|
89 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
90 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
91 in HOLogic.mk_eq (lhs, rhs) |
|
92 end) |
|
93 (perm_frees ~~ |
|
94 map body_type perm_types ~~ perm_indnames)))) |
|
95 (fn _ => EVERY [indtac induct perm_indnames 1, |
|
96 ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))), |
|
97 length new_type_names); |
|
98 fun tac ctxt perm_thms = |
|
99 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
|
100 simp_tac (@{simpset} addsimps perm_thms |
|
101 ))); |
|
102 fun morphism phi = map (Morphism.thm phi); |
|
103 in |
|
104 Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy' |
|
105 end |
|
106 |
76 *} |
107 *} |
77 |
108 |
78 local_setup {* |
109 (* Test |
79 snd o (Primrec.add_primrec |
110 atom_decl name |
80 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs) |
|
81 *} |
|
82 |
111 |
|
112 datatype rtrm1 = |
|
113 rVr1 "name" |
|
114 | rAp1 "rtrm1" "rtrm1 list" |
|
115 | rLm1 "name" "rtrm1" |
|
116 | rLt1 "bp" "rtrm1" "rtrm1" |
|
117 and bp = |
|
118 BUnit |
|
119 | BVr "name" |
|
120 | BPr "bp" "bp" |
|
121 |
|
122 |
|
123 setup {* snd o define_raw_perms ["rtrm1", "bp"] ["Perm.rtrm1", "Perm.bp"] *} |
83 print_theorems |
124 print_theorems |
|
125 *) |
84 |
126 |
85 ML {* |
|
86 val perm_empty_thms = |
|
87 let |
|
88 val gl = |
|
89 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
90 (map (fn ((s, T), x) => HOLogic.mk_eq |
|
91 (Const (s, @{typ perm} --> T --> T) $ |
|
92 @{term "0 :: perm"} $ Free (x, T), |
|
93 Free (x, T))) |
|
94 (perm_names ~~ |
|
95 map body_type perm_types ~~ perm_indnames))); |
|
96 fun tac _ = |
|
97 EVERY [indtac induct perm_indnames 1, |
|
98 ALLGOALS (asm_full_simp_tac @{simpset})]; |
|
99 in |
|
100 map Drule.export_without_context (List.take (split_conj_thm |
|
101 (Goal.prove @{context} [] [] gl tac), |
|
102 length new_type_names)) |
|
103 end |
|
104 *} |
|
105 |
|
106 ML {* |
|
107 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
|
108 val pi1 = Free ("pi1", @{typ perm}); |
|
109 val pi2 = Free ("pi2", @{typ perm}); |
|
110 val perm_append_thms = |
|
111 List.take (map Drule.export_without_context (split_conj_thm |
|
112 (Goal.prove @{context} [] [] |
|
113 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
114 (map (fn ((s, T), x) => |
|
115 let |
|
116 val perm = Const (s, @{typ perm} --> T --> T); |
|
117 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
118 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
119 in HOLogic.mk_eq (lhs, rhs) |
|
120 end) |
|
121 (perm_names ~~ |
|
122 map body_type perm_types ~~ perm_indnames)))) |
|
123 (fn _ => EVERY [indtac induct perm_indnames 1, |
|
124 ALLGOALS (asm_full_simp_tac @{simpset})]))), |
|
125 length new_type_names) |
|
126 *} |
|
127 |
|
128 instance |
|
129 apply(tactic {* |
|
130 (Class.intro_classes_tac []) THEN |
|
131 (ALLGOALS (simp_tac (@{simpset} addsimps (perm_empty_thms @ perm_append_thms)))) *}) |
|
132 done |
|
133 end |
127 end |