1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(* Title: nominal_eqvt.ML
|
1835
|
2 |
Author: Stefan Berghofer (original code)
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
Author: Christian Urban
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
Automatic proofs for equivariance of inductive predicates.
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
*)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
signature NOMINAL_EQVT =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
sig
|
1835
|
10 |
val equivariance: string -> Proof.context -> local_theory
|
|
11 |
val eqvt_rel_tac: Proof.context -> string list -> term -> thm -> thm list -> int -> tactic
|
1948
|
12 |
val eqvt_rel_single_case_tac: Proof.context -> string list -> term -> thm -> int -> tactic
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
structure Nominal_Eqvt : NOMINAL_EQVT =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
struct
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
open Nominal_Permeq;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
19 |
open Nominal_ThmDecls;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
20 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
val atomize_conv =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
MetaSimplifier.rewrite_cterm (true, false, false) (K (K NONE))
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
(HOL_basic_ss addsimps @{thms induct_atomize});
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
val atomize_intr = Conv.fconv_rule (Conv.prems_conv ~1 atomize_conv);
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
fun atomize_induct ctxt = Conv.fconv_rule (Conv.prems_conv ~1
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
(Conv.params_conv ~1 (K (Conv.prems_conv ~1 atomize_conv)) ctxt));
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
|
1835
|
28 |
|
|
29 |
(**
|
1948
|
30 |
given the theorem F[t]; proves the theorem F[f t]
|
|
31 |
|
1835
|
32 |
- F needs to be monotone
|
1948
|
33 |
- f returns either SOME for a term it fires on
|
1835
|
34 |
and NONE elsewhere
|
|
35 |
**)
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
36 |
fun map_term f t =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
37 |
(case f t of
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
38 |
NONE => map_term' f t
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
39 |
| x => x)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
40 |
and map_term' f (t $ u) =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
41 |
(case (map_term f t, map_term f u) of
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
42 |
(NONE, NONE) => NONE
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
43 |
| (SOME t'', NONE) => SOME (t'' $ u)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
| (NONE, SOME u'') => SOME (t $ u'')
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
| (SOME t'', SOME u'') => SOME (t'' $ u''))
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
| map_term' f (Abs (s, T, t)) =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
47 |
(case map_term f t of
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
48 |
NONE => NONE
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
49 |
| SOME t'' => SOME (Abs (s, T, t'')))
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
50 |
| map_term' _ _ = NONE;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
51 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
52 |
fun map_thm_tac ctxt tac thm =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
53 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
54 |
val monos = Inductive.get_monos ctxt
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
55 |
in
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
56 |
EVERY [cut_facts_tac [thm] 1, etac rev_mp 1,
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
57 |
REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
58 |
REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
59 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
60 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
61 |
fun map_thm ctxt f tac thm =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
62 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
63 |
val opt_goal_trm = map_term f (prop_of thm)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
64 |
in
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
65 |
case opt_goal_trm of
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
66 |
NONE => thm
|
1835
|
67 |
| SOME goal =>
|
|
68 |
Goal.prove ctxt [] [] goal (fn _ => map_thm_tac ctxt tac thm)
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
69 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
70 |
|
1835
|
71 |
(*
|
|
72 |
inductive premises can be of the form
|
|
73 |
R ... /\ P ...; split_conj picks out
|
|
74 |
the part P ...
|
|
75 |
*)
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
76 |
fun transform_prem ctxt names thm =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
77 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
78 |
fun split_conj names (Const ("op &", _) $ p $ q) =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
79 |
(case head_of p of
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
80 |
Const (name, _) => if name mem names then SOME q else NONE
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
81 |
| _ => NONE)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
82 |
| split_conj _ _ = NONE;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
83 |
in
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
84 |
map_thm ctxt (split_conj names) (etac conjunct2 1) thm
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
85 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
86 |
|
1835
|
87 |
|
|
88 |
(** equivariance tactics **)
|
|
89 |
|
1866
|
90 |
val perm_boolE = @{thm permute_boolE}
|
|
91 |
val perm_cancel = @{thms permute_minus_cancel(2)}
|
|
92 |
val perm_expand_bool = @{thms permute_fun_def minus_minus permute_bool_def}
|
|
93 |
|
1948
|
94 |
fun eqvt_rel_single_case_tac ctxt pred_names pi intro =
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
95 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
96 |
val thy = ProofContext.theory_of ctxt
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
97 |
val cpi = Thm.cterm_of thy (mk_minus pi)
|
1866
|
98 |
val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE
|
|
99 |
val simps = HOL_basic_ss addsimps perm_expand_bool
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
100 |
in
|
1866
|
101 |
eqvt_strict_tac ctxt [] pred_names THEN'
|
|
102 |
SUBPROOF (fn {prems, context as ctxt, ...} =>
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
val prems' = map (transform_prem ctxt pred_names) prems
|
1866
|
105 |
val tac1 = resolve_tac prems'
|
|
106 |
val tac2 = EVERY' [ rtac pi_intro_rule,
|
|
107 |
eqvt_strict_tac ctxt perm_cancel pred_names, resolve_tac prems' ]
|
|
108 |
val tac3 = EVERY' [ rtac pi_intro_rule,
|
|
109 |
eqvt_strict_tac ctxt perm_cancel pred_names, simp_tac simps, resolve_tac prems']
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
110 |
in
|
1866
|
111 |
(rtac intro THEN_ALL_NEW FIRST' [tac1, tac2, tac3]) 1
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
112 |
end) ctxt
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
113 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
114 |
|
1835
|
115 |
fun eqvt_rel_tac ctxt pred_names pi induct intros =
|
|
116 |
let
|
1948
|
117 |
val cases = map (eqvt_rel_single_case_tac ctxt pred_names pi) intros
|
1835
|
118 |
in
|
|
119 |
EVERY' (rtac induct :: cases)
|
|
120 |
end
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
121 |
|
1835
|
122 |
|
|
123 |
(** equivariance procedure *)
|
|
124 |
|
|
125 |
(* sets up goal and makes sure parameters
|
|
126 |
are untouched PROBLEM: this violates the
|
|
127 |
form of eqvt lemmas *)
|
|
128 |
fun prepare_goal params_no pi pred =
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
129 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
130 |
val (c, xs) = strip_comb pred;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
131 |
val (xs1, xs2) = chop params_no xs
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
132 |
in
|
1835
|
133 |
HOLogic.mk_imp (pred, list_comb (c, xs1 @ map (mk_perm pi) xs2))
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
134 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
135 |
|
1835
|
136 |
(* stores thm under name.eqvt and adds [eqvt]-attribute *)
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
137 |
fun note_named_thm (name, thm) ctxt =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
138 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
139 |
val thm_name = Binding.qualified_name
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
140 |
(Long_Name.qualify (Long_Name.base_name name) "eqvt")
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
141 |
val attr = Attrib.internal (K eqvt_add)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
142 |
in
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
143 |
Local_Theory.note ((thm_name, [attr]), [thm]) ctxt
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
144 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
145 |
|
1835
|
146 |
fun equivariance pred_name ctxt =
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
147 |
let
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
148 |
val thy = ProofContext.theory_of ctxt
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
149 |
val ({names, ...}, {raw_induct, intrs, ...}) =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
150 |
Inductive.the_inductive ctxt (Sign.intern_const thy pred_name)
|
1835
|
151 |
val raw_induct = atomize_induct ctxt raw_induct
|
|
152 |
val intros = map atomize_intr intrs
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
153 |
val params_no = length (Inductive.params_of raw_induct)
|
1948
|
154 |
val (([raw_concl], [raw_pi]), ctxt') =
|
|
155 |
ctxt
|
|
156 |
|> Variable.import_terms false [concl_of raw_induct]
|
|
157 |
||>> Variable.variant_fixes ["p"]
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
158 |
val pi = Free (raw_pi, @{typ perm})
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
159 |
val preds = map (fst o HOLogic.dest_imp)
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
160 |
(HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl));
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
161 |
val goal = HOLogic.mk_Trueprop
|
1835
|
162 |
(foldr1 HOLogic.mk_conj (map (prepare_goal params_no pi) preds))
|
|
163 |
val thms = Datatype_Aux.split_conj_thm (Goal.prove ctxt' [] [] goal
|
|
164 |
(fn {context,...} => eqvt_rel_tac context names pi raw_induct intros 1)
|
|
165 |
|> singleton (ProofContext.export ctxt' ctxt))
|
|
166 |
val thms' = map (fn th => zero_var_indexes (th RS mp)) thms
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
167 |
in
|
1835
|
168 |
ctxt |> fold_map note_named_thm (names ~~ thms') |> snd
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
169 |
end
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
170 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
171 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
172 |
local structure P = OuterParse and K = OuterKeyword in
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
173 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
174 |
val _ =
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
175 |
OuterSyntax.local_theory "equivariance"
|
1948
|
176 |
"Proves equivariance for inductive predicate involving nominal datatypes."
|
1835
|
177 |
K.thy_decl (P.xname >> equivariance);
|
1833
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
178 |
end;
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
179 |
|
2050b5723c04
added a library for basic nominal functions; separated nominal_eqvt file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
180 |
end (* structure *) |