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 |
10 |
11 ML {* |
11 ML {* |
12 fun prove_perm_empty lthy induct perm_def perm_frees perm_indnames = |
12 fun prove_perm_empty lthy induct perm_def perm_frees = |
13 let |
13 let |
14 val perm_types = map fastype_of perm_frees |
14 val perm_types = map fastype_of perm_frees; |
|
15 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
15 val gl = |
16 val gl = |
16 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
17 HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
17 (map (fn ((perm, T), x) => HOLogic.mk_eq |
18 (map (fn ((perm, T), x) => HOLogic.mk_eq |
18 (perm $ @{term "0 :: perm"} $ Free (x, T), |
19 (perm $ @{term "0 :: perm"} $ Free (x, T), |
19 Free (x, T))) |
20 Free (x, T))) |
27 in |
28 in |
28 split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
29 split_conj_thm (Goal.prove lthy perm_indnames [] gl tac) |
29 end; |
30 end; |
30 *} |
31 *} |
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 *} |
32 |
59 |
33 ML {* |
60 ML {* |
34 |
|
35 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
61 (* TODO: full_name can be obtained from new_type_names with Datatype *) |
36 fun define_raw_perms new_type_names full_tnames thy = |
62 fun define_raw_perms new_type_names full_tnames thy = |
37 let |
63 let |
38 val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); |
64 val {descr, induct, ...} = Datatype.the_info thy (hd full_tnames); |
39 (* TODO: [] should be the sorts that we'll take from the specification *) |
65 (* TODO: [] should be the sorts that we'll take from the specification *) |
42 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
68 val perm_names' = Datatype_Prop.indexify_names (map (fn (i, _) => |
43 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
69 "permute_" ^ name_of_typ (nth_dtyp i)) descr); |
44 val perm_types = map (fn (i, _) => |
70 val perm_types = map (fn (i, _) => |
45 let val T = nth_dtyp i |
71 let val T = nth_dtyp i |
46 in @{typ perm} --> T --> T end) descr; |
72 in @{typ perm} --> T --> T end) descr; |
47 val perm_indnames = Datatype_Prop.make_tnames (map body_type perm_types); |
|
48 val perm_names_types' = perm_names' ~~ perm_types; |
73 val perm_names_types' = perm_names' ~~ perm_types; |
49 val pi = Free ("pi", @{typ perm}); |
74 val pi = Free ("pi", @{typ perm}); |
50 fun perm_eq_constr i (cname, dts) = |
75 fun perm_eq_constr i (cname, dts) = |
51 let |
76 let |
52 val Ts = map (typ_of_dtyp descr sorts) dts; |
77 val Ts = map (typ_of_dtyp descr sorts) dts; |
80 val ((_, perm_ldef), lthy') = |
105 val ((_, perm_ldef), lthy') = |
81 Primrec.add_primrec |
106 Primrec.add_primrec |
82 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
107 (map (fn s => (Binding.name s, NONE, NoSyn)) perm_names') perm_eqs lthy; |
83 val perm_frees = |
108 val perm_frees = |
84 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
109 (distinct (op =)) (map (fst o strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) perm_ldef); |
85 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees perm_indnames, length new_type_names); |
110 val perm_empty_thms = List.take (prove_perm_empty lthy' induct perm_ldef perm_frees, length new_type_names); |
86 val add_perm = @{term "op + :: (perm \<Rightarrow> perm \<Rightarrow> perm)"} |
111 val perm_append_thms = List.take (prove_perm_append lthy' induct perm_ldef perm_frees, length new_type_names) |
87 val pi1 = Free ("pi1", @{typ perm}); |
|
88 val pi2 = Free ("pi2", @{typ perm}); |
|
89 val perm_append_thms = |
|
90 List.take ((split_conj_thm |
|
91 (Goal.prove lthy' ("pi1" :: "pi2" :: perm_indnames) [] |
|
92 (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj |
|
93 (map (fn ((perm, T), x) => |
|
94 let |
|
95 val lhs = perm $ (add_perm $ pi1 $ pi2) $ Free (x, T) |
|
96 val rhs = perm $ pi1 $ (perm $ pi2 $ Free (x, T)) |
|
97 in HOLogic.mk_eq (lhs, rhs) |
|
98 end) |
|
99 (perm_frees ~~ |
|
100 map body_type perm_types ~~ perm_indnames)))) |
|
101 (fn _ => EVERY [indtac induct perm_indnames 1, |
|
102 ALLGOALS (asm_full_simp_tac (@{simpset} addsimps perm_ldef))]))), |
|
103 length new_type_names); |
|
104 fun tac ctxt perm_thms = |
112 fun tac ctxt perm_thms = |
105 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
113 (Class.intro_classes_tac []) THEN (ALLGOALS ( |
106 simp_tac (@{simpset} addsimps perm_thms |
114 simp_tac (HOL_ss addsimps perm_thms |
107 ))); |
115 ))); |
108 fun morphism phi = map (Morphism.thm phi); |
116 fun morphism phi = map (Morphism.thm phi); |
109 in |
117 in |
110 Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy' |
118 Class_Target.prove_instantiation_exit_result morphism tac (perm_empty_thms @ perm_append_thms) lthy' |
111 end |
119 end |