src/HOL/Tools/Meson/meson.ML
changeset 59582 0fbed69ff081
parent 59580 cbc38731d42f
child 59586 ddf6deaadfe8
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -101,13 +101,13 @@
     1.4  fun first_order_resolve thA thB =
     1.5    (case
     1.6      try (fn () =>
     1.7 -      let val thy = theory_of_thm thA
     1.8 -          val tmA = concl_of thA
     1.9 -          val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB
    1.10 +      let val thy = Thm.theory_of_thm thA
    1.11 +          val tmA = Thm.concl_of thA
    1.12 +          val Const(@{const_name Pure.imp},_) $ tmB $ _ = Thm.prop_of thB
    1.13            val tenv =
    1.14              Pattern.first_order_match thy (tmB, tmA)
    1.15                                            (Vartab.empty, Vartab.empty) |> snd
    1.16 -          val ct_pairs = map (apply2 (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.17 +          val ct_pairs = map (apply2 (Thm.cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.18        in  thA RS (cterm_instantiate ct_pairs thB)  end) () of
    1.19      SOME th => th
    1.20    | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
    1.21 @@ -152,10 +152,10 @@
    1.22  (* Forward proof while preserving bound variables names *)
    1.23  fun rename_bound_vars_RS th rl =
    1.24    let
    1.25 -    val t = concl_of th
    1.26 -    val r = concl_of rl
    1.27 +    val t = Thm.concl_of th
    1.28 +    val r = Thm.concl_of rl
    1.29      val th' = th RS Thm.rename_boundvars r (protect_bound_var_names r) rl
    1.30 -    val t' = concl_of th'
    1.31 +    val t' = Thm.concl_of th'
    1.32    in Thm.rename_boundvars t' (fix_bound_var_names t t') th' end
    1.33  
    1.34  (*raises exception if no rules apply*)
    1.35 @@ -171,11 +171,11 @@
    1.36     problem, due to the (spurious) choices between projection and imitation. The
    1.37     workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
    1.38  fun quant_resolve_tac ctxt th i st =
    1.39 -  case (concl_of st, prop_of th) of
    1.40 +  case (Thm.concl_of st, Thm.prop_of th) of
    1.41      (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
    1.42      let
    1.43 -      val cc = cterm_of (theory_of_thm th) c
    1.44 -      val ct = Thm.dest_arg (cprop_of th)
    1.45 +      val cc = Thm.cterm_of (Thm.theory_of_thm th) c
    1.46 +      val ct = Thm.dest_arg (Thm.cprop_of th)
    1.47      in resolve_tac ctxt [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
    1.48    | _ => resolve_tac ctxt [th] i st
    1.49  
    1.50 @@ -228,7 +228,7 @@
    1.51    | signed_lits_aux (Const(@{const_name Not},_) $ P) (poslits, neglits) = (poslits, P::neglits)
    1.52    | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
    1.53  
    1.54 -fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (concl_of th)) ([],[]);
    1.55 +fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (Thm.concl_of th)) ([],[]);
    1.56  
    1.57  (*Literals like X=X are tautologous*)
    1.58  fun taut_poslit (Const(@{const_name HOL.eq},_) $ t $ u) = t aconv u
    1.59 @@ -258,7 +258,7 @@
    1.60  
    1.61  fun refl_clause_aux 0 th = th
    1.62    | refl_clause_aux n th =
    1.63 -       case HOLogic.dest_Trueprop (concl_of th) of
    1.64 +       case HOLogic.dest_Trueprop (Thm.concl_of th) of
    1.65            (Const (@{const_name HOL.disj}, _) $ (Const (@{const_name HOL.disj}, _) $ _ $ _) $ _) =>
    1.66              refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
    1.67          | (Const (@{const_name HOL.disj}, _) $ (Const(@{const_name Not},_) $ (Const(@{const_name HOL.eq},_) $ t $ u)) $ _) =>
    1.68 @@ -275,7 +275,7 @@
    1.69  
    1.70  (*Simplify a clause by applying reflexivity to its negated equality literals*)
    1.71  fun refl_clause th =
    1.72 -  let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (concl_of th))
    1.73 +  let val neqs = notequal_lits_count (HOLogic.dest_Trueprop (Thm.concl_of th))
    1.74    in  zero_var_indexes (refl_clause_aux neqs th)  end
    1.75    handle TERM _ => th;  (*probably dest_Trueprop on a weird theorem*)
    1.76  
    1.77 @@ -302,7 +302,7 @@
    1.78  
    1.79  (*Remove duplicate literals, if there are any*)
    1.80  fun nodups ctxt th =
    1.81 -  if has_duplicates (op =) (literals (prop_of th))
    1.82 +  if has_duplicates (op =) (literals (Thm.prop_of th))
    1.83      then nodups_aux ctxt [] th
    1.84      else th;
    1.85  
    1.86 @@ -353,7 +353,8 @@
    1.87    fun freeze_spec th ctxt =
    1.88      let
    1.89        val cert = Proof_Context.cterm_of ctxt;
    1.90 -      val ([x], ctxt') = Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (concl_of th))] ctxt;
    1.91 +      val ([x], ctxt') =
    1.92 +        Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
    1.93        val spec' = Thm.instantiate ([], [(spec_var, cert (Free (x, spec_varT)))]) spec;
    1.94      in (th RS spec', ctxt') end
    1.95  end;
    1.96 @@ -371,10 +372,10 @@
    1.97  fun cnf old_skolem_ths ctxt (th, ths) =
    1.98    let val ctxt_ref = Unsynchronized.ref ctxt   (* FIXME ??? *)
    1.99        fun cnf_aux (th,ths) =
   1.100 -        if not (can HOLogic.dest_Trueprop (prop_of th)) then ths (*meta-level: ignore*)
   1.101 -        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (prop_of th))
   1.102 +        if not (can HOLogic.dest_Trueprop (Thm.prop_of th)) then ths (*meta-level: ignore*)
   1.103 +        else if not (has_conns [@{const_name All}, @{const_name Ex}, @{const_name HOL.conj}] (Thm.prop_of th))
   1.104          then nodups ctxt th :: ths (*no work to do, terminate*)
   1.105 -        else case head_of (HOLogic.dest_Trueprop (concl_of th)) of
   1.106 +        else case head_of (HOLogic.dest_Trueprop (Thm.concl_of th)) of
   1.107              Const (@{const_name HOL.conj}, _) => (*conjunction*)
   1.108                  cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
   1.109            | Const (@{const_name All}, _) => (*universal quantifier*)
   1.110 @@ -395,7 +396,7 @@
   1.111            | _ => nodups ctxt th :: ths  (*no work to do*)
   1.112        and cnf_nil th = cnf_aux (th, [])
   1.113        val cls =
   1.114 -        if has_too_many_clauses ctxt (concl_of th) then
   1.115 +        if has_too_many_clauses ctxt (Thm.concl_of th) then
   1.116            (trace_msg ctxt (fn () =>
   1.117                 "cnf is ignoring: " ^ Display.string_of_thm ctxt th); ths)
   1.118          else
   1.119 @@ -417,7 +418,7 @@
   1.120  
   1.121  (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
   1.122  fun assoc_right th =
   1.123 -  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
   1.124 +  if is_left (Thm.prop_of th) then assoc_right (th RS disj_assoc)
   1.125    else th;
   1.126  
   1.127  (*Must check for negative literal first!*)
   1.128 @@ -439,7 +440,7 @@
   1.129  
   1.130  (*Create a meta-level Horn clause*)
   1.131  fun make_horn crules th =
   1.132 -  if ok4horn (concl_of th)
   1.133 +  if ok4horn (Thm.concl_of th)
   1.134    then make_horn crules (tryres(th,crules)) handle THM _ => th
   1.135    else th;
   1.136  
   1.137 @@ -449,7 +450,7 @@
   1.138    let fun rots (0,_) = hcs
   1.139          | rots (k,th) = zero_var_indexes (make_horn crules th) ::
   1.140                          rots(k-1, assoc_right (th RS disj_comm))
   1.141 -  in case nliterals(prop_of th) of
   1.142 +  in case nliterals(Thm.prop_of th) of
   1.143          1 => th::hcs
   1.144        | n => rots(n, assoc_right th)
   1.145    end;
   1.146 @@ -461,7 +462,7 @@
   1.147      in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
   1.148  
   1.149  (*Is the given disjunction an all-negative support clause?*)
   1.150 -fun is_negative th = forall (not o #1) (literals (prop_of th));
   1.151 +fun is_negative th = forall (not o #1) (literals (Thm.prop_of th));
   1.152  
   1.153  val neg_clauses = filter is_negative;
   1.154  
   1.155 @@ -489,12 +490,12 @@
   1.156         TRYING_eq_assume_tac (i-1) (Thm.eq_assumption i st)
   1.157         handle THM _ => TRYING_eq_assume_tac (i-1) st;
   1.158  
   1.159 -fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (nprems_of st) st;
   1.160 +fun TRYALL_eq_assume_tac st = TRYING_eq_assume_tac (Thm.nprems_of st) st;
   1.161  
   1.162  (*Loop checking: FAIL if trying to prove the same thing twice
   1.163    -- if *ANY* subgoal has repeated literals*)
   1.164  fun check_tac st =
   1.165 -  if exists (fn prem => has_reps (rhyps(prem,[]))) (prems_of st)
   1.166 +  if exists (fn prem => has_reps (rhyps(prem,[]))) (Thm.prems_of st)
   1.167    then  Seq.empty  else  Seq.single st;
   1.168  
   1.169  
   1.170 @@ -506,7 +507,7 @@
   1.171  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
   1.172  fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
   1.173  
   1.174 -fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
   1.175 +fun size_of_subgoals st = fold_rev addconcl (Thm.prems_of st) 0;
   1.176  
   1.177  
   1.178  (*Negation Normal Form*)
   1.179 @@ -518,7 +519,7 @@
   1.180    | ok4nnf _ = false;
   1.181  
   1.182  fun make_nnf1 ctxt th =
   1.183 -  if ok4nnf (concl_of th)
   1.184 +  if ok4nnf (Thm.concl_of th)
   1.185    then make_nnf1 ctxt (tryres(th, nnf_rls))
   1.186      handle THM ("tryres", _, _) =>
   1.187          forward_res ctxt (make_nnf1 ctxt)
   1.188 @@ -552,9 +553,10 @@
   1.189    #> simplify (put_simpset nnf_ss ctxt)
   1.190    #> rewrite_rule ctxt @{thms Let_def [abs_def]}
   1.191  
   1.192 -fun make_nnf ctxt th = case prems_of th of
   1.193 +fun make_nnf ctxt th =
   1.194 +  (case Thm.prems_of th of
   1.195      [] => th |> presimplify ctxt |> make_nnf1 ctxt
   1.196 -  | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
   1.197 +  | _ => raise THM ("make_nnf: premises in argument", 0, [th]));
   1.198  
   1.199  fun choice_theorems thy =
   1.200    try (Global_Theory.get_thm thy) "Hilbert_Choice.choice" |> the_list
   1.201 @@ -564,7 +566,7 @@
   1.202  fun skolemize_with_choice_theorems ctxt choice_ths =
   1.203    let
   1.204      fun aux th =
   1.205 -      if not (has_conns [@{const_name Ex}] (prop_of th)) then
   1.206 +      if not (has_conns [@{const_name Ex}] (Thm.prop_of th)) then
   1.207          th
   1.208        else
   1.209          tryres (th, choice_ths @
   1.210 @@ -615,35 +617,35 @@
   1.211  
   1.212  val ext_cong_neq = @{thm ext_cong_neq}
   1.213  val F_ext_cong_neq =
   1.214 -  Term.add_vars (prop_of @{thm ext_cong_neq}) []
   1.215 +  Term.add_vars (Thm.prop_of @{thm ext_cong_neq}) []
   1.216    |> filter (fn ((s, _), _) => s = "F")
   1.217    |> the_single |> Var
   1.218  
   1.219  (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
   1.220  fun cong_extensionalize_thm thy th =
   1.221 -  case concl_of th of
   1.222 +  (case Thm.concl_of th of
   1.223      @{const Trueprop} $ (@{const Not}
   1.224          $ (Const (@{const_name HOL.eq}, Type (_, [T, _]))
   1.225             $ (t as _ $ _) $ (u as _ $ _))) =>
   1.226      (case get_F_pattern T t u of
   1.227         SOME p =>
   1.228 -       let val inst = [apply2 (cterm_of thy) (F_ext_cong_neq, p)] in
   1.229 +       let val inst = [apply2 (Thm.cterm_of thy) (F_ext_cong_neq, p)] in
   1.230           th RS cterm_instantiate inst ext_cong_neq
   1.231         end
   1.232       | NONE => th)
   1.233 -  | _ => th
   1.234 +  | _ => th)
   1.235  
   1.236  (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
   1.237     would be desirable to do this symmetrically but there's at least one existing
   1.238     proof in "Tarski" that relies on the current behavior. *)
   1.239  fun abs_extensionalize_conv ctxt ct =
   1.240 -  case term_of ct of
   1.241 +  (case Thm.term_of ct of
   1.242      Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
   1.243      ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
   1.244             then_conv abs_extensionalize_conv ctxt)
   1.245    | _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
   1.246    | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
   1.247 -  | _ => Conv.all_conv ct
   1.248 +  | _ => Conv.all_conv ct)
   1.249  
   1.250  val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
   1.251  
   1.252 @@ -673,7 +675,7 @@
   1.253    in Variable.export ctxt' ctxt cnfs @ cls end;
   1.254  
   1.255  (*Sort clauses by number of literals*)
   1.256 -fun fewerlits (th1, th2) = nliterals (prop_of th1) < nliterals (prop_of th2)
   1.257 +fun fewerlits (th1, th2) = nliterals (Thm.prop_of th1) < nliterals (Thm.prop_of th2)
   1.258  
   1.259  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   1.260    The resulting clauses are HOL disjunctions.*)