more antiquotations;
authorwenzelm
Thu Feb 25 22:32:09 2010 +0100 (2010-02-25)
changeset 35364b8c62d60195c
parent 35363 09489d8ffece
child 35365 2fcd08c62495
more antiquotations;
src/HOL/Groups.thy
src/HOL/HOL.thy
src/HOL/Orderings.thy
src/HOL/Product_Type.thy
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_aux.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/simpdata.ML
     1.1 --- a/src/HOL/Groups.thy	Thu Feb 25 22:17:33 2010 +0100
     1.2 +++ b/src/HOL/Groups.thy	Thu Feb 25 22:32:09 2010 +0100
     1.3 @@ -1250,7 +1250,7 @@
     1.4  val eqI_rules = [@{thm less_eqI}, @{thm le_eqI}, @{thm eq_eqI}];
     1.5  
     1.6  val dest_eqI = 
     1.7 -  fst o HOLogic.dest_bin "op =" HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
     1.8 +  fst o HOLogic.dest_bin @{const_name "op ="} HOLogic.boolT o HOLogic.dest_Trueprop o concl_of;
     1.9  
    1.10  );
    1.11  *}
     2.1 --- a/src/HOL/HOL.thy	Thu Feb 25 22:17:33 2010 +0100
     2.2 +++ b/src/HOL/HOL.thy	Thu Feb 25 22:32:09 2010 +0100
     2.3 @@ -846,9 +846,12 @@
     2.4  setup {*
     2.5  let
     2.6    (*prevent substitution on bool*)
     2.7 -  fun hyp_subst_tac' i thm = if i <= Thm.nprems_of thm andalso
     2.8 -    Term.exists_Const (fn ("op =", Type (_, [T, _])) => T <> Type ("bool", []) | _ => false)
     2.9 -      (nth (Thm.prems_of thm) (i - 1)) then Hypsubst.hyp_subst_tac i thm else no_tac thm;
    2.10 +  fun hyp_subst_tac' i thm =
    2.11 +    if i <= Thm.nprems_of thm andalso
    2.12 +        Term.exists_Const
    2.13 +          (fn (@{const_name "op ="}, Type (_, [T, _])) => T <> @{typ bool} | _ => false)
    2.14 +          (nth (Thm.prems_of thm) (i - 1))
    2.15 +    then Hypsubst.hyp_subst_tac i thm else no_tac thm;
    2.16  in
    2.17    Hypsubst.hypsubst_setup
    2.18    #> Context_Rules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)
    2.19 @@ -1721,8 +1724,8 @@
    2.20  
    2.21  fun eq_codegen thy defs dep thyname b t gr =
    2.22      (case strip_comb t of
    2.23 -       (Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
    2.24 -     | (Const ("op =", _), [t, u]) =>
    2.25 +       (Const (@{const_name "op ="}, Type (_, [Type ("fun", _), _])), _) => NONE
    2.26 +     | (Const (@{const_name "op ="}, _), [t, u]) =>
    2.27            let
    2.28              val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
    2.29              val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
    2.30 @@ -1731,7 +1734,7 @@
    2.31              SOME (Codegen.parens
    2.32                (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
    2.33            end
    2.34 -     | (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
    2.35 +     | (t as Const (@{const_name "op ="}, _), ts) => SOME (Codegen.invoke_codegen
    2.36           thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
    2.37       | _ => NONE);
    2.38  
    2.39 @@ -2050,7 +2053,7 @@
    2.40  
    2.41  (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
    2.42  local
    2.43 -  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
    2.44 +  fun wrong_prem (Const (@{const_name All}, _) $ Abs (_, _, t)) = wrong_prem t
    2.45      | wrong_prem (Bound _) = true
    2.46      | wrong_prem _ = false;
    2.47    val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
     3.1 --- a/src/HOL/Orderings.thy	Thu Feb 25 22:17:33 2010 +0100
     3.2 +++ b/src/HOL/Orderings.thy	Thu Feb 25 22:32:09 2010 +0100
     3.3 @@ -657,13 +657,14 @@
     3.4  
     3.5    fun matches_bound v t =
     3.6      (case t of
     3.7 -      Const ("_bound", _) $ Free (v', _) => v = v'
     3.8 +      Const (@{syntax_const "_bound"}, _) $ Free (v', _) => v = v'
     3.9      | _ => false);
    3.10    fun contains_var v = Term.exists_subterm (fn Free (x, _) => x = v | _ => false);
    3.11    fun mk v c n P = Syntax.const c $ Syntax.mark_bound v $ n $ P;
    3.12  
    3.13    fun tr' q = (q,
    3.14 -    fn [Const ("_bound", _) $ Free (v, _), Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    3.15 +    fn [Const (@{syntax_const "_bound"}, _) $ Free (v, _),
    3.16 +        Const (c, _) $ (Const (d, _) $ t $ u) $ P] =>
    3.17          (case AList.lookup (op =) trans (q, c, d) of
    3.18            NONE => raise Match
    3.19          | SOME (l, g) =>
     4.1 --- a/src/HOL/Product_Type.thy	Thu Feb 25 22:17:33 2010 +0100
     4.2 +++ b/src/HOL/Product_Type.thy	Thu Feb 25 22:32:09 2010 +0100
     4.3 @@ -448,44 +448,44 @@
     4.4  *}
     4.5  
     4.6  ML {*
     4.7 -
     4.8  local
     4.9 -  val cond_split_eta_ss = HOL_basic_ss addsimps [thm "cond_split_eta"]
    4.10 -  fun  Pair_pat k 0 (Bound m) = (m = k)
    4.11 -  |    Pair_pat k i (Const ("Pair",  _) $ Bound m $ t) = i > 0 andalso
    4.12 -                        m = k+i andalso Pair_pat k (i-1) t
    4.13 -  |    Pair_pat _ _ _ = false;
    4.14 -  fun no_args k i (Abs (_, _, t)) = no_args (k+1) i t
    4.15 -  |   no_args k i (t $ u) = no_args k i t andalso no_args k i u
    4.16 -  |   no_args k i (Bound m) = m < k orelse m > k+i
    4.17 -  |   no_args _ _ _ = true;
    4.18 -  fun split_pat tp i (Abs  (_,_,t)) = if tp 0 i t then SOME (i,t) else NONE
    4.19 -  |   split_pat tp i (Const ("split", _) $ Abs (_, _, t)) = split_pat tp (i+1) t
    4.20 -  |   split_pat tp i _ = NONE;
    4.21 +  val cond_split_eta_ss = HOL_basic_ss addsimps @{thms cond_split_eta};
    4.22 +  fun Pair_pat k 0 (Bound m) = (m = k)
    4.23 +    | Pair_pat k i (Const (@{const_name Pair},  _) $ Bound m $ t) =
    4.24 +        i > 0 andalso m = k + i andalso Pair_pat k (i - 1) t
    4.25 +    | Pair_pat _ _ _ = false;
    4.26 +  fun no_args k i (Abs (_, _, t)) = no_args (k + 1) i t
    4.27 +    | no_args k i (t $ u) = no_args k i t andalso no_args k i u
    4.28 +    | no_args k i (Bound m) = m < k orelse m > k + i
    4.29 +    | no_args _ _ _ = true;
    4.30 +  fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
    4.31 +    | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
    4.32 +    | split_pat tp i _ = NONE;
    4.33    fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
    4.34 -        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs,rhs)))
    4.35 +        (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
    4.36          (K (simp_tac (Simplifier.inherit_context ss cond_split_eta_ss) 1)));
    4.37  
    4.38 -  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k+1) i t
    4.39 -  |   beta_term_pat k i (t $ u) = Pair_pat k i (t $ u) orelse
    4.40 -                        (beta_term_pat k i t andalso beta_term_pat k i u)
    4.41 -  |   beta_term_pat k i t = no_args k i t;
    4.42 -  fun  eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
    4.43 -  |    eta_term_pat _ _ _ = false;
    4.44 +  fun beta_term_pat k i (Abs (_, _, t)) = beta_term_pat (k + 1) i t
    4.45 +    | beta_term_pat k i (t $ u) =
    4.46 +        Pair_pat k i (t $ u) orelse (beta_term_pat k i t andalso beta_term_pat k i u)
    4.47 +    | beta_term_pat k i t = no_args k i t;
    4.48 +  fun eta_term_pat k i (f $ arg) = no_args k i f andalso Pair_pat k i arg
    4.49 +    | eta_term_pat _ _ _ = false;
    4.50    fun subst arg k i (Abs (x, T, t)) = Abs (x, T, subst arg (k+1) i t)
    4.51 -  |   subst arg k i (t $ u) = if Pair_pat k i (t $ u) then incr_boundvars k arg
    4.52 -                              else (subst arg k i t $ subst arg k i u)
    4.53 -  |   subst arg k i t = t;
    4.54 -  fun beta_proc ss (s as Const ("split", _) $ Abs (_, _, t) $ arg) =
    4.55 +    | subst arg k i (t $ u) =
    4.56 +        if Pair_pat k i (t $ u) then incr_boundvars k arg
    4.57 +        else (subst arg k i t $ subst arg k i u)
    4.58 +    | subst arg k i t = t;
    4.59 +  fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
    4.60          (case split_pat beta_term_pat 1 t of
    4.61 -        SOME (i,f) => SOME (metaeq ss s (subst arg 0 i f))
    4.62 +          SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
    4.63          | NONE => NONE)
    4.64 -  |   beta_proc _ _ = NONE;
    4.65 -  fun eta_proc ss (s as Const ("split", _) $ Abs (_, _, t)) =
    4.66 +    | beta_proc _ _ = NONE;
    4.67 +  fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
    4.68          (case split_pat eta_term_pat 1 t of
    4.69 -          SOME (_,ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    4.70 +          SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
    4.71          | NONE => NONE)
    4.72 -  |   eta_proc _ _ = NONE;
    4.73 +    | eta_proc _ _ = NONE;
    4.74  in
    4.75    val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    4.76    val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    4.77 @@ -565,11 +565,11 @@
    4.78  
    4.79  ML {*
    4.80  local (* filtering with exists_p_split is an essential optimization *)
    4.81 -  fun exists_p_split (Const ("split",_) $ _ $ (Const ("Pair",_)$_$_)) = true
    4.82 +  fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
    4.83      | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
    4.84      | exists_p_split (Abs (_, _, t)) = exists_p_split t
    4.85      | exists_p_split _ = false;
    4.86 -  val ss = HOL_basic_ss addsimps [thm "split_conv"];
    4.87 +  val ss = HOL_basic_ss addsimps @{thms split_conv};
    4.88  in
    4.89  val split_conv_tac = SUBGOAL (fn (t, i) =>
    4.90      if exists_p_split t then safe_full_simp_tac ss i else no_tac);
    4.91 @@ -634,10 +634,11 @@
    4.92  lemma internal_split_conv: "internal_split c (a, b) = c a b"
    4.93    by (simp only: internal_split_def split_conv)
    4.94  
    4.95 +use "Tools/split_rule.ML"
    4.96 +setup SplitRule.setup
    4.97 +
    4.98  hide const internal_split
    4.99  
   4.100 -use "Tools/split_rule.ML"
   4.101 -setup SplitRule.setup
   4.102  
   4.103  lemmas prod_caseI = prod.cases [THEN iffD2, standard]
   4.104  
   4.105 @@ -1049,7 +1050,6 @@
   4.106    "Pair"    ("(_,/ _)")
   4.107  
   4.108  setup {*
   4.109 -
   4.110  let
   4.111  
   4.112  fun strip_abs_split 0 t = ([], t)
   4.113 @@ -1058,16 +1058,18 @@
   4.114          val s' = Codegen.new_name t s;
   4.115          val v = Free (s', T)
   4.116        in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
   4.117 -  | strip_abs_split i (u as Const ("split", _) $ t) = (case strip_abs_split (i+1) t of
   4.118 +  | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
   4.119 +      (case strip_abs_split (i+1) t of
   4.120          (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
   4.121        | _ => ([], u))
   4.122    | strip_abs_split i t =
   4.123        strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
   4.124  
   4.125 -fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
   4.126 -    (t1 as Const ("Let", _), t2 :: t3 :: ts) =>
   4.127 +fun let_codegen thy defs dep thyname brack t gr =
   4.128 +  (case strip_comb t of
   4.129 +    (t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
   4.130      let
   4.131 -      fun dest_let (l as Const ("Let", _) $ t $ u) =
   4.132 +      fun dest_let (l as Const (@{const_name Let}, _) $ t $ u) =
   4.133            (case strip_abs_split 1 u of
   4.134               ([p], u') => apfst (cons (p, t)) (dest_let u')
   4.135             | _ => ([], l))
   4.136 @@ -1098,7 +1100,7 @@
   4.137    | _ => NONE);
   4.138  
   4.139  fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
   4.140 -    (t1 as Const ("split", _), t2 :: ts) =>
   4.141 +    (t1 as Const (@{const_name split}, _), t2 :: ts) =>
   4.142        let
   4.143          val ([p], u) = strip_abs_split 1 (t1 $ t2);
   4.144          val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
     5.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Thu Feb 25 22:17:33 2010 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Thu Feb 25 22:32:09 2010 +0100
     5.3 @@ -75,7 +75,7 @@
     5.4      val leafTs' = get_nonrec_types descr' sorts;
     5.5      val branchTs = get_branching_types descr' sorts;
     5.6      val branchT = if null branchTs then HOLogic.unitT
     5.7 -      else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) branchTs;
     5.8 +      else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) branchTs;
     5.9      val arities = remove (op =) 0 (get_arities descr');
    5.10      val unneeded_vars =
    5.11        subtract (op =) (List.foldr OldTerm.add_typ_tfree_names [] (leafTs' @ branchTs)) (hd tyvars);
    5.12 @@ -83,7 +83,7 @@
    5.13      val recTs = get_rec_types descr' sorts;
    5.14      val (newTs, oldTs) = chop (length (hd descr)) recTs;
    5.15      val sumT = if null leafTs then HOLogic.unitT
    5.16 -      else Balanced_Tree.make (fn (T, U) => Type ("+", [T, U])) leafTs;
    5.17 +      else Balanced_Tree.make (fn (T, U) => Type (@{type_name "+"}, [T, U])) leafTs;
    5.18      val Univ_elT = HOLogic.mk_setT (Type (node_name, [sumT, branchT]));
    5.19      val UnivT = HOLogic.mk_setT Univ_elT;
    5.20      val UnivT' = Univ_elT --> HOLogic.boolT;
    5.21 @@ -104,9 +104,9 @@
    5.22                val Type (_, [T1, T2]) = T
    5.23            in
    5.24              if i <= n2 then
    5.25 -              Const (@{const_name "Sum_Type.Inl"}, T1 --> T) $ (mk_inj' T1 n2 i)
    5.26 +              Const (@{const_name Inl}, T1 --> T) $ (mk_inj' T1 n2 i)
    5.27              else
    5.28 -              Const (@{const_name "Sum_Type.Inr"}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
    5.29 +              Const (@{const_name Inr}, T2 --> T) $ (mk_inj' T2 (n - n2) (i - n2))
    5.30            end
    5.31        in mk_inj' sumT (length leafTs) (1 + find_index (fn T'' => T'' = T') leafTs)
    5.32        end;
     6.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Feb 25 22:17:33 2010 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Feb 25 22:32:09 2010 +0100
     6.3 @@ -53,7 +53,7 @@
     6.4      fun prove_casedist_thm (i, (T, t)) =
     6.5        let
     6.6          val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
     6.7 -          Abs ("z", T', Const ("True", T''))) induct_Ps;
     6.8 +          Abs ("z", T', Const (@{const_name True}, T''))) induct_Ps;
     6.9          val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    6.10            Var (("P", 0), HOLogic.boolT))
    6.11          val insts = take i dummyPs @ (P::(drop (i + 1) dummyPs));
    6.12 @@ -200,7 +200,7 @@
    6.13      val rec_unique_thms =
    6.14        let
    6.15          val rec_unique_ts = map (fn (((set_t, T1), T2), i) =>
    6.16 -          Const ("Ex1", (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
    6.17 +          Const (@{const_name Ex1}, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
    6.18              absfree ("y", T2, set_t $ mk_Free "x" T1 i $ Free ("y", T2)))
    6.19                (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
    6.20          val cert = cterm_of thy1
    6.21 @@ -236,7 +236,7 @@
    6.22            (reccomb_names ~~ recTs ~~ rec_result_Ts))
    6.23        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
    6.24            (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
    6.25 -           Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    6.26 +           Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    6.27               set $ Free ("x", T) $ Free ("y", T'))))))
    6.28                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
    6.29        ||> Sign.parent_path
    6.30 @@ -416,7 +416,7 @@
    6.31      fun prove_case_cong ((t, nchotomy), case_rewrites) =
    6.32        let
    6.33          val (Const ("==>", _) $ tm $ _) = t;
    6.34 -        val (Const ("Trueprop", _) $ (Const ("op =", _) $ _ $ Ma)) = tm;
    6.35 +        val (Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, _) $ _ $ Ma)) = tm;
    6.36          val cert = cterm_of thy;
    6.37          val nchotomy' = nchotomy RS spec;
    6.38          val [v] = Term.add_vars (concl_of nchotomy') [];
     7.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Feb 25 22:17:33 2010 +0100
     7.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Thu Feb 25 22:32:09 2010 +0100
     7.3 @@ -120,8 +120,8 @@
     7.4  fun split_conj_thm th =
     7.5    ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
     7.6  
     7.7 -val mk_conj = foldr1 (HOLogic.mk_binop "op &");
     7.8 -val mk_disj = foldr1 (HOLogic.mk_binop "op |");
     7.9 +val mk_conj = foldr1 (HOLogic.mk_binop @{const_name "op &"});
    7.10 +val mk_disj = foldr1 (HOLogic.mk_binop @{const_name "op |"});
    7.11  
    7.12  fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
    7.13  
     8.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Feb 25 22:17:33 2010 +0100
     8.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Thu Feb 25 22:32:09 2010 +0100
     8.3 @@ -70,7 +70,7 @@
     8.4            val frees' = map Free ((map ((op ^) o (rpair "'")) tnames) ~~ Ts);
     8.5          in cons (HOLogic.mk_Trueprop (HOLogic.mk_eq
     8.6            (HOLogic.mk_eq (list_comb (constr_t, frees), list_comb (constr_t, frees')),
     8.7 -           foldr1 (HOLogic.mk_binop "op &")
     8.8 +           foldr1 (HOLogic.mk_binop @{const_name "op &"})
     8.9               (map HOLogic.mk_eq (frees ~~ frees')))))
    8.10          end;
    8.11    in
    8.12 @@ -149,7 +149,7 @@
    8.13      val prems = maps (fn ((i, (_, _, constrs)), T) =>
    8.14        map (make_ind_prem i T) constrs) (descr' ~~ recTs);
    8.15      val tnames = make_tnames recTs;
    8.16 -    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    8.17 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
    8.18        (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
    8.19          (descr' ~~ recTs ~~ tnames)))
    8.20  
     9.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 25 22:17:33 2010 +0100
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Thu Feb 25 22:32:09 2010 +0100
     9.3 @@ -16,10 +16,11 @@
     9.4  
     9.5  open Datatype_Aux;
     9.6  
     9.7 -fun subsets i j = if i <= j then
     9.8 -       let val is = subsets (i+1) j
     9.9 -       in map (fn ks => i::ks) is @ is end
    9.10 -     else [[]];
    9.11 +fun subsets i j =
    9.12 +  if i <= j then
    9.13 +    let val is = subsets (i+1) j
    9.14 +    in map (fn ks => i::ks) is @ is end
    9.15 +  else [[]];
    9.16  
    9.17  fun forall_intr_prf (t, prf) =
    9.18    let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
    9.19 @@ -102,7 +103,7 @@
    9.20          if i mem is then SOME
    9.21            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
    9.22          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    9.23 -    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
    9.24 +    val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
    9.25        (map (fn ((((i, _), T), U), tname) =>
    9.26          make_pred i U T (mk_proj i is r) (Free (tname, T)))
    9.27            (descr ~~ recTs ~~ rec_result_Ts ~~ tnames)));
    9.28 @@ -129,8 +130,8 @@
    9.29  
    9.30      val ivs = rev (Term.add_vars (Logic.varify (Datatype_Prop.make_ind [descr] sorts)) []);
    9.31      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    9.32 -    val ivs1 = map Var (filter_out (fn (_, T) =>
    9.33 -      tname_of (body_type T) mem ["set", "bool"]) ivs);
    9.34 +    val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
    9.35 +      tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
    9.36      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    9.37  
    9.38      val prf =
    10.1 --- a/src/HOL/Tools/inductive.ML	Thu Feb 25 22:17:33 2010 +0100
    10.2 +++ b/src/HOL/Tools/inductive.ML	Thu Feb 25 22:32:09 2010 +0100
    10.3 @@ -183,7 +183,7 @@
    10.4    in
    10.5      case concl_of thm of
    10.6        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    10.7 -    | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    10.8 +    | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => eq2mono thm
    10.9      | _ $ (Const (@{const_name Orderings.less_eq}, _) $ _ $ _) =>
   10.10        dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
   10.11          (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))
   10.12 @@ -300,7 +300,7 @@
   10.13        else err_in_prem ctxt err_name rule prem "Non-atomic premise";
   10.14    in
   10.15      (case concl of
   10.16 -       Const ("Trueprop", _) $ t =>
   10.17 +       Const (@{const_name Trueprop}, _) $ t =>
   10.18           if head_of t mem cs then
   10.19             (check_ind (err_in_rule ctxt err_name rule') t;
   10.20              List.app check_prem (prems ~~ aprems))
    11.1 --- a/src/HOL/Tools/inductive_codegen.ML	Thu Feb 25 22:17:33 2010 +0100
    11.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Thu Feb 25 22:32:09 2010 +0100
    11.3 @@ -51,12 +51,13 @@
    11.4      fun thyname_of s = (case optmod of
    11.5        NONE => Codegen.thyname_of_const thy s | SOME s => s);
    11.6    in (case Option.map strip_comb (try HOLogic.dest_Trueprop (concl_of thm)) of
    11.7 -      SOME (Const ("op =", _), [t, _]) => (case head_of t of
    11.8 -        Const (s, _) =>
    11.9 -          CodegenData.put {intros = intros, graph = graph,
   11.10 -             eqns = eqns |> Symtab.map_default (s, [])
   11.11 -               (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
   11.12 -      | _ => (warn thm; thy))
   11.13 +      SOME (Const (@{const_name "op ="}, _), [t, _]) =>
   11.14 +        (case head_of t of
   11.15 +          Const (s, _) =>
   11.16 +            CodegenData.put {intros = intros, graph = graph,
   11.17 +               eqns = eqns |> Symtab.map_default (s, [])
   11.18 +                 (AList.update Thm.eq_thm_prop (thm, thyname_of s))} thy
   11.19 +        | _ => (warn thm; thy))
   11.20      | SOME (Const (s, _), _) =>
   11.21          let
   11.22            val cs = fold Term.add_const_names (Thm.prems_of thm) [];
   11.23 @@ -186,7 +187,7 @@
   11.24          end)) (AList.lookup op = modes name)
   11.25  
   11.26    in (case strip_comb t of
   11.27 -      (Const ("op =", Type (_, [T, _])), _) =>
   11.28 +      (Const (@{const_name "op ="}, Type (_, [T, _])), _) =>
   11.29          [Mode ((([], [1]), false), [1], []), Mode ((([], [2]), false), [2], [])] @
   11.30          (if is_eqT T then [Mode ((([], [1, 2]), false), [1, 2], [])] else [])
   11.31      | (Const (name, _), args) => the_default default (mk_modes name args)
   11.32 @@ -577,17 +578,20 @@
   11.33        fun get_nparms s = if s mem names then SOME nparms else
   11.34          Option.map #3 (get_clauses thy s);
   11.35  
   11.36 -      fun dest_prem (_ $ (Const ("op :", _) $ t $ u)) = Prem ([t], Envir.beta_eta_contract u, true)
   11.37 -        | dest_prem (_ $ ((eq as Const ("op =", _)) $ t $ u)) = Prem ([t, u], eq, false)
   11.38 +      fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
   11.39 +            Prem ([t], Envir.beta_eta_contract u, true)
   11.40 +        | dest_prem (_ $ ((eq as Const (@{const_name "op ="}, _)) $ t $ u)) =
   11.41 +            Prem ([t, u], eq, false)
   11.42          | dest_prem (_ $ t) =
   11.43              (case strip_comb t of
   11.44 -               (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
   11.45 -             | (c as Const (s, _), ts) => (case get_nparms s of
   11.46 -                 NONE => Sidecond t
   11.47 -               | SOME k =>
   11.48 -                   let val (ts1, ts2) = chop k ts
   11.49 -                   in Prem (ts2, list_comb (c, ts1), false) end)
   11.50 -             | _ => Sidecond t);
   11.51 +              (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
   11.52 +            | (c as Const (s, _), ts) =>
   11.53 +                (case get_nparms s of
   11.54 +                  NONE => Sidecond t
   11.55 +                | SOME k =>
   11.56 +                    let val (ts1, ts2) = chop k ts
   11.57 +                    in Prem (ts2, list_comb (c, ts1), false) end)
   11.58 +            | _ => Sidecond t);
   11.59  
   11.60        fun add_clause intr (clauses, arities) =
   11.61          let
   11.62 @@ -600,7 +604,7 @@
   11.63            (AList.update op = (name, these (AList.lookup op = clauses name) @
   11.64               [(ts2, prems)]) clauses,
   11.65             AList.update op = (name, (map (fn U => (case strip_type U of
   11.66 -                 (Rs as _ :: _, Type ("bool", [])) => SOME (length Rs)
   11.67 +                 (Rs as _ :: _, @{typ bool}) => SOME (length Rs)
   11.68                 | _ => NONE)) Ts,
   11.69               length Us)) arities)
   11.70          end;
   11.71 @@ -632,7 +636,7 @@
   11.72      val (ts1, ts2) = chop k ts;
   11.73      val u = list_comb (Const (s, T), ts1);
   11.74  
   11.75 -    fun mk_mode (Const ("dummy_pattern", _)) ((ts, mode), i) = ((ts, mode), i + 1)
   11.76 +    fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
   11.77        | mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
   11.78  
   11.79      val module' = if_library thyname module;
   11.80 @@ -715,7 +719,7 @@
   11.81    end;
   11.82  
   11.83  fun inductive_codegen thy defs dep module brack t gr  = (case strip_comb t of
   11.84 -    (Const ("Collect", _), [u]) =>
   11.85 +    (Const (@{const_name Collect}, _), [u]) =>
   11.86        let val (r, Ts, fs) = HOLogic.strip_psplits u
   11.87        in case strip_comb r of
   11.88            (Const (s, T), ts) =>
    12.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Feb 25 22:17:33 2010 +0100
    12.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Feb 25 22:32:09 2010 +0100
    12.3 @@ -21,7 +21,7 @@
    12.4      [name] => name
    12.5    | _ => error ("name_of_thm: bad proof of theorem\n" ^ Display.string_of_thm_without_context thm));
    12.6  
    12.7 -val all_simps = map (symmetric o mk_meta_eq) (thms "HOL.all_simps");
    12.8 +val all_simps = map (symmetric o mk_meta_eq) @{thms HOL.all_simps};
    12.9  
   12.10  fun prf_of thm =
   12.11    let
   12.12 @@ -57,7 +57,7 @@
   12.13  
   12.14  fun relevant_vars prop = List.foldr (fn
   12.15        (Var ((a, i), T), vs) => (case strip_type T of
   12.16 -        (_, Type (s, _)) => if s mem ["bool"] then (a, T) :: vs else vs
   12.17 +        (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs
   12.18        | _ => vs)
   12.19      | (_, vs) => vs) [] (OldTerm.term_vars prop);
   12.20  
   12.21 @@ -150,9 +150,10 @@
   12.22  
   12.23      fun is_meta (Const ("all", _) $ Abs (s, _, P)) = is_meta P
   12.24        | is_meta (Const ("==>", _) $ _ $ Q) = is_meta Q
   12.25 -      | is_meta (Const ("Trueprop", _) $ t) = (case head_of t of
   12.26 -          Const (s, _) => can (Inductive.the_inductive ctxt) s
   12.27 -        | _ => true)
   12.28 +      | is_meta (Const (@{const_name Trueprop}, _) $ t) =
   12.29 +          (case head_of t of
   12.30 +            Const (s, _) => can (Inductive.the_inductive ctxt) s
   12.31 +          | _ => true)
   12.32        | is_meta _ = false;
   12.33  
   12.34      fun fun_of ts rts args used (prem :: prems) =
   12.35 @@ -174,7 +175,7 @@
   12.36                      (Free (r, U) :: Free (x, T) :: args) (x :: r :: used) prems'
   12.37                  end
   12.38                else (case strip_type T of
   12.39 -                  (Ts, Type ("*", [T1, T2])) =>
   12.40 +                  (Ts, Type (@{type_name "*"}, [T1, T2])) =>
   12.41                      let
   12.42                        val fx = Free (x, Ts ---> T1);
   12.43                        val fr = Free (r, Ts ---> T2);
   12.44 @@ -211,8 +212,9 @@
   12.45        let
   12.46          val fs = map (fn (rule, (ivs, intr)) =>
   12.47            fun_of_prem thy rsets vs params rule ivs intr) (prems ~~ intrs)
   12.48 -      in if dummy then Const ("HOL.default_class.default",
   12.49 -          HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   12.50 +      in
   12.51 +        if dummy then Const (@{const_name default},
   12.52 +            HOLogic.unitT --> body_type (fastype_of (hd fs))) :: fs
   12.53          else fs
   12.54        end) (premss ~~ dummies);
   12.55      val frees = fold Term.add_frees fs [];
   12.56 @@ -439,7 +441,7 @@
   12.57          val r = if null Ps then Extraction.nullt
   12.58            else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T),
   12.59              (if dummy then
   12.60 -               [Abs ("x", HOLogic.unitT, Const ("HOL.default_class.default", body_type T))]
   12.61 +               [Abs ("x", HOLogic.unitT, Const (@{const_name default}, body_type T))]
   12.62               else []) @
   12.63              map reorder2 (intrs ~~ (length prems - 1 downto 0)) @
   12.64              [Bound (length prems)]));
    13.1 --- a/src/HOL/Tools/inductive_set.ML	Thu Feb 25 22:17:33 2010 +0100
    13.2 +++ b/src/HOL/Tools/inductive_set.ML	Thu Feb 25 22:32:09 2010 +0100
    13.3 @@ -33,10 +33,10 @@
    13.4  
    13.5  val collect_mem_simproc =
    13.6    Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
    13.7 -    fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
    13.8 +    fn S as Const (@{const_name Collect}, Type ("fun", [_, T])) $ t =>
    13.9           let val (u, _, ps) = HOLogic.strip_psplits t
   13.10           in case u of
   13.11 -           (c as Const ("op :", _)) $ q $ S' =>
   13.12 +           (c as Const (@{const_name "op :"}, _)) $ q $ S' =>
   13.13               (case try (HOLogic.strip_ptuple ps) q of
   13.14                  NONE => NONE
   13.15                | SOME ts =>
   13.16 @@ -74,18 +74,20 @@
   13.17          in Drule.instantiate' [] (rev (map (SOME o cterm_of thy o Var) vs))
   13.18            (p (fold (Logic.all o Var) vs t) f)
   13.19          end;
   13.20 -      fun mkop "op &" T x = SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   13.21 -        | mkop "op |" T x = SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   13.22 +      fun mkop @{const_name "op &"} T x =
   13.23 +            SOME (Const (@{const_name Lattices.inf}, T --> T --> T), x)
   13.24 +        | mkop @{const_name "op |"} T x =
   13.25 +            SOME (Const (@{const_name Lattices.sup}, T --> T --> T), x)
   13.26          | mkop _ _ _ = NONE;
   13.27        fun mk_collect p T t =
   13.28          let val U = HOLogic.dest_setT T
   13.29          in HOLogic.Collect_const U $
   13.30            HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
   13.31          end;
   13.32 -      fun decomp (Const (s, _) $ ((m as Const ("op :",
   13.33 +      fun decomp (Const (s, _) $ ((m as Const (@{const_name "op :"},
   13.34              Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
   13.35                mkop s T (m, p, S, mk_collect p T (head_of u))
   13.36 -        | decomp (Const (s, _) $ u $ ((m as Const ("op :",
   13.37 +        | decomp (Const (s, _) $ u $ ((m as Const (@{const_name "op :"},
   13.38              Type (_, [_, Type (_, [T, _])]))) $ p $ S)) =
   13.39                mkop s T (m, p, mk_collect p T (head_of u), S)
   13.40          | decomp _ = NONE;
   13.41 @@ -263,13 +265,13 @@
   13.42  
   13.43  fun add ctxt thm (tab as {to_set_simps, to_pred_simps, set_arities, pred_arities}) =
   13.44    case prop_of thm of
   13.45 -    Const ("Trueprop", _) $ (Const ("op =", Type (_, [T, _])) $ lhs $ rhs) =>
   13.46 +    Const (@{const_name Trueprop}, _) $ (Const (@{const_name "op ="}, Type (_, [T, _])) $ lhs $ rhs) =>
   13.47        (case body_type T of
   13.48 -         Type ("bool", []) =>
   13.49 +         @{typ bool} =>
   13.50             let
   13.51               val thy = Context.theory_of ctxt;
   13.52               fun factors_of t fs = case strip_abs_body t of
   13.53 -                 Const ("op :", _) $ u $ S =>
   13.54 +                 Const (@{const_name "op :"}, _) $ u $ S =>
   13.55                     if is_Free S orelse is_Var S then
   13.56                       let val ps = HOLogic.flat_tuple_paths u
   13.57                       in (SOME ps, (S, ps) :: fs) end
   13.58 @@ -279,7 +281,7 @@
   13.59               val (pfs, fs) = fold_map factors_of ts [];
   13.60               val ((h', ts'), fs') = (case rhs of
   13.61                   Abs _ => (case strip_abs_body rhs of
   13.62 -                     Const ("op :", _) $ u $ S =>
   13.63 +                     Const (@{const_name "op :"}, _) $ u $ S =>
   13.64                         (strip_comb S, SOME (HOLogic.flat_tuple_paths u))
   13.65                     | _ => error "member symbol on right-hand side expected")
   13.66                 | _ => (strip_comb rhs, NONE))
   13.67 @@ -412,7 +414,7 @@
   13.68      val {set_arities, pred_arities, to_pred_simps, ...} =
   13.69        PredSetConvData.get (Context.Proof lthy);
   13.70      fun infer (Abs (_, _, t)) = infer t
   13.71 -      | infer (Const ("op :", _) $ t $ u) =
   13.72 +      | infer (Const (@{const_name "op :"}, _) $ t $ u) =
   13.73            infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u)
   13.74        | infer (t $ u) = infer t #> infer u
   13.75        | infer _ = I;
    14.1 --- a/src/HOL/Tools/simpdata.ML	Thu Feb 25 22:17:33 2010 +0100
    14.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Feb 25 22:32:09 2010 +0100
    14.3 @@ -10,11 +10,11 @@
    14.4  structure Quantifier1 = Quantifier1Fun
    14.5  (struct
    14.6    (*abstract syntax*)
    14.7 -  fun dest_eq ((c as Const("op =",_)) $ s $ t) = SOME (c, s, t)
    14.8 +  fun dest_eq ((c as Const(@{const_name "op ="},_)) $ s $ t) = SOME (c, s, t)
    14.9      | dest_eq _ = NONE;
   14.10 -  fun dest_conj ((c as Const("op &",_)) $ s $ t) = SOME (c, s, t)
   14.11 +  fun dest_conj ((c as Const(@{const_name "op &"},_)) $ s $ t) = SOME (c, s, t)
   14.12      | dest_conj _ = NONE;
   14.13 -  fun dest_imp ((c as Const("op -->",_)) $ s $ t) = SOME (c, s, t)
   14.14 +  fun dest_imp ((c as Const(@{const_name "op -->"},_)) $ s $ t) = SOME (c, s, t)
   14.15      | dest_imp _ = NONE;
   14.16    val conj = HOLogic.conj
   14.17    val imp  = HOLogic.imp
   14.18 @@ -43,9 +43,9 @@
   14.19  
   14.20  fun mk_eq th = case concl_of th
   14.21    (*expects Trueprop if not == *)
   14.22 -  of Const ("==",_) $ _ $ _ => th
   14.23 -   | _ $ (Const ("op =", _) $ _ $ _) => mk_meta_eq th
   14.24 -   | _ $ (Const ("Not", _) $ _) => th RS @{thm Eq_FalseI}
   14.25 +  of Const (@{const_name "=="},_) $ _ $ _ => th
   14.26 +   | _ $ (Const (@{const_name "op ="}, _) $ _ $ _) => mk_meta_eq th
   14.27 +   | _ $ (Const (@{const_name "Not"}, _) $ _) => th RS @{thm Eq_FalseI}
   14.28     | _ => th RS @{thm Eq_TrueI}
   14.29  
   14.30  fun mk_eq_True r =
   14.31 @@ -57,7 +57,7 @@
   14.32  
   14.33  fun lift_meta_eq_to_obj_eq i st =
   14.34    let
   14.35 -    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
   14.36 +    fun count_imp (Const (@{const_name HOL.simp_implies}, _) $ P $ Q) = 1 + count_imp Q
   14.37        | count_imp _ = 0;
   14.38      val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
   14.39    in if j = 0 then @{thm meta_eq_to_obj_eq}
   14.40 @@ -65,7 +65,7 @@
   14.41        let
   14.42          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
   14.43          fun mk_simp_implies Q = fold_rev (fn R => fn S =>
   14.44 -          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Ps Q
   14.45 +          Const (@{const_name HOL.simp_implies}, propT --> propT --> propT) $ R $ S) Ps Q
   14.46          val aT = TFree ("'a", HOLogic.typeS);
   14.47          val x = Free ("x", aT);
   14.48          val y = Free ("y", aT)
   14.49 @@ -98,7 +98,7 @@
   14.50            else Variable.trade (K (fn [thm'] => res thm' rls)) (Variable.thm_context thm) [thm];
   14.51        in
   14.52          case concl_of thm
   14.53 -          of Const ("Trueprop", _) $ p => (case head_of p
   14.54 +          of Const (@{const_name Trueprop}, _) $ p => (case head_of p
   14.55              of Const (a, _) => (case AList.lookup (op =) pairs a
   14.56                of SOME rls => (maps atoms (res_fixed rls) handle THM _ => [thm])
   14.57                | NONE => [thm])
   14.58 @@ -159,9 +159,12 @@
   14.59    (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
   14.60  
   14.61  val mksimps_pairs =
   14.62 -  [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
   14.63 -   ("All", [@{thm spec}]), ("True", []), ("False", []),
   14.64 -   ("HOL.If", [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
   14.65 + [(@{const_name "op -->"}, [@{thm mp}]),
   14.66 +  (@{const_name "op &"}, [@{thm conjunct1}, @{thm conjunct2}]),
   14.67 +  (@{const_name All}, [@{thm spec}]),
   14.68 +  (@{const_name True}, []),
   14.69 +  (@{const_name False}, []),
   14.70 +  (@{const_name If}, [@{thm if_bool_eq_conj} RS @{thm iffD1}])];
   14.71  
   14.72  val HOL_basic_ss =
   14.73    Simplifier.global_context @{theory} empty_ss