Petros, your consider code is a huge step toward what I need. I'll try to
finish modifying your code tonight. Here's the string version I have now, and
below that is an earlier term version:
let consider vars_t prfs lab =
let len = String.length vars_t in
let rec findSuchThat = function
n -> if String.sub vars_t n 9 = "such that" then n
else findSuchThat (n + 1) in
let n = findSuchThat 1 in
let vars = String.sub vars_t 0 (n - 1) and
t = String.sub vars_t (n + 9) (len - n - 9) in
let tm = parse_term ("?" ^ vars ^ ". " ^ t) in
match prfs with
p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
THENL [p; ALL_TAC])
| [] -> failwith "consider: no subproof given";;
let CONSIDER_TAC xl lab t prfs =
match prfs with
p::ps -> (warn (ps <> []) "CONSIDER_TAC: additional subproofs ignored";
let tm = itlist (curry mk_exists) xl t in
SUBGOAL_THEN tm ((EVERY_TCL (map X_CHOOSE_THEN xl)) (LABEL_TAC lab))
THENL [p; ALL_TAC])
| [] -> failwith "CONSIDER_TAC: no subproof given";;
It shouldn't be hard to fuse this this with your code:
let try_type tp tm =
try inst (type_match (type_of tm) tp []) tm
with Failure _ -> tm;;
(* Check if two variables match allowing only type instantiations: *)
let vars_match tm1 tm2 =
let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
match inst with
[],[],_ -> tm2
| _ -> failwith "vars_match: no match";;
let consider:(term -> string -> term -> term) =
fun x _ t ->
(* Find the type of a matching variable in t. *)
let tp = try type_of (tryfind (vars_match x) (frees t))
with Failure _ ->
warn true ("consider: `" ^ string_of_term x ^ "` could not be found in
`" ^ string_of_term t ^ "`") ;
type_of x in
(* Try to force x to type tp. *)
let x' = try_type tp x in
mk_exists (x',t);;
If you can't bear not to work on it, you'll probably beat me to it.
I really like your code, and I wonder if you can't do even better. I feel that
we should never have to make an explicit type annotation of a variable that is
in the scope of a typed variable. Assuming that's the right terminology. So
there ought to be an "environment" out of which variable typing can be pulled.
Obviously the values of the variables, once they're typed correctly, can be
pulled out of this "environment".
BTW maybe you can post here the point of the IsabelleLight code you and Jacques
wrote. I think the MizarLight stuff doesn't require you to understand Mizar,
it's all explained in the HOL Light tutorial in the section "Towards more
readable proofs", but maybe IsabelleLight requires you to understand Isabelle,
and I don't.
--
Best,
Bill
------------------------------------------------------------------------------
Minimize network downtime and maximize team effectiveness.
Reduce network management and security costs.Learn how to hire
the most talented Cisco Certified professionals. Visit the
Employer Resources Portal
http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
