author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 67710 | cc2db3239932 |
permissions | -rw-r--r-- |
62858 | 1 |
(* Title: HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, Inria, LORIA, MPII |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
3 |
Copyright 2016 |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
4 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
5 |
Tactics for generalized corecursor sugar. |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
6 |
*) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
7 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
8 |
signature BNF_GFP_GREC_SUGAR_TACTICS = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
9 |
sig |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
10 |
val rho_transfer_simps: thm list |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
11 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
12 |
val mk_case_dtor_tac: Proof.context -> term -> thm -> thm -> thm list -> thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
13 |
val mk_cong_intro_ctr_or_friend_tac: Proof.context -> thm -> thm list -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
14 |
val mk_code_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
15 |
thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
16 |
thm list -> thm list -> thm list -> thm list -> thm list -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
17 |
val mk_eq_algrho_tac: Proof.context -> term list -> term -> term -> term -> term -> term -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
18 |
thm -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
19 |
thm list -> thm list -> thm -> thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
20 |
thm list -> thm list -> thm list -> thm list -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
21 |
val mk_eq_corecUU_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
22 |
thm list -> thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
23 |
thm list -> thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
24 |
val mk_last_disc_tac: Proof.context -> term -> thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
25 |
val mk_rho_transfer_tac: Proof.context -> bool -> thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
26 |
val mk_unique_tac: Proof.context -> int -> term list -> term -> term -> thm -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
27 |
thm list -> thm list -> thm list -> thm -> thm -> thm list -> thm list -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
28 |
thm list -> thm list -> thm list -> thm list -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
29 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
30 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
31 |
structure BNF_GFP_Grec_Sugar_Tactics : BNF_GFP_GREC_SUGAR_TACTICS = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
32 |
struct |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
33 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
34 |
open Ctr_Sugar |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
35 |
open BNF_Util |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
36 |
open BNF_Tactics |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
37 |
open BNF_FP_Def_Sugar_Tactics |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
38 |
open BNF_GFP_Grec_Tactics |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
39 |
open BNF_GFP_Grec_Sugar_Util |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
40 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
41 |
fun apply_func f = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
42 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
43 |
val arg_Ts = binder_fun_types (fastype_of f); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
44 |
val args = map_index (fn (j, T) => Var (("a" ^ string_of_int j, 0), T)) arg_Ts; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
45 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
46 |
list_comb (f, args) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
47 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
48 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
49 |
fun instantiate_distrib thm ctxt t = |
62727 | 50 |
infer_instantiate' ctxt [SOME (Thm.incr_indexes_cterm 1 (Thm.cterm_of ctxt t))] thm; |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
51 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
52 |
val mk_if_distrib_of = instantiate_distrib @{thm if_distrib}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
53 |
val mk_case_sum_distrib_of = instantiate_distrib @{thm sum.case_distrib}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
54 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
55 |
fun mk_case_dtor_tac ctxt u abs_inverse dtor_ctor ctr_defs exhaust cases = |
62727 | 56 |
let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
57 |
HEADGOAL (rtac ctxt exhaust') THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
58 |
REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
59 |
SELECT_GOAL (unfold_thms_tac ctxt cases THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
60 |
unfold_thms_tac ctxt (abs_inverse :: dtor_ctor :: ctr_defs @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
61 |
@{thms prod.case sum.case})) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
62 |
rtac ctxt refl)) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
63 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
64 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
65 |
fun mk_cong_intro_ctr_or_friend_tac ctxt ctr_or_friend_def extra_simps cong_alg_intro = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
66 |
HEADGOAL (REPEAT_DETERM_N 2 o subst_tac ctxt NONE [ctr_or_friend_def] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
67 |
rtac ctxt cong_alg_intro) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
68 |
unfold_thms_tac ctxt (extra_simps @ sumprod_thms_rel @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
69 |
@{thms vimage2p_def prod.rel_eq sum.rel_eq}) THEN |
62744 | 70 |
REPEAT_DETERM (HEADGOAL (rtac ctxt conjI ORELSE' assume_tac ctxt ORELSE' rtac ctxt refl ORELSE' |
71 |
etac ctxt subst)); |
|
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
72 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
73 |
val shared_simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
74 |
@{thms map_prod_simp map_sum.simps sum.case prod.case_eq_if split_beta' prod.sel |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
75 |
sum.disc(1)[THEN eq_True[THEN iffD2]] sum.disc(2)[THEN eq_False[THEN iffD2]] sum.sel |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
76 |
isl_map_sum map_sum_sel if_True if_False if_True_False Let_def[abs_def] o_def[abs_def] id_def |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
77 |
BNF_Composition.id_bnf_def}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
78 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
79 |
fun mk_code_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
80 |
fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
81 |
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs corecUU all_sig_maps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
82 |
ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps inner_fp_simps fun_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
83 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
84 |
val fun_def' = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
85 |
if null inner_fp_simps andalso num_args > 0 then |
67710
cc2db3239932
added HOLogic.mk_obj_eq convenience and eliminated some clones;
wenzelm
parents:
64379
diff
changeset
|
86 |
HOLogic.mk_obj_eq fun_def RS (mk_curry_uncurryN_balanced ctxt num_args RS iffD2) RS sym |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
87 |
else |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
88 |
fun_def; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
89 |
val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
90 |
val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
91 |
val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
92 |
(eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
93 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
94 |
val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
95 |
fp_map_ident :: (if null inner_fp_simps then [] else [corecUU]) @ fpsig_nesting_map_ident0s @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
96 |
fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
97 |
case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ all_algLam_alg_pointfuls @ all_algrho_eqs @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
98 |
eval_simps @ if_distribs @ shared_simps); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
99 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
100 |
HEADGOAL (subst_tac ctxt NONE [fun_def] THEN' subst_tac ctxt NONE [corecUU] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
101 |
(if null inner_fp_simps then K all_tac else subst_tac ctxt NONE inner_fp_simps)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
102 |
unfold_thms_tac ctxt [fun_def'] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
103 |
unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
104 |
HEADGOAL (rtac ctxt refl) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
105 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
106 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
107 |
fun mk_eq_algrho_tac ctxt fpsig_nesting_maps abs rep ctor ssig_map eval pre_map_def abs_inverse |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
108 |
fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
109 |
live_nesting_map_ident0s fp_map_ident dtor_ctor ctor_iff_dtor ctr_defs nullary_disc_defs |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
110 |
disc_sel_eq_cases case_dtor case_eq_ifs const_pointful_naturals fp_nesting_k_map_disc_sels' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
111 |
rho_def dtor_algrho corecUU_unique eq_corecUU all_sig_maps ssig_map_thms |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
112 |
all_algLam_alg_pointfuls all_algrho_eqs eval_simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
113 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
114 |
val nullary_disc_defs' = nullary_disc_defs |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
115 |
|> map (fn thm => thm RS sym) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
116 |
|> maps (fn thm => [thm, thm RS @{thm subst[OF eq_commute, of "%e. e = z" for z]}]); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
117 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
118 |
val case_dtor' = unfold_thms ctxt shared_simps case_dtor; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
119 |
val disc_sel_eq_cases' = map (mk_abs_def |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
120 |
o unfold_thms ctxt (case_dtor' :: ctr_defs @ shared_simps)) disc_sel_eq_cases; |
64379
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
63856
diff
changeset
|
121 |
val extra_naturals = Facts.retrieve (Context.Proof ctxt) (Proof_Context.facts_of ctxt) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
63856
diff
changeset
|
122 |
("friend_of_corec_simps", Position.none) |> #thms; |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
63856
diff
changeset
|
123 |
val const_pointful_naturals' = map (unfold_thms ctxt shared_simps) |
71f42dcaa1df
additional user-specified simp (naturality) rules used in friend_of_corec
traytel
parents:
63856
diff
changeset
|
124 |
(extra_naturals @ const_pointful_naturals); |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
125 |
val const_pointful_naturals_sym' = map (fn thm => thm RS sym) const_pointful_naturals'; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
126 |
val case_eq_ifs' = map mk_abs_def (@{thm sum.case_eq_if} :: case_eq_ifs); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
127 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
128 |
val distrib_consts = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
129 |
abs :: rep :: ctor :: eval :: map apply_func (ssig_map :: fpsig_nesting_maps); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
130 |
val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) distrib_consts; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
131 |
val case_sum_distribs = map (mk_case_sum_distrib_of ctxt) distrib_consts; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
132 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
133 |
val simp_ctxt = (ctxt |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
134 |
|> Context_Position.set_visible false |
69593 | 135 |
|> put_simpset (simpset_of (Proof_Context.init_global \<^theory>\<open>Main\<close>)) |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
136 |
|> Raw_Simplifier.add_cong @{thm if_cong}) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
137 |
addsimps pre_map_def :: abs_inverse :: fp_map_ident :: dtor_ctor :: rho_def :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
138 |
@{thm convol_def} :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
139 |
fpsig_nesting_map_thms @ live_nesting_map_ident0s @ ctr_defs @ disc_sel_eq_cases' @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
140 |
fp_nesting_k_map_disc_sels' @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
141 |
all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ case_sum_distribs @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
142 |
shared_simps; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
143 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
144 |
fun mk_main_simp const_pointful_naturals_maybe_sym' = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
145 |
simp_tac (simp_ctxt addsimps const_pointful_naturals_maybe_sym'); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
146 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
147 |
unfold_thms_tac ctxt [eq_corecUU] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
148 |
HEADGOAL (REPEAT_DETERM o rtac ctxt ext THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
149 |
rtac ctxt (corecUU_unique RS sym RS fun_cong) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
150 |
subst_tac ctxt NONE [dtor_algrho RS (ctor_iff_dtor RS iffD2)] THEN' rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
151 |
unfold_thms_tac ctxt (nullary_disc_defs' @ shared_simps) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
152 |
HEADGOAL (rtac ctxt meta_eq_to_obj_eq) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
153 |
REPEAT_DETERM_N (length const_pointful_naturals' + 1) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
154 |
(ALLGOALS (mk_main_simp const_pointful_naturals_sym') THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
155 |
ALLGOALS (mk_main_simp const_pointful_naturals')) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
156 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
157 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
158 |
fun mk_eq_corecUU_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
159 |
fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
160 |
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
161 |
ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique fun_code = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
162 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
163 |
val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
164 |
val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
165 |
val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
166 |
(eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
167 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
168 |
val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
169 |
fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
170 |
live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
171 |
all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
172 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
173 |
HEADGOAL (rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
174 |
rtac ctxt corecUU_unique THEN' rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
175 |
unfold_thms_tac ctxt @{thms prod.case_eq_if} THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
176 |
HEADGOAL (rtac ctxt (fun_code RS trans)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
177 |
unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
178 |
HEADGOAL (rtac ctxt refl) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
179 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
180 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
181 |
fun mk_last_disc_tac ctxt u exhaust discs' = |
62727 | 182 |
let val exhaust' = infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt u)] exhaust in |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
183 |
HEADGOAL (rtac ctxt exhaust') THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
184 |
REPEAT_DETERM (HEADGOAL (etac ctxt ssubst THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
185 |
simp_tac (ss_only (distinct Thm.eq_thm discs' @ @{thms simp_thms}) ctxt))) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
186 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
187 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
188 |
val rho_transfer_simps = @{thms BNF_Def.vimage2p_def[abs_def] BNF_Composition.id_bnf_def}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
189 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
190 |
fun mk_rho_transfer_tac ctxt unfold rel_def const_transfers = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
191 |
(if unfold then unfold_thms_tac ctxt (rel_def :: rho_transfer_simps) else all_tac) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
192 |
HEADGOAL (transfer_prover_add_tac ctxt [] const_transfers); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
193 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
194 |
fun mk_unique_tac ctxt num_args fpsig_nesting_maps ssig_map eval pre_map_def abs_inverse |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
195 |
fpsig_nesting_map_ident0s fpsig_nesting_map_comps fpsig_nesting_map_thms |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
196 |
live_nesting_map_ident0s fp_map_ident case_trivial ctr_defs case_eq_ifs all_sig_maps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
197 |
ssig_map_thms all_algLam_alg_pointfuls all_algrho_eqs eval_simps corecUU_unique eq_corecUU = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
198 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
199 |
val case_trivial' = unfold_thms ctxt (case_eq_ifs @ ctr_defs @ shared_simps) case_trivial; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
200 |
val case_eq_ifs' = map (Drule.abs_def o (fn thm => thm RS eq_reflection)) case_eq_ifs; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
201 |
val if_distribs = @{thm if_distrib_fun} :: map (mk_if_distrib_of ctxt) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
202 |
(eval :: map apply_func (ssig_map :: fpsig_nesting_maps)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
203 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
204 |
val unfold_tac = unfold_thms_tac ctxt (case_trivial' :: pre_map_def :: abs_inverse :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
205 |
fp_map_ident :: fpsig_nesting_map_ident0s @ fpsig_nesting_map_comps @ fpsig_nesting_map_thms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
206 |
live_nesting_map_ident0s @ ctr_defs @ case_eq_ifs' @ all_sig_maps @ ssig_map_thms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
207 |
all_algLam_alg_pointfuls @ all_algrho_eqs @ eval_simps @ if_distribs @ shared_simps); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
208 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
209 |
HEADGOAL (subst_tac ctxt NONE [eq_corecUU] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
210 |
rtac ctxt (mk_curry_uncurryN_balanced ctxt num_args RS iffD1) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
211 |
rtac ctxt corecUU_unique THEN' rtac ctxt ext THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
212 |
etac ctxt @{thm ssubst[of _ _ "\<lambda>x. f x = u" for f u]}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
213 |
unfold_tac THEN HEADGOAL (CONVERSION Thm.eta_long_conversion) THEN unfold_tac THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
214 |
HEADGOAL (rtac ctxt refl) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
215 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
216 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
217 |
end; |