1 (* Title: nominal_eqvt.ML |
1 (* Title: nominal_eqvt.ML |
2 Author: Stefan Berghofer (original code) |
2 Author: Stefan Berghofer (original code) |
3 Author: Christian Urban |
3 Author: Christian Urban |
|
4 Author: Tjark Weber |
4 |
5 |
5 Automatic proofs for equivariance of inductive predicates. |
6 Automatic proofs for equivariance of inductive predicates. |
6 *) |
7 *) |
7 |
8 |
8 |
|
9 signature NOMINAL_EQVT = |
9 signature NOMINAL_EQVT = |
10 sig |
10 sig |
11 val raw_equivariance: term list -> thm -> thm list -> Proof.context -> thm list |
11 val raw_equivariance: Proof.context -> term list -> thm -> thm list -> thm list |
12 val equivariance_cmd: string -> Proof.context -> local_theory |
12 val equivariance_cmd: string -> Proof.context -> local_theory |
13 end |
13 end |
14 |
14 |
15 structure Nominal_Eqvt : NOMINAL_EQVT = |
15 structure Nominal_Eqvt : NOMINAL_EQVT = |
16 struct |
16 struct |
17 |
17 |
18 open Nominal_Permeq; |
18 open Nominal_Permeq; |
19 open Nominal_ThmDecls; |
19 open Nominal_ThmDecls; |
20 |
20 |
21 val atomize_conv = |
21 val atomize_conv = |
22 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
22 Raw_Simplifier.rewrite_cterm (true, false, false) (K (K NONE)) |
23 (HOL_basic_ss addsimps @{thms induct_atomize}); |
23 (HOL_basic_ss addsimps @{thms induct_atomize}) |
24 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv); |
24 |
|
25 val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv) |
|
26 |
25 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
27 fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1 |
26 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)); |
28 (Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt)) |
27 |
29 |
28 |
30 |
29 (** equivariance tactics **) |
31 (** equivariance tactics **) |
30 |
32 |
31 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
32 let |
34 let |
33 val thy = Proof_Context.theory_of ctxt |
35 val thy = Proof_Context.theory_of ctxt |
34 val cpi = Thm.cterm_of thy pi |
36 val cpi = Thm.cterm_of thy pi |
35 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
37 val pi_intro_rule = Drule.instantiate' [] [NONE, SOME cpi] @{thm permute_boolI} |
36 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
38 val eqvt_sconfig = eqvt_strict_config addexcls pred_names |
37 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} |
39 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def permute_self split_paired_all} |
38 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
40 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def permute_minus_cancel(2)} |
39 in |
41 in |
40 eqvt_tac ctxt eqvt_sconfig THEN' |
42 eqvt_tac ctxt eqvt_sconfig THEN' |
41 SUBPROOF (fn {prems, context as ctxt, ...} => |
43 SUBPROOF (fn {prems, context as ctxt, ...} => |
42 let |
44 let |
43 val prems' = map (transform_prem2 ctxt pred_names) prems |
45 val prems' = map (transform_prem2 ctxt pred_names) prems |
44 val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' |
46 val prems'' = map (fn thm => eqvt_rule ctxt eqvt_sconfig (thm RS pi_intro_rule)) prems' |
45 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
47 val prems''' = map (simplify simps2 o simplify simps1) prems'' |
46 |
|
47 in |
48 in |
48 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) |
49 HEADGOAL (rtac intro THEN_ALL_NEW resolve_tac (prems' @ prems'' @ prems''')) |
49 end) ctxt |
50 end) ctxt |
50 end |
51 end |
51 |
52 |
52 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
53 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
53 let |
54 let |
55 in |
56 in |
56 EVERY' ((DETERM o rtac induct) :: cases) |
57 EVERY' ((DETERM o rtac induct) :: cases) |
57 end |
58 end |
58 |
59 |
59 |
60 |
60 (** equivariance procedure *) |
61 (** equivariance procedure **) |
61 |
62 |
62 fun prepare_goal pi pred = |
63 fun prepare_goal ctxt pi pred_with_args = |
63 let |
64 let |
64 val (c, xs) = strip_comb pred; |
65 val (c, xs) = strip_comb pred_with_args |
|
66 fun is_nonfixed_Free (Free (s, _)) = not (Variable.is_fixed ctxt s) |
|
67 | is_nonfixed_Free _ = false |
|
68 fun mk_perm_nonfixed_Free t = |
|
69 if is_nonfixed_Free t then mk_perm pi t else t |
65 in |
70 in |
66 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
71 HOLogic.mk_imp (pred_with_args, |
|
72 list_comb (c, map mk_perm_nonfixed_Free xs)) |
67 end |
73 end |
68 |
74 |
69 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
75 fun name_of (Const (s, _)) = s |
70 |
76 |
71 fun get_name (Const (a, _)) = a |
77 fun raw_equivariance ctxt preds raw_induct intrs = |
72 | get_name (Free (a, _)) = a |
78 let |
|
79 (* FIXME: polymorphic predicates should either be rejected or |
|
80 specialized to arguments of sort pt *) |
73 |
81 |
74 fun raw_equivariance pred_trms raw_induct intrs ctxt = |
82 val is_already_eqvt = filter (is_eqvt ctxt) preds |
75 let |
|
76 val is_already_eqvt = |
|
77 filter (is_eqvt ctxt) pred_trms |
|
78 |> map (Syntax.string_of_term ctxt) |
|
79 val _ = if null is_already_eqvt then () |
83 val _ = if null is_already_eqvt then () |
80 else error ("Already equivariant: " ^ commas is_already_eqvt) |
84 else error ("Already equivariant: " ^ commas |
|
85 (map (Syntax.string_of_term ctxt) is_already_eqvt)) |
81 |
86 |
82 val pred_names = map get_name pred_trms |
87 val pred_names = map (name_of o head_of) preds |
83 val raw_induct' = atomize_induct ctxt raw_induct |
88 val raw_induct' = atomize_induct ctxt raw_induct |
84 val intrs' = map atomize_intr intrs |
89 val intrs' = map atomize_intr intrs |
85 |
90 |
86 val (([raw_concl], [raw_pi]), ctxt') = |
91 val (([raw_concl], [raw_pi]), ctxt') = |
87 ctxt |
92 ctxt |
88 |> Variable.import_terms false [concl_of raw_induct'] |
93 |> Variable.import_terms false [concl_of raw_induct'] |
89 ||>> Variable.variant_fixes ["p"] |
94 ||>> Variable.variant_fixes ["p"] |
90 val pi = Free (raw_pi, @{typ perm}) |
95 val pi = Free (raw_pi, @{typ perm}) |
91 |
96 |
92 val preds = map (fst o HOLogic.dest_imp) |
97 val preds_with_args = raw_concl |
93 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
98 |> HOLogic.dest_Trueprop |
94 |
99 |> HOLogic.dest_conj |
95 val goal = HOLogic.mk_Trueprop |
100 |> map (fst o HOLogic.dest_imp) |
96 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
101 |
97 in |
102 val goal = preds_with_args |
98 Goal.prove ctxt' [] [] goal |
103 |> map (prepare_goal ctxt pi) |
99 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
104 |> foldr1 HOLogic.mk_conj |
100 |> Datatype_Aux.split_conj_thm |
105 |> HOLogic.mk_Trueprop |
|
106 in |
|
107 Goal.prove ctxt' [] [] goal |
|
108 (fn {context, ...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
|
109 |> Datatype_Aux.split_conj_thm |
101 |> Proof_Context.export ctxt' ctxt |
110 |> Proof_Context.export ctxt' ctxt |
102 |> map (fn th => th RS mp) |
111 |> map (fn th => th RS mp) |
103 |> map zero_var_indexes |
112 |> map zero_var_indexes |
104 end |
113 end |
105 |
114 |
106 |
115 |
107 fun note_named_thm (name, thm) ctxt = |
116 (** stores thm under name.eqvt and adds [eqvt]-attribute **) |
|
117 |
|
118 fun note_named_thm (name, thm) ctxt = |
108 let |
119 let |
109 val thm_name = Binding.qualified_name |
120 val thm_name = Binding.qualified_name |
110 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
121 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
111 val attr = Attrib.internal (K eqvt_add) |
122 val attr = Attrib.internal (K eqvt_add) |
112 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
123 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
113 in |
124 in |
114 (thm', ctxt') |
125 (thm', ctxt') |
115 end |
126 end |
116 |
127 |
|
128 |
|
129 (** equivariance command **) |
|
130 |
117 fun equivariance_cmd pred_name ctxt = |
131 fun equivariance_cmd pred_name ctxt = |
118 let |
132 let |
119 val thy = Proof_Context.theory_of ctxt |
|
120 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
133 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
121 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
134 Inductive.the_inductive ctxt (long_name ctxt pred_name) |
122 val thms = raw_equivariance preds raw_induct intrs ctxt |
135 val thms = raw_equivariance ctxt preds raw_induct intrs |
123 in |
136 in |
124 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
137 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
125 end |
138 end |
126 |
139 |
127 |
|
128 val _ = |
140 val _ = |
129 Outer_Syntax.local_theory @{command_spec "equivariance"} |
141 Outer_Syntax.local_theory @{command_spec "equivariance"} |
130 "Proves equivariance for inductive predicate involving nominal datatypes." |
142 "Proves equivariance for inductive predicate involving nominal datatypes." |
131 (Parse.xname >> equivariance_cmd) |
143 (Parse.const >> equivariance_cmd) |
132 |
|
133 |
144 |
134 end (* structure *) |
145 end (* structure *) |