src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

 
 val nitpicksimp_attrs = @{attributes [nitpick_simp]};
 val simp_attrs = @{attributes [simp]};
 
 fun use_primcorecursive () =
-  error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^
-    quote (#1 @{command_keyword primcorec}) ^ ")");
+  error ("\"auto\" failed (try " ^ quote (#1 \<^command_keyword>\<open>primcorecursive\<close>) ^ " instead of " ^
+    quote (#1 \<^command_keyword>\<open>primcorec\<close>) ^ ")");
 
 datatype corec_option =
   Plugins_Option of Proof.context -> Plugin_Name.filter |
   Sequential_Option |
   Exhaustive_Option |

     abs 0
   end;
 
 val abs_tuple_balanced = HOLogic.tupled_lambda o mk_tuple_balanced;
 
-fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) =
+fun curried_type (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>prod\<close>, Ts), T])) =
   Ts ---> T;
 
 fun sort_list_duplicates xs = map snd (sort (int_ord o apply2 fst) xs);
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};

   let
     val thy = Proof_Context.theory_of ctxt;
 
     fun fld conds t =
       (case Term.strip_comb t of
-        (Const (@{const_name Let}, _), [_, _]) => fld conds (unfold_lets_splits t)
-      | (Const (@{const_name If}, _), [cond, then_branch, else_branch]) =>
+        (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => fld conds (unfold_lets_splits t)
+      | (Const (\<^const_name>\<open>If\<close>, _), [cond, then_branch, else_branch]) =>
         fld (conds @ conjuncts_s cond) then_branch o fld (conds @ s_not_conj [cond]) else_branch
       | (Const (c, _), args as _ :: _ :: _) =>
         let val n = num_binder_types (Sign.the_const_type thy c) - 1 in
           if n >= 0 andalso n < length args then
             (case fastype_of1 (bound_Ts, nth args n) of

           Abs (Name.uu, T, massage_abs (T :: bound_Ts) (m - 1) (incr_boundvars 1 t $ Bound 0))
         end
     and massage_rec bound_Ts t =
       let val typof = curry fastype_of1 bound_Ts in
         (case Term.strip_comb t of
-          (Const (@{const_name Let}, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
-        | (Const (@{const_name If}, _), obj :: (branches as [_, _])) =>
+          (Const (\<^const_name>\<open>Let\<close>, _), [_, _]) => massage_rec bound_Ts (unfold_lets_splits t)
+        | (Const (\<^const_name>\<open>If\<close>, _), obj :: (branches as [_, _])) =>
           (case List.partition Term.is_dummy_pattern (map (massage_rec bound_Ts) branches) of
             (dummy_branch' :: _, []) => dummy_branch'
           | (_, [branch']) => branch'
           | (_, branches') =>
             Term.list_comb (If_const (typof (hd branches')) $ tap (check_no_call bound_Ts) obj,
               branches'))
-        | (c as Const (@{const_name case_prod}, _), arg :: args) =>
+        | (c as Const (\<^const_name>\<open>case_prod\<close>, _), arg :: args) =>
           massage_rec bound_Ts
             (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
         | (Const (c, _), args as _ :: _ :: _) =>
           (case try strip_fun_type (Sign.the_const_type thy c) of
             SOME (gen_branch_Ts, gen_body_fun_T) =>

         | _ => massage_leaf bound_Ts t)
       end;
   in
     massage_rec bound_Ts t0
     |> Term.map_aterms (fn t =>
-      if Term.is_dummy_pattern t then Const (@{const_name undefined}, fastype_of t) else t)
+      if Term.is_dummy_pattern t then Const (\<^const_name>\<open>undefined\<close>, fastype_of t) else t)
   end;
 
 fun massage_let_if_case_corec ctxt has_call massage_leaf bound_Ts t0 =
   massage_let_if_case ctxt has_call massage_leaf (K (unexpected_corec_call_in ctxt [t0]))
     (K (unsupported_case_around_corec_call ctxt [t0])) bound_Ts t0;
 
 fun massage_nested_corec_call ctxt has_call massage_call massage_noncall bound_Ts U T t0 =
   let
     fun check_no_call t = if has_call t then unexpected_corec_call_in ctxt [t0] t else ();
 
-    fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2]))
-        (Type (@{type_name fun}, [T1, T2])) t =
+    fun massage_mutual_call bound_Ts (Type (\<^type_name>\<open>fun\<close>, [_, U2]))
+        (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) t =
         Abs (Name.uu, T1, massage_mutual_call (T1 :: bound_Ts) U2 T2 (incr_boundvars 1 t $ Bound 0))
       | massage_mutual_call bound_Ts U T t =
         (if has_call t then massage_call else massage_noncall) bound_Ts U T t;
 
     fun massage_map bound_Ts (Type (_, Us)) (Type (s, Ts)) t =

         fun massage_body () =
           Term.lambda var (Term.incr_boundvars 1 (massage_any_call bound_Ts U T
             (betapply (t, var))));
       in
         (case t of
-          Const (@{const_name comp}, _) $ t1 $ t2 =>
+          Const (\<^const_name>\<open>comp\<close>, _) $ t1 $ t2 =>
           if has_call t2 then massage_body ()
           else mk_comp bound_Ts (massage_mutual_fun bound_Ts U T t1, t2)
         | _ => massage_body ())
       end
     and massage_any_call bound_Ts U T =

                 Term.list_comb (f',
                   @{map 3} (massage_any_call bound_Ts) (binder_types f'_T) arg_Ts args)
               end
             | NONE =>
               (case t of
-                Const (@{const_name case_prod}, _) $ t' =>
+                Const (\<^const_name>\<open>case_prod\<close>, _) $ t' =>
                 let
                   val U' = curried_type U;
                   val T' = curried_type T;
                 in
-                  Const (@{const_name case_prod}, U' --> U) $ massage_any_call bound_Ts U' T' t'
+                  Const (\<^const_name>\<open>case_prod\<close>, U' --> U) $ massage_any_call bound_Ts U' T' t'
                 end
               | t1 $ t2 =>
                 (if has_call t2 then
                    massage_mutual_call bound_Ts U T t
                  else

     val substAT = Term.typ_subst_TVars As_rho;
     val substCT = Term.typ_subst_TVars Cs_rho;
 
     val perm_Cs' = map substCT perm_Cs;
 
-    fun call_of nullary [] [g_i] [Type (@{type_name fun}, [_, T])] =
+    fun call_of nullary [] [g_i] [Type (\<^type_name>\<open>fun\<close>, [_, T])] =
         (if exists_subtype_in Cs T then Nested_Corec
          else if nullary then Dummy_No_Corec
          else No_Corec) g_i
       | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
 

      co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
      co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
      is_some gfp_sugar_thms, lthy)
   end;
 
-val undef_const = Const (@{const_name undefined}, dummyT);
+val undef_const = Const (\<^const_name>\<open>undefined\<close>, dummyT);
 
 type coeqn_data_disc =
   {fun_name: string,
    fun_T: typ,
    fun_args: term list,

     val (sequential, basic_ctr_specs) =
       the (AList.lookup (op =) (fun_names ~~ (sequentials ~~ basic_ctr_specss)) fun_name);
 
     val discs = map #disc basic_ctr_specs;
     val ctrs = map #ctr basic_ctr_specs;
-    val not_disc = head_of concl = @{term Not};
+    val not_disc = head_of concl = \<^term>\<open>Not\<close>;
     val _ = not_disc andalso length ctrs <> 2 andalso
       error_at ctxt [concl] "Negated discriminator for a type with \<noteq> 2 constructors";
     val disc' = find_subterm (member (op =) discs o head_of) concl;
     val eq_ctr0 = concl |> perhaps (try HOLogic.dest_not) |> try (HOLogic.dest_eq #> snd)
       |> (fn SOME t => let val n = find_index (curry (op =) t) ctrs in

     NONE => (I, I, I)
   | SOME {fun_args, rhs_term, ... } =>
     let
       val bound_Ts = List.rev (map fastype_of fun_args);
 
-      fun rewrite_stop _ t = if has_call t then @{term False} else @{term True};
+      fun rewrite_stop _ t = if has_call t then \<^term>\<open>False\<close> else \<^term>\<open>True\<close>;
       fun rewrite_end _ t = if has_call t then undef_const else t;
       fun rewrite_cont bound_Ts t =
         if has_call t then mk_tuple1_balanced bound_Ts (snd (strip_comb t)) else undef_const;
       fun massage f _ = massage_let_if_case_corec ctxt has_call f bound_Ts rhs_term
         |> abs_tuple_balanced fun_args;

           fun rewrite bound_Ts (Abs (s, T', t')) = Abs (s, T', rewrite (T' :: bound_Ts) t')
             | rewrite bound_Ts (t as _ $ _) =
               let val (u, vs) = strip_comb t in
                 if is_Free u andalso has_call u then
                   Inr_const T U2 $ mk_tuple1_balanced bound_Ts vs
-                else if try (fst o dest_Const) u = SOME @{const_name case_prod} then
+                else if try (fst o dest_Const) u = SOME \<^const_name>\<open>case_prod\<close> then
                   map (rewrite bound_Ts) vs |> chop 1
                   |>> HOLogic.mk_case_prod o the_single
                   |> Term.list_comb
                 else
                   Term.list_comb (rewrite bound_Ts u, map (rewrite bound_Ts) vs)

     val corecs = map #corec corec_specs;
     val ctr_specss = map #ctr_specs corec_specs;
     val corec_args = hd corecs
       |> fst o split_last o binder_types o fastype_of
       |> map (fn T =>
-          if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, @{term False})
-          else Const (@{const_name undefined}, T))
+          if range_type T = HOLogic.boolT then Abs (Name.uu_, domain_type T, \<^term>\<open>False\<close>)
+          else Const (\<^const_name>\<open>undefined\<close>, T))
       |> fold2 (fold o build_corec_arg_disc) ctr_specss disc_eqnss
       |> fold2 (fold o build_corec_args_sel ctxt has_call) sel_eqnss ctr_specss;
 
     val bad = fold (add_extra_frees ctxt [] []) corec_args [];
     val _ = null bad orelse

           map2 (fn excludes => mk_excludesss excludes o length o #ctr_specs)
             (map2 append excludess' taut_thmss) corec_specs;
 
         fun prove_disc ({ctr_specs, ...} : corec_spec) excludesss
             ({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
-          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), @{term "\<lambda>x. x = x"}) then
+          if Term.aconv_untyped (#disc (nth ctr_specs ctr_no), \<^term>\<open>\<lambda>x. x = x\<close>) then
             []
           else
             let
               val {disc, corec_disc, ...} = nth ctr_specs ctr_no;
               val k = 1 + ctr_no;

                 |> curry betapply disc
                 |> HOLogic.mk_Trueprop
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
             in
-              if prems = [@{term False}] then
+              if prems = [\<^term>\<open>False\<close>] then
                 []
               else
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_primcorec_disc_tac ctxt def_thms corec_disc k m excludesss)

                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
               val disc_thm_opt = AList.lookup (op =) disc_alist disc;
               val sel_thms = map (snd o snd) (filter (member (op =) sels o fst) sel_alist);
             in
-              if prems = [@{term False}] then
+              if prems = [\<^term>\<open>False\<close>] then
                 []
               else
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} =>
                     mk_primcorec_ctr_tac ctxt m collapse disc_thm_opt sel_thms)

                           andalso exists #auto_gen disc_eqns;
                       val rhs =
                         (if exhaustive_code then
                            split_last (map_filter I ctr_conds_argss_opt) ||> snd
                          else
-                           Const (@{const_name Code.abort}, @{typ String.literal} -->
+                           Const (\<^const_name>\<open>Code.abort\<close>, \<^typ>\<open>String.literal\<close> -->
                                (HOLogic.unitT --> body_type fun_T) --> body_type fun_T) $
                              HOLogic.mk_literal fun_name $
                              absdummy HOLogic.unitT (incr_boundvars 1 lhs)
                            |> pair (map_filter I ctr_conds_argss_opt))
                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)

    || Parse.reserved "transfer" >> K Transfer_Option);
 
 val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
   ((Parse.prop >> pair Binding.empty_atts) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
 
-val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
+val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>primcorecursive\<close>
   "define primitive corecursive functions"
-  ((Scan.optional (@{keyword "("} |--
-      Parse.!!! (Parse.list1 corec_option_parser) --| @{keyword ")"}) []) --
+  ((Scan.optional (\<^keyword>\<open>(\<close> |--
+      Parse.!!! (Parse.list1 corec_option_parser) --| \<^keyword>\<open>)\<close>) []) --
     (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorecursive_cmd true));
 
-val _ = Outer_Syntax.local_theory @{command_keyword primcorec}
+val _ = Outer_Syntax.local_theory \<^command_keyword>\<open>primcorec\<close>
   "define primitive corecursive functions"
-  ((Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 corec_option_parser)
-      --| @{keyword ")"}) []) --
+  ((Scan.optional (\<^keyword>\<open>(\<close> |-- Parse.!!! (Parse.list1 corec_option_parser)
+      --| \<^keyword>\<open>)\<close>) []) --
     (Parse.vars -- where_alt_props_of_parser) >> uncurry (primcorec_cmd true));
 
 val _ = Theory.setup (gfp_rec_sugar_interpretation transfer_plugin
   gfp_rec_sugar_transfer_interpretation);