diff -r 6468a5d6a16e -r 6389511d4609 src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Thu Jul 14 19:29:00 2005 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Thu Jul 14 20:32:37 2005 +0200 @@ -19,8 +19,6 @@ val current_sign : unit -> Sign.sg - structure fvartabS : TABLE - (* Matching/unification with exceptions handled *) val clean_match : Type.tsig -> Term.term * Term.term -> ((Term.indexname * (Term.sort * Term.typ)) list @@ -53,11 +51,6 @@ val term_of_thm : Thm.thm -> Term.term val get_prems_of_sg_term : Term.term -> Term.term list val triv_thm_from_string : string -> Thm.thm -(* val make_term_into_simp_thm : - (string * Term.typ) list -> Sign.sg -> Term.term -> Thm.thm - val thms_of_prems_in_goal : int -> Thm.thm -> Thm.thm list -*) - (* some common term manipulations *) val try_dest_Goal : Term.term -> Term.term @@ -101,8 +94,7 @@ (* Isar term skolemisationm and unsolemisation *) (* I think this is written also in IsarRTechn and also in somewhere else *) - (* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term - val unskolemise_term : (string,Term.typ) list -> Term.term -> Term.term *) + (* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term *) val unskolemise_all_term : Term.term -> (((string * Term.typ) * string) list * Term.term) @@ -112,7 +104,7 @@ val readwty : string -> string -> Term.term (* pretty stuff *) - val pp_term : Term.term -> unit + val print_term : Term.term -> unit val pretty_print_sort : string list -> string val pretty_print_term : Term.term -> string val pretty_print_type : Term.typ -> string @@ -255,47 +247,13 @@ fun writetype t = writeln (pretty_print_type t); fun writesort s = writeln (pretty_print_sort s); - -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Turn on show types *) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - -(* if (!show_types) then true else set show_types; *) - -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* functions *) -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) - fun current_sign () = Theory.sign_of (the_context()); fun cterm_of_term (t : term) = Thm.cterm_of (current_sign()) t; fun term_of_thm t = (Thm.prop_of t); -(* little function to make a trueprop of anything by putting a P - function in front of it... -fun HOL_mk_term_prop t = - ((Const("Trueprop", Type("fun", - [Type("bool", []), Type("prop", [])]))) $ - ((Free("P", Type("fun", [type_of t, - Type("bool", [])]))) $ t)); - -*) - fun string_of_term t = (Sign.string_of_term (current_sign()) t); - -(* -(allt as (Const("Trueprop", ty) $ m)) = - (string_of_cterm (cterm_of_term allt)) - | string_of_term (t : term) = - string_of_cterm (cterm_of_term (HOL_mk_term_prop t)); -*) - -(* creates a simple cterm of the term if it's not already a prop by - prefixing it with a polymorphic function P, then create the cterm - and print that. Handy tool for printing terms that are not - already propositions, or not cterms. -*) -fun pp_term t = writeln (string_of_term t); +fun print_term t = writeln (string_of_term t); (* create a trivial HOL thm from anything... *) fun triv_thm_from_string s = @@ -330,13 +288,6 @@ [] => false | (_::_) => true); - (* working with Isar terms and their skolemisation(s) *) -(* val skolemise_term : (string,Term.typ) list -> Term.term -> Term.term - val unskolemise_term : (string,Term.typ) list -> Term.term -> Term.term -*) - -(* cunning version *) - (* This version avoids name conflicts that might be introduced by unskolemisation, and returns a list of (string * Term.typ) * string, where the outer string is the original name, and the inner string is @@ -371,17 +322,6 @@ in (renames,t') end; end -(* fun unskolemise_all_term t = - let - fun fmap fv = - let (n,ty) = (Term.dest_Free fv) in - SOME (fv, Free (Syntax.dest_skolem n, ty)) handle LIST _ => NONE - end - val substfrees = List.mapPartial fmap (Term.term_frees t) - in - Term.subst_free substfrees t - end; *) - (* true if the type t is a function *) fun is_fun_typ (Type(s, l)) = if s = "fun" then true else false @@ -420,40 +360,31 @@ Also, the isabelle term.ML version of aeconv uses a function that it claims doesn't work! *) - fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l = if ty1 = ty2 then term_name_eq t1 t2 l else NONE - | term_name_eq (ah $ at) (bh $ bt) l = let val lopt = (term_name_eq ah bh l) in if isSome lopt then - term_name_eq at bt (valOf lopt) + term_name_eq at bt (valOf lopt) else NONE end - | term_name_eq (Const(a,T)) (Const(b,U)) l = if a=b andalso T=U then SOME l else NONE - | term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l = same_var_check a b l - | term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l = same_var_check a b l - | term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l = same_var_check a b l - | term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l = same_var_check a b l - | term_name_eq (Bound i) (Bound j) l = if i = j then SOME l else NONE - | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE); (* checks to see if the term in a name-equivalent member of the list of terms. *) @@ -570,15 +501,9 @@ (_ :: _) => true | [] => false; - - (* pp_term a; pp_term b; writeln "EQTerm matches are: "; map (fn (a,b) => writeln ("(" ^ (string_of_term a) ^ ", " ^ (string_of_term b) ^ ")")) L;*) - - (* change all bound variables to see ones with appropriate name and type *) - (* naming convention is OK as we use 'variant' from term.ML *) - (* Note "bounds_to_frees" defined below, its better and quicker, but keeps the quantifiers handing about, and changes all bounds, not just universally quantified ones. *) @@ -599,25 +524,21 @@ (subst_bounds ((bnds_to_frees vars frees_names []), body)) end; - - -structure fvartabS = TableFun(type key = string val ord = string_ord); - (* a runtime-quick function which makes sure that every variable has a unique name *) fun unique_namify_aux (ntab,(Abs(s,ty,t))) = - (case (fvartabS.lookup (ntab,s)) of + (case (Symtab.lookup (ntab,s)) of NONE => let - val (ntab2,t2) = unique_namify_aux ((fvartabS.update ((s,s),ntab)), t) + val (ntab2,t2) = unique_namify_aux ((Symtab.update ((s,s),ntab)), t) in (ntab2,Abs(s,ty,t2)) end | SOME s2 => let - val s_new = (Term.variant (fvartabS.keys ntab) s) + val s_new = (Term.variant (Symtab.keys ntab) s) val (ntab2,t2) = - unique_namify_aux ((fvartabS.update ((s_new,s_new),ntab)), t) + unique_namify_aux ((Symtab.update ((s_new,s_new),ntab)), t) in (ntab2,Abs(s_new,ty,t2)) end) @@ -630,17 +551,17 @@ end | unique_namify_aux (nt as (ntab,Const x)) = nt | unique_namify_aux (nt as (ntab,f as Free (s,ty))) = - (case (fvartabS.lookup (ntab,s)) of - NONE => ((fvartabS.update ((s,s),ntab)), f) + (case (Symtab.lookup (ntab,s)) of + NONE => ((Symtab.update ((s,s),ntab)), f) | SOME _ => nt) | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) = - (case (fvartabS.lookup (ntab,s)) of - NONE => ((fvartabS.update ((s,s),ntab)), v) + (case (Symtab.lookup (ntab,s)) of + NONE => ((Symtab.update ((s,s),ntab)), v) | SOME _ => nt) | unique_namify_aux (nt as (ntab, Bound i)) = nt; fun unique_namify t = - #2 (unique_namify_aux (fvartabS.empty, t)); + #2 (unique_namify_aux (Symtab.empty, t)); (* a runtime-quick function which makes sure that every variable has a unique name and also changes bound variables to free variables, used @@ -649,20 +570,20 @@ sematics of the term. This is really a trick for our embedding code. *) fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) = - (case (fvartabS.lookup (ntab,s)) of + (case (Symtab.lookup (ntab,s)) of NONE => let val (ntab2,t2) = bounds_to_frees_aux ((s,ty)::T) - ((fvartabS.update ((s,s),ntab)), t) + ((Symtab.update ((s,s),ntab)), t) in (ntab2,Abs(s,ty,t2)) end | SOME s2 => let - val s_new = (Term.variant (fvartabS.keys ntab) s) + val s_new = (Term.variant (Symtab.keys ntab) s) val (ntab2,t2) = bounds_to_frees_aux ((s_new,ty)::T) - (fvartabS.update (((s_new,s_new),ntab)), t) + (Symtab.update (((s_new,s_new),ntab)), t) in (ntab2,Abs(s_new,ty,t2)) end) @@ -675,12 +596,12 @@ end | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) = - (case (fvartabS.lookup (ntab,s)) of - NONE => ((fvartabS.update ((s,s),ntab)), f) + (case (Symtab.lookup (ntab,s)) of + NONE => ((Symtab.update ((s,s),ntab)), f) | SOME _ => nt) | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) = - (case (fvartabS.lookup (ntab,s)) of - NONE => ((fvartabS.update ((s,s),ntab)), v) + (case (Symtab.lookup (ntab,s)) of + NONE => ((Symtab.update ((s,s),ntab)), v) | SOME _ => nt) | bounds_to_frees_aux T (nt as (ntab, Bound i)) = let @@ -691,10 +612,10 @@ fun bounds_to_frees t = - #2 (bounds_to_frees_aux [] (fvartabS.empty,t)); + #2 (bounds_to_frees_aux [] (Symtab.empty,t)); fun bounds_to_frees_with_vars vars t = - #2 (bounds_to_frees_aux vars (fvartabS.empty,t)); + #2 (bounds_to_frees_aux vars (Symtab.empty,t)); @@ -713,39 +634,6 @@ fun loose_bnds_to_frees vars t = loose_bnds_to_frees_aux (0,vars) t; -(* puts prems of a theorem into a useful form, (rulify) - Note that any loose bound variables are treated as free vars -*) -(* fun make_term_into_simp_thm vars sgn t = - let - val triv = - Thm.trivial (Thm.cterm_of - sgn (loose_bnds_to_frees vars t)) - in - SplitterData.mk_eq (Drule.standard (ObjectLogic.rulify_no_asm triv)) - end; - -fun thms_of_prems_in_goal i tm= - let - val goal = (List.nth (Thm.prems_of tm,i-1)) - val vars = rev (strip_all_vars goal) - val prems = Logic.strip_assums_hyp (strip_all_body goal) - val simp_prem_thms = - map (make_term_into_simp_thm vars (Thm.sign_of_thm tm)) prems - in - simp_prem_thms - end; -*) - - (* replace all universally quantifief variables (at HOL object level) - with free vars - fun HOL_Alls_to_frees TL (Const("All", _) $ Abs(v, ty, t)) = - HOL_Alls_to_frees ((Free (v, ty)) :: TL) t - | HOL_Alls_to_frees TL t = - (TL,(subst_bounds (TL, t))); -*) - - (* this is just a hack for mixing with interactive mode, and using topthm() *) fun try_dest_Goal (Const("Goal", _) $ T) = T | try_dest_Goal T = T; @@ -785,16 +673,6 @@ (prems, (try_dest_Trueprop (try_dest_Goal concl))) end; -(* old version - fun cleaned_term t = - let - val concl = (HOLogic.dest_Trueprop (Logic.strip_imp_concl - (change_bounds_to_frees t) )) - in - concl - end; -*) - (* change free variables to vars and visa versa *) (* *** check naming is OK, can we just use the vasr old name? *) (* *** Check: Logic.varify and Logic.unvarify *) @@ -813,36 +691,4 @@ | change_frees_to_vars l = l; -end; - - - - (* ignores lambda abstractions, ie (\x y = y) - same as embedding check code, ie. (f a b) = can "a" be embedded in "b" - *) - (* fun term_is_same_or_simpler_than (Abs(s,ty,t)) b = - term_is_same_or_simpler_than t b - - | term_is_same_or_simpler_than a (Abs(s,ty,t)) = - term_is_same_or_simpler_than a t - - | term_is_same_or_simpler_than (ah $ at) (bh $ bt) = - (term_is_same_or_simpler_than (ah $ at) bh) orelse - (term_is_same_or_simpler_than (ah $ at) bt) orelse - ((term_is_same_or_simpler_than ah bh) andalso - (term_is_same_or_simpler_than at bt)) - - | term_is_same_or_simpler_than (ah $ at) b = false - - | term_is_same_or_simpler_than a (bh $ bt) = - (term_is_same_or_simpler_than a bh) orelse - (term_is_same_or_simpler_than a bt) - - | term_is_same_or_simpler_than a b = - if a = b then true else false; - *) - -(* fun term_is_simpler_than t1 t2 = - (are_different_terms t1 t2) andalso - (term_is_same_or_simpler_than t1 t2); -*) +end; \ No newline at end of file