author | haftmann |
Fri, 28 Oct 2005 16:35:40 +0200 | |
changeset 18011 | 685d95c793ff |
parent 17795 | 5b18c3343028 |
child 18591 | 04b9f2bf5a48 |
permissions | -rw-r--r-- |
16978 | 1 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
2 |
(* Title: Provers/eqsubst.ML |
16434 | 3 |
ID: $Id$ |
15481 | 4 |
Author: Lucas Dixon, University of Edinburgh |
5 |
lucas.dixon@ed.ac.uk |
|
16978 | 6 |
Modified: 18 Feb 2005 - Lucas - |
15481 | 7 |
Created: 29 Jan 2005 |
8 |
*) |
|
16978 | 9 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
15481 | 10 |
(* DESCRIPTION: |
11 |
||
12 |
A Tactic to perform a substiution using an equation. |
|
13 |
||
14 |
*) |
|
15 |
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) |
|
16 |
||
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
17 |
|
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
18 |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
19 |
(* Logic specific data stub *) |
15481 | 20 |
signature EQRULE_DATA = |
21 |
sig |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
22 |
|
15481 | 23 |
(* to make a meta equality theorem in the current logic *) |
24 |
val prep_meta_eq : thm -> thm list |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
25 |
|
15481 | 26 |
end; |
27 |
||
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
28 |
|
15481 | 29 |
(* the signature of an instance of the SQSUBST tactic *) |
16978 | 30 |
signature EQSUBST_TAC = |
15481 | 31 |
sig |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
32 |
|
16978 | 33 |
exception eqsubst_occL_exp of |
34 |
string * (int list) * (thm list) * int * thm; |
|
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
35 |
|
17795 | 36 |
type match |
37 |
type searchinfo |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
38 |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
39 |
val prep_subst_in_asm : |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
40 |
int (* subgoal to subst in *) |
16978 | 41 |
-> thm (* target theorem with subgoals *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
42 |
-> int (* premise to subst in *) |
16978 | 43 |
-> (cterm list (* certified free var placeholders for vars *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
44 |
* int (* premice no. to subst *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
45 |
* int (* number of assumptions of premice *) |
16978 | 46 |
* thm) (* premice as a new theorem for forward reasoning *) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
47 |
* searchinfo (* search info: prem id etc *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
48 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
49 |
val prep_subst_in_asms : |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
50 |
int (* subgoal to subst in *) |
16978 | 51 |
-> thm (* target theorem with subgoals *) |
52 |
-> ((cterm list (* certified free var placeholders for vars *) |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
53 |
* int (* premice no. to subst *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
54 |
* int (* number of assumptions of premice *) |
16978 | 55 |
* thm) (* premice as a new theorem for forward reasoning *) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
56 |
* searchinfo) list |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
57 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
58 |
val apply_subst_in_asm : |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
59 |
int (* subgoal *) |
16978 | 60 |
-> thm (* overall theorem *) |
61 |
-> thm (* rule *) |
|
62 |
-> (cterm list (* certified free var placeholders for vars *) |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
63 |
* int (* assump no being subst *) |
16978 | 64 |
* int (* num of premises of asm *) |
65 |
* thm) (* premthm *) |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
66 |
* match |
16978 | 67 |
-> thm Seq.seq |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
68 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
69 |
val prep_concl_subst : |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
70 |
int (* subgoal *) |
16978 | 71 |
-> thm (* overall goal theorem *) |
72 |
-> (cterm list * thm) * searchinfo (* (cvfs, conclthm), matchf *) |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
73 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
74 |
val apply_subst_in_concl : |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
75 |
int (* subgoal *) |
16978 | 76 |
-> thm (* thm with all goals *) |
77 |
-> cterm list (* certified free var placeholders for vars *) |
|
78 |
* thm (* trivial thm of goal concl *) |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
79 |
(* possible matches/unifiers *) |
16978 | 80 |
-> thm (* rule *) |
15550
806214035275
lucas - added more comments and an extra type to clarify the code.
dixon
parents:
15538
diff
changeset
|
81 |
-> match |
16978 | 82 |
-> thm Seq.seq (* substituted goal *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
83 |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
84 |
(* basic notion of search *) |
16978 | 85 |
val searchf_tlr_unify_all : |
86 |
(searchinfo |
|
87 |
-> term (* lhs *) |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
88 |
-> match Seq.seq Seq.seq) |
16978 | 89 |
val searchf_tlr_unify_valid : |
90 |
(searchinfo |
|
91 |
-> term (* lhs *) |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
92 |
-> match Seq.seq Seq.seq) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
93 |
|
16978 | 94 |
(* specialise search constructor for conclusion skipping occurrences. *) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
95 |
val skip_first_occs_search : |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
96 |
int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
97 |
(* specialised search constructor for assumptions using skips *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
98 |
val skip_first_asm_occs_search : |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
99 |
('a -> 'b -> 'c Seq.seq Seq.seq) -> |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
100 |
'a -> int -> 'b -> 'c IsaPLib.skipseqT |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
101 |
|
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
102 |
(* tactics and methods *) |
16978 | 103 |
val eqsubst_asm_meth : int list -> thm list -> Proof.method |
104 |
val eqsubst_asm_tac : |
|
105 |
int list -> thm list -> int -> thm -> thm Seq.seq |
|
106 |
val eqsubst_asm_tac' : |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
107 |
(* search function with skips *) |
16978 | 108 |
(searchinfo -> int -> term -> match IsaPLib.skipseqT) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
109 |
-> int (* skip to *) |
16978 | 110 |
-> thm (* rule *) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
111 |
-> int (* subgoal number *) |
16978 | 112 |
-> thm (* tgt theorem with subgoals *) |
113 |
-> thm Seq.seq (* new theorems *) |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
114 |
|
16978 | 115 |
val eqsubst_meth : int list -> thm list -> Proof.method |
116 |
val eqsubst_tac : |
|
117 |
int list -> thm list -> int -> thm -> thm Seq.seq |
|
118 |
val eqsubst_tac' : |
|
119 |
(searchinfo -> term -> match Seq.seq) |
|
120 |
-> thm -> int -> thm -> thm Seq.seq |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
121 |
|
16978 | 122 |
val meth : (bool * int list) * thm list -> Proof.context -> Proof.method |
15481 | 123 |
val setup : (Theory.theory -> Theory.theory) list |
124 |
end; |
|
125 |
||
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
126 |
|
16978 | 127 |
functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
128 |
: EQSUBST_TAC |
15481 | 129 |
= struct |
130 |
||
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15855
diff
changeset
|
131 |
(* a type abriviation for match information *) |
16978 | 132 |
type match = |
133 |
((indexname * (sort * typ)) list (* type instantiations *) |
|
134 |
* (indexname * (typ * term)) list) (* term instantiations *) |
|
135 |
* (string * typ) list (* fake named type abs env *) |
|
136 |
* (string * typ) list (* type abs env *) |
|
137 |
* term (* outer term *) |
|
15550
806214035275
lucas - added more comments and an extra type to clarify the code.
dixon
parents:
15538
diff
changeset
|
138 |
|
16978 | 139 |
type searchinfo = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
140 |
Sign.sg (* sign for matching *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
141 |
* int (* maxidx *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
142 |
* BasicIsaFTerm.FcTerm (* focusterm to search under *) |
15550
806214035275
lucas - added more comments and an extra type to clarify the code.
dixon
parents:
15538
diff
changeset
|
143 |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
144 |
(* FOR DEBUGGING... |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
145 |
type trace_subst_errT = int (* subgoal *) |
16978 | 146 |
* thm (* thm with all goals *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
147 |
* (Thm.cterm list (* certified free var placeholders for vars *) |
16978 | 148 |
* thm) (* trivial thm of goal concl *) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
149 |
(* possible matches/unifiers *) |
16978 | 150 |
* thm (* rule *) |
151 |
* (((indexname * typ) list (* type instantiations *) |
|
152 |
* (indexname * term) list ) (* term instantiations *) |
|
153 |
* (string * typ) list (* Type abs env *) |
|
154 |
* term) (* outer term *); |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
155 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
156 |
val trace_subst_err = (ref NONE : trace_subst_errT option ref); |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
157 |
val trace_subst_search = ref false; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
158 |
exception trace_subst_exp of trace_subst_errT; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
159 |
*) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
160 |
|
16978 | 161 |
(* also defined in /HOL/Tools/inductive_codegen.ML, |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
162 |
maybe move this to seq.ML ? *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
163 |
infix 5 :->; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
164 |
fun s :-> f = Seq.flat (Seq.map f s); |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
165 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
166 |
(* search from top, left to right, then down *) |
16978 | 167 |
fun search_tlr_all_f f ft = |
15481 | 168 |
let |
16978 | 169 |
fun maux ft = |
170 |
let val t' = (IsaFTerm.focus_of_fcterm ft) |
|
171 |
(* val _ = |
|
172 |
if !trace_subst_search then |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
173 |
(writeln ("Examining: " ^ (TermLib.string_of_term t')); |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
174 |
TermLib.writeterm t'; ()) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
175 |
else (); *) |
16978 | 176 |
in |
177 |
(case t' of |
|
178 |
(_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), |
|
179 |
Seq.cons(f ft, |
|
15481 | 180 |
maux (IsaFTerm.focus_right ft))) |
15929
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
181 |
| (Abs _) => Seq.cons(f ft, maux (IsaFTerm.focus_abs ft)) |
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
182 |
| leaf => Seq.single (f ft)) end |
15481 | 183 |
in maux ft end; |
184 |
||
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
185 |
(* search from top, left to right, then down *) |
16978 | 186 |
fun search_tlr_valid_f f ft = |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
187 |
let |
16978 | 188 |
fun maux ft = |
189 |
let |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
190 |
val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty |
16978 | 191 |
in |
192 |
(case (IsaFTerm.focus_of_fcterm ft) of |
|
193 |
(_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft), |
|
194 |
Seq.cons(hereseq, |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
195 |
maux (IsaFTerm.focus_right ft))) |
15929
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
196 |
| (Abs _) => Seq.cons(hereseq, maux (IsaFTerm.focus_abs ft)) |
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
197 |
| leaf => Seq.single (hereseq)) |
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
198 |
end |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
199 |
in maux ft end; |
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
200 |
|
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
201 |
(* search all unifications *) |
16978 | 202 |
fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs = |
203 |
IsaFTerm.find_fcterm_matches |
|
204 |
search_tlr_all_f |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
205 |
(IsaFTerm.clean_unify_ft sgn maxidx lhs) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
206 |
ft; |
15481 | 207 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
208 |
(* search only for 'valid' unifiers (non abs subterms and non vars) *) |
16978 | 209 |
fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs = |
210 |
IsaFTerm.find_fcterm_matches |
|
211 |
search_tlr_valid_f |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
212 |
(IsaFTerm.clean_unify_ft sgn maxidx lhs) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
213 |
ft; |
15929
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
214 |
|
15814
d65f461c8672
lucas - fixed a big with renaming of bound variables. Other small changes.
dixon
parents:
15550
diff
changeset
|
215 |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
216 |
(* apply a substitution in the conclusion of the theorem th *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
217 |
(* cfvs are certified free var placeholders for goal params *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
218 |
(* conclthm is a theorem of for just the conclusion *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
219 |
(* m is instantiation/match information *) |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
220 |
(* rule is the equation for substitution *) |
16978 | 221 |
fun apply_subst_in_concl i th (cfvs, conclthm) rule m = |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
222 |
(RWInst.rw m rule conclthm) |
15855 | 223 |
|> IsaND.unfix_frees cfvs |
15915
b0e8b37642a4
lucas - improved interface to isand.ML and cleaned up clean-unification code, and added some better comments.
dixon
parents:
15855
diff
changeset
|
224 |
|> RWInst.beta_eta_contract |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
225 |
|> (fn r => Tactic.rtac r i th); |
15481 | 226 |
|
227 |
(* substitute within the conclusion of goal i of gth, using a meta |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
228 |
equation rule. Note that we assume rule has var indicies zero'd *) |
16978 | 229 |
fun prep_concl_subst i gth = |
230 |
let |
|
15481 | 231 |
val th = Thm.incr_indexes 1 gth; |
232 |
val tgt_term = Thm.prop_of th; |
|
233 |
||
234 |
val sgn = Thm.sign_of_thm th; |
|
235 |
val ctermify = Thm.cterm_of sgn; |
|
236 |
val trivify = Thm.trivial o ctermify; |
|
237 |
||
238 |
val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; |
|
239 |
val cfvs = rev (map ctermify fvs); |
|
240 |
||
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
241 |
val conclterm = Logic.strip_imp_concl fixedbody; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
242 |
val conclthm = trivify conclterm; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
243 |
val maxidx = Term.maxidx_of_term conclterm; |
16978 | 244 |
val ft = ((IsaFTerm.focus_right |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
245 |
o IsaFTerm.focus_left |
16978 | 246 |
o IsaFTerm.fcterm_of_term |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
247 |
o Thm.prop_of) conclthm) |
15481 | 248 |
in |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
249 |
((cfvs, conclthm), (sgn, maxidx, ft)) |
15481 | 250 |
end; |
251 |
||
252 |
(* substitute using an object or meta level equality *) |
|
16978 | 253 |
fun eqsubst_tac' searchf instepthm i th = |
254 |
let |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
255 |
val (cvfsconclthm, searchinfo) = prep_concl_subst i th; |
16978 | 256 |
val stepthms = |
257 |
Seq.map Drule.zero_var_indexes |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
258 |
(Seq.of_list (EqRuleData.prep_meta_eq instepthm)); |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
259 |
fun rewrite_with_thm r = |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
260 |
let val (lhs,_) = Logic.dest_equals (Thm.concl_of r); |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
261 |
in (searchf searchinfo lhs) |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
262 |
:-> (apply_subst_in_concl i th cvfsconclthm r) end; |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
263 |
in stepthms :-> rewrite_with_thm end; |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
264 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
265 |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
266 |
(* Tactic.distinct_subgoals_tac -- fails to free type variables *) |
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
267 |
|
16978 | 268 |
(* custom version of distinct subgoals that works with term and |
269 |
type variables. Asssumes th is in beta-eta normal form. |
|
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
270 |
Also, does nothing if flexflex contraints are present. *) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
271 |
fun distinct_subgoals th = |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
272 |
if List.null (Thm.tpairs_of th) then |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
273 |
let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
274 |
val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
275 |
in |
16978 | 276 |
IsaND.unfix_frees_and_tfrees |
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
277 |
fixes |
16978 | 278 |
(Drule.implies_intr_list |
279 |
(Library.gen_distinct |
|
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
280 |
(fn (x, y) => Thm.term_of x = Thm.term_of y) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
281 |
cprems) fixedthconcl) |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
282 |
end |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
283 |
else th; |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
284 |
|
16978 | 285 |
(* General substiuttion of multiple occurances using one of |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
286 |
the given theorems*) |
16978 | 287 |
exception eqsubst_occL_exp of |
288 |
string * (int list) * (thm list) * int * thm; |
|
289 |
fun skip_first_occs_search occ srchf sinfo lhs = |
|
290 |
case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
291 |
IsaPLib.skipmore _ => Seq.empty |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
292 |
| IsaPLib.skipseq ss => Seq.flat ss; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
293 |
|
16978 | 294 |
fun eqsubst_tac occL thms i th = |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
295 |
let val nprems = Thm.nprems_of th in |
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
296 |
if nprems < i then Seq.empty else |
16978 | 297 |
let val thmseq = (Seq.of_list thms) |
298 |
fun apply_occ occ th = |
|
299 |
thmseq :-> |
|
300 |
(fn r => eqsubst_tac' (skip_first_occs_search |
|
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
301 |
occ searchf_tlr_unify_valid) r |
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
302 |
(i + ((Thm.nprems_of th) - nprems)) |
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
303 |
th); |
16978 | 304 |
val sortedoccL = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
305 |
Library.sort (Library.rev_order o Library.int_ord) occL; |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
306 |
in |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
307 |
Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th) |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
308 |
end |
15959
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
309 |
end |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
310 |
handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); |
366d39e95d3c
lucas - fixed bug with uninstantiated type contexts in eqsubst and added the automatic removal of duplicate subgoals (when there are no flex-flex constraints)
dixon
parents:
15936
diff
changeset
|
311 |
|
15481 | 312 |
|
313 |
(* inthms are the given arguments in Isar, and treated as eqstep with |
|
314 |
the first one, then the second etc *) |
|
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
315 |
fun eqsubst_meth occL inthms = |
16978 | 316 |
Method.METHOD |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
317 |
(fn facts => |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
318 |
HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms )); |
15481 | 319 |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
320 |
(* apply a substitution inside assumption j, keeps asm in the same place *) |
16978 | 321 |
fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = |
322 |
let |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
323 |
val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *) |
16978 | 324 |
val preelimrule = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
325 |
(RWInst.rw m rule pth) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
326 |
|> (Seq.hd o Tactic.prune_params_tac) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
327 |
|> Thm.permute_prems 0 ~1 (* put old asm first *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
328 |
|> IsaND.unfix_frees cfvs (* unfix any global params *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
329 |
|> RWInst.beta_eta_contract; (* normal form *) |
16978 | 330 |
(* val elimrule = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
331 |
preelimrule |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
332 |
|> Tactic.make_elim (* make into elim rule *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
333 |
|> Thm.lift_rule (th2, i); (* lift into context *) |
16007
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
334 |
*) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
335 |
in |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
336 |
(* ~j because new asm starts at back, thus we subtract 1 *) |
16007
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
337 |
Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i)) |
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
338 |
(Tactic.dtac preelimrule i th2) |
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
339 |
|
16978 | 340 |
(* (Thm.bicompose |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
341 |
false (* use unification *) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
342 |
(true, (* elim resolution *) |
16007
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
343 |
elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems) |
4dcccaa11a13
lucas - bugfix to subst in assumptions: fixed index error for conditional rules.
dixon
parents:
16004
diff
changeset
|
344 |
i th2) *) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
345 |
end; |
15481 | 346 |
|
347 |
||
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
348 |
(* prepare to substitute within the j'th premise of subgoal i of gth, |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
349 |
using a meta-level equation. Note that we assume rule has var indicies |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
350 |
zero'd. Note that we also assume that premt is the j'th premice of |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
351 |
subgoal i of gth. Note the repetition of work done for each |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
352 |
assumption, i.e. this can be made more efficient for search over |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
353 |
multiple assumptions. *) |
16978 | 354 |
fun prep_subst_in_asm i gth j = |
355 |
let |
|
15481 | 356 |
val th = Thm.incr_indexes 1 gth; |
357 |
val tgt_term = Thm.prop_of th; |
|
358 |
||
359 |
val sgn = Thm.sign_of_thm th; |
|
360 |
val ctermify = Thm.cterm_of sgn; |
|
361 |
val trivify = Thm.trivial o ctermify; |
|
362 |
||
363 |
val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term; |
|
364 |
val cfvs = rev (map ctermify fvs); |
|
365 |
||
18011
685d95c793ff
cleaned up nth, nth_update, nth_map and nth_string functions
haftmann
parents:
17795
diff
changeset
|
366 |
val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1); |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
367 |
val asm_nprems = length (Logic.strip_imp_prems asmt); |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
368 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
369 |
val pth = trivify asmt; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
370 |
val maxidx = Term.maxidx_of_term asmt; |
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
371 |
|
16978 | 372 |
val ft = ((IsaFTerm.focus_right |
373 |
o IsaFTerm.fcterm_of_term |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
374 |
o Thm.prop_of) pth) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
375 |
in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end; |
15481 | 376 |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
377 |
(* prepare subst in every possible assumption *) |
16978 | 378 |
fun prep_subst_in_asms i gth = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
379 |
map (prep_subst_in_asm i gth) |
16978 | 380 |
((rev o IsaPLib.mk_num_list o length) |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
381 |
(Logic.prems_of_goal (Thm.prop_of gth) i)); |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
382 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
383 |
|
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
384 |
(* substitute in an assumption using an object or meta level equality *) |
16978 | 385 |
fun eqsubst_asm_tac' searchf skipocc instepthm i th = |
386 |
let |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
387 |
val asmpreps = prep_subst_in_asms i th; |
16978 | 388 |
val stepthms = |
389 |
Seq.map Drule.zero_var_indexes |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
390 |
(Seq.of_list (EqRuleData.prep_meta_eq instepthm)) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
391 |
fun rewrite_with_thm r = |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
392 |
let val (lhs,_) = Logic.dest_equals (Thm.concl_of r) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
393 |
fun occ_search occ [] = Seq.empty |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
394 |
| occ_search occ ((asminfo, searchinfo)::moreasms) = |
16978 | 395 |
(case searchf searchinfo occ lhs of |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
396 |
IsaPLib.skipmore i => occ_search i moreasms |
16978 | 397 |
| IsaPLib.skipseq ss => |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
398 |
Seq.append (Seq.map (Library.pair asminfo) |
16978 | 399 |
(Seq.flat ss), |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
400 |
occ_search 1 moreasms)) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
401 |
(* find later substs also *) |
16978 | 402 |
in |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
403 |
(occ_search skipocc asmpreps) :-> (apply_subst_in_asm i th r) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
404 |
end; |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
405 |
in stepthms :-> rewrite_with_thm end; |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
406 |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
407 |
|
16978 | 408 |
fun skip_first_asm_occs_search searchf sinfo occ lhs = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
409 |
IsaPLib.skipto_seqseq occ (searchf sinfo lhs); |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
410 |
|
16978 | 411 |
fun eqsubst_asm_tac occL thms i th = |
412 |
let val nprems = Thm.nprems_of th |
|
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
413 |
in |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
414 |
if nprems < i then Seq.empty else |
16978 | 415 |
let val thmseq = (Seq.of_list thms) |
416 |
fun apply_occ occK th = |
|
417 |
thmseq :-> |
|
418 |
(fn r => |
|
419 |
eqsubst_asm_tac' (skip_first_asm_occs_search |
|
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
420 |
searchf_tlr_unify_valid) occK r |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
421 |
(i + ((Thm.nprems_of th) - nprems)) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
422 |
th); |
16978 | 423 |
val sortedoccs = |
16004
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
424 |
Library.sort (Library.rev_order o Library.int_ord) occL |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
425 |
in |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
426 |
Seq.map distinct_subgoals |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
427 |
(Seq.EVERY (map apply_occ sortedoccs) th) |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
428 |
end |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
429 |
end |
031f56012483
lucas - fixed subst in assumptions to count redexes from left to right.
dixon
parents:
15959
diff
changeset
|
430 |
handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th); |
15481 | 431 |
|
432 |
(* inthms are the given arguments in Isar, and treated as eqstep with |
|
433 |
the first one, then the second etc *) |
|
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
434 |
fun eqsubst_asm_meth occL inthms = |
16978 | 435 |
Method.METHOD |
15538
d8edf54cc28c
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
dixon
parents:
15486
diff
changeset
|
436 |
(fn facts => |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
437 |
HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac occL inthms )); |
15481 | 438 |
|
439 |
(* combination method that takes a flag (true indicates that subst |
|
440 |
should be done to an assumption, false = apply to the conclusion of |
|
441 |
the goal) as well as the theorems to use *) |
|
16978 | 442 |
fun meth ((asmflag, occL), inthms) ctxt = |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
443 |
if asmflag then eqsubst_asm_meth occL inthms else eqsubst_meth occL inthms; |
15481 | 444 |
|
445 |
(* syntax for options, given "(asm)" will give back true, without |
|
446 |
gives back false *) |
|
447 |
val options_syntax = |
|
448 |
(Args.parens (Args.$$$ "asm") >> (K true)) || |
|
449 |
(Scan.succeed false); |
|
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
450 |
|
15929
68bd1e16552a
lucas - added option to select occurance to rewrite e.g. (occ 4)
dixon
parents:
15915
diff
changeset
|
451 |
val ith_syntax = |
15936
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
452 |
(Args.parens (Scan.repeat Args.nat)) |
817ac93ee786
lucas - added ability to provide multiple replacements for subst: syntax is now: subst (1 3) myrule
dixon
parents:
15929
diff
changeset
|
453 |
|| (Scan.succeed [0]); |
15481 | 454 |
|
455 |
(* method syntax, first take options, then theorems *) |
|
456 |
fun meth_syntax meth src ctxt = |
|
16978 | 457 |
meth (snd (Method.syntax ((Scan.lift options_syntax) |
458 |
-- (Scan.lift ith_syntax) |
|
459 |
-- Attrib.local_thms) src ctxt)) |
|
15481 | 460 |
ctxt; |
461 |
||
462 |
(* setup function for adding method to theory. *) |
|
16978 | 463 |
val setup = |
15481 | 464 |
[Method.add_method ("subst", meth_syntax meth, "Substiution with an equation. Use \"(asm)\" option to substitute in an assumption.")]; |
465 |
||
16978 | 466 |
end; |