src/FOLP/simp.ML
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 59621 291934bac95e
     1.1 --- a/src/FOLP/simp.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/FOLP/simp.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -67,7 +67,7 @@
     1.4  
     1.5  (*insert a thm in a discrimination net by its lhs*)
     1.6  fun lhs_insert_thm th net =
     1.7 -    Net.insert_term eq_brl (lhs_of (concl_of th), (false,th)) net
     1.8 +    Net.insert_term eq_brl (lhs_of (Thm.concl_of th), (false,th)) net
     1.9      handle  Net.INSERT => net;
    1.10  
    1.11  (*match subgoal i against possible theorems in the net.
    1.12 @@ -83,7 +83,7 @@
    1.13            biresolve0_tac (Net.unify_term net
    1.14                         (lhs_of (Logic.strip_assums_concl prem))) i);
    1.15  
    1.16 -fun nth_subgoal i thm = nth (prems_of thm) (i - 1);
    1.17 +fun nth_subgoal i thm = nth (Thm.prems_of thm) (i - 1);
    1.18  
    1.19  fun goal_concl i thm = Logic.strip_assums_concl (nth_subgoal i thm);
    1.20  
    1.21 @@ -111,7 +111,7 @@
    1.22  (*Get the norm constants from norm_thms*)
    1.23  val norms =
    1.24    let fun norm thm =
    1.25 -      case lhs_of(concl_of thm) of
    1.26 +      case lhs_of (Thm.concl_of thm) of
    1.27            Const(n,_)$_ => n
    1.28          | _ => error "No constant in lhs of a norm_thm"
    1.29    in map norm normE_thms end;
    1.30 @@ -145,7 +145,7 @@
    1.31  
    1.32  (*get name of the constant from conclusion of a congruence rule*)
    1.33  fun cong_const cong =
    1.34 -    case head_of (lhs_of (concl_of cong)) of
    1.35 +    case head_of (lhs_of (Thm.concl_of cong)) of
    1.36          Const(c,_) => c
    1.37        | _ => ""                 (*a placeholder distinct from const names*);
    1.38  
    1.39 @@ -189,10 +189,10 @@
    1.40  fun add_norms(congs,ccs,new_asms) thm =
    1.41  let val thm' = mk_trans2 thm;
    1.42  (* thm': [?z -> l; Prems; r -> ?t] ==> ?z -> ?t *)
    1.43 -    val nops = nprems_of thm'
    1.44 +    val nops = Thm.nprems_of thm'
    1.45      val lhs = rhs_of_eq 1 thm'
    1.46      val rhs = lhs_of_eq nops thm'
    1.47 -    val asms = tl(rev(tl(prems_of thm')))
    1.48 +    val asms = tl(rev(tl(Thm.prems_of thm')))
    1.49      val hvars = fold_rev (add_hidden_vars ccs) (lhs::rhs::asms) []
    1.50      val hvars = add_new_asm_vars new_asms (rhs,hvars)
    1.51      fun it_asms asm hvars =
    1.52 @@ -216,7 +216,7 @@
    1.53  fun add_norm_tags congs =
    1.54      let val ccs = map cong_const congs
    1.55          val new_asms = filter (exists not o #2)
    1.56 -                (ccs ~~ (map (map atomic o prems_of) congs));
    1.57 +                (ccs ~~ (map (map atomic o Thm.prems_of) congs));
    1.58      in add_norms(congs,ccs,new_asms) end;
    1.59  
    1.60  fun normed_rews congs =
    1.61 @@ -252,7 +252,7 @@
    1.62  
    1.63  (*insert a thm in a thm net*)
    1.64  fun insert_thm_warn th net =
    1.65 -  Net.insert_term Thm.eq_thm_prop (concl_of th, th) net
    1.66 +  Net.insert_term Thm.eq_thm_prop (Thm.concl_of th, th) net
    1.67    handle Net.INSERT =>
    1.68      (writeln ("Duplicate rewrite or congruence rule:\n" ^
    1.69          Display.string_of_thm_without_context th); net);
    1.70 @@ -278,7 +278,7 @@
    1.71  
    1.72  (*delete a thm from a thm net*)
    1.73  fun delete_thm_warn th net =
    1.74 -  Net.delete_term Thm.eq_thm_prop (concl_of th, th) net
    1.75 +  Net.delete_term Thm.eq_thm_prop (Thm.concl_of th, th) net
    1.76    handle Net.DELETE =>
    1.77      (writeln ("No such rewrite or congruence rule:\n" ^
    1.78          Display.string_of_thm_without_context th); net);
    1.79 @@ -348,7 +348,7 @@
    1.80                | seq_try([],_) thm = no_tac thm
    1.81          and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm
    1.82          and one_subt thm =
    1.83 -                let val test = has_fewer_prems (nprems_of thm + 1)
    1.84 +                let val test = has_fewer_prems (Thm.nprems_of thm + 1)
    1.85                      fun loop thm =
    1.86                          COND test no_tac
    1.87                            ((try_rew THEN DEPTH_FIRST test (refl_tac i))
    1.88 @@ -424,8 +424,8 @@
    1.89      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    1.90      else case Seq.pull(cong_tac i thm) of
    1.91              SOME(thm',_) =>
    1.92 -                    let val ps = prems_of thm
    1.93 -                        and ps' = prems_of thm';
    1.94 +                    let val ps = Thm.prems_of thm
    1.95 +                        and ps' = Thm.prems_of thm';
    1.96                          val n = length(ps')-length(ps);
    1.97                          val a = length(Logic.strip_assums_hyp(nth ps (i - 1)))
    1.98                          val l = map (length o Logic.strip_assums_hyp) (take n (drop (i-1) ps'));
    1.99 @@ -436,7 +436,7 @@
   1.100        are represented by rules, generalized over their parameters*)
   1.101  fun add_asms(ss,thm,a,anet,ats,cs) =
   1.102      let val As = strip_varify(nth_subgoal i thm, a, []);
   1.103 -        val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
   1.104 +        val thms = map (Thm.trivial o Thm.cterm_of(Thm.theory_of_thm thm)) As;
   1.105          val new_rws = maps mk_rew_rules thms;
   1.106          val rwrls = map mk_trans (maps mk_rew_rules thms);
   1.107          val anet' = fold_rev lhs_insert_thm rwrls anet;
   1.108 @@ -449,7 +449,7 @@
   1.109  
   1.110  fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
   1.111        SOME(thm',seq') =>
   1.112 -            let val n = (nprems_of thm') - (nprems_of thm)
   1.113 +            let val n = (Thm.nprems_of thm') - (Thm.nprems_of thm)
   1.114              in pr_rew(i,n,thm,thm',more);
   1.115                 if n=0 then (SIMP_LHS::ss, thm', anet, ats, cs)
   1.116                 else ((replicate n PROVE) @ (POP_CS::SIMP_LHS::ss),
   1.117 @@ -499,7 +499,7 @@
   1.118  let val cong_tac = net_tac cong_net
   1.119  in fn i =>
   1.120      (fn thm =>
   1.121 -     if i <= 0 orelse nprems_of thm < i then Seq.empty
   1.122 +     if i <= 0 orelse Thm.nprems_of thm < i then Seq.empty
   1.123       else Seq.single(execute(ss,fl,auto_tac,cong_tac,simp_net,i,thm)))
   1.124      THEN TRY(auto_tac i)
   1.125  end;
   1.126 @@ -547,8 +547,8 @@
   1.127  
   1.128  fun find_subst sg T =
   1.129  let fun find (thm::thms) =
   1.130 -        let val (Const(_,cT), va, vb) = dest_red(hd(prems_of thm));
   1.131 -            val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (concl_of thm, []));
   1.132 +        let val (Const(_,cT), va, vb) = dest_red(hd(Thm.prems_of thm));
   1.133 +            val [P] = subtract (op =) [va, vb] (Misc_Legacy.add_term_vars (Thm.concl_of thm, []));
   1.134              val eqT::_ = binder_types cT
   1.135          in if Sign.typ_instance sg (T,eqT) then SOME(thm,va,vb,P)
   1.136             else find thms
   1.137 @@ -559,12 +559,12 @@
   1.138  fun mk_cong sg (f,aTs,rT) (refl,eq) =
   1.139  let val k = length aTs;
   1.140      fun ri((subst,va as Var(_,Ta),vb as Var(_,Tb),P),i,si,T,yik) =
   1.141 -        let val ca = cterm_of sg va
   1.142 -            and cx = cterm_of sg (eta_Var(("X"^si,0),T))
   1.143 -            val cb = cterm_of sg vb
   1.144 -            and cy = cterm_of sg (eta_Var(("Y"^si,0),T))
   1.145 -            val cP = cterm_of sg P
   1.146 -            and cp = cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
   1.147 +        let val ca = Thm.cterm_of sg va
   1.148 +            and cx = Thm.cterm_of sg (eta_Var(("X"^si,0),T))
   1.149 +            val cb = Thm.cterm_of sg vb
   1.150 +            and cy = Thm.cterm_of sg (eta_Var(("Y"^si,0),T))
   1.151 +            val cP = Thm.cterm_of sg P
   1.152 +            and cp = Thm.cterm_of sg (Pinst(f,rT,eq,k,i,T,yik,aTs))
   1.153          in cterm_instantiate [(ca,cx),(cb,cy),(cP,cp)] subst end;
   1.154      fun mk(c,T::Ts,i,yik) =
   1.155          let val si = radixstring(26,"a",i)
   1.156 @@ -579,7 +579,7 @@
   1.157  fun mk_cong_type sg (f,T) =
   1.158  let val (aTs,rT) = strip_type T;
   1.159      fun find_refl(r::rs) =
   1.160 -        let val (Const(eq,eqT),_,_) = dest_red(concl_of r)
   1.161 +        let val (Const(eq,eqT),_,_) = dest_red(Thm.concl_of r)
   1.162          in if Sign.typ_instance sg (rT, hd(binder_types eqT))
   1.163             then SOME(r,(eq,body_type eqT)) else find_refl rs
   1.164          end