author | wenzelm |
Fri, 04 Jan 2019 23:22:53 +0100 | |
changeset 69593 | 3dda49e08b9d |
parent 64378 | e9eb0b99a44c |
permissions | -rw-r--r-- |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/BNF/bnf_gfp_grec_tactics.ML |
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 |
Author: Dmitriy Traytel, ETH Zurich |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
4 |
Copyright 2015, 2016 |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
5 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
6 |
Tactics for generalized corecursor construction. |
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 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
9 |
signature BNF_GFP_GREC_TACTICS = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
10 |
sig |
64378 | 11 |
val transfer_prover_eq_tac: Proof.context -> int -> tactic |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
12 |
val transfer_prover_add_tac: Proof.context -> thm list -> thm list -> int -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
13 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
14 |
val mk_algLam_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
15 |
tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
16 |
val mk_algLam_algrho_tac: Proof.context -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
17 |
val mk_algLam_base_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
18 |
thm list -> thm -> 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
|
19 |
val mk_algLam_step_tac: Proof.context -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
20 |
val mk_cong_locale_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm list -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
21 |
thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
22 |
val mk_corecU_pointfree_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm list -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
23 |
thm list -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
24 |
val mk_corecUU_pointfree_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
25 |
thm -> thm -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
26 |
val mk_corecUU_unique_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
27 |
thm -> thm -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
28 |
val mk_corecUU_Inl_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm list -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
29 |
thm list -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
30 |
val mk_dtor_algLam_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
31 |
thm -> thm -> thm list -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
32 |
val mk_dtor_algrho_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
33 |
val mk_dtor_transfer_tac: Proof.context -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
34 |
val mk_equivp_Retr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
35 |
val mk_eval_core_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
36 |
thm -> thm -> thm -> 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
|
37 |
val mk_eval_core_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
38 |
thm list -> thm -> thm list -> thm -> thm -> thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
39 |
val mk_eval_core_k_as_ssig_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
40 |
thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
41 |
val mk_eval_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
42 |
val mk_eval_flat_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
43 |
tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
44 |
val mk_eval_sctr_tac: Proof.context -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
45 |
val mk_eval_Oper_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
46 |
thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
47 |
val mk_eval_V_or_CLeaf_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
48 |
tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
49 |
val mk_extdd_mor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
50 |
thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
51 |
val mk_extdd_o_VLeaf_tac: Proof.context -> thm -> thm -> thm -> thm list -> thm list -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
52 |
thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
53 |
val mk_flat_embL_tac: Proof.context -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
54 |
thm list -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
55 |
val mk_flat_VLeaf_or_flat_tac: Proof.context -> thm -> thm -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
56 |
val mk_Lam_Inl_Inr_tac: Proof.context -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
57 |
val mk_mor_cutSsig_flat_tac: Proof.context -> term -> thm -> thm -> thm -> thm -> thm -> thm -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
58 |
thm list -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
59 |
val mk_natural_from_transfer_tac: Proof.context -> int -> bool list -> thm -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
60 |
thm list -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
61 |
val mk_natural_by_unfolding_tac: Proof.context -> thm list -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
62 |
val mk_Retr_coinduct_tac: Proof.context -> thm -> thm -> tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
63 |
val mk_sig_transfer_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
|
64 |
val mk_transfer_by_transfer_prover_tac: Proof.context -> thm list -> thm list -> thm list -> |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
65 |
tactic |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
66 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
67 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
68 |
structure BNF_GFP_Grec_Tactics : BNF_GFP_GREC_TACTICS = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
69 |
struct |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
70 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
71 |
open BNF_Util |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
72 |
open BNF_Tactics |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
73 |
open BNF_FP_Util |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
74 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
75 |
val o_assoc = @{thm o_assoc}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
76 |
val o_def = @{thm o_def}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
77 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
78 |
fun ss_only_silent thms ctxt = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
79 |
ss_only thms (ctxt |> Context_Position.set_visible false); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
80 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
81 |
fun context_relator_eq_add rel_eqs ctxt = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
82 |
fold (snd oo Thm.proof_attributes (map (Attrib.attribute ctxt) @{attributes [relator_eq]})) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
83 |
rel_eqs ctxt; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
84 |
val context_transfer_rule_add = fold (snd oo Thm.proof_attributes [Transfer.transfer_add]); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
85 |
|
64378 | 86 |
fun transfer_prover_eq_tac ctxt = |
87 |
SELECT_GOAL (Local_Defs.fold_tac ctxt (Transfer.get_relator_eq ctxt)) THEN' |
|
88 |
Transfer.transfer_prover_tac ctxt; |
|
89 |
||
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
90 |
fun transfer_prover_add_tac ctxt rel_eqs transfers = |
64378 | 91 |
transfer_prover_eq_tac (ctxt |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
92 |
|> context_relator_eq_add rel_eqs |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
93 |
|> context_transfer_rule_add transfers); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
94 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
95 |
fun instantiate_natural_rule_with_id ctxt live = |
69593 | 96 |
Rule_Insts.of_rule ctxt ([], NONE :: replicate live (SOME \<^const_name>\<open>id\<close>)) []; |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
97 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
98 |
fun instantiate_transfer_rule_with_Grp_UNIV ctxt alives thm = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
99 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
100 |
val n = length alives; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
101 |
val fs = map (prefix "f" o string_of_int) (1 upto n); |
69593 | 102 |
val ss = map2 (fn live => fn f => SOME (\<^const_name>\<open>BNF_Def.Grp\<close> ^ " " ^ \<^const_name>\<open>top\<close> ^ |
103 |
" " ^ (if live then f else \<^const_name>\<open>id\<close>))) alives fs; |
|
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
104 |
val bs = map_filter (fn (live, f) => if live then SOME (Binding.name f, NONE, NoSyn) else NONE) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
105 |
(alives ~~ fs); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
106 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
107 |
Rule_Insts.of_rule ctxt ([], ss) bs thm |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
108 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
109 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
110 |
fun mk_algLam_algLam_tac ctxt dead_pre_map_comp dtor_inject unsig sig_map Lam_def eval_embL |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
111 |
old_dtor_algLam dtor_algLam = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
112 |
HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
113 |
unfold_thms_tac ctxt (dead_pre_map_comp :: unsig :: sig_map :: Lam_def :: eval_embL :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
114 |
old_dtor_algLam :: dtor_algLam :: @{thms o_apply id_o map_sum.simps sum.case}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
115 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
116 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
117 |
fun mk_algLam_algrho_tac ctxt algLam_def algrho_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
118 |
HEADGOAL (rtac ctxt ext) THEN unfold_thms_tac ctxt [algLam_def, algrho_def, o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
119 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
120 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
121 |
fun mk_algLam_base_tac ctxt dead_pre_map_dtor dead_pre_map_id dead_pre_map_comp ctor_dtor dtor_ctor |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
122 |
dtor_unfold_unique unsig Sig_pointful_natural ssig_maps Lam_def flat_simps eval_core_simps eval |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
123 |
algLam_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
124 |
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt dead_pre_map_dtor)] |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
125 |
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext])) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
126 |
ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: ctor_dtor :: dtor_ctor :: unsig :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
127 |
Sig_pointful_natural :: Lam_def :: eval :: algLam_def :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
128 |
unfold_thms ctxt [o_def] dead_pre_map_comp :: ssig_maps @ flat_simps @ eval_core_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
129 |
@{thms o_apply id_apply id_def[symmetric] snd_conv convol_apply}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
130 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
131 |
fun mk_algLam_step_tac ctxt proto_sctr_def old_algLam_pointful algLam_algLam_pointful = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
132 |
HEADGOAL (rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
133 |
unfold_thms_tac ctxt [proto_sctr_def, old_algLam_pointful, algLam_algLam_pointful, o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
134 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
135 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
136 |
fun mk_cong_locale_tac ctxt dead_pre_rel_mono dead_pre_rel_maps equivp_Retr |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
137 |
ssig_rel_mono ssig_rel_maps eval eval_core_transfer = |
69593 | 138 |
HEADGOAL (resolve_tac ctxt (Locale.get_unfolds \<^context>) THEN' |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
139 |
etac ctxt ssig_rel_mono THEN' etac ctxt equivp_Retr) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
140 |
unfold_thms_tac ctxt (eval :: dead_pre_rel_maps @ @{thms id_apply}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
141 |
HEADGOAL (rtac ctxt (@{thm predicate2I} RS (dead_pre_rel_mono RS @{thm predicate2D})) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
142 |
etac ctxt @{thm rel_funD} THEN' assume_tac ctxt THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
143 |
rtac ctxt (eval_core_transfer RS @{thm rel_funD})) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
144 |
unfold_thms_tac ctxt (ssig_rel_maps @ @{thms vimage2p_rel_prod vimage2p_id}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
145 |
unfold_thms_tac ctxt @{thms vimage2p_def} THEN HEADGOAL (assume_tac ctxt); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
146 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
147 |
fun mk_corecU_pointfree_tac ctxt dead_pre_map_comp dtor_unfold ssig_maps dead_ssig_map_comp0 |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
148 |
flat_simps flat_VLeaf eval_core_simps cutSsig_def mor_cutSsig_flat corecU_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
149 |
unfold_thms_tac ctxt [corecU_def, dead_ssig_map_comp0, o_assoc] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
150 |
HEADGOAL (subst_tac ctxt NONE [ext RS mor_cutSsig_flat] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
151 |
asm_simp_tac (ss_only_silent [dtor_unfold, o_apply] ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
152 |
asm_simp_tac (ss_only_silent (dtor_unfold :: flat_VLeaf :: cutSsig_def :: ssig_maps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
153 |
flat_simps @ eval_core_simps @ unfold_thms ctxt [o_def] dead_pre_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
154 |
@{thms o_def id_apply id_def[symmetric] snd_conv convol_apply}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
155 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
156 |
fun mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
157 |
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
158 |
eval_sctr_pointful = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
159 |
asm_simp_tac (ss_only_silent (dtor_ctor :: flat_pointful_natural :: eval :: eval_flat :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
160 |
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp, ssig_map_comp] @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
161 |
@{thms o_apply id_apply id_def[symmetric] convol_apply}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
162 |
asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: sctr_pointful_natural :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
163 |
eval_sctr_pointful :: map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
164 |
@{thms id_apply id_def[symmetric] convol_apply map_prod_simp}) ctxt); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
165 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
166 |
fun mk_corecUU_pointfree_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor dtor_inject |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
167 |
ssig_map_comp flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_ctor |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
168 |
sctr_pointful_natural eval_sctr_pointful corecUU_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
169 |
unfold_thms_tac ctxt [corecUU_def] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
170 |
HEADGOAL (rtac ctxt ext THEN' subst_tac ctxt NONE [corecU_ctor RS sym]) THEN |
62727 | 171 |
unfold_thms_tac ctxt [corecUU_def RS symmetric_thm] THEN |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
172 |
HEADGOAL (rtac ctxt (dtor_inject RS iffD1) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
173 |
mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
174 |
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
175 |
eval_sctr_pointful); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
176 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
177 |
fun mk_corecUU_unique_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
178 |
flat_pointful_natural eval_core_pointful_natural eval eval_flat corecU_unique |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
179 |
sctr_pointful_natural eval_sctr_pointful corecUU_def prem = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
180 |
unfold_thms_tac ctxt [corecUU_def] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
181 |
HEADGOAL (rtac ctxt corecU_unique THEN' rtac ctxt sym THEN' subst_tac ctxt NONE [prem] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
182 |
rtac ctxt ext THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
183 |
mk_corecUU_tail_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_ctor ssig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
184 |
flat_pointful_natural eval_core_pointful_natural eval eval_flat sctr_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
185 |
eval_sctr_pointful); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
186 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
187 |
fun mk_corecUU_Inl_tac ctxt inl_case' pre_map_comp dead_pre_map_ident dead_pre_map_comp0 ctor_dtor |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
188 |
ssig_maps ssig_map_id0 eval_core_simps eval_core_pointful_natural eval_VLeaf corecUU_pointfree |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
189 |
corecUU_unique = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
190 |
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt inl_case')] |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
191 |
(trans OF [corecUU_unique, corecUU_unique RS sym]) OF [ext, ext]) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
192 |
subst_tac ctxt NONE [corecUU_pointfree] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
193 |
asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: eval_core_pointful_natural :: ssig_maps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
194 |
@{thms o_apply sum.case convol_apply id_apply map_prod_simp}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
195 |
asm_simp_tac (ss_only_silent (dead_pre_map_ident :: ctor_dtor :: ssig_map_id0 :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
196 |
eval_core_pointful_natural :: eval_VLeaf :: unfold_thms ctxt [o_def] pre_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
197 |
ssig_maps @ eval_core_simps @ @{thms o_apply prod.map_id convol_apply snd_conv id_apply}) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
198 |
ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
199 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
200 |
fun mk_dtor_algLam_tac ctxt pre_map_comp dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
201 |
sig_map_comp Oper_pointful_natural ssig_maps dead_ssig_map_comp0 Lam_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
202 |
eval_core_simps eval eval_flat eval_VLeaf algLam_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
203 |
unfold_thms_tac ctxt [dead_ssig_map_comp0, o_assoc] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
204 |
HEADGOAL (asm_simp_tac (ss_only_silent (sig_map_comp :: Oper_pointful_natural :: eval :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
205 |
eval_flat :: algLam_def :: unfold_thms ctxt [o_def] dead_pre_map_comp :: eval_core_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
206 |
@{thms o_apply id_apply id_def[symmetric]}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
207 |
asm_simp_tac (ss_only_silent (Lam_pointful_natural :: eval_VLeaf :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
208 |
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ ssig_maps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
209 |
eval_core_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
210 |
@{thms o_apply convol_apply snd_conv fst_conv id_apply map_prod_simp}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
211 |
asm_simp_tac (ss_only_silent (dead_pre_map_id :: eval_VLeaf :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
212 |
unfold_thms ctxt [o_def] pre_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
213 |
@{thms id_apply id_def[symmetric] convol_def}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
214 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
215 |
fun mk_dtor_algrho_tac ctxt eval k_as_ssig_natural_pointful eval_core_k_as_ssig algrho_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
216 |
HEADGOAL (asm_simp_tac (ss_only_silent [eval, k_as_ssig_natural_pointful, algrho_def, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
217 |
eval_core_k_as_ssig RS sym, o_apply] ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
218 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
219 |
fun mk_dtor_transfer_tac ctxt dtor_rel = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
220 |
HEADGOAL (rtac ctxt refl ORELSE' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
221 |
rtac ctxt @{thm rel_funI} THEN' rtac ctxt (dtor_rel RS iffD1) THEN' assume_tac ctxt); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
222 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
223 |
fun mk_equivp_Retr_tac ctxt dead_pre_rel_refl dead_pre_rel_flip dead_pre_rel_mono |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
224 |
dead_pre_rel_compp = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
225 |
HEADGOAL (EVERY' [etac ctxt @{thm equivpE}, rtac ctxt @{thm equivpI}, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
226 |
rtac ctxt @{thm reflpI}, rtac ctxt dead_pre_rel_refl, etac ctxt @{thm reflpD}, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
227 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms symp_iff}), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
228 |
REPEAT_DETERM o rtac ctxt ext, rtac ctxt (dead_pre_rel_flip RS sym RS trans), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
229 |
rtac ctxt ((@{thm conversep_iff} RS sym) RSN (2, trans)), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
230 |
asm_simp_tac (ss_only_silent @{thms conversep_eq} ctxt), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
231 |
SELECT_GOAL (unfold_thms_tac ctxt @{thms transp_relcompp}), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
232 |
rtac ctxt @{thm predicate2I}, etac ctxt @{thm relcomppE}, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
233 |
etac ctxt (dead_pre_rel_mono RS @{thm rev_predicate2D[rotated -1]}), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
234 |
SELECT_GOAL (unfold_thms_tac ctxt |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
235 |
(unfold_thms ctxt [@{thm eq_OO}] dead_pre_rel_compp :: @{thms relcompp_apply})), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
236 |
REPEAT_DETERM o resolve_tac ctxt [exI, conjI], assume_tac ctxt, assume_tac ctxt]); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
237 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
238 |
fun mk_eval_core_k_as_ssig_tac ctxt pre_map_comp dead_pre_map_id sig_map_comp ssig_maps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
239 |
Lam_natural_pointful Lam_Inr flat_VLeaf eval_core_simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
240 |
HEADGOAL (asm_simp_tac (ss_only_silent (dead_pre_map_id :: flat_VLeaf :: (Lam_Inr RS sym) :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
241 |
o_apply :: id_apply :: @{thm id_def[symmetric]} :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
242 |
unfold_thms ctxt @{thms map_prod_def split_def} Lam_natural_pointful :: ssig_maps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
243 |
eval_core_simps @ map (unfold_thms ctxt [o_def]) [pre_map_comp, sig_map_comp]) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
244 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
245 |
fun mk_eval_embL_tac ctxt dead_pre_map_comp0 dtor_unfold_unique embL_pointful_natural eval_core_embL |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
246 |
old_eval eval = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
247 |
HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
248 |
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] OF [ext, ext]) |
62727 | 249 |
OF [asm_rl, old_eval RS sym])) THEN |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
250 |
unfold_thms_tac ctxt [dead_pre_map_comp0, embL_pointful_natural, eval_core_embL, eval, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
251 |
o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
252 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
253 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
254 |
fun mk_eval_flat_tac ctxt dead_pre_map_comp0 ssig_map_id ssig_map_comp flat_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
255 |
eval_core_pointful_natural eval_core_flat eval cond_eval_o_flat = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
256 |
HEADGOAL (rtac ctxt (unfold_thms ctxt [o_apply] cond_eval_o_flat)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
257 |
unfold_thms_tac ctxt [dead_pre_map_comp0, flat_pointful_natural, eval_core_flat, eval, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
258 |
o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
259 |
HEADGOAL (rtac ctxt refl THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
260 |
asm_simp_tac (ss_only_silent (ssig_map_id :: eval_core_pointful_natural :: eval :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
261 |
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
262 |
@{thms id_apply id_def[symmetric] fst_conv map_prod_simp convol_apply}) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
263 |
ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
264 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
265 |
fun instantiate_map_comp_with_f_g ctxt = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
266 |
Rule_Insts.of_rule ctxt ([], [NONE, SOME ("%x. f (g x)")]) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
267 |
[(Binding.name "f", NONE, NoSyn), (Binding.name "g", NONE, NoSyn)]; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
268 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
269 |
fun mk_eval_core_embL_tac ctxt old_ssig_induct dead_pre_map_comp0 dead_pre_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
270 |
Sig_pointful_natural unsig_thm old_sig_map_comp old_sig_map_cong old_Lam_pointful_natural |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
271 |
Lam_def flat_embL old_eval_core_simps eval_core_simps embL_simps embL_pointful_natural = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
272 |
HEADGOAL (rtac ctxt old_ssig_induct) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
273 |
ALLGOALS (asm_simp_tac (ss_only_silent (Sig_pointful_natural :: unsig_thm :: Lam_def :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
274 |
(flat_embL RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: embL_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
275 |
old_eval_core_simps @ eval_core_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
276 |
@{thms id_apply id_def[symmetric] o_apply map_sum.simps sum.case}) ctxt)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
277 |
HEADGOAL (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
278 |
(old_Lam_pointful_natural :: embL_pointful_natural :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
279 |
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, instantiate_map_comp_with_f_g ctxt |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
280 |
dead_pre_map_comp0, old_sig_map_comp] @ @{thms map_prod_simp}) ctxt))); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
281 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
282 |
fun mk_eval_core_flat_tac ctxt ssig_induct dead_pre_map_id dead_pre_map_comp0 dead_pre_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
283 |
fp_map_id sig_map_comp sig_map_cong ssig_maps ssig_map_comp flat_simps flat_natural flat_flat |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
284 |
Lam_natural_sym eval_core_simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
285 |
HEADGOAL (rtac ctxt ssig_induct) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
286 |
ALLGOALS (full_simp_tac (ss_only_silent ((flat_flat RS sym) :: dead_pre_map_id :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
287 |
dead_pre_map_comp :: fp_map_id :: sig_map_comp :: ssig_map_comp :: ssig_maps @ flat_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
288 |
eval_core_simps @ @{thms o_def id_def[symmetric] convol_apply id_apply snd_conv}) ctxt)) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
289 |
HEADGOAL (asm_simp_tac (Simplifier.add_cong sig_map_cong (ss_only_silent |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
290 |
(map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, sig_map_comp] @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
291 |
flat_natural :: Lam_natural_sym :: @{thms id_apply fst_conv map_prod_simp}) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
292 |
ctxt))); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
293 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
294 |
fun mk_eval_sctr_tac ctxt proto_sctr_pointful_natural eval_Oper algLam sctr_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
295 |
HEADGOAL (rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
296 |
unfold_thms_tac ctxt [proto_sctr_pointful_natural, eval_Oper, algLam RS sym, sctr_def, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
297 |
o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
298 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
299 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
300 |
fun mk_eval_V_or_CLeaf_tac ctxt dead_pre_map_id dead_pre_map_comp fp_map_id dtor_unfold_unique |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
301 |
V_or_CLeaf_map eval_core_simps eval = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
302 |
HEADGOAL (rtac ctxt (trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym] RS fun_cong |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
303 |
OF [ext, ext])) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
304 |
ALLGOALS (asm_simp_tac (ss_only_silent (dead_pre_map_id :: fp_map_id :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
305 |
unfold_thms ctxt @{thms o_def} dead_pre_map_comp :: V_or_CLeaf_map :: eval :: eval_core_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
306 |
@{thms o_apply id_def[symmetric] id_apply snd_conv convol_apply}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
307 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
308 |
fun mk_eval_Oper_tac ctxt live sig_map_ident sig_map_comp0 sig_map_comp Oper_natural_pointful |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
309 |
VLeaf_natural flat_simps eval_flat algLam_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
310 |
let val VLeaf_natural' = instantiate_natural_rule_with_id ctxt live VLeaf_natural in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
311 |
unfold_thms_tac ctxt [sig_map_comp, VLeaf_natural', algLam_def, o_apply] THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
312 |
unfold_thms_tac ctxt (sig_map_comp0 :: Oper_natural_pointful :: (eval_flat RS sym) :: o_apply :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
313 |
flat_simps) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
314 |
unfold_thms_tac ctxt (@{thm id_apply} :: sig_map_ident :: unfold_thms ctxt [o_def] sig_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
315 |
flat_simps) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
316 |
HEADGOAL (rtac ctxt refl) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
317 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
318 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
319 |
fun mk_extdd_mor_tac ctxt dead_pre_map_comp0 dead_pre_map_comp VLeaf_map ssig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
320 |
flat_pointful_natural eval_core_pointful_natural eval eval_flat eval_VLeaf cutSsig_def prem = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
321 |
HEADGOAL (rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
322 |
unfold_thms_tac ctxt (ssig_map_comp :: unfold_thms ctxt [o_def] dead_pre_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
323 |
flat_pointful_natural :: eval :: eval_flat :: cutSsig_def :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
324 |
@{thms o_apply convol_o id_o id_apply id_def[symmetric]}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
325 |
unfold_thms_tac ctxt (unfold_thms ctxt [dead_pre_map_comp0] prem :: dead_pre_map_comp0 :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
326 |
ssig_map_comp :: eval_core_pointful_natural :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
327 |
@{thms o_def[symmetric] o_apply map_prod_o_convol}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
328 |
unfold_thms_tac ctxt (VLeaf_map :: eval_VLeaf :: @{thms o_def id_apply id_def[symmetric]}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
329 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
330 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
331 |
fun mk_extdd_o_VLeaf_tac ctxt dead_pre_map_comp0 dead_pre_map_comp dtor_inject ssig_maps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
332 |
eval_core_simps eval eval_VLeaf prem = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
333 |
HEADGOAL (rtac ctxt ext THEN' rtac ctxt (dtor_inject RS iffD1) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
334 |
asm_simp_tac (ss_only_silent (dead_pre_map_comp0 :: ssig_maps @ eval_core_simps @ eval :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
335 |
eval_VLeaf :: (mk_pointful ctxt prem RS sym) :: unfold_thms ctxt [o_def] dead_pre_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
336 |
@{thms o_apply convol_apply snd_conv id_apply}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
337 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
338 |
fun mk_flat_embL_tac ctxt old_ssig_induct fp_map_id Sig_pointful_natural old_sig_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
339 |
old_sig_map_cong old_ssig_maps old_flat_simps flat_simps embL_simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
340 |
HEADGOAL (rtac ctxt old_ssig_induct) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
341 |
ALLGOALS (asm_simp_tac (Simplifier.add_cong old_sig_map_cong (ss_only_silent |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
342 |
(fp_map_id :: Sig_pointful_natural :: unfold_thms ctxt [o_def] old_sig_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
343 |
old_ssig_maps @ old_flat_simps @ flat_simps @ embL_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
344 |
@{thms id_apply id_def[symmetric] map_sum.simps}) ctxt))); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
345 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
346 |
fun mk_flat_VLeaf_or_flat_tac ctxt ssig_induct cong simps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
347 |
HEADGOAL (rtac ctxt ssig_induct) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
348 |
ALLGOALS (asm_simp_tac (Simplifier.add_cong cong (ss_only_silent simps ctxt))); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
349 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
350 |
fun mk_Lam_Inl_Inr_tac ctxt unsig Lam_def = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
351 |
TRYALL Goal.conjunction_tac THEN ALLGOALS (rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
352 |
unfold_thms_tac ctxt (o_apply :: Lam_def :: unsig :: @{thms sum.case}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
353 |
ALLGOALS (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
354 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
355 |
fun mk_mor_cutSsig_flat_tac ctxt eval_core_o_map dead_pre_map_comp0 dead_pre_map_comp |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
356 |
dead_pre_map_cong dtor_unfold_unique dead_ssig_map_comp0 ssig_map_comp flat_simps |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
357 |
flat_pointful_natural eval_core_pointful_natural flat_flat flat_VLeaf eval_core_flat cutSsig_def |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
358 |
cutSsig_def_pointful_natural eval_thm prem = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
359 |
HEADGOAL (rtac ctxt (infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt eval_core_o_map)] |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
360 |
(trans OF [dtor_unfold_unique, dtor_unfold_unique RS sym]) OF [ext, ext]) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
361 |
asm_simp_tac (ss_only_silent ((prem RS sym) :: dead_pre_map_comp0 :: ssig_map_comp :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
362 |
eval_core_pointful_natural :: eval_thm :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
363 |
@{thms o_apply map_prod_o_convol o_id convol_o id_o}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
364 |
asm_simp_tac (ss_only_silent ((mk_pointful ctxt prem RS sym) :: dead_pre_map_comp0 :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
365 |
cutSsig_def_pointful_natural :: flat_simps @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
366 |
@{thms o_apply convol_apply map_prod_simp id_apply}) ctxt) THEN' |
62727 | 367 |
rtac ctxt (dead_pre_map_cong OF [asm_rl, refl]) THEN' |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
368 |
asm_simp_tac (ss_only_silent (ssig_map_comp :: cutSsig_def :: flat_pointful_natural :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
369 |
eval_core_flat :: unfold_thms ctxt [o_def] dead_pre_map_comp :: (dead_ssig_map_comp0 RS sym) :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
370 |
(flat_flat RS sym) :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
371 |
@{thms o_apply convol_o fst_convol id_apply id_def[symmetric]}) ctxt) THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
372 |
asm_simp_tac (ss_only_silent (eval_core_pointful_natural :: flat_VLeaf :: |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
373 |
map (unfold_thms ctxt [o_def]) [dead_pre_map_comp0, ssig_map_comp] @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
374 |
@{thms o_apply id_apply id_def[symmetric] map_prod_simp convol_def}) ctxt)); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
375 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
376 |
fun mk_natural_from_transfer_tac ctxt m alives transfer map_ids rel_Grps subst_rel_Grps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
377 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
378 |
val unfold_eq = unfold_thms ctxt @{thms Grp_UNIV_id[symmetric]}; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
379 |
val (rel_Grps', subst_rel_Grps') = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
380 |
apply2 (map (fn thm => unfold_eq (thm RS eq_reflection))) (rel_Grps, subst_rel_Grps); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
381 |
val transfer' = instantiate_transfer_rule_with_Grp_UNIV ctxt alives (unfold_eq transfer) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
382 |
|> unfold_thms ctxt rel_Grps'; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
383 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
384 |
HEADGOAL (Method.insert_tac ctxt [transfer'] THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
385 |
EVERY' (map (subst_asm_tac ctxt NONE o single) subst_rel_Grps')) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
386 |
unfold_thms_tac ctxt (map_ids @ @{thms Grp_def rel_fun_def}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
387 |
HEADGOAL (REPEAT_DETERM_N m o rtac ctxt ext THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
388 |
asm_full_simp_tac (ss_only_silent @{thms simp_thms id_apply o_apply mem_Collect_eq |
63170 | 389 |
top_greatest UNIV_I subset_UNIV[simplified UNIV_def]} ctxt)) THEN |
62692
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
390 |
ALLGOALS (REPEAT_DETERM o etac ctxt @{thm meta_allE} THEN' REPEAT_DETERM o etac ctxt allE THEN' |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
391 |
forward_tac ctxt [sym] THEN' assume_tac ctxt) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
392 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
393 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
394 |
fun mk_natural_by_unfolding_tac ctxt maps = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
395 |
HEADGOAL (rtac ctxt ext) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
396 |
unfold_thms_tac ctxt (@{thms o_def[abs_def] id_apply id_def[symmetric]} @ maps) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
397 |
HEADGOAL (rtac ctxt refl); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
398 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
399 |
fun mk_Retr_coinduct_tac ctxt dtor_rel_coinduct rel_eq = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
400 |
HEADGOAL (EVERY' [rtac ctxt allI, rtac ctxt impI, |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
401 |
rtac ctxt (@{thm ord_le_eq_trans} OF [dtor_rel_coinduct, rel_eq]), |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
402 |
etac ctxt @{thm predicate2D}, assume_tac ctxt]); |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
403 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
404 |
fun mk_sig_transfer_tac ctxt pre_rel_def rel_eqs0 transfer = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
405 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
406 |
val rel_eqs = no_refl rel_eqs0; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
407 |
val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
408 |
val transfer' = unfold_thms ctxt rel_eq_syms transfer |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
409 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
410 |
HEADGOAL (rtac ctxt transfer') ORELSE |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
411 |
unfold_thms_tac ctxt (pre_rel_def :: rel_eq_syms @ |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
412 |
@{thms BNF_Def.vimage2p_def BNF_Composition.id_bnf_def}) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
413 |
HEADGOAL (rtac ctxt transfer') |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
414 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
415 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
416 |
fun mk_transfer_by_transfer_prover_tac ctxt defs rel_eqs0 transfers = |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
417 |
let |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
418 |
val rel_eqs = no_refl rel_eqs0; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
419 |
val rel_eq_syms = map (fn thm => thm RS sym) rel_eqs; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
420 |
in |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
421 |
unfold_thms_tac ctxt (defs @ rel_eq_syms) THEN |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
422 |
HEADGOAL (transfer_prover_add_tac ctxt rel_eqs transfers) |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
423 |
end; |
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
424 |
|
0701f25fac39
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
blanchet
parents:
diff
changeset
|
425 |
end; |