src/HOL/Tools/Argo/argo_tactic.ML
changeset 67149 e61557884799
parent 67091 1393c2340eec
child 69576 cfac69e7b962
     1.1 --- a/src/HOL/Tools/Argo/argo_tactic.ML	Wed Dec 06 19:34:59 2017 +0100
     1.2 +++ b/src/HOL/Tools/Argo/argo_tactic.ML	Wed Dec 06 20:43:09 2017 +0100
     1.3 @@ -62,7 +62,7 @@
     1.4    | requires_mode Basic = [Basic, Full]
     1.5    | requires_mode Full = [Full]
     1.6  
     1.7 -val trace = Attrib.setup_config_string @{binding argo_trace} (K (string_of_mode None))
     1.8 +val trace = Attrib.setup_config_string \<^binding>\<open>argo_trace\<close> (K (string_of_mode None))
     1.9  
    1.10  fun allows_mode ctxt = exists (equal (Config.get ctxt trace) o string_of_mode) o requires_mode
    1.11  
    1.12 @@ -77,7 +77,7 @@
    1.13  
    1.14  (* timeout *)
    1.15  
    1.16 -val timeout = Attrib.setup_config_real @{binding argo_timeout} (K 10.0)
    1.17 +val timeout = Attrib.setup_config_real \<^binding>\<open>argo_timeout\<close> (K 10.0)
    1.18  
    1.19  fun time_of_timeout ctxt = Time.fromReal (Config.get ctxt timeout)
    1.20  
    1.21 @@ -144,8 +144,8 @@
    1.22      SOME ty => (ty, tcx)
    1.23    | NONE => add_new_type T tcx)
    1.24  
    1.25 -fun trans_type _ @{typ HOL.bool} = pair Argo_Expr.Bool
    1.26 -  | trans_type ctxt (Type (@{type_name "fun"}, [T1, T2])) =
    1.27 +fun trans_type _ \<^typ>\<open>HOL.bool\<close> = pair Argo_Expr.Bool
    1.28 +  | trans_type ctxt (Type (\<^type_name>\<open>fun\<close>, [T1, T2])) =
    1.29        trans_type ctxt T1 ##>> trans_type ctxt T2 #>> Argo_Expr.Func
    1.30    | trans_type ctxt T = (fn tcx =>
    1.31        (case ext_trans_type ctxt (trans_type ctxt) T tcx of
    1.32 @@ -164,22 +164,22 @@
    1.33      SOME c => (Argo_Expr.mk_con c, tcx)
    1.34    | NONE => add_new_term ctxt t (Term.fastype_of t) tcx)
    1.35  
    1.36 -fun mk_eq @{typ HOL.bool} = Argo_Expr.mk_iff
    1.37 +fun mk_eq \<^typ>\<open>HOL.bool\<close> = Argo_Expr.mk_iff
    1.38    | mk_eq _ = Argo_Expr.mk_eq
    1.39  
    1.40 -fun trans_term _ @{const HOL.True} = pair Argo_Expr.true_expr
    1.41 -  | trans_term _ @{const HOL.False} = pair Argo_Expr.false_expr
    1.42 -  | trans_term ctxt (@{const HOL.Not} $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
    1.43 -  | trans_term ctxt (@{const HOL.conj} $ t1 $ t2) =
    1.44 +fun trans_term _ \<^const>\<open>HOL.True\<close> = pair Argo_Expr.true_expr
    1.45 +  | trans_term _ \<^const>\<open>HOL.False\<close> = pair Argo_Expr.false_expr
    1.46 +  | trans_term ctxt (\<^const>\<open>HOL.Not\<close> $ t) = trans_term ctxt t #>> Argo_Expr.mk_not
    1.47 +  | trans_term ctxt (\<^const>\<open>HOL.conj\<close> $ t1 $ t2) =
    1.48        trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_and2
    1.49 -  | trans_term ctxt (@{const HOL.disj} $ t1 $ t2) =
    1.50 +  | trans_term ctxt (\<^const>\<open>HOL.disj\<close> $ t1 $ t2) =
    1.51        trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_or2
    1.52 -  | trans_term ctxt (@{const HOL.implies} $ t1 $ t2) =
    1.53 +  | trans_term ctxt (\<^const>\<open>HOL.implies\<close> $ t1 $ t2) =
    1.54        trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry Argo_Expr.mk_imp
    1.55 -  | trans_term ctxt (Const (@{const_name HOL.If}, _) $ t1 $ t2 $ t3) =
    1.56 +  | trans_term ctxt (Const (\<^const_name>\<open>HOL.If\<close>, _) $ t1 $ t2 $ t3) =
    1.57        trans_term ctxt t1 ##>> trans_term ctxt t2 ##>> trans_term ctxt t3 #>>
    1.58        (fn ((u1, u2), u3) => Argo_Expr.mk_ite u1 u2 u3)
    1.59 -  | trans_term ctxt (Const (@{const_name HOL.eq}, T) $ t1 $ t2) =
    1.60 +  | trans_term ctxt (Const (\<^const_name>\<open>HOL.eq\<close>, T) $ t1 $ t2) =
    1.61        trans_term ctxt t1 ##>> trans_term ctxt t2 #>> uncurry (mk_eq (Term.domain_type T))
    1.62    | trans_term ctxt (t as (t1 $ t2)) = (fn tcx =>
    1.63        (case ext_trans_term ctxt (trans_term ctxt) t tcx of
    1.64 @@ -260,16 +260,16 @@
    1.65  fun mk_ite t1 t2 t3 =
    1.66    let
    1.67      val T = Term.fastype_of t2
    1.68 -    val ite = Const (@{const_name HOL.If}, [@{typ HOL.bool}, T, T] ---> T)
    1.69 +    val ite = Const (\<^const_name>\<open>HOL.If\<close>, [\<^typ>\<open>HOL.bool\<close>, T, T] ---> T)
    1.70    in ite $ t1 $ t2 $ t3 end
    1.71  
    1.72 -fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = @{const HOL.True}
    1.73 -  | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = @{const HOL.False}
    1.74 +fun term_of _ (Argo_Expr.E (Argo_Expr.True, _)) = \<^const>\<open>HOL.True\<close>
    1.75 +  | term_of _ (Argo_Expr.E (Argo_Expr.False, _)) = \<^const>\<open>HOL.False\<close>
    1.76    | term_of cx (Argo_Expr.E (Argo_Expr.Not, [e])) = HOLogic.mk_not (term_of cx e)
    1.77    | term_of cx (Argo_Expr.E (Argo_Expr.And, es)) =
    1.78 -      mk_nary' @{const HOL.True} HOLogic.mk_conj (map (term_of cx) es)
    1.79 +      mk_nary' \<^const>\<open>HOL.True\<close> HOLogic.mk_conj (map (term_of cx) es)
    1.80    | term_of cx (Argo_Expr.E (Argo_Expr.Or, es)) =
    1.81 -      mk_nary' @{const HOL.False} HOLogic.mk_disj (map (term_of cx) es)
    1.82 +      mk_nary' \<^const>\<open>HOL.False\<close> HOLogic.mk_disj (map (term_of cx) es)
    1.83    | term_of cx (Argo_Expr.E (Argo_Expr.Imp, [e1, e2])) =
    1.84        HOLogic.mk_imp (term_of cx e1, term_of cx e2)
    1.85    | term_of cx (Argo_Expr.E (Argo_Expr.Iff, [e1, e2])) =
    1.86 @@ -289,7 +289,7 @@
    1.87          SOME t => t
    1.88        | NONE => raise Fail "bad expression")
    1.89  
    1.90 -fun as_prop ct = Thm.apply @{cterm HOL.Trueprop} ct
    1.91 +fun as_prop ct = Thm.apply \<^cterm>\<open>HOL.Trueprop\<close> ct
    1.92  
    1.93  fun cterm_of ctxt cons e = Thm.cterm_of ctxt (term_of (ctxt, cons) e)
    1.94  fun cprop_of ctxt cons e = as_prop (cterm_of ctxt cons e)
    1.95 @@ -316,7 +316,7 @@
    1.96  fun with_frees ctxt n mk =
    1.97    let
    1.98      val ns = map (fn i => "P" ^ string_of_int i) (0 upto (n - 1))
    1.99 -    val ts = map (Free o rpair @{typ bool}) ns
   1.100 +    val ts = map (Free o rpair \<^typ>\<open>bool\<close>) ns
   1.101      val t = mk_nary HOLogic.mk_disj (mk ts)
   1.102    in prove_taut ctxt ns t end
   1.103  
   1.104 @@ -373,12 +373,12 @@
   1.105  
   1.106  fun flat_conj_conv ct =
   1.107    (case Thm.term_of ct of
   1.108 -    @{const HOL.conj} $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
   1.109 +    \<^const>\<open>HOL.conj\<close> $ _ $ _ => flatten_conv flat_conj_conv flatten_and_thm ct
   1.110    | _ => Conv.all_conv ct)
   1.111  
   1.112  fun flat_disj_conv ct =
   1.113    (case Thm.term_of ct of
   1.114 -    @{const HOL.disj} $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
   1.115 +    \<^const>\<open>HOL.disj\<close> $ _ $ _ => flatten_conv flat_disj_conv flatten_or_thm ct
   1.116    | _ => Conv.all_conv ct)
   1.117  
   1.118  fun explode rule1 rule2 thm =
   1.119 @@ -414,7 +414,7 @@
   1.120    in mk_rewr (discharge2 lhs rhs rule) end
   1.121  
   1.122  fun with_conj f g ct = iff_intro iff_conj_thm (f o explode_conj) g ct
   1.123 -fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply @{cterm HOL.Not} ct)
   1.124 +fun with_ndis f g ct = iff_intro iff_ndis_thm (f o explode_ndis) g (Thm.apply \<^cterm>\<open>HOL.Not\<close> ct)
   1.125  
   1.126  fun swap_indices n iss = map (fn i => find_index (fn is => member (op =) is i) iss) (0 upto (n - 1))
   1.127  fun sort_nary w f g (n, iss) = w (f (map hd iss)) (under_assumption (f (swap_indices n iss) o g))
   1.128 @@ -484,7 +484,7 @@
   1.129    | replay_args_conv ctxt [c1, c2] ct = binop_conv (replay_conv ctxt c1) (replay_conv ctxt c2) ct
   1.130    | replay_args_conv ctxt (c :: cs) ct =
   1.131        (case Term.head_of (Thm.term_of ct) of
   1.132 -        Const (@{const_name HOL.If}, _) =>
   1.133 +        Const (\<^const_name>\<open>HOL.If\<close>, _) =>
   1.134            let val (cs', c') = split_last cs
   1.135            in Conv.combination_conv (replay_args_conv ctxt (c :: cs')) (replay_conv ctxt c') ct end
   1.136        | _ => binop_conv (replay_conv ctxt c) (replay_args_conv ctxt cs) ct)
   1.137 @@ -520,7 +520,7 @@
   1.138  
   1.139  val unit_rule = @{lemma "(P \<Longrightarrow> False) \<Longrightarrow> (\<not>P \<Longrightarrow> False) \<Longrightarrow> False" by fast}
   1.140  val unit_rule_var = Thm.dest_arg (Thm.dest_arg1 (Thm.cprem_of unit_rule 1))
   1.141 -val bogus_ct = @{cterm HOL.True}
   1.142 +val bogus_ct = \<^cterm>\<open>HOL.True\<close>
   1.143  
   1.144  fun replay_unit_res lit (pthm, plits) (nthm, nlits) =
   1.145    let
   1.146 @@ -543,7 +543,7 @@
   1.147  fun replay_hyp i ct =
   1.148    if i < 0 then (Thm.assume ct, [(~i, ct)])
   1.149    else
   1.150 -    let val cu = as_prop (Thm.apply @{cterm HOL.Not} (Thm.apply @{cterm HOL.Not} (Thm.dest_arg ct)))
   1.151 +    let val cu = as_prop (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.apply \<^cterm>\<open>HOL.Not\<close> (Thm.dest_arg ct)))
   1.152      in (discharge (Thm.assume cu) dneg_rule, [(~i, cu)]) end
   1.153  
   1.154  
   1.155 @@ -601,7 +601,7 @@
   1.156  
   1.157  fun unclausify (thm, lits) ls =
   1.158    (case (Thm.prop_of thm, lits) of
   1.159 -    (@{const HOL.Trueprop} $ @{const HOL.False}, [(_, ct)]) =>
   1.160 +    (\<^const>\<open>HOL.Trueprop\<close> $ \<^const>\<open>HOL.False\<close>, [(_, ct)]) =>
   1.161        let val thm = Thm.implies_intr ct thm
   1.162        in (discharge thm unclausify_rule1 handle THM _ => discharge thm unclausify_rule2, ls) end
   1.163    | _ => (thm, Ord_List.union lit_ord lits ls))
   1.164 @@ -668,22 +668,22 @@
   1.165    let val ct = Drule.strip_imp_concl (Thm.cprop_of thm)
   1.166    in
   1.167      (case Thm.term_of ct of
   1.168 -      @{const HOL.Trueprop} $ Var (_, @{typ HOL.bool}) =>
   1.169 -        instantiate (Thm.dest_arg ct) @{cterm HOL.False} thm
   1.170 -    | Var _ => instantiate ct @{cprop HOL.False} thm
   1.171 +      \<^const>\<open>HOL.Trueprop\<close> $ Var (_, \<^typ>\<open>HOL.bool\<close>) =>
   1.172 +        instantiate (Thm.dest_arg ct) \<^cterm>\<open>HOL.False\<close> thm
   1.173 +    | Var _ => instantiate ct \<^cprop>\<open>HOL.False\<close> thm
   1.174      | _ => thm)
   1.175    end
   1.176  
   1.177  fun atomize_conv ctxt ct =
   1.178    (case Thm.term_of ct of
   1.179 -    @{const HOL.Trueprop} $ _ => Conv.all_conv
   1.180 -  | @{const Pure.imp} $ _ $ _ =>
   1.181 +    \<^const>\<open>HOL.Trueprop\<close> $ _ => Conv.all_conv
   1.182 +  | \<^const>\<open>Pure.imp\<close> $ _ $ _ =>
   1.183        Conv.binop_conv (atomize_conv ctxt) then_conv
   1.184        Conv.rewr_conv @{thm atomize_imp}
   1.185 -  | Const (@{const_name Pure.eq}, _) $ _ $ _ =>
   1.186 +  | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ =>
   1.187        Conv.binop_conv (atomize_conv ctxt) then_conv
   1.188        Conv.rewr_conv @{thm atomize_eq}
   1.189 -  | Const (@{const_name Pure.all}, _) $ Abs _ =>
   1.190 +  | Const (\<^const_name>\<open>Pure.all\<close>, _) $ Abs _ =>
   1.191        Conv.binder_conv (atomize_conv o snd) ctxt then_conv
   1.192        Conv.rewr_conv @{thm atomize_all}
   1.193    | _ => Conv.all_conv) ct
   1.194 @@ -723,7 +723,7 @@
   1.195      | (NONE, _) => Tactical.no_tac)) ctxt
   1.196  
   1.197  val _ =
   1.198 -  Theory.setup (Method.setup @{binding argo}
   1.199 +  Theory.setup (Method.setup \<^binding>\<open>argo\<close>
   1.200      (Scan.optional Attrib.thms [] >>
   1.201        (fn thms => fn ctxt => METHOD (fn facts =>
   1.202          HEADGOAL (argo_tac ctxt (thms @ facts)))))