equal
deleted
inserted
replaced
7 By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
7 By attaching [eqvt] [bij] or [fresh] to a lemma, the lemma gets stored |
8 in a data-slot in the context. Possible modifiers |
8 in a data-slot in the context. Possible modifiers |
9 are [attribute add] and [attribute del] for adding and deleting, |
9 are [attribute add] and [attribute del] for adding and deleting, |
10 respectively the lemma from the data-slot. |
10 respectively the lemma from the data-slot. |
11 *) |
11 *) |
12 |
|
13 fun dynamic_thm thy name = PureThy.get_thm thy (Facts.Named (name, NONE)); |
|
14 fun dynamic_thms thy name = PureThy.get_thms thy (Facts.Named (name, NONE)); |
|
15 |
12 |
16 signature NOMINAL_THMDECLS = |
13 signature NOMINAL_THMDECLS = |
17 sig |
14 sig |
18 val print_data: Proof.context -> unit |
15 val print_data: Proof.context -> unit |
19 val eqvt_add: attribute |
16 val eqvt_add: attribute |
81 |
78 |
82 fun tactic_eqvt ctx orig_thm pi typi = |
79 fun tactic_eqvt ctx orig_thm pi typi = |
83 let |
80 let |
84 val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
81 val mypi = Thm.cterm_of ctx (Var (pi,typi)) |
85 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
82 val mypifree = Thm.cterm_of ctx (Const ("List.rev",typi --> typi) $ Free (fst pi,typi)) |
86 val perm_pi_simp = dynamic_thms ctx "perm_pi_simp" |
83 val perm_pi_simp = PureThy.get_thms ctx "perm_pi_simp" |
87 in |
84 in |
88 EVERY [tactic ("iffI applied",rtac iffI 1), |
85 EVERY [tactic ("iffI applied",rtac iffI 1), |
89 tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), |
86 tactic ("remove pi with perm_boolE", (dtac @{thm perm_boolE} 1)), |
90 tactic ("solve with orig_thm", (etac orig_thm 1)), |
87 tactic ("solve with orig_thm", (etac orig_thm 1)), |
91 tactic ("applies orig_thm instantiated with rev pi", |
88 tactic ("applies orig_thm instantiated with rev pi", |