On 04/04/2013 03:55, Bill Richter wrote:
> Petros, I have some understanding now of your X_MATCH_CHOOSE_TAC: the
> variable x' doesn't need a type annotation that X_CHOOSE_TAC would need,
> because it infers the type from the existential statement xth by
> xtm = concl xth
> x,bod = dest_exists xtm
> (type_of x)
> Is that more or less correct? I know I'm missing a lot of details. I
> couldn't understand how rule_tac worked. I didn't understand much of your
> Isabelle Light paper, so I wonder if you can try to apply your skills to my
> problems. First, I'd like to be able to pluck the type of a variable out of
> the "environment". I don't think you're doing that. I think you can only
> infer the type of a variable in very specific circumstances. Let's fix the
> manual example for X_CHOOSE_TAC:
>
> g `(?y. x = y + 2) ==> x < x * x`;;
> e(DISCH_THEN(X_CHOOSE_TAC `d:num`));;
> e(ASM_REWRITE_TAC[] THEN ARITH_TAC);;
>
> needs "IsabelleLight/make.ml";;
> g `(?y. x = y + 2) ==> x < x * x`;;
> e(DISCH_THEN(X_MATCH_CHOOSE_TAC `d`));;
> e(ASM_REWRITE_TAC[] THEN ARITH_TAC);;
>
> So we got rid of a type annotation :num, but we inferred it from something
> nearby, the (?y. x = y + 2) that we just discharged. Is that right? Well,
> how about something else nearby.
Yes that's exactly right.
> How about we try to define a function consider of type
> term -> string -> term -> term
> so that
> consider `x` "such that" `t`;;
> would evaluate to the term
> `?x. t`
> and x would not be typed, but would infer its type from the term `t`. Can
> you do that? If we know that a variable x occurs free in a term, can you
> access the type of x by IsabelleLight techniques?
>
Yes you can, and I actually had to do that for the *rule_tac tactics.
Here you go:
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);;
Examples:
# consider `x` "such that" `x >0`;;
val it : term = `?x. x > 0`
# (type_of o fst o dest_exists) it;;
val it : hol_type = `:num`
# consider `y` "any string can go here!" `x >0`;;
Warning: consider: `y` could not be found in `x > 0`
val it : term = `?y. x > 0`
There are some (extreme) cases where you can run into "trouble" with
this. In HOL Light it is possible to construct a term t that contains
two variables `x` with different types. These are treated as two
independent variables, and the code above will use the type of the first
free one it encounters.
Regards,
Petros
--
Petros Papapanagiotou
CISA, School of Informatics
The University of Edinburgh
Email: p.papapanagio...@sms.ed.ac.uk
---
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
------------------------------------------------------------------------------
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
