equal
deleted
inserted
replaced
30 |
30 |
31 val perm_boolE = @{thm permute_boolE} |
31 val perm_boolE = @{thm permute_boolE} |
32 |
32 |
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
33 fun eqvt_rel_single_case_tac ctxt pred_names pi intro = |
34 let |
34 let |
35 val thy = ProofContext.theory_of ctxt |
35 val thy = Proof_Context.theory_of ctxt |
36 val cpi = Thm.cterm_of thy (mk_minus pi) |
36 val cpi = Thm.cterm_of thy (mk_minus pi) |
37 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
37 val pi_intro_rule = Drule.instantiate' [] [SOME cpi] perm_boolE |
38 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
38 val simps1 = HOL_basic_ss addsimps @{thms permute_fun_def minus_minus split_paired_all} |
39 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
39 val simps2 = HOL_basic_ss addsimps @{thms permute_bool_def} |
40 val eqvt_sconfig = |
40 val eqvt_sconfig = |
102 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
102 (foldr1 HOLogic.mk_conj (map (prepare_goal pi) preds)) |
103 in |
103 in |
104 Goal.prove ctxt' [] [] goal |
104 Goal.prove ctxt' [] [] goal |
105 (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) |
106 |> Datatype_Aux.split_conj_thm |
106 |> Datatype_Aux.split_conj_thm |
107 |> ProofContext.export ctxt' ctxt |
107 |> Proof_Context.export ctxt' ctxt |
108 |> map (fn th => th RS mp) |
108 |> map (fn th => th RS mp) |
109 |> map zero_var_indexes |
109 |> map zero_var_indexes |
110 end |
110 end |
111 |
111 |
112 |
112 |
120 (thm', ctxt') |
120 (thm', ctxt') |
121 end |
121 end |
122 |
122 |
123 fun equivariance_cmd pred_name ctxt = |
123 fun equivariance_cmd pred_name ctxt = |
124 let |
124 let |
125 val thy = ProofContext.theory_of ctxt |
125 val thy = Proof_Context.theory_of ctxt |
126 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
126 val ({names, ...}, {preds, raw_induct, intrs, ...}) = |
127 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
127 Inductive.the_inductive ctxt (Sign.intern_const thy pred_name) |
128 val thms = raw_equivariance preds raw_induct intrs ctxt |
128 val thms = raw_equivariance preds raw_induct intrs ctxt |
129 in |
129 in |
130 fold_map note_named_thm (names ~~ thms) ctxt |> snd |
130 fold_map note_named_thm (names ~~ thms) ctxt |> snd |