src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 59582 0fbed69ff081
parent 59498 50b60f501b05
child 59621 291934bac95e
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Mar 03 19:08:04 2015 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 04 19:53:18 2015 +0100
     1.3 @@ -459,13 +459,13 @@
     1.4        (Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ _ $ _)) = true
     1.5    | is_equationlike_term _ = false
     1.6  
     1.7 -val is_equationlike = is_equationlike_term o prop_of
     1.8 +val is_equationlike = is_equationlike_term o Thm.prop_of
     1.9  
    1.10  fun is_pred_equation_term (Const (@{const_name Pure.eq}, _) $ u $ v) =
    1.11        (fastype_of u = @{typ bool}) andalso (fastype_of v = @{typ bool})
    1.12    | is_pred_equation_term _ = false
    1.13  
    1.14 -val is_pred_equation = is_pred_equation_term o prop_of
    1.15 +val is_pred_equation = is_pred_equation_term o Thm.prop_of
    1.16  
    1.17  fun is_intro_term constname t =
    1.18    the_default false (try (fn t =>
    1.19 @@ -473,7 +473,7 @@
    1.20        Const (c, _) => c = constname
    1.21      | _ => false) t)
    1.22  
    1.23 -fun is_intro constname t = is_intro_term constname (prop_of t)
    1.24 +fun is_intro constname t = is_intro_term constname (Thm.prop_of t)
    1.25  
    1.26  fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
    1.27    | is_predT _ = false
    1.28 @@ -528,7 +528,8 @@
    1.29      val t'' = Term.subst_bounds (rev vs, t');
    1.30    in ((ps', t''), nctxt') end
    1.31  
    1.32 -val strip_intro_concl = strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of
    1.33 +val strip_intro_concl =
    1.34 +  strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of
    1.35  
    1.36  
    1.37  (* introduction rule combinators *)
    1.38 @@ -610,7 +611,7 @@
    1.39  (* lifting term operations to theorems *)
    1.40  
    1.41  fun map_term thy f th =
    1.42 -  Skip_Proof.make_thm thy (f (prop_of th))
    1.43 +  Skip_Proof.make_thm thy (f (Thm.prop_of th))
    1.44  
    1.45  (*
    1.46  fun equals_conv lhs_cv rhs_cv ct =
    1.47 @@ -860,23 +861,23 @@
    1.48    end
    1.49  
    1.50  fun dest_conjunct_prem th =
    1.51 -  (case HOLogic.dest_Trueprop (prop_of th) of
    1.52 +  (case HOLogic.dest_Trueprop (Thm.prop_of th) of
    1.53      (Const (@{const_name HOL.conj}, _) $ _ $ _) =>
    1.54 -      dest_conjunct_prem (th RS @{thm conjunct1})
    1.55 -        @ dest_conjunct_prem (th RS @{thm conjunct2})
    1.56 -   | _ => [th])
    1.57 +      dest_conjunct_prem (th RS @{thm conjunct1}) @
    1.58 +      dest_conjunct_prem (th RS @{thm conjunct2})
    1.59 +  | _ => [th])
    1.60  
    1.61  fun expand_tuples thy intro =
    1.62    let
    1.63      val ctxt = Proof_Context.init_global thy
    1.64      val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt
    1.65 -    val intro_t = prop_of intro'
    1.66 +    val intro_t = Thm.prop_of intro'
    1.67      val concl = Logic.strip_imp_concl intro_t
    1.68      val (_, args) = strip_comb (HOLogic.dest_Trueprop concl)
    1.69      val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1)
    1.70      val (pats', _, ctxt3) = fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2)
    1.71      fun rewrite_pat (ct1, ct2) =
    1.72 -      (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2)))
    1.73 +      (ct1, Thm.cterm_of thy (Pattern.rewrite_term thy pats' [] (Thm.term_of ct2)))
    1.74      val t_insts' = map rewrite_pat t_insts
    1.75      val intro'' = Thm.instantiate (T_insts, t_insts') intro
    1.76      val [intro'''] = Variable.export ctxt3 ctxt [intro'']
    1.77 @@ -939,7 +940,7 @@
    1.78    let
    1.79      val th = case_rewrite thy Tcon
    1.80      val ctxt = Proof_Context.init_global thy
    1.81 -    val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th)))))
    1.82 +    val f = fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of th)))))
    1.83      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
    1.84      val ([yname], ctxt') = Variable.add_fixes ["y"] ctxt
    1.85      val T' = TFree ("'t'", @{sort type})
    1.86 @@ -1026,7 +1027,7 @@
    1.87  (* Some last processing *)
    1.88  
    1.89  fun remove_pointless_clauses intro =
    1.90 -  if Logic.strip_imp_prems (prop_of intro) = [@{prop "False"}] then
    1.91 +  if Logic.strip_imp_prems (Thm.prop_of intro) = [@{prop "False"}] then
    1.92      []
    1.93    else [intro]
    1.94  
    1.95 @@ -1045,7 +1046,7 @@
    1.96        map_filter_premises (fn p => if p = @{prop True} then NONE else SOME p) intro_t
    1.97    in
    1.98      Option.map (Skip_Proof.make_thm thy)
    1.99 -      (process_False (process_True (prop_of (process intro))))
   1.100 +      (process_False (process_True (Thm.prop_of (process intro))))
   1.101    end
   1.102  
   1.103  
   1.104 @@ -1089,7 +1090,7 @@
   1.105          fun instantiate_ho_args th =
   1.106            let
   1.107              val (_, args') =
   1.108 -              (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
   1.109 +              (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) th
   1.110              val ho_args' = map dest_Var (ho_args_of_typ T args')
   1.111            in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
   1.112          val outp_pred =
   1.113 @@ -1136,7 +1137,7 @@
   1.114      val (((pred, params), intros_th), ctxt1) = import_intros pred introrules ctxt
   1.115      (* TODO: distinct required ? -- test case with more than one parameter! *)
   1.116      val params = distinct (op aconv) params
   1.117 -    val intros = map prop_of intros_th
   1.118 +    val intros = map Thm.prop_of intros_th
   1.119      val ([propname], ctxt2) = Variable.variant_fixes ["thesis"] ctxt1
   1.120      val prop = HOLogic.mk_Trueprop (Free (propname, HOLogic.boolT))
   1.121      val argsT = binder_types (fastype_of pred)