64 -> (thm list -> tactic list) -> unit |
55 -> (thm list -> tactic list) -> unit |
65 end; |
56 end; |
66 |
57 |
67 structure OldGoals: OLD_GOALS = |
58 structure OldGoals: OLD_GOALS = |
68 struct |
59 struct |
69 |
|
70 fun mk_defpair (lhs, rhs) = |
|
71 (case Term.head_of lhs of |
|
72 Const (name, _) => |
|
73 (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) |
|
74 | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
|
75 |
|
76 |
|
77 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
|
78 METAHYPS (fn prems => tac prems) i |
|
79 |
|
80 converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new |
|
81 proof state A==>A, supplying A1,...,An as meta-level assumptions (in |
|
82 "prems"). The parameters x1,...,xm become free variables. If the |
|
83 resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) |
|
84 then it is lifted back into the original context, yielding k subgoals. |
|
85 |
|
86 Replaces unknowns in the context by Frees having the prefix METAHYP_ |
|
87 New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. |
|
88 DOES NOT HANDLE TYPE UNKNOWNS. |
|
89 |
|
90 |
|
91 NOTE: This version does not observe the proof context, and thus cannot |
|
92 work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for |
|
93 properly localized variants of the same idea. |
|
94 ****) |
|
95 |
|
96 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
|
97 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
|
98 Main difference from strip_assums concerns parameters: |
|
99 it replaces the bound variables by free variables. *) |
|
100 fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) = |
|
101 strip_context_aux (params, H :: Hs, B) |
|
102 | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) = |
|
103 let val (b, u) = Syntax.variant_abs (a, T, t) |
|
104 in strip_context_aux ((b, T) :: params, Hs, u) end |
|
105 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
|
106 |
|
107 fun strip_context A = strip_context_aux ([], [], A); |
|
108 |
|
109 local |
|
110 |
|
111 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
|
112 Instantiates distinct free variables by terms of same type.*) |
|
113 fun free_instantiate ctpairs = |
|
114 forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); |
|
115 |
|
116 fun free_of s ((a, i), T) = |
|
117 Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) |
|
118 |
|
119 fun mk_inst v = (Var v, free_of "METAHYP1_" v) |
|
120 in |
|
121 |
|
122 (*Common code for METAHYPS and metahyps_thms*) |
|
123 fun metahyps_split_prem prem = |
|
124 let (*find all vars in the hyps -- should find tvars also!*) |
|
125 val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] |
|
126 val insts = map mk_inst hyps_vars |
|
127 (*replace the hyps_vars by Frees*) |
|
128 val prem' = subst_atomic insts prem |
|
129 val (params,hyps,concl) = strip_context prem' |
|
130 in (insts,params,hyps,concl) end; |
|
131 |
|
132 fun metahyps_aux_tac tacf (prem,gno) state = |
|
133 let val (insts,params,hyps,concl) = metahyps_split_prem prem |
|
134 val maxidx = Thm.maxidx_of state |
|
135 val cterm = Thm.cterm_of (Thm.theory_of_thm state) |
|
136 val chyps = map cterm hyps |
|
137 val hypths = map Thm.assume chyps |
|
138 val subprems = map (Thm.forall_elim_vars 0) hypths |
|
139 val fparams = map Free params |
|
140 val cparams = map cterm fparams |
|
141 fun swap_ctpair (t,u) = (cterm u, cterm t) |
|
142 (*Subgoal variables: make Free; lift type over params*) |
|
143 fun mk_subgoal_inst concl_vars (v, T) = |
|
144 if member (op =) concl_vars (v, T) |
|
145 then ((v, T), true, free_of "METAHYP2_" (v, T)) |
|
146 else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) |
|
147 (*Instantiate subgoal vars by Free applied to params*) |
|
148 fun mk_ctpair (v, in_concl, u) = |
|
149 if in_concl then (cterm (Var v), cterm u) |
|
150 else (cterm (Var v), cterm (list_comb (u, fparams))) |
|
151 (*Restore Vars with higher type and index*) |
|
152 fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = |
|
153 if in_concl then (cterm u, cterm (Var ((a, i), T))) |
|
154 else (cterm u, cterm (Var ((a, i + maxidx), U))) |
|
155 (*Embed B in the original context of params and hyps*) |
|
156 fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
|
157 (*Strip the context using elimination rules*) |
|
158 fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
|
159 (*A form of lifting that discharges assumptions.*) |
|
160 fun relift st = |
|
161 let val prop = Thm.prop_of st |
|
162 val subgoal_vars = (*Vars introduced in the subgoals*) |
|
163 fold Term.add_vars (Logic.strip_imp_prems prop) [] |
|
164 and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] |
|
165 val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
|
166 val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st |
|
167 val emBs = map (cterm o embed) (prems_of st') |
|
168 val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) |
|
169 in (*restore the unknowns to the hypotheses*) |
|
170 free_instantiate (map swap_ctpair insts @ |
|
171 map mk_subgoal_swap_ctpair subgoal_insts) |
|
172 (*discharge assumptions from state in same order*) |
|
173 (implies_intr_list emBs |
|
174 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
|
175 end |
|
176 (*function to replace the current subgoal*) |
|
177 fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state |
|
178 in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; |
|
179 |
|
180 end; |
|
181 |
|
182 (*Returns the theorem list that METAHYPS would supply to its tactic*) |
|
183 fun metahyps_thms i state = |
|
184 let val prem = Logic.nth_prem (i, Thm.prop_of state) |
|
185 and cterm = cterm_of (Thm.theory_of_thm state) |
|
186 val (_,_,hyps,_) = metahyps_split_prem prem |
|
187 in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end |
|
188 handle TERM ("nth_prem", [A]) => NONE; |
|
189 |
|
190 local |
|
191 |
|
192 fun print_vars_terms n thm = |
|
193 let |
|
194 val thy = theory_of_thm thm |
|
195 fun typed s ty = |
|
196 " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty; |
|
197 fun find_vars (Const (c, ty)) = |
|
198 if null (Term.add_tvarsT ty []) then I |
|
199 else insert (op =) (typed c ty) |
|
200 | find_vars (Var (xi, ty)) = |
|
201 insert (op =) (typed (Term.string_of_vname xi) ty) |
|
202 | find_vars (Free _) = I |
|
203 | find_vars (Bound _) = I |
|
204 | find_vars (Abs (_, _, t)) = find_vars t |
|
205 | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2; |
|
206 val prem = Logic.nth_prem (n, Thm.prop_of thm) |
|
207 val tms = find_vars prem [] |
|
208 in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; |
|
209 |
|
210 in |
|
211 |
|
212 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm |
|
213 handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty) |
|
214 |
|
215 end; |
|
216 |
|
217 |
|
218 (* old ways of reading terms *) |
|
219 |
|
220 fun simple_read_term thy T s = |
|
221 let |
|
222 val ctxt = ProofContext.init_global thy |
|
223 |> ProofContext.allow_dummies |
|
224 |> ProofContext.set_mode ProofContext.mode_schematic; |
|
225 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; |
|
226 in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end; |
|
227 |
|
228 fun read_term thy = simple_read_term thy dummyT; |
|
229 fun read_prop thy = simple_read_term thy propT; |
|
230 |
|
231 |
|
232 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
|
233 |
60 |
234 |
61 |
235 (*** Goal package ***) |
62 (*** Goal package ***) |
236 |
63 |
237 (*Each level of goal stack includes a proof state and alternative states, |
64 (*Each level of goal stack includes a proof state and alternative states, |