32 |
32 |
33 val perm_boolE = @{thm permute_boolE} |
33 val perm_boolE = @{thm permute_boolE} |
34 val perm_cancel = @{thms permute_minus_cancel(2)} |
34 val perm_cancel = @{thms permute_minus_cancel(2)} |
35 |
35 |
36 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
36 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
37 let |
37 let |
38 val thy = ProofContext.theory_of ctxt |
38 val thy = ProofContext.theory_of ctxt |
39 val cpi = Thm.cterm_of thy (mk_minus pi) |
39 val cpi = Thm.cterm_of thy (mk_minus pi) |
40 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
40 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
41 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
41 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
42 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
42 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
43 in |
43 in |
44 eqvt_strict_tac ctxt [] pred_names THEN' |
44 eqvt_strict_tac ctxt [] pred_names THEN' |
45 SUBPROOF (fn {prems, context as ctxt, ...} => |
45 SUBPROOF (fn {prems, context as ctxt, ...} => |
46 let |
46 let |
47 val prems' = map (transform_prem2 ctxt pred_names) prems |
47 val prems' = map (transform_prem2 ctxt pred_names) prems |
48 val tac1 = resolve_tac prems' |
48 val tac1 = resolve_tac prems' |
49 val tac2 = EVERY' [ rtac pi_intro_rule, |
49 val tac2 = EVERY' [ rtac pi_intro_rule, |
50 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
50 eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ] |
51 val tac3 = EVERY' [ rtac pi_intro_rule, |
51 val tac3 = EVERY' [ rtac pi_intro_rule, |
52 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, |
52 eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps1, |
53 simp_tac simps2, resolve_tac prems'] |
53 simp_tac simps2, resolve_tac prems'] |
54 in |
54 in |
55 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
55 (rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1 |
56 end) ctxt |
56 end) ctxt |
57 end |
57 end |
58 |
58 |
59 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
59 fun eqvt_rel_tac ctxt pred_names pi induct intros = |
60 let |
60 let |
61 val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros |
61 val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros |
62 in |
62 in |
63 EVERY' (rtac induct :: cases) |
63 EVERY' (rtac induct :: cases) |
64 end |
64 end |
65 |
65 |
66 |
66 |
67 (** equivariance procedure *) |
67 (** equivariance procedure *) |
68 |
68 |
69 (* sets up goal and makes sure parameters |
|
70 are untouched PROBLEM: this violates the |
|
71 form of eqvt lemmas *) |
|
72 fun prepare_goal pi pred = |
69 fun prepare_goal pi pred = |
73 let |
70 let |
74 val (c, xs) = strip_comb pred; |
71 val (c, xs) = strip_comb pred; |
75 in |
72 in |
76 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
73 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
77 end |
74 end |
78 |
75 |
79 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
76 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
|
77 |
80 fun note_named_thm (name, thm) ctxt = |
78 fun note_named_thm (name, thm) ctxt = |
81 let |
79 let |
82 val thm_name = Binding.qualified_name |
80 val thm_name = Binding.qualified_name |
83 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
81 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
84 val attr = Attrib.internal (K eqvt_add) |
82 val attr = Attrib.internal (K eqvt_add) |
85 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
83 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
86 in |
84 in |
87 (thm', ctxt') |
85 (thm', ctxt') |
88 end |
86 end |
89 |
87 |
90 fun equivariance note_flag pred_trms raw_induct intrs ctxt = |
88 fun equivariance note_flag pred_trms raw_induct intrs ctxt = |
91 let |
89 let |
92 val is_already_eqvt = |
90 val is_already_eqvt = |
93 filter (is_eqvt ctxt) pred_trms |
91 filter (is_eqvt ctxt) pred_trms |
94 |> map (Syntax.string_of_term ctxt) |
92 |> map (Syntax.string_of_term ctxt) |
95 val _ = if null is_already_eqvt then () |
93 val _ = if null is_already_eqvt then () |
96 else error ("Already equivariant: " ^ commas is_already_eqvt) |
94 else error ("Already equivariant: " ^ commas is_already_eqvt) |
97 |
95 |
98 val pred_names = map (fst o dest_Const) pred_trms |
96 val pred_names = map (fst o dest_Const) pred_trms |
99 val raw_induct' = atomize_induct ctxt raw_induct |
97 val raw_induct' = atomize_induct ctxt raw_induct |
100 val intrs' = map atomize_intr intrs |
98 val intrs' = map atomize_intr intrs |
101 val (([raw_concl], [raw_pi]), ctxt') = |
99 |
102 ctxt |
100 val (([raw_concl], [raw_pi]), ctxt') = |
103 |> Variable.import_terms false [concl_of raw_induct'] |
101 ctxt |
104 ||>> Variable.variant_fixes ["p"] |
102 |> Variable.import_terms false [concl_of raw_induct'] |
105 val pi = Free (raw_pi, @{typ perm}) |
103 ||>> Variable.variant_fixes ["p"] |
106 val preds = map (fst o HOLogic.dest_imp) |
104 val pi = Free (raw_pi, @{typ perm}) |
107 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
105 |
108 val goal = HOLogic.mk_Trueprop |
106 val preds = map (fst o HOLogic.dest_imp) |
109 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
107 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
110 val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal |
108 |
111 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
109 val goal = HOLogic.mk_Trueprop |
112 |> singleton (ProofContext.export ctxt' ctxt)) |
110 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
113 val thms' = map (fn th => zero_var_indexes (th RS mp)) thms |
111 |
114 in |
112 val thms = Goal.prove ctxt' [] [] goal |
115 if note_flag |
113 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
116 then ctxt |> fold_map note_named_thm (pred_names ~~ thms') |
114 |> Datatype_Aux.split_conj_thm |
117 else (thms', ctxt) |
115 |> ProofContext.export ctxt' ctxt |
118 end |
116 |> map (fn th => th RS mp) |
|
117 |> map zero_var_indexes |
|
118 in |
|
119 if note_flag |
|
120 then fold_map note_named_thm (pred_names ~~ thms) ctxt |
|
121 else (thms, ctxt) |
|
122 end |
119 |
123 |
120 fun equivariance_cmd pred_name ctxt = |
124 fun equivariance_cmd pred_name ctxt = |
121 let |
125 let |
122 val thy = ProofContext.theory_of ctxt |
126 val thy = ProofContext.theory_of ctxt |
123 val (_, {preds, raw_induct, intrs, ...}) = |
127 val (_, {preds, raw_induct, intrs, ...}) = |
124 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
128 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
125 in |
129 in |
126 equivariance true preds raw_induct intrs ctxt |> snd |
130 equivariance true preds raw_induct intrs ctxt |> snd |
127 end |
131 end |
128 |
132 |
129 local structure P = Parse and K = Keyword in |
133 local structure P = Parse and K = Keyword in |
130 |
134 |
131 val _ = |
135 val _ = |
132 Outer_Syntax.local_theory "equivariance" |
136 Outer_Syntax.local_theory "equivariance" |
133 "Proves equivariance for inductive predicate involving nominal datatypes." |
137 "Proves equivariance for inductive predicate involving nominal datatypes." |
134 K.thy_decl (P.xname >> equivariance_cmd); |
138 K.thy_decl (P.xname >> equivariance_cmd); |
|
139 |
135 end; |
140 end; |
136 |
141 |
137 end (* structure *) |
142 end (* structure *) |