1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 21 14:39:52 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jun 21 15:36:09 2021 +0200
1.3 @@ -306,8 +306,8 @@
1.4 in subst t end;
1.5
1.6 (* is a term a substitution for a bdv as found in programs and tactics *)
1.7 -fun is_bdv_subst (Const ("List.list.Cons", _) $
1.8 - (Const ("Product_Type.Pair", _) $ str $ _) $ _) = is_bdv (HOLogic.dest_string str)
1.9 +fun is_bdv_subst (Const (\<^const_name>\<open>Cons\<close>, _) $
1.10 + (Const (\<^const_name>\<open>Pair\<close>, _) $ str $ _) $ _) = is_bdv (HOLogic.dest_string str)
1.11 | is_bdv_subst _ = false;
1.12
1.13 (* this shall be improved due to future requirements *)
1.14 @@ -336,54 +336,54 @@
1.15 | free2var (t1 $ t2) = (free2var t1) $ (free2var t2);
1.16 \<close>
1.17
1.18 -fun mk_listT T = Type ("List.list", [T]);
1.19 -fun list_const T = Const ("List.list.Cons", [T, mk_listT T] ---> mk_listT T);
1.20 -fun list2isalist T [] = Const ("List.list.Nil", mk_listT T)
1.21 +fun mk_listT T = Type (\<^type_name>\<open>list\<close>, [T]);
1.22 +fun list_const T = Const (\<^const_name>\<open>Cons\<close>, [T, mk_listT T] ---> mk_listT T);
1.23 +fun list2isalist T [] = Const (\<^const_name>\<open>Nil\<close>, mk_listT T)
1.24 | list2isalist T (t :: ts) = (list_const T) $ t $ (list2isalist T ts);
1.25
1.26 -fun isapair2pair (Const ("Product_Type.Pair",_) $ a $ b) = (a, b)
1.27 +fun isapair2pair (Const (\<^const_name>\<open>Pair\<close>,_) $ a $ b) = (a, b)
1.28 | isapair2pair t =
1.29 raise ERROR ("isapair2pair called with " ^ UnparseC.term t);
1.30 fun isalist2list ls =
1.31 let
1.32 - fun get es (Const("List.list.Cons", _) $ t $ ls) = get (t :: es) ls
1.33 - | get es (Const("List.list.Nil", _)) = es
1.34 + fun get es (Const(\<^const_name>\<open>Cons\<close>, _) $ t $ ls) = get (t :: es) ls
1.35 + | get es (Const(\<^const_name>\<open>Nil\<close>, _)) = es
1.36 | get _ t = raise TERM ("isalist2list applied to NON-list: ", [t])
1.37 in (rev o (get [])) ls end;
1.38
1.39 -fun is_list ((Const ("List.list.Cons", _)) $ _ $ _) = true
1.40 +fun is_list ((Const (\<^const_name>\<open>Cons\<close>, _)) $ _ $ _) = true
1.41 | is_list _ = false;
1.42 -fun dest_listT (Type ("List.list", [T])) = T
1.43 +fun dest_listT (Type (\<^type_name>\<open>list\<close>, [T])) = T
1.44 | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], []);
1.45 fun is_bool_list t =
1.46 (if dest_listT (Term.type_of t) = HOLogic.boolT then true else false)
1.47 handle TYPE _ => false
1.48
1.49
1.50 -fun dest_binop_typ (Type ("fun", [range, Type ("fun", [arg2, arg1])])) = (arg1, arg2, range)
1.51 +fun dest_binop_typ (Type (\<^type_name>\<open>fun\<close>, [range, Type (\<^type_name>\<open>fun\<close>, [arg2, arg1])])) = (arg1, arg2, range)
1.52 | dest_binop_typ _ = raise ERROR "dest_binop_typ: not binary";
1.53 -fun dest_equals (Const("HOL.eq", _) $ t $ u) = (t, u) (* Pure/logic.ML: Const ("==", ..*)
1.54 +fun dest_equals (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) = (t, u) (* Pure/logic.ML: Const ("==", ..*)
1.55 | dest_equals t = raise TERM ("dest_equals'", [t]);
1.56 -fun is_equality (Const("HOL.eq",_) $ _ $ _) = true (* logic.ML: Const("=="*)
1.57 +fun is_equality (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = true (* logic.ML: Const("=="*)
1.58 | is_equality _ = false;
1.59 -fun mk_equality (t, u) = (Const("HOL.eq", [type_of t, type_of u] ---> HOLogic.boolT) $ t $ u);
1.60 -fun is_expliceq (Const("HOL.eq",_) $ (Free _) $ _) = true
1.61 +fun mk_equality (t, u) = (Const(\<^const_name>\<open>HOL.eq\<close>, [type_of t, type_of u] ---> HOLogic.boolT) $ t $ u);
1.62 +fun is_expliceq (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ (Free _) $ _) = true
1.63 | is_expliceq _ = false;
1.64 -fun strip_trueprop (Const ("HOL.Trueprop", _) $ t) = t
1.65 +fun strip_trueprop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = t
1.66 | strip_trueprop t = t;
1.67
1.68 (* (A1==>...An==>B) goes to (A1==>...An==>) Pure/logic.ML: term -> term list*)
1.69 -fun strip_imp_prems' (Const ("Pure.imp", _) $ A $ t) =
1.70 +fun strip_imp_prems' (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ A $ t) =
1.71 let
1.72 - fun coll_prems As (Const("Pure.imp", _) $ A $ t) =
1.73 + fun coll_prems As (Const(\<^const_name>\<open>Pure.imp\<close>, _) $ A $ t) =
1.74 coll_prems (As $ (Logic.implies $ A)) t
1.75 | coll_prems As _ = SOME As
1.76 in coll_prems (Logic.implies $ A) t end
1.77 | strip_imp_prems' _ = NONE; (* *)
1.78
1.79 (* (A1==>...An==>) (B) goes to (A1==>...An==>B), where B is lowest branch, 2002 Pure/thm.ML *)
1.80 -fun ins_concl (Const ("Pure.imp", _) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
1.81 - | ins_concl (Const ("Pure.imp", _) $ A ) B = Logic.implies $ A $ B
1.82 +fun ins_concl (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ A $ t) B = Logic.implies $ A $ (ins_concl t B)
1.83 + | ins_concl (Const (\<^const_name>\<open>Pure.imp\<close>, _) $ A ) B = Logic.implies $ A $ B
1.84 | ins_concl t B = raise TERM ("ins_concl", [t, B]);
1.85
1.86 fun vperm (Var _, Var _) = true (* 2002 Pure/thm.ML *)
1.87 @@ -431,10 +431,10 @@
1.88
1.89 fun pairT T1 T2 = Type ("*", [T1, T2]);
1.90 fun PairT T1 T2 = ([T1, T2] ---> Type ("*", [T1, T2]));
1.91 -fun pairt t1 t2 = Const ("Product_Type.Pair", PairT (type_of t1) (type_of t2)) $ t1 $ t2;
1.92 +fun pairt t1 t2 = Const (\<^const_name>\<open>Pair\<close>, PairT (type_of t1) (type_of t2)) $ t1 $ t2;
1.93
1.94 fun mk_factroot op_(*=thy.sqrt*) T fact root =
1.95 - Const ("Groups.times_class.times", [T, T] ---> T) $ (term_of_num T fact) $
1.96 + Const (\<^const_name>\<open>times\<close>, [T, T] ---> T) $ (term_of_num T fact) $
1.97 (Const (op_, T --> T) $ term_of_num T root);
1.98 fun mk_var_op_num v op_ optype ntyp n = Const (op_, optype) $ v $ Free (str_of_int n, ntyp);
1.99 fun mk_num_op_var v op_ optype ntyp n = Const (op_, optype) $ Free (str_of_int n, ntyp) $ v;
1.100 @@ -447,7 +447,7 @@
1.101 val (T1, T2) = (type_of t1, type_of t2)
1.102 in
1.103 if T1 <> T2 then raise TYPE ("mk_add gets ", [T1, T2], [t1,t2])
1.104 - else (Const ("Groups.plus_class.plus", [T1, T2] ---> T1) $ t1 $ t2)
1.105 + else (Const (\<^const_name>\<open>plus\<close>, [T1, T2] ---> T1) $ t1 $ t2)
1.106 end;
1.107
1.108 (** transform binary numeralsstrings **)
1.109 @@ -474,9 +474,9 @@
1.110 | inst_abs (Free sT) = Free sT
1.111 | inst_abs (Bound n) = Bound n
1.112 | inst_abs (Var iT) = Var iT
1.113 - | inst_abs (Const ("HOL.Let",T1) $ e $ (Abs (v, T2, b))) =
1.114 + | inst_abs (Const (\<^const_name>\<open>Let\<close>,T1) $ e $ (Abs (v, T2, b))) =
1.115 let val b' = subst_bound (Free (v, T2), b); (*fun variant_abs: term.ML*)
1.116 - in Const ("HOL.Let", T1) $ inst_abs e $ (Abs (v, T2, inst_abs b')) end
1.117 + in Const (\<^const_name>\<open>Let\<close>, T1) $ inst_abs e $ (Abs (v, T2, inst_abs b')) end
1.118 | inst_abs (t1 $ t2) = inst_abs t1 $ inst_abs t2
1.119 | inst_abs t = t;
1.120
1.121 @@ -572,9 +572,9 @@
1.122 | var_for vs (t1 $ t2) id = (var_for vs t1 id) @ (var_for vs t2 id)
1.123
1.124 val poly_consts = (* TODO: adopt syntax-const from Isabelle*)
1.125 - ["Groups.plus_class.plus", "Groups.minus_class.minus",
1.126 - "Rings.divide_class.divide", "Groups.times_class.times",
1.127 - "Transcendental.powr"];
1.128 + [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
1.129 + \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
1.130 + \<^const_name>\<open>powr\<close>];
1.131 (* treat Free, Const, Var as variables in polynomials *)
1.132 fun vars_of t =
1.133 let
1.134 @@ -585,7 +585,7 @@
1.135 use only, if description is not available, eg. not input ?WN:14.5.03 ??!?*)
1.136 fun dest_list' t = if is_list t then isalist2list t else [t];
1.137
1.138 -fun negat (Const ("HOL.Not", _) $ P, P') = P = P'
1.139 +fun negat (Const (\<^const_name>\<open>Not\<close>, _) $ P, P') = P = P'
1.140 | negat _ = false
1.141 fun negates p1 p2 = negat (p1, p2) orelse negat (swap (p1, p2));
1.142