src/HOL/Tools/SMT2/smt2_normalize.ML
changeset 57230 ec5ff6bb2a92
parent 57229 489083abce44
child 57696 fb71c6f100f8
     1.1 --- a/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT2/smt2_normalize.ML	Thu Jun 12 01:00:49 2014 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  (* general theorem normalizations *)
     1.5  
     1.6  (** instantiate elimination rules **)
     1.7 - 
     1.8 +
     1.9  local
    1.10    val (cpfalse, cfalse) = `SMT2_Util.mk_cprop (Thm.cterm_of @{theory} @{const False})
    1.11  
    1.12 @@ -113,8 +113,8 @@
    1.13  
    1.14    fun proper_trigger t =
    1.15      t
    1.16 -    |> these o try HOLogic.dest_list
    1.17 -    |> map (map_filter dest_trigger o these o try HOLogic.dest_list)
    1.18 +    |> these o try SMT2_Util.dest_symb_list
    1.19 +    |> map (map_filter dest_trigger o these o try SMT2_Util.dest_symb_list)
    1.20      |> (fn [] => false | bss => forall eq_list bss)
    1.21  
    1.22    fun proper_quant inside f t =
    1.23 @@ -185,16 +185,17 @@
    1.24              Pattern.matches thy (t', u) andalso not (t aconv u))
    1.25          in not (Term.exists_subterm some_match u) end
    1.26  
    1.27 -  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name SMT2.pat} SMT2_Util.destT1
    1.28 +  val pat = SMT2_Util.mk_const_pat @{theory} @{const_name pat} SMT2_Util.destT1
    1.29    fun mk_pat ct = Thm.apply (SMT2_Util.instT' ct pat) ct
    1.30  
    1.31 -  fun mk_clist T = pairself (Thm.cterm_of @{theory}) (HOLogic.cons_const T, HOLogic.nil_const T)
    1.32 +  fun mk_clist T =
    1.33 +    pairself (Thm.cterm_of @{theory}) (SMT2_Util.symb_cons_const T, SMT2_Util.symb_nil_const T)
    1.34    fun mk_list (ccons, cnil) f cts = fold_rev (Thm.mk_binop ccons o f) cts cnil
    1.35 -  val mk_pat_list = mk_list (mk_clist @{typ SMT2.pattern})
    1.36 -  val mk_mpat_list = mk_list (mk_clist @{typ "SMT2.pattern list"})  
    1.37 +  val mk_pat_list = mk_list (mk_clist @{typ pattern})
    1.38 +  val mk_mpat_list = mk_list (mk_clist @{typ "pattern symb_list"})
    1.39    fun mk_trigger ctss = mk_mpat_list (mk_pat_list mk_pat) ctss
    1.40  
    1.41 -  val trigger_eq = mk_meta_eq @{lemma "p = SMT2.trigger t p" by (simp add: trigger_def)}
    1.42 +  val trigger_eq = mk_meta_eq @{lemma "p = trigger t p" by (simp add: trigger_def)}
    1.43  
    1.44    fun insert_trigger_conv [] ct = Conv.all_conv ct
    1.45      | insert_trigger_conv ctss ct =
    1.46 @@ -216,7 +217,7 @@
    1.47  
    1.48      in insert_trigger_conv (filter_mpats (get_mpats lhs)) ct end
    1.49  
    1.50 -  fun has_trigger (@{const SMT2.trigger} $ _ $ _) = true
    1.51 +  fun has_trigger (@{const trigger} $ _ $ _) = true
    1.52      | has_trigger _ = false
    1.53  
    1.54    fun try_trigger_conv cv ct =
    1.55 @@ -234,7 +235,7 @@
    1.56  
    1.57  val setup_trigger =
    1.58    fold SMT2_Builtin.add_builtin_fun_ext''
    1.59 -    [@{const_name SMT2.pat}, @{const_name SMT2.nopat}, @{const_name SMT2.trigger}]
    1.60 +    [@{const_name pat}, @{const_name nopat}, @{const_name trigger}]
    1.61  
    1.62  end
    1.63  
    1.64 @@ -317,7 +318,7 @@
    1.65  
    1.66  fun unfold_abs_min_max_conv ctxt =
    1.67    SMT2_Util.if_exists_conv (is_some o abs_min_max ctxt) (Conv.top_conv unfold_amm_conv ctxt)
    1.68 -  
    1.69 +
    1.70  val setup_abs_min_max = fold (SMT2_Builtin.add_builtin_fun_ext'' o fst) abs_min_max_table
    1.71  
    1.72  end
    1.73 @@ -481,18 +482,17 @@
    1.74  
    1.75    val schematic_consts_of =
    1.76      let
    1.77 -      fun collect (@{const SMT2.trigger} $ p $ t) =
    1.78 -            collect_trigger p #> collect t
    1.79 +      fun collect (@{const trigger} $ p $ t) = collect_trigger p #> collect t
    1.80          | collect (t $ u) = collect t #> collect u
    1.81          | collect (Abs (_, _, t)) = collect t
    1.82 -        | collect (t as Const (n, _)) = 
    1.83 +        | collect (t as Const (n, _)) =
    1.84              if not (ignored n) then Monomorph.add_schematic_consts_of t else I
    1.85          | collect _ = I
    1.86        and collect_trigger t =
    1.87 -        let val dest = these o try HOLogic.dest_list 
    1.88 +        let val dest = these o try SMT2_Util.dest_symb_list
    1.89          in fold (fold collect_pat o dest) (dest t) end
    1.90 -      and collect_pat (Const (@{const_name SMT2.pat}, _) $ t) = collect t
    1.91 -        | collect_pat (Const (@{const_name SMT2.nopat}, _) $ t) = collect t
    1.92 +      and collect_pat (Const (@{const_name pat}, _) $ t) = collect t
    1.93 +        | collect_pat (Const (@{const_name nopat}, _) $ t) = collect t
    1.94          | collect_pat _ = I
    1.95      in (fn t => collect t Symtab.empty) end
    1.96  in