use regular Term.add_vars, Term.add_frees etc.;
authorwenzelm
Wed Dec 31 00:08:13 2008 +0100 (2008-12-31)
changeset 292664a478f9d2847
parent 29265 5b4247055bd7
child 29267 8615b4f54047
use regular Term.add_vars, Term.add_frees etc.;
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
src/HOL/Tools/datatype_case.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/old_primrec_package.ML
src/Pure/codegen.ML
src/Tools/quickcheck.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_case.ML	Wed Dec 31 00:08:13 2008 +0100
     1.2 +++ b/src/HOL/Tools/datatype_case.ML	Wed Dec 31 00:08:13 2008 +0100
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      HOL/Tools/datatype_case.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
     1.7 -                Stefan Berghofer, TU Muenchen
     1.8 +    Author:     Stefan Berghofer, TU Muenchen
     1.9  
    1.10  Nested case expressions on datatypes.
    1.11  *)
    1.12 @@ -426,9 +425,9 @@
    1.13  fun strip_case' dest (pat, rhs) =
    1.14    case dest (add_term_free_names (pat, [])) rhs of
    1.15      SOME (exp as Free _, clauses) =>
    1.16 -      if member op aconv (term_frees pat) exp andalso
    1.17 +      if member op aconv (OldTerm.term_frees pat) exp andalso
    1.18          not (exists (fn (_, rhs') =>
    1.19 -          member op aconv (term_frees rhs') exp) clauses)
    1.20 +          member op aconv (OldTerm.term_frees rhs') exp) clauses)
    1.21        then
    1.22          maps (strip_case' dest) (map (fn (pat', rhs') =>
    1.23            (subst_free [(exp, pat')] pat, rhs')) clauses)
    1.24 @@ -451,7 +450,7 @@
    1.25      val thy = ProofContext.theory_of ctxt;
    1.26      val consts = ProofContext.consts_of ctxt;
    1.27      fun mk_clause (pat, rhs) =
    1.28 -      let val xs = term_frees pat
    1.29 +      let val xs = Term.add_frees pat []
    1.30        in
    1.31          Syntax.const "_case1" $
    1.32            map_aterms
    1.33 @@ -459,8 +458,8 @@
    1.34                | Const (s, _) => Const (Consts.extern_early consts s, dummyT)
    1.35                | t => t) pat $
    1.36            map_aterms
    1.37 -            (fn x as Free (s, _) =>
    1.38 -                  if member op aconv xs x then Syntax.mark_bound s else x
    1.39 +            (fn x as Free (s, T) =>
    1.40 +                  if member (op =) xs (s, T) then Syntax.mark_bound s else x
    1.41                | t => t) rhs
    1.42        end
    1.43    in case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
     2.1 --- a/src/HOL/Tools/metis_tools.ML	Wed Dec 31 00:08:13 2008 +0100
     2.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Dec 31 00:08:13 2008 +0100
     2.3 @@ -2,7 +2,7 @@
     2.4      Author:     Kong W. Susanto and Lawrence C. Paulson, CU Computer Laboratory
     2.5      Copyright   Cambridge University 2007
     2.6  
     2.7 -HOL setup for the Metis prover (version 2.0 from 2007).
     2.8 +HOL setup for the Metis prover.
     2.9  *)
    2.10  
    2.11  signature METIS_TOOLS =
    2.12 @@ -280,9 +280,10 @@
    2.13  
    2.14    fun cterm_incr_types thy idx = cterm_of thy o (map_types (Logic.incr_tvar idx));
    2.15  
    2.16 -  fun inst_excluded_middle th thy i_atm =
    2.17 -    let val vx = hd (term_vars (prop_of th))
    2.18 -        val substs = [(cterm_of thy vx, cterm_of thy i_atm)]
    2.19 +  fun inst_excluded_middle thy i_atm =
    2.20 +    let val th = EXCLUDED_MIDDLE
    2.21 +        val [vx] = Term.add_vars (prop_of th) []
    2.22 +        val substs = [(cterm_of thy (Var vx), cterm_of thy i_atm)]
    2.23      in  cterm_instantiate substs th  end;
    2.24  
    2.25    (* INFERENCE RULE: AXIOM *)
    2.26 @@ -291,7 +292,7 @@
    2.27  
    2.28    (* INFERENCE RULE: ASSUME *)
    2.29    fun assume_inf ctxt atm =
    2.30 -    inst_excluded_middle EXCLUDED_MIDDLE
    2.31 +    inst_excluded_middle
    2.32        (ProofContext.theory_of ctxt)
    2.33        (singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm));
    2.34  
    2.35 @@ -301,12 +302,12 @@
    2.36    fun inst_inf ctxt thpairs fsubst th =    
    2.37      let val thy = ProofContext.theory_of ctxt
    2.38          val i_th   = lookth thpairs th
    2.39 -        val i_th_vars = term_vars (prop_of i_th)
    2.40 -        fun find_var x = valOf (List.find (fn Term.Var((a,_),_) => a=x) i_th_vars)
    2.41 +        val i_th_vars = Term.add_vars (prop_of i_th) []
    2.42 +        fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
    2.43          fun subst_translation (x,y) =
    2.44                let val v = find_var x
    2.45                    val t = fol_term_to_hol_RAW ctxt y (*we call infer_types below*)
    2.46 -              in  SOME (cterm_of thy v, t)  end
    2.47 +              in  SOME (cterm_of thy (Var v), t)  end
    2.48                handle Option =>
    2.49                    (Output.debug (fn() => "List.find failed for the variable " ^ x ^
    2.50                                           " in " ^ Display.string_of_thm i_th);
    2.51 @@ -370,7 +371,7 @@
    2.52      end;
    2.53  
    2.54    (* INFERENCE RULE: REFL *)
    2.55 -  val refl_x = cterm_of (the_context ()) (hd (term_vars (prop_of REFL_THM)));
    2.56 +  val refl_x = cterm_of (the_context ()) (Var (hd (Term.add_vars (prop_of REFL_THM) [])));
    2.57    val refl_idx = 1 + Thm.maxidx_of REFL_THM;
    2.58  
    2.59    fun refl_inf ctxt t =
    2.60 @@ -429,7 +430,7 @@
    2.61          val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
    2.62          val _ = Output.debug (fn () => "subst' " ^ Display.string_of_thm subst')
    2.63          val eq_terms = map (pairself (cterm_of thy))
    2.64 -                           (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
    2.65 +                           (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
    2.66      in  cterm_instantiate eq_terms subst'  end;
    2.67  
    2.68    val factor = Seq.hd o distinct_subgoals_tac;
     3.1 --- a/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
     3.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
     3.3 @@ -1,6 +1,6 @@
     3.4  (*  Title:      HOL/Tools/old_primrec_package.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
     3.7 +    Author:     Norbert Voelker, FernUni Hagen
     3.8 +    Author:     Stefan Berghofer, TU Muenchen
     3.9  
    3.10  Package for defining functions on datatypes by primitive recursion.
    3.11  *)
    3.12 @@ -58,7 +58,7 @@
    3.13  fun process_eqn thy eq rec_fns =
    3.14    let
    3.15      val (lhs, rhs) =
    3.16 -      if null (term_vars eq) then
    3.17 +      if null (Term.add_vars eq []) then
    3.18          HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    3.19          handle TERM _ => raise RecError "not a proper equation"
    3.20        else raise RecError "illegal schematic variable(s)";
    3.21 @@ -91,7 +91,7 @@
    3.22      else
    3.23       (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
    3.24        check_vars "extra variables on rhs: "
    3.25 -        (map dest_Free (term_frees rhs) \\ lfrees);
    3.26 +        (map dest_Free (OldTerm.term_frees rhs) \\ lfrees);
    3.27        case AList.lookup (op =) rec_fns fnameT of
    3.28          NONE =>
    3.29            (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
     4.1 --- a/src/Pure/codegen.ML	Wed Dec 31 00:08:13 2008 +0100
     4.2 +++ b/src/Pure/codegen.ML	Wed Dec 31 00:08:13 2008 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      Pure/codegen.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Stefan Berghofer, TU Muenchen
     4.7  
     4.8  Generic code generator.
     4.9 @@ -598,7 +597,7 @@
    4.10       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
    4.11  
    4.12  fun new_names t xs = Name.variant_list
    4.13 -  (map (fst o fst o dest_Var) (term_vars t) union
    4.14 +  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
    4.15      add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
    4.16  
    4.17  fun new_name t x = hd (new_names t [x]);
    4.18 @@ -917,9 +916,9 @@
    4.19      val ctxt = ProofContext.init thy;
    4.20      val e =
    4.21        let
    4.22 -        val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    4.23 +        val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
    4.24            error "Term to be evaluated contains type variables";
    4.25 -        val _ = (null (term_vars t) andalso null (term_frees t)) orelse
    4.26 +        val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
    4.27            error "Term to be evaluated contains variables";
    4.28          val (code, gr) = setmp mode ["term_of"]
    4.29            (generate_code_i thy [] "Generated")
     5.1 --- a/src/Tools/quickcheck.ML	Wed Dec 31 00:08:13 2008 +0100
     5.2 +++ b/src/Tools/quickcheck.ML	Wed Dec 31 00:08:13 2008 +0100
     5.3 @@ -70,11 +70,11 @@
     5.4  
     5.5  fun prep_test_term t =
     5.6    let
     5.7 -    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
     5.8 +    val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
     5.9        error "Term to be tested contains type variables";
    5.10 -    val _ = null (term_vars t) orelse
    5.11 +    val _ = null (Term.add_vars t []) orelse
    5.12        error "Term to be tested contains schematic variables";
    5.13 -    val frees = map dest_Free (term_frees t);
    5.14 +    val frees = map dest_Free (OldTerm.term_frees t);
    5.15    in (map fst frees, list_abs_free (frees, t)) end
    5.16  
    5.17  fun test_term ctxt quiet generator_name size i t =
     6.1 --- a/src/ZF/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
     6.2 +++ b/src/ZF/Tools/primrec_package.ML	Wed Dec 31 00:08:13 2008 +0100
     6.3 @@ -1,10 +1,9 @@
     6.4  (*  Title:      ZF/Tools/primrec_package.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Stefan Berghofer and Norbert Voelker
     6.7 -    Copyright   1998  TU Muenchen
     6.8 -    ZF version by Lawrence C Paulson (Cambridge)
     6.9 +    Author:     Norbert Voelker, FernUni Hagen
    6.10 +    Author:     Stefan Berghofer, TU Muenchen
    6.11 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    6.12  
    6.13 -Package for defining functions on datatypes by primitive recursion
    6.14 +Package for defining functions on datatypes by primitive recursion.
    6.15  *)
    6.16  
    6.17  signature PRIMREC_PACKAGE =
    6.18 @@ -33,7 +32,7 @@
    6.19  fun process_eqn thy (eq, rec_fn_opt) =
    6.20    let
    6.21      val (lhs, rhs) =
    6.22 -        if null (term_vars eq) then
    6.23 +        if null (Term.add_vars eq []) then
    6.24              dest_eqn eq handle TERM _ => raise RecError "not a proper equation"
    6.25          else raise RecError "illegal schematic variable(s)";
    6.26  
    6.27 @@ -66,7 +65,7 @@
    6.28    in
    6.29      if has_duplicates (op =) lfrees then
    6.30        raise RecError "repeated variable name in pattern"
    6.31 -    else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
    6.32 +    else if not ((map dest_Free (OldTerm.term_frees rhs)) subset lfrees) then
    6.33        raise RecError "extra variables on rhs"
    6.34      else if length middle > 1 then
    6.35        raise RecError "more than one non-variable in pattern"