src/Pure/raw_simplifier.ML
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 59586 ddf6deaadfe8
     1.1 --- a/src/Pure/raw_simplifier.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -182,11 +182,11 @@
     1.4    end;
     1.5  
     1.6  fun rrule_extra_vars elhs thm =
     1.7 -  rewrite_rule_extra_vars [] (term_of elhs) (Thm.full_prop_of thm);
     1.8 +  rewrite_rule_extra_vars [] (Thm.term_of elhs) (Thm.full_prop_of thm);
     1.9  
    1.10  fun mk_rrule2 {thm, name, lhs, elhs, perm} =
    1.11    let
    1.12 -    val t = term_of elhs;
    1.13 +    val t = Thm.term_of elhs;
    1.14      val fo = Pattern.first_order t orelse not (Pattern.pattern t);
    1.15      val extra = rrule_extra_vars elhs thm;
    1.16    in {thm = thm, name = name, lhs = lhs, elhs = elhs, extra = extra, fo = fo, perm = perm} end;
    1.17 @@ -461,7 +461,7 @@
    1.18  
    1.19  fun del_rrule (rrule as {thm, elhs, ...}) ctxt =
    1.20    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.21 -    (Net.delete_term eq_rrule (term_of elhs, rrule) rules, prems, depth))
    1.22 +    (Net.delete_term eq_rrule (Thm.term_of elhs, rrule) rules, prems, depth))
    1.23    handle Net.DELETE =>
    1.24      (cond_warning ctxt (fn () => print_thm ctxt "Rewrite rule not in simpset:" ("", thm)); ctxt);
    1.25  
    1.26 @@ -470,7 +470,7 @@
    1.27    ctxt |> map_simpset1 (fn (rules, prems, depth) =>
    1.28      let
    1.29        val rrule2 as {elhs, ...} = mk_rrule2 rrule;
    1.30 -      val rules' = Net.insert_term eq_rrule (term_of elhs, rrule2) rules;
    1.31 +      val rules' = Net.insert_term eq_rrule (Thm.term_of elhs, rrule2) rules;
    1.32      in (rules', prems, depth) end)
    1.33    handle Net.INSERT =>
    1.34      (cond_warning ctxt (fn () => print_thm ctxt "Ignoring duplicate rewrite rule:" ("", thm));
    1.35 @@ -496,12 +496,12 @@
    1.36      val (lhs, rhs) = Thm.dest_equals concl handle TERM _ =>
    1.37        raise SIMPLIFIER ("Rewrite rule not a meta-equality", [thm]);
    1.38      val elhs = Thm.dest_arg (Thm.cprop_of (Thm.eta_conversion lhs));
    1.39 -    val erhs = Envir.eta_contract (term_of rhs);
    1.40 +    val erhs = Envir.eta_contract (Thm.term_of rhs);
    1.41      val perm =
    1.42 -      var_perm (term_of elhs, erhs) andalso
    1.43 -      not (term_of elhs aconv erhs) andalso
    1.44 -      not (is_Var (term_of elhs));
    1.45 -  in (prems, term_of lhs, elhs, term_of rhs, perm) end;
    1.46 +      var_perm (Thm.term_of elhs, erhs) andalso
    1.47 +      not (Thm.term_of elhs aconv erhs) andalso
    1.48 +      not (is_Var (Thm.term_of elhs));
    1.49 +  in (prems, Thm.term_of lhs, elhs, Thm.term_of rhs, perm) end;
    1.50  
    1.51  end;
    1.52  
    1.53 @@ -534,7 +534,7 @@
    1.54      if perm then [{thm = thm, name = name, lhs = lhs, elhs = elhs, perm = true}]
    1.55      else
    1.56        (*weak test for loops*)
    1.57 -      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (term_of elhs)
    1.58 +      if rewrite_rule_extra_vars prems lhs rhs orelse is_Var (Thm.term_of elhs)
    1.59        then mk_eq_True ctxt (thm, name)
    1.60        else rrule_eq_True ctxt thm name lhs elhs rhs thm
    1.61    end;
    1.62 @@ -681,7 +681,7 @@
    1.63  
    1.64  fun mk_simproc name lhss proc =
    1.65    make_simproc {name = name, lhss = lhss, proc = fn _ => fn ctxt => fn ct =>
    1.66 -    proc ctxt (term_of ct), identifier = []};
    1.67 +    proc ctxt (Thm.term_of ct), identifier = []};
    1.68  
    1.69  (* FIXME avoid global thy and Logic.varify_global *)
    1.70  fun simproc_global_i thy name = mk_simproc name o map (Thm.cterm_of thy o Logic.varify_global);
    1.71 @@ -692,10 +692,10 @@
    1.72  
    1.73  fun add_proc (proc as Proc {name, lhs, ...}) ctxt =
    1.74   (cond_tracing ctxt (fn () =>
    1.75 -    print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (term_of lhs));
    1.76 +    print_term ctxt ("Adding simplification procedure " ^ quote name ^ " for") (Thm.term_of lhs));
    1.77    ctxt |> map_simpset2
    1.78      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.79 -      (congs, Net.insert_term eq_proc (term_of lhs, proc) procs,
    1.80 +      (congs, Net.insert_term eq_proc (Thm.term_of lhs, proc) procs,
    1.81          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
    1.82    handle Net.INSERT =>
    1.83      (cond_warning ctxt (fn () => "Ignoring duplicate simplification procedure " ^ quote name);
    1.84 @@ -704,7 +704,7 @@
    1.85  fun del_proc (proc as Proc {name, lhs, ...}) ctxt =
    1.86    ctxt |> map_simpset2
    1.87      (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
    1.88 -      (congs, Net.delete_term eq_proc (term_of lhs, proc) procs,
    1.89 +      (congs, Net.delete_term eq_proc (Thm.term_of lhs, proc) procs,
    1.90          mk_rews, termless, subgoal_tac, loop_tacs, solvers))
    1.91    handle Net.DELETE =>
    1.92      (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset");
    1.93 @@ -917,7 +917,7 @@
    1.94      val Simpset ({rules, ...}, {congs, procs, termless, ...}) = simpset_of ctxt;
    1.95      val eta_thm = Thm.eta_conversion t;
    1.96      val eta_t' = Thm.rhs_of eta_thm;
    1.97 -    val eta_t = term_of eta_t';
    1.98 +    val eta_t = Thm.term_of eta_t';
    1.99      fun rew rrule =
   1.100        let
   1.101          val {thm, name, lhs, elhs, extra, fo, perm} = rrule
   1.102 @@ -989,7 +989,7 @@
   1.103  
   1.104      fun proc_rews [] = NONE
   1.105        | proc_rews (Proc {name, proc, lhs, ...} :: ps) =
   1.106 -          if Pattern.matches (Proof_Context.theory_of ctxt) (term_of lhs, term_of t) then
   1.107 +          if Pattern.matches (Proof_Context.theory_of ctxt) (Thm.term_of lhs, Thm.term_of t) then
   1.108              (cond_tracing' ctxt simp_debug (fn () =>
   1.109                print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
   1.110               (case proc ctxt eta_t' of
   1.111 @@ -1021,11 +1021,12 @@
   1.112  fun congc prover ctxt maxt cong t =
   1.113    let
   1.114      val rthm = Thm.incr_indexes (maxt + 1) cong;
   1.115 -    val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (cprop_of rthm)));
   1.116 +    val rlhs = fst (Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of rthm)));
   1.117      val insts = Thm.match (rlhs, t)
   1.118      (* Thm.match can raise Pattern.MATCH;
   1.119         is handled when congc is called *)
   1.120 -    val thm' = Thm.instantiate insts (Thm.rename_boundvars (term_of rlhs) (term_of t) rthm);
   1.121 +    val thm' =
   1.122 +      Thm.instantiate insts (Thm.rename_boundvars (Thm.term_of rlhs) (Thm.term_of t) rthm);
   1.123      val _ =
   1.124        cond_tracing ctxt (fn () => print_thm ctxt "Applying congruence rule:" ("", thm'));
   1.125      fun err (msg, thm) = (cond_tracing ctxt (fn () => print_thm ctxt msg ("", thm)); NONE);
   1.126 @@ -1036,7 +1037,7 @@
   1.127          (case check_conv ctxt true (Drule.beta_eta_conversion t) thm2 of
   1.128            NONE => err ("Congruence proof failed.  Should not have proved", thm2)
   1.129          | SOME thm2' =>
   1.130 -            if op aconv (apply2 term_of (Thm.dest_equals (cprop_of thm2')))
   1.131 +            if op aconv (apply2 Thm.term_of (Thm.dest_equals (Thm.cprop_of thm2')))
   1.132              then NONE else SOME thm2'))
   1.133    end;
   1.134  
   1.135 @@ -1076,13 +1077,13 @@
   1.136  
   1.137      and subc skel ctxt t0 =
   1.138          let val Simpset (_, {congs, ...}) = simpset_of ctxt in
   1.139 -          (case term_of t0 of
   1.140 +          (case Thm.term_of t0 of
   1.141                Abs (a, T, _) =>
   1.142                  let
   1.143                      val (v, ctxt') = Variable.next_bound (a, T) ctxt;
   1.144                      val b = #1 (Term.dest_Free v);
   1.145                      val (v', t') = Thm.dest_abs (SOME b) t0;
   1.146 -                    val b' = #1 (Term.dest_Free (term_of v'));
   1.147 +                    val b' = #1 (Term.dest_Free (Thm.term_of v'));
   1.148                      val _ =
   1.149                        if b <> b' then
   1.150                          warning ("Bad Simplifier context: renamed bound variable " ^
   1.151 @@ -1155,11 +1156,11 @@
   1.152        else nonmut_impc ct ctxt
   1.153  
   1.154      and rules_of_prem prem ctxt =
   1.155 -      if maxidx_of_term (term_of prem) <> ~1
   1.156 +      if maxidx_of_term (Thm.term_of prem) <> ~1
   1.157        then
   1.158         (cond_tracing ctxt (fn () =>
   1.159            print_term ctxt "Cannot add premise as rewrite rule because it contains (type) unknowns:"
   1.160 -            (term_of prem));
   1.161 +            (Thm.term_of prem));
   1.162          (([], NONE), ctxt))
   1.163        else
   1.164          let val (asm, ctxt') = Thm.assume_hyps prem ctxt
   1.165 @@ -1233,7 +1234,7 @@
   1.166          | SOME eqn =>
   1.167              let
   1.168                val prem' = Thm.rhs_of eqn;
   1.169 -              val tprems = map term_of prems;
   1.170 +              val tprems = map Thm.term_of prems;
   1.171                val i = 1 + fold Integer.max (map (fn p =>
   1.172                  find_index (fn q => q aconv p) tprems) (Thm.hyps_of eqn)) ~1;
   1.173                val ((rrs', asm'), ctxt') = rules_of_prem prem' ctxt;
   1.174 @@ -1294,18 +1295,18 @@
   1.175      val ct = Thm.adjust_maxidx_cterm ~1 raw_ct;
   1.176      val {maxidx, ...} = Thm.rep_cterm ct;
   1.177      val _ =
   1.178 -      Theory.subthy (theory_of_cterm ct, thy) orelse
   1.179 +      Theory.subthy (Thm.theory_of_cterm ct, thy) orelse
   1.180          raise CTERM ("rewrite_cterm: bad background theory", [ct]);
   1.181  
   1.182      val ctxt =
   1.183        raw_ctxt
   1.184        |> Context_Position.set_visible false
   1.185        |> inc_simp_depth
   1.186 -      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = term_of ct} ctxt);
   1.187 +      |> (fn ctxt => trace_invoke {depth = simp_depth ctxt, term = Thm.term_of ct} ctxt);
   1.188  
   1.189      val _ =
   1.190        cond_tracing ctxt (fn () =>
   1.191 -        print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (term_of ct));
   1.192 +        print_term ctxt "SIMPLIFIER INVOKED ON THE FOLLOWING TERM:" (Thm.term_of ct));
   1.193    in bottomc (mode, Option.map (Drule.flexflex_unique (SOME ctxt)) oo prover, maxidx) ctxt ct end;
   1.194  
   1.195  val simple_prover =
   1.196 @@ -1356,7 +1357,7 @@
   1.197    | term_depth (f $ t) = 1 + Int.max (term_depth f, term_depth t)
   1.198    | term_depth _ = 0;
   1.199  
   1.200 -val lhs_of_thm = #1 o Logic.dest_equals o prop_of;
   1.201 +val lhs_of_thm = #1 o Logic.dest_equals o Thm.prop_of;
   1.202  
   1.203  (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
   1.204    Returns longest lhs first to avoid folding its subexpressions.*)