I do not know if this qualifies as "simple" or if it is what you are really looking for, but you can use the "trick" I have been using in my "Isabelle Light" library.
Basically, if you know (or if you can determine) what the well-behaved type of your term (string?) is, then you can (try to) force it into that type. eg. (from http://code.google.com/p/hol-light/source/browse/trunk/IsabelleLight/new_tactics.ml ) : let (X_MATCH_CHOOSE_TAC: term -> thm_tactic) = fun x' xth -> try let xtm = concl xth in let x,bod = dest_exists xtm in let x'type = type_of x' in let x'' = if (is_vartype x'type) then inst (type_match x'type (type_of x) []) x' else x' in let pat = vsubst[x'',x] bod in let xth' = ASSUME pat in fun (asl,w) -> let avoids = itlist (union o frees o concl o snd) asl (union (frees w) (thm_frees xth)) in if mem x' avoids then failwith "X_CHOOSE_TAC" else null_meta,[("",xth')::asl,w], fun i [th] -> CHOOSE(x'',INSTANTIATE_ALL i xth) th with Failure _ -> failwith "X_CHOOSE_TAC";; (Compare this to X_CHOOSE_TAC in tactics.ml for contrast.) This allows you to do: prove (` (?x . x = 5) ==> ?y . y > 4`, DISCH_THEN (X_MATCH_CHOOSE_TAC `x`) THEN EXISTS_TAC `x:num` THEN FIRST_ASSUM SUBST1_TAC THEN ARITH_TAC);; instead of: [...] DISCH_THEN (X_CHOOSE_TAC `x:num`) THEN [...] (You can also replace "EXISTS_TAC `x:num`" with "rule_tac [`a`,`x`] exI" to avoid the other type annotation since rule_tac uses the same type instantiation mechanism.) Similarly you could write your disj_term so that it forces t1 and t2 to be bool: let (disj_term: term -> term -> term) = fun t1 t2 -> let mk_bool tm = let ty = type_of tm in if (is_vartype ty) then inst (type_match ty `:bool` []) tm else tm in mk_disj (mk_bool t1,mk_bool t2);; # disj_term `x` `y`;; Warning: inventing type variables Warning: inventing type variables val it : term = `x \/ y` # disj_term `5` `6`;; Exception: Failure "mk_binary". Switching off the "inventing type variables" warning becomes standard practice when using this kind of "tricks": # type_invention_warning := false;; val it : unit = () You may also want to catch any exceptions and give more meaningful error messages, but it is up to you how you want to handle failures. Hope this helps! Regards, Petros On 01/04/2013 05:19, Vincent Aravantinos wrote: > So there is no (simple) way to get a function disj_term that behaves the > way you want. On 31/03/13 23:38, Bill Richter wrote: > > Let me clarify what I want. Take two blocks of text t1 and t2. I want a functions like disj_term so that evaluating > > disj_term `t1` `t2`;; > > yields `t1 \/ t2`. That's not going to be possible if HOL Light does type inference on `t1` and `t2 before disj_term goes to work. And I'm sure from Freek's miz3 that HOL Light does not perform such type inference. > -- 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. ------------------------------------------------------------------------------ Own the Future-Intel® Level Up Game Demo Contest 2013 Rise to greatness in Intel's independent game demo contest. Compete for recognition, cash, and the chance to get your game on Steam. $5K grand prize plus 10 genre and skill prizes. Submit your demo by 6/6/13. http://p.sf.net/sfu/intel_levelupd2d _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
