|
1 (* Title: Tools/misc_legacy.ML |
|
2 |
|
3 Misc legacy stuff -- to be phased out eventually. |
|
4 *) |
|
5 |
|
6 signature MISC_LEGACY = |
|
7 sig |
|
8 val mk_defpair: term * term -> string * term |
|
9 val get_def: theory -> xstring -> thm |
|
10 val simple_read_term: theory -> typ -> string -> term |
|
11 val METAHYPS: (thm list -> tactic) -> int -> tactic |
|
12 end; |
|
13 |
|
14 structure Misc_Legacy: MISC_LEGACY = |
|
15 struct |
|
16 |
|
17 fun mk_defpair (lhs, rhs) = |
|
18 (case Term.head_of lhs of |
|
19 Const (name, _) => |
|
20 (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) |
|
21 | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); |
|
22 |
|
23 |
|
24 fun get_def thy = Thm.axiom thy o Name_Space.intern (Theory.axiom_space thy) o Thm.def_name; |
|
25 |
|
26 |
|
27 fun simple_read_term thy T s = |
|
28 let |
|
29 val ctxt = ProofContext.init_global thy |
|
30 |> ProofContext.allow_dummies |
|
31 |> ProofContext.set_mode ProofContext.mode_schematic; |
|
32 val parse = if T = propT then Syntax.parse_prop else Syntax.parse_term; |
|
33 in parse ctxt s |> Type_Infer.constrain T |> Syntax.check_term ctxt end; |
|
34 |
|
35 |
|
36 (**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
|
37 METAHYPS (fn prems => tac prems) i |
|
38 |
|
39 converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new |
|
40 proof state A==>A, supplying A1,...,An as meta-level assumptions (in |
|
41 "prems"). The parameters x1,...,xm become free variables. If the |
|
42 resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) |
|
43 then it is lifted back into the original context, yielding k subgoals. |
|
44 |
|
45 Replaces unknowns in the context by Frees having the prefix METAHYP_ |
|
46 New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. |
|
47 DOES NOT HANDLE TYPE UNKNOWNS. |
|
48 |
|
49 |
|
50 NOTE: This version does not observe the proof context, and thus cannot |
|
51 work reliably. See also Subgoal.SUBPROOF and Subgoal.FOCUS for |
|
52 properly localized variants of the same idea. |
|
53 ****) |
|
54 |
|
55 local |
|
56 |
|
57 (*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
|
58 H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
|
59 Main difference from strip_assums concerns parameters: |
|
60 it replaces the bound variables by free variables. *) |
|
61 fun strip_context_aux (params, Hs, Const ("==>", _) $ H $ B) = |
|
62 strip_context_aux (params, H :: Hs, B) |
|
63 | strip_context_aux (params, Hs, Const ("all",_) $ Abs (a, T, t)) = |
|
64 let val (b, u) = Syntax.variant_abs (a, T, t) |
|
65 in strip_context_aux ((b, T) :: params, Hs, u) end |
|
66 | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
|
67 |
|
68 fun strip_context A = strip_context_aux ([], [], A); |
|
69 |
|
70 (*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
|
71 Instantiates distinct free variables by terms of same type.*) |
|
72 fun free_instantiate ctpairs = |
|
73 forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); |
|
74 |
|
75 fun free_of s ((a, i), T) = |
|
76 Free (s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), T) |
|
77 |
|
78 fun mk_inst v = (Var v, free_of "METAHYP1_" v) |
|
79 |
|
80 fun metahyps_split_prem prem = |
|
81 let (*find all vars in the hyps -- should find tvars also!*) |
|
82 val hyps_vars = fold Term.add_vars (Logic.strip_assums_hyp prem) [] |
|
83 val insts = map mk_inst hyps_vars |
|
84 (*replace the hyps_vars by Frees*) |
|
85 val prem' = subst_atomic insts prem |
|
86 val (params,hyps,concl) = strip_context prem' |
|
87 in (insts,params,hyps,concl) end; |
|
88 |
|
89 fun metahyps_aux_tac tacf (prem,gno) state = |
|
90 let val (insts,params,hyps,concl) = metahyps_split_prem prem |
|
91 val maxidx = Thm.maxidx_of state |
|
92 val cterm = Thm.cterm_of (Thm.theory_of_thm state) |
|
93 val chyps = map cterm hyps |
|
94 val hypths = map Thm.assume chyps |
|
95 val subprems = map (Thm.forall_elim_vars 0) hypths |
|
96 val fparams = map Free params |
|
97 val cparams = map cterm fparams |
|
98 fun swap_ctpair (t,u) = (cterm u, cterm t) |
|
99 (*Subgoal variables: make Free; lift type over params*) |
|
100 fun mk_subgoal_inst concl_vars (v, T) = |
|
101 if member (op =) concl_vars (v, T) |
|
102 then ((v, T), true, free_of "METAHYP2_" (v, T)) |
|
103 else ((v, T), false, free_of "METAHYP2_" (v, map #2 params ---> T)) |
|
104 (*Instantiate subgoal vars by Free applied to params*) |
|
105 fun mk_ctpair (v, in_concl, u) = |
|
106 if in_concl then (cterm (Var v), cterm u) |
|
107 else (cterm (Var v), cterm (list_comb (u, fparams))) |
|
108 (*Restore Vars with higher type and index*) |
|
109 fun mk_subgoal_swap_ctpair (((a, i), T), in_concl, u as Free (_, U)) = |
|
110 if in_concl then (cterm u, cterm (Var ((a, i), T))) |
|
111 else (cterm u, cterm (Var ((a, i + maxidx), U))) |
|
112 (*Embed B in the original context of params and hyps*) |
|
113 fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
|
114 (*Strip the context using elimination rules*) |
|
115 fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
|
116 (*A form of lifting that discharges assumptions.*) |
|
117 fun relift st = |
|
118 let val prop = Thm.prop_of st |
|
119 val subgoal_vars = (*Vars introduced in the subgoals*) |
|
120 fold Term.add_vars (Logic.strip_imp_prems prop) [] |
|
121 and concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [] |
|
122 val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
|
123 val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st |
|
124 val emBs = map (cterm o embed) (prems_of st') |
|
125 val Cth = implies_elim_list st' (map (elim o Thm.assume) emBs) |
|
126 in (*restore the unknowns to the hypotheses*) |
|
127 free_instantiate (map swap_ctpair insts @ |
|
128 map mk_subgoal_swap_ctpair subgoal_insts) |
|
129 (*discharge assumptions from state in same order*) |
|
130 (implies_intr_list emBs |
|
131 (forall_intr_list cparams (implies_intr_list chyps Cth))) |
|
132 end |
|
133 (*function to replace the current subgoal*) |
|
134 fun next st = Thm.bicompose false (false, relift st, nprems_of st) gno state |
|
135 in Seq.maps next (tacf subprems (Thm.trivial (cterm concl))) end; |
|
136 |
|
137 fun print_vars_terms n thm = |
|
138 let |
|
139 val thy = theory_of_thm thm |
|
140 fun typed s ty = |
|
141 " " ^ s ^ " has type: " ^ Syntax.string_of_typ_global thy ty; |
|
142 fun find_vars (Const (c, ty)) = |
|
143 if null (Term.add_tvarsT ty []) then I |
|
144 else insert (op =) (typed c ty) |
|
145 | find_vars (Var (xi, ty)) = |
|
146 insert (op =) (typed (Term.string_of_vname xi) ty) |
|
147 | find_vars (Free _) = I |
|
148 | find_vars (Bound _) = I |
|
149 | find_vars (Abs (_, _, t)) = find_vars t |
|
150 | find_vars (t1 $ t2) = find_vars t1 #> find_vars t2; |
|
151 val prem = Logic.nth_prem (n, Thm.prop_of thm) |
|
152 val tms = find_vars prem [] |
|
153 in warning (cat_lines ("Found schematic vars in assumptions:" :: tms)) end; |
|
154 |
|
155 in |
|
156 |
|
157 fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm |
|
158 handle THM("assume: variables",_,_) => (print_vars_terms n thm; Seq.empty) |
|
159 |
|
160 end; |
|
161 |
|
162 end; |
|
163 |