73 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
72 HOLogic.mk_imp (pred, list_comb (c, map (mk_perm pi) xs)) |
74 end |
73 end |
75 |
74 |
76 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
75 (* stores thm under name.eqvt and adds [eqvt]-attribute *) |
77 |
76 |
78 fun note_named_thm (name, thm) ctxt = |
|
79 let |
|
80 val thm_name = Binding.qualified_name |
|
81 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
|
82 val attr = Attrib.internal (K eqvt_add) |
|
83 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
|
84 in |
|
85 (thm', ctxt') |
|
86 end |
|
87 |
|
88 fun get_name (Const (a, _)) = a |
77 fun get_name (Const (a, _)) = a |
89 | get_name (Free (a, _)) = a |
78 | get_name (Free (a, _)) = a |
90 |
79 |
91 fun raw_equivariance note_flag pred_trms raw_induct intrs ctxt = |
80 fun raw_equivariance pred_trms raw_induct intrs ctxt = |
92 let |
81 let |
93 val is_already_eqvt = |
82 val is_already_eqvt = |
94 filter (is_eqvt ctxt) pred_trms |
83 filter (is_eqvt ctxt) pred_trms |
95 |> map (Syntax.string_of_term ctxt) |
84 |> map (Syntax.string_of_term ctxt) |
96 val _ = if null is_already_eqvt then () |
85 val _ = if null is_already_eqvt then () |
108 |
97 |
109 val preds = map (fst o HOLogic.dest_imp) |
98 val preds = map (fst o HOLogic.dest_imp) |
110 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
99 (HOLogic.dest_conj (HOLogic.dest_Trueprop raw_concl)); |
111 |
100 |
112 val goal = HOLogic.mk_Trueprop |
101 val goal = HOLogic.mk_Trueprop |
113 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
102 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
114 |
103 in |
115 val thms = Goal.prove ctxt' [] [] goal |
104 Goal.prove ctxt' [] [] goal |
116 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
105 (fn {context,...} => eqvt_rel_tac context pred_names pi raw_induct' intrs' 1) |
117 |> Datatype_Aux.split_conj_thm |
106 |> Datatype_Aux.split_conj_thm |
118 |> ProofContext.export ctxt' ctxt |
107 |> ProofContext.export ctxt' ctxt |
119 |> map (fn th => th RS mp) |
108 |> map (fn th => th RS mp) |
120 |> map zero_var_indexes |
109 |> map zero_var_indexes |
121 in |
|
122 if note_flag |
|
123 then fold_map note_named_thm (pred_names ~~ thms) ctxt |
|
124 else (thms, ctxt) |
|
125 end |
110 end |
126 |
111 |
127 fun equivariance pred_name ctxt = |
112 fun note_named_thm (name, thm) ctxt = |
128 let |
113 let |
129 val thy = ProofContext.theory_of ctxt |
114 val thm_name = Binding.qualified_name |
130 val (_, {preds, raw_induct, intrs, ...}) = |
115 (Long_Name.qualify (Long_Name.base_name name) "eqvt") |
131 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
116 val attr = Attrib.internal (K eqvt_add) |
|
117 val ((_, [thm']), ctxt') = Local_Theory.note ((thm_name, [attr]), [thm]) ctxt |
132 in |
118 in |
133 raw_equivariance false preds raw_induct intrs ctxt |
119 (thm', ctxt') |
134 end |
120 end |
135 |
121 |
136 fun equivariance_cmd pred_name ctxt = |
122 fun equivariance_cmd pred_name ctxt = |
137 let |
123 let |
138 val thy = ProofContext.theory_of ctxt |
124 val thy = ProofContext.theory_of ctxt |
139 val (_, {preds, raw_induct, intrs, ...}) = |
125 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
140 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
126 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
|
127 val thms = raw_equivariance preds raw_induct intrs ctxt |
141 in |
128 in |
142 raw_equivariance true preds raw_induct intrs ctxt |> snd |
129 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
143 end |
130 end |
144 |
131 |
145 local structure P = Parse and K = Keyword in |
132 local structure P = Parse and K = Keyword in |
146 |
133 |
147 val _ = |
134 val _ = |