1.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Sun Jul 18 21:19:25 2021 +0200
1.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 15:34:54 2021 +0200
1.3 @@ -163,7 +163,7 @@
1.4 (sort |> map quote |> commas |> enclose "List(" ")"))
1.5
1.6 fun scala_of_term (Const (s, T)) =
1.7 - enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T)
1.8 + enclose "Const (" ")" (quote s ^ ", " ^ scala_of_typ T)
1.9 | scala_of_term (Free (s, T)) =
1.10 enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T)
1.11 | scala_of_term (Var ((s, i), T)) =
1.12 @@ -254,26 +254,26 @@
1.13 val int_opt_of_string = ThmC_Def.int_opt_of_string
1.14 fun is_num' str = case int_opt_of_string str of SOME _ => true | NONE => false;
1.15
1.16 -fun is_num (Const ("Num.numeral_class.numeral", _) $ _) = true
1.17 - | is_num (Const ("Groups.uminus_class.uminus", _) $
1.18 - (Const ("Num.numeral_class.numeral", _) $ _)) = true
1.19 - | is_num (Const ("Groups.one_class.one", _)) = true
1.20 - | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _)) = true
1.21 - | is_num (Const ("Groups.zero_class.zero", _)) = true
1.22 - | is_num (Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.zero_class.zero", _)) = true
1.23 +fun is_num (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = true
1.24 + | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $
1.25 + (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) = true
1.26 + | is_num (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
1.27 + | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
1.28 + | is_num (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
1.29 + | is_num (Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
1.30 | is_num _ = false;
1.31
1.32 fun string_of_num n = (n |> HOLogic.dest_number |> snd |> string_of_int)
1.33
1.34 -fun mk_negative T t = Const ("Groups.uminus_class.uminus", T --> T) $ t
1.35 +fun mk_negative T t = Const (\<^const_name>\<open>uminus\<close>, T --> T) $ t
1.36 fun mk_frac T (sg, (i1, i2)) =
1.37 if sg = 1 then
1.38 if i2 = 1 then HOLogic.mk_number T i1
1.39 - else Const ("Rings.divide_class.divide", T --> T --> T) $
1.40 + else Const (\<^const_name>\<open>divide_class.divide\<close>, T --> T --> T) $
1.41 HOLogic.mk_number T i1 $ HOLogic.mk_number T i2
1.42 else (*take negative*)
1.43 if i2 = 1 then mk_negative T (HOLogic.mk_number T i1)
1.44 - else Const ("Rings.divide_class.divide", T --> T --> T) $
1.45 + else Const (\<^const_name>\<open>divide_class.divide\<close>, T --> T --> T) $
1.46 mk_negative T (HOLogic.mk_number T i1) $ HOLogic.mk_number T i2
1.47
1.48 val numerals_to_Free = (* Makarius 100308 *)
1.49 @@ -407,7 +407,7 @@
1.50 | dest_binop_typ _ = raise ERROR "dest_binop_typ: not binary";
1.51 fun dest_equals (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t $ u) = (t, u) (* Pure/logic.ML: Const ("==", ..*)
1.52 | dest_equals t = raise TERM ("dest_equals'", [t]);
1.53 -fun is_equality (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = true (* logic.ML: Const("=="*)
1.54 +fun is_equality (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _) = true (* logic.ML: Const ("=="*)
1.55 | is_equality _ = false;
1.56 fun mk_equality (t, u) = (Const(\<^const_name>\<open>HOL.eq\<close>, [type_of t, type_of u] ---> HOLogic.boolT) $ t $ u);
1.57 fun is_expliceq (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ (Free _) $ _) = true
1.58 @@ -576,16 +576,16 @@
1.59 |> typ_a2real; (*TODO drop*)
1.60 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str
1.61
1.62 -fun is_atom (Const ("Num.numeral_class.numeral", _) $ _) = true
1.63 - | is_atom (Const ("Groups.one_class.one", _)) = true
1.64 - | is_atom (Const ("Groups.zero_class.zero", _)) = true
1.65 +fun is_atom (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = true
1.66 + | is_atom (Const (\<^const_name>\<open>one_class.one\<close>, _)) = true
1.67 + | is_atom (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = true
1.68 | is_atom (Const _) = true
1.69 | is_atom (Free _) = true
1.70 | is_atom (Var _) = true
1.71 | is_atom _ = false;
1.72 -fun string_of_atom (t as Const ("Num.numeral_class.numeral", _) $ _) = to_string t
1.73 - | string_of_atom (t as Const ("Groups.one_class.one", _)) = to_string t
1.74 - | string_of_atom (t as Const ("Groups.zero_class.zero", _)) = to_string t
1.75 +fun string_of_atom (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) = to_string t
1.76 + | string_of_atom (t as Const (\<^const_name>\<open>one_class.one\<close>, _)) = to_string t
1.77 + | string_of_atom (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = to_string t
1.78 | string_of_atom (Const (str, _)) = str
1.79 | string_of_atom (Free (str, _)) = str
1.80 | string_of_atom (Var ((str, int), _)) = str ^ "_" ^ string_of_int int
2.1 --- a/src/Tools/isac/Interpret/li-tool.sml Sun Jul 18 21:19:25 2021 +0200
2.2 +++ b/src/Tools/isac/Interpret/li-tool.sml Mon Jul 19 15:34:54 2021 +0200
2.3 @@ -68,28 +68,28 @@
2.4 in (flat o (map (itm2arg itms))) pats end;
2.5
2.6 (* convert a Prog_Tac to Tactic.input; specific for "Prog_Tac.SubProblem" *)
2.7 -fun tac_from_prog _ thy (Const ("Prog_Tac.Rewrite", _) $ thmID $ _) =
2.8 +fun tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID $ _) =
2.9 let
2.10 val tid = HOLogic.dest_string thmID
2.11 in (Tactic.Rewrite (tid, ThmC.thm_from_thy thy tid)) end
2.12 - | tac_from_prog _ thy (Const ("Prog_Tac.Rewrite_Inst", _) $ sub $ thmID $ _) =
2.13 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ sub $ thmID $ _) =
2.14 let
2.15 val tid = HOLogic.dest_string thmID
2.16 in (Tactic.Rewrite_Inst (Subst.program_to_input sub, (tid, ThmC.thm_from_thy thy tid))) end
2.17 - | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite_Set",_) $ rls $ _) =
2.18 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls $ _) =
2.19 (Tactic.Rewrite_Set (HOLogic.dest_string rls))
2.20 - | tac_from_prog _ _ (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ sub $ rls $ _) =
2.21 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ sub $ rls $ _) =
2.22 (Tactic.Rewrite_Set_Inst (Subst.program_to_input sub, HOLogic.dest_string rls))
2.23 - | tac_from_prog _ _ (Const ("Prog_Tac.Calculate", _) $ op_ $ _) =
2.24 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>, _) $ op_ $ _) =
2.25 (Tactic.Calculate (HOLogic.dest_string op_))
2.26 - | tac_from_prog _ _ (Const ("Prog_Tac.Take", _) $ t) = (Tactic.Take (UnparseC.term t))
2.27 - | tac_from_prog _ _ (Const ("Prog_Tac.Substitute", _) $ isasub $ _) =
2.28 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ t) = (Tactic.Take (UnparseC.term t))
2.29 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ isasub $ _) =
2.30 (Tactic.Substitute ((Subst.eqs_to_input o TermC.isalist2list) isasub))
2.31 - | tac_from_prog _ thy (Const("Prog_Tac.Check_elementwise", _) $ _ $
2.32 + | tac_from_prog _ thy (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>, _) $ _ $
2.33 (Const (\<^const_name>\<open>Collect\<close>, _) $ Abs (_, _, pred))) =
2.34 (Tactic.Check_elementwise (UnparseC.term_in_thy thy pred))
2.35 - | tac_from_prog _ _ (Const("Prog_Tac.Or_to_List", _) $ _ ) = Tactic.Or_to_List
2.36 - | tac_from_prog pt _ (ptac as Const ("Prog_Tac.SubProblem", _) $ _ $ _) =
2.37 + | tac_from_prog _ _ (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _ ) = Tactic.Or_to_List
2.38 + | tac_from_prog pt _ (ptac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _) =
2.39 fst (Sub_Problem.tac_from_prog pt ptac) (*might involve problem refinement etc*)
2.40 | tac_from_prog _ thy t = raise ERROR ("stac2tac_ TODO: no match for " ^ UnparseC.term_in_thy thy t);
2.41
2.42 @@ -114,13 +114,13 @@
2.43 fun associate _ ctxt (m as Tactic.Rewrite_Inst'
2.44 (_, _, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
2.45 (case stac of
2.46 - (Const ("Prog_Tac.Rewrite_Inst", _) $ _ $ thmID_ $ f_) =>
2.47 + (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>, _) $ _ $ thmID_ $ f_) =>
2.48 if thmID = HOLogic.dest_string thmID_ then
2.49 if f = f_ then
2.50 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.51 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
2.52 else Not_Associated
2.53 - | (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ rls_ $ f_) =>
2.54 + | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ rls_ $ f_) =>
2.55 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
2.56 if f = f_ then
2.57 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.58 @@ -129,13 +129,13 @@
2.59 | _ => Not_Associated)
2.60 | associate _ ctxt (m as Tactic.Rewrite' (_, _, _, _, thm'' as (thmID, _), f, (f', asms')), stac) =
2.61 (case stac of
2.62 - (Const ("Prog_Tac.Rewrite", _) $ thmID_ $ f_) =>
2.63 + (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>, _) $ thmID_ $ f_) =>
2.64 if thmID = HOLogic.dest_string thmID_ then
2.65 if f = f_ then
2.66 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.67 else Ass_Weak (m, f', ContextC.insert_assumptions asms' ctxt)
2.68 else Not_Associated
2.69 - | (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_) =>
2.70 + | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_) =>
2.71 if Rule_Set.contains (Rule.Thm thm'') (assoc_rls (HOLogic.dest_string rls_)) then
2.72 if f = f_ then
2.73 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.74 @@ -143,14 +143,14 @@
2.75 else Not_Associated
2.76 | _ => Not_Associated)
2.77 | associate _ ctxt (m as Tactic.Rewrite_Set_Inst' (_, _, _, rls, f, (f', asms')),
2.78 - (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ _ $ rls_ $ f_)) =
2.79 + (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_)) =
2.80 if Rule_Set.id rls = HOLogic.dest_string rls_ then
2.81 if f = f_ then
2.82 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.83 else Ass_Weak (m ,f', ContextC.insert_assumptions asms' ctxt)
2.84 else Not_Associated
2.85 | associate _ ctxt (m as Tactic.Rewrite_Set' (_, _, rls, f, (f', asms')),
2.86 - (Const ("Prog_Tac.Rewrite_Set", _) $ rls_ $ f_)) =
2.87 + (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>, _) $ rls_ $ f_)) =
2.88 if Rule_Set.id rls = HOLogic.dest_string rls_ then
2.89 if f = f_ then
2.90 Associated (m, f', ContextC.insert_assumptions asms' ctxt)
2.91 @@ -158,30 +158,30 @@
2.92 else Not_Associated
2.93 | associate _ ctxt (m as Tactic.Calculate' (_, op_, f, (f', _)), stac) =
2.94 (case stac of
2.95 - (Const ("Prog_Tac.Calculate",_) $ op__ $ f_) =>
2.96 + (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op__ $ f_) =>
2.97 if op_ = HOLogic.dest_string op__ then
2.98 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
2.99 else Not_Associated
2.100 - | (Const ("Prog_Tac.Rewrite_Set_Inst", _) $ _ $ rls_ $ f_) =>
2.101 + | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>, _) $ _ $ rls_ $ f_) =>
2.102 if Rule_Set.contains (Rule.Eval (assoc_calc' (ThyC.get_theory "Isac_Knowledge")
2.103 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
2.104 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
2.105 else Not_Associated
2.106 - | (Const ("Prog_Tac.Rewrite_Set",_) $ rls_ $ f_) =>
2.107 + | (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ rls_ $ f_) =>
2.108 if Rule_Set.contains (Rule.Eval (assoc_calc' ( ThyC.get_theory "Isac_Knowledge")
2.109 op_ |> snd)) (assoc_rls (HOLogic.dest_string rls_)) then
2.110 if f = f_ then Associated (m, f', ctxt) else Ass_Weak (m ,f', ctxt)
2.111 else Not_Associated
2.112 | _ => Not_Associated)
2.113 | associate _ ctxt (m as Tactic.Check_elementwise' (consts, _, (consts_chkd, _)),
2.114 - (Const ("Prog_Tac.Check_elementwise",_) $ consts' $ _)) =
2.115 + (Const (\<^const_name>\<open>Prog_Tac.Check_elementwise\<close>,_) $ consts' $ _)) =
2.116 if consts = consts' then Associated (m, consts_chkd, ctxt) else Not_Associated
2.117 - | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const ("Prog_Tac.Or_to_List", _) $ _)) =
2.118 + | associate _ ctxt (m as Tactic.Or_to_List' (_, list), (Const (\<^const_name>\<open>Prog_Tac.Or_to_List\<close>, _) $ _)) =
2.119 Associated (m, list, ctxt)
2.120 - | associate _ ctxt (m as Tactic.Take' term, (Const ("Prog_Tac.Take", _) $ _)) =
2.121 + | associate _ ctxt (m as Tactic.Take' term, (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
2.122 Associated (m, term, ctxt)
2.123 | associate _ ctxt (m as Tactic.Substitute' (ro, erls, subte, f, f'),
2.124 - (Const ("Prog_Tac.Substitute", _) $ _ $ t)) =
2.125 + (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>, _) $ _ $ t)) =
2.126 if f = t then
2.127 Associated (m, f', ctxt)
2.128 else (*compare | applicable_in (p,p_) pt (m as Substitute sube)*)
2.129 @@ -197,7 +197,7 @@
2.130 SOME (t', _) => Associated (Tactic.Substitute' (ro, erls, subte, t, t'), t', ctxt)
2.131 | NONE => raise ERROR "associate: Substitute' not applicable to val of Expr")
2.132 | associate pt ctxt (Tactic.Subproblem' ((domID, pblID, _), _, _, _, _, _),
2.133 - (stac as Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
2.134 + (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
2.135 (case Sub_Problem.tac_from_prog pt stac of
2.136 (_, tac as Tactic.Subproblem' ((dI, pI, _), _, _, _, _, f)) =>
2.137 if domID = dI andalso pblID = pI then Associated (tac, f, ctxt) else Not_Associated
3.1 --- a/src/Tools/isac/Interpret/lucas-interpreter.sml Sun Jul 18 21:19:25 2021 +0200
3.2 +++ b/src/Tools/isac/Interpret/lucas-interpreter.sml Mon Jul 19 15:34:54 2021 +0200
3.3 @@ -76,7 +76,7 @@
3.4 | t => raise ERROR ("scan_up1..\"HOL.Let $ _\" with: \"" ^ UnparseC.term t ^ "\"")
3.5 fun check_Seq_up ({path, ...}: pstate) prog =
3.6 case TermC.sub_at (drop_last path) prog of
3.7 - Const ("Tactical.Chain",_) $ _ $ e2=> e2
3.8 + Const (\<^const_name>\<open>Tactical.Chain\<close>,_) $ _ $ e2=> e2
3.9 | t => raise ERROR ("scan_up1..\"Tactical.Chain $ _\" with: \"" ^ UnparseC.term t ^ "\"")
3.10
3.11
3.12 @@ -124,25 +124,25 @@
3.13 (3) scan_up resumes according to the interpreter-state.
3.14 Call of (2) means that there was an applicable Prog_Tac below = before.
3.15 *)
3.16 -fun scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*1*), _) $ e $ a) =
3.17 +fun scan_dn cc (ist as {act_arg, ...}) (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ e $ a) =
3.18 (case scan_dn cc (ist|> path_down_form ([L, R], a)) e of
3.19 Reject_Tac => Term_Val act_arg
3.20 | (*Accept_Tac*) goback => goback)
3.21 - | scan_dn cc (ist as {act_arg, ...}) (Const ("Tactical.Try"(*2*), _) $ e) =
3.22 + | scan_dn cc (ist as {act_arg, ...}) (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e) =
3.23 (case scan_dn cc (ist |> path_down [R]) e of
3.24 Reject_Tac => Term_Val act_arg
3.25 | (*Accept_Tac*) goback => goback)
3.26
3.27 - | scan_dn cc ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
3.28 + | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
3.29 scan_dn cc (ist |> path_down_form ([L, R], a)) e
3.30 - | scan_dn cc ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
3.31 + | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
3.32 scan_dn cc (ist |> path_down [R]) e
3.33
3.34 - | scan_dn cc ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
3.35 + | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a) =
3.36 (case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
3.37 Term_Val v => scan_dn cc (ist |> path_down_form ([L, R], a) |> set_act v) e2
3.38 | (*Accept_Tac*) goback => goback)
3.39 - | scan_dn cc ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
3.40 + | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2) =
3.41 (case scan_dn cc (ist |> path_down [L, R]) e1 of
3.42 Term_Val v => scan_dn cc (ist |> path_down [R] |> set_act v) e2
3.43 | (*Accept_Tac*) goback => goback)
3.44 @@ -152,25 +152,25 @@
3.45 Term_Val res => scan_dn cc (ist |> path_down [R, D] |> upd_env'' (Free (i, T), res)) b
3.46 | (*Accept_Tac*) goback => goback)
3.47
3.48 - | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
3.49 + | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ a) =
3.50 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
3.51 then scan_dn cc (ist |> path_down_form ([L, R], a)) e
3.52 else Term_Val act_arg
3.53 - | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const ("Tactical.While"(*2*), _) $ c $ e) =
3.54 + | scan_dn (cc as (_, ctxt)) (ist as {eval, act_arg, ...}) (Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
3.55 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.56 then scan_dn cc (ist |> path_down [R]) e
3.57 else Term_Val act_arg
3.58
3.59 - |scan_dn cc ist (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
3.60 + |scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $e1 $ e2 $ a) =
3.61 (case scan_dn cc (ist |> path_down_form ([L, L, R], a)) e1 of
3.62 Accept_Tac lme => Accept_Tac lme
3.63 | _ => scan_dn cc (ist |> path_down_form ([L, R], a)) e2)
3.64 - | scan_dn cc ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
3.65 + | scan_dn cc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $e1 $ e2) =
3.66 (case scan_dn cc (ist |> path_down [L, R]) e1 of
3.67 Accept_Tac lme => Accept_Tac lme
3.68 | _ => scan_dn cc (ist |> path_down [R]) e2)
3.69
3.70 - | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const ("Tactical.If"(*1*), _) $ c $ e1 $ e2) =
3.71 + | scan_dn (cc as (_, ctxt)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ c $ e1 $ e2) =
3.72 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.73 then scan_dn cc (ist |> path_down [L, R]) e1
3.74 else scan_dn cc (ist |> path_down [R]) e2
3.75 @@ -191,23 +191,23 @@
3.76 else raise ERROR "LItool.find_next_step without result"
3.77 else scan_up pcc (ist |> path_up) (go_up path sc)
3.78 (* scan is strictly to R, because at L there was an \<open>expr_val\<close> *)
3.79 -and scan_up pcc ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up pcc ist
3.80 - | scan_up pcc ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up pcc ist
3.81 +and scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ $ _) = go_scan_up pcc ist
3.82 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _) = go_scan_up pcc ist
3.83
3.84 - | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*1*), _) $ e $ _) =
3.85 + | scan_up (pcc as (_, cc)) ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ _) =
3.86 (case scan_dn cc (ist |> path_down [L, R]) e of
3.87 Accept_Tac ict => Accept_Tac ict
3.88 | Reject_Tac => go_scan_up pcc ist
3.89 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
3.90 - | scan_up (pcc as (_, cc)) ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
3.91 + | scan_up (pcc as (_, cc)) ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
3.92 (case scan_dn cc (ist |> path_down [R]) e of
3.93 Accept_Tac ict => Accept_Tac ict
3.94 | Reject_Tac => go_scan_up pcc ist
3.95 | Term_Val v => go_scan_up pcc (ist |> set_act v |> set_found))
3.96
3.97 - | scan_up pcc ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.98 - | scan_up pcc ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up pcc ist
3.99 - | scan_up (pcc as (sc, cc)) ist (Const ("Tactical.Chain"(*3*), _) $ _) =
3.100 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.101 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _) = go_scan_up pcc ist
3.102 + | scan_up (pcc as (sc, cc)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _) =
3.103 let
3.104 val e2 = check_Seq_up ist sc
3.105 in
3.106 @@ -230,7 +230,7 @@
3.107 | scan_up pcc ist (Const (\<^const_name>\<open>Let\<close>(*3*), _) $ _ $ (Abs _)) = go_scan_up pcc ist
3.108
3.109 | scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
3.110 - (Const ("Tactical.While"(*1*), _) $ c $ e $ _) =
3.111 + (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ _) =
3.112 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.113 then
3.114 case scan_dn cc (ist |> path_down [L, R]) e of
3.115 @@ -240,7 +240,7 @@
3.116 else
3.117 go_scan_up pcc (ist (*|> set_found*))
3.118 | scan_up (pcc as (_, cc as (_, ctxt))) (ist as {eval, ...})
3.119 - (Const ("Tactical.While"(*2*), _) $ c $ e) =
3.120 + (Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
3.121 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.122 then
3.123 case scan_dn cc (ist |> path_down [R]) e of
3.124 @@ -250,11 +250,11 @@
3.125 else
3.126 go_scan_up pcc ist
3.127
3.128 - | scan_up pcc ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.129 - | scan_up pcc ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up pcc ist
3.130 - | scan_up pcc ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up pcc ist
3.131 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.132 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up pcc ist
3.133 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*3*), _) $ _ ) = go_scan_up pcc ist
3.134
3.135 - | scan_up pcc ist (Const ("Tactical.If"(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.136 + | scan_up pcc ist (Const (\<^const_name>\<open>Tactical.If\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up pcc ist
3.137
3.138 | scan_up _ _ t = raise ERROR ("scan_up not impl for " ^ UnparseC.term t)
3.139
3.140 @@ -327,23 +327,23 @@
3.141 (** scan to a Prog_Tac **)
3.142
3.143 (* scan is strictly first L, then R; tacticals have 2 args at maximum *)
3.144 -fun scan_dn1 cct ist (Const ("Tactical.Try"(*1*), _) $ e $ a) =
3.145 +fun scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ e $ a) =
3.146 (case scan_dn1 cct (ist |> path_down_form ([L, R], a)) e of goback => goback)
3.147 - | scan_dn1 cct ist (Const ("Tactical.Try"(*2*), _) $ e) =
3.148 + | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ e) =
3.149 (case scan_dn1 cct (ist |> path_down [R]) e of goback => goback)
3.150
3.151 - | scan_dn1 cct ist (Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
3.152 + | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
3.153 scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
3.154 - | scan_dn1 cct ist (Const ("Tactical.Repeat"(*2*), _) $ e) =
3.155 + | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
3.156 scan_dn1 cct (ist |> path_down [R]) e
3.157
3.158 - | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*1*), _) $ e1 $ e2 $ a) =
3.159 + | scan_dn1 (cct as (cstate, _, _)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ e1 $ e2 $ a) =
3.160 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a)) e1 of
3.161 Term_Val1 v => scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v)) e2
3.162 | Reject_Tac1 (ist', ctxt', tac') => scan_dn1 (cstate, ctxt', tac') (ist
3.163 |> path_down_form ([L, R], a) |> trans_env_act ist') e2
3.164 | goback => goback)
3.165 - | scan_dn1 (cct as (cstate, _, _)) ist (Const ("Tactical.Chain"(*2*), _) $ e1 $ e2) =
3.166 + | scan_dn1 (cct as (cstate, _, _)) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ e1 $ e2) =
3.167 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
3.168 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
3.169 | Reject_Tac1 (ist', ctxt', tac') =>
3.170 @@ -359,17 +359,17 @@
3.171 | goback => goback)
3.172
3.173 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
3.174 - (Const ("Tactical.While"(*1*), _) $ c $ e $ a) =
3.175 + (Const (\<^const_name>\<open>Tactical.While\<close>(*1*), _) $ c $ e $ a) =
3.176 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (ist |> get_act_env |> Env.update' a) c)
3.177 then scan_dn1 cct (ist |> path_down_form ([L, R], a)) e
3.178 else Term_Val1 act_arg
3.179 | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, act_arg, ...})
3.180 - (Const ("Tactical.While"(*2*),_) $ c $ e) =
3.181 + (Const (\<^const_name>\<open>Tactical.While\<close>(*2*),_) $ c $ e) =
3.182 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.183 then scan_dn1 cct (ist |> path_down [R]) e
3.184 else Term_Val1 act_arg
3.185
3.186 - | scan_dn1 cct (ist as {or = ORundef, ...}) (Const ("Tactical.Or"(*1*), _) $e1 $ e2 $ a) =
3.187 + | scan_dn1 cct (ist as {or = ORundef, ...}) (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $e1 $ e2 $ a) =
3.188 (case scan_dn1 cct (ist |> path_down_form ([L, L, R], a) |> set_or AssOnly) e1 of
3.189 Term_Val1 v =>
3.190 (case scan_dn1 cct (ist |> path_down [L, R] |> set_subst' (a, v) |> set_or AssOnly) e2 of
3.191 @@ -381,12 +381,12 @@
3.192 | goback => goback)
3.193 | Reject_Tac1 _ => raise ERROR ("scan_dn1 Tactical.Or(*1*): must not return Reject_Tac1")
3.194 | goback => goback)
3.195 - | scan_dn1 cct ist (Const ("Tactical.Or"(*2*), _) $e1 $ e2) =
3.196 + | scan_dn1 cct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $e1 $ e2) =
3.197 (case scan_dn1 cct (ist |> path_down [L, R]) e1 of
3.198 Term_Val1 v => scan_dn1 cct (ist |> path_down [R] |> set_act v) e2
3.199 | goback => goback)
3.200
3.201 - | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const ("Tactical.If", _) $ c $ e1 $ e2) =
3.202 + | scan_dn1 (cct as (_, ctxt, _)) (ist as {eval, ...}) (Const (\<^const_name>\<open>Tactical.If\<close>, _) $ c $ e1 $ e2) =
3.203 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.204 then scan_dn1 cct (ist |> path_down [L, R]) e1
3.205 else scan_dn1 cct (ist |> path_down [R]) e2
3.206 @@ -406,24 +406,24 @@
3.207 scan_up1 pcct (ist |> path_up) (TermC.sub_at (path_up' path) prog)
3.208 else Term_Val1 act_arg
3.209 (* scan is strictly to R, because at L there was a expr_val *)
3.210 -and scan_up1 pcct ist (Const ("Tactical.Try"(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
3.211 - | scan_up1 pcct ist (Const ("Tactical.Try"(*2*), _) $ _) = go_scan_up1 pcct ist
3.212 +and scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*1*), _) $ _ $ _) = go_scan_up1 pcct ist
3.213 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Try\<close>(*2*), _) $ _) = go_scan_up1 pcct ist
3.214
3.215 - | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*1*), _) $ e $ a) =
3.216 + | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const (\<^const_name>\<open>Tactical.Repeat\<close>(*1*), _) $ e $ a) =
3.217 (case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
3.218 Term_Val1 v => go_scan_up1 pcct (ist |> set_act v |> set_form a)
3.219 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
3.220 | goback => goback)
3.221 - | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const ("Tactical.Repeat"(*2*), _) $ e) =
3.222 + | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (t as Const (\<^const_name>\<open>Tactical.Repeat\<close>(*2*), _) $ e) =
3.223 (case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
3.224 Term_Val1 v' => go_scan_up1 pcct (ist |> set_act v')
3.225 | Reject_Tac1 (ist', ctxt', tac') => scan_up1 (prog, (cstate, ctxt', tac')) ist' t
3.226 | goback => goback)
3.227
3.228 (*all has been done in (*2*) below*)
3.229 - | scan_up1 pcct ist (Const ("Tactical.Chain"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.230 - | scan_up1 pcct ist (Const ("Tactical.Chain"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
3.231 - | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const ("Tactical.Chain"(*3*), _) $ _ ) =
3.232 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.233 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist (*comes from e2*)
3.234 + | scan_up1 (pcct as (prog, cct as (cstate, _, _))) ist (Const (\<^const_name>\<open>Tactical.Chain\<close>(*3*), _) $ _ ) =
3.235 let
3.236 val e2 = check_Seq_up ist prog (*comes from e1, goes to e2*)
3.237 in
3.238 @@ -445,7 +445,7 @@
3.239 | scan_up1 pcct ist (Const (\<^const_name>\<open>Let\<close>(*3*), _) $ _ $ (Abs _)) = go_scan_up1 pcct ist
3.240
3.241 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
3.242 - (t as Const ("Tactical.While"(*1*),_) $ c $ e $ a) =
3.243 + (t as Const (\<^const_name>\<open>Tactical.While\<close>(*1*),_) $ c $ e $ a) =
3.244 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update' a (get_act_env ist)) c)
3.245 then
3.246 case scan_dn1 cct (ist |> path_down_form ([L, R], a) |> set_or ORundef) e of
3.247 @@ -455,7 +455,7 @@
3.248 | goback => goback
3.249 else go_scan_up1 pcct (ist |> set_form a)
3.250 | scan_up1 (pcct as (prog, cct as (cstate, ctxt, _))) (ist as {eval, ...})
3.251 - (t as Const ("Tactical.While"(*2*), _) $ c $ e) =
3.252 + (t as Const (\<^const_name>\<open>Tactical.While\<close>(*2*), _) $ c $ e) =
3.253 if Rewrite.eval_true_ (Proof_Context.theory_of ctxt) eval (subst_atomic (Env.update_opt' (get_subst ist)) c)
3.254 then
3.255 case scan_dn1 cct (ist |> path_down [R] |> set_or ORundef) e of
3.256 @@ -464,13 +464,13 @@
3.257 | goback => goback
3.258 else go_scan_up1 pcct ist
3.259
3.260 - | scan_up1 pcct ist (Const ("If", _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.261 + | scan_up1 pcct ist (Const ("If"(*TOODOO*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.262
3.263 - | scan_up1 pcct ist (Const ("Tactical.Or"(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.264 - | scan_up1 pcct ist (Const ("Tactical.Or"(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
3.265 - | scan_up1 pcct ist (Const ("Tactical.Or"(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
3.266 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*1*), _) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.267 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*2*), _) $ _ $ _) = go_scan_up1 pcct ist
3.268 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.Or\<close>(*3*), _) $ _ ) = go_scan_up1 pcct (ist |> path_up)
3.269
3.270 - | scan_up1 pcct ist (Const ("Tactical.If",_) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.271 + | scan_up1 pcct ist (Const (\<^const_name>\<open>Tactical.If\<close>,_) $ _ $ _ $ _) = go_scan_up1 pcct ist
3.272
3.273 | scan_up1 _ _ t = raise ERROR ("scan_up1 not impl for t= " ^ UnparseC.term t)
3.274
4.1 --- a/src/Tools/isac/Interpret/sub-problem.sml Sun Jul 18 21:19:25 2021 +0200
4.2 +++ b/src/Tools/isac/Interpret/sub-problem.sml Mon Jul 19 15:34:54 2021 +0200
4.3 @@ -8,7 +8,7 @@
4.4 struct
4.5 (**)
4.6
4.7 -fun tac_from_prog pt (stac as Const ("Prog_Tac.SubProblem", _) $ spec' $ ags') =
4.8 +fun tac_from_prog pt (stac as Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ spec' $ ags') =
4.9 let
4.10 val (dI, pI, mI) = Prog_Tac.dest_spec spec'
4.11 val thy = ThyC.sub_common (ThyC.get_theory dI, Ctree.rootthy pt);
5.1 --- a/src/Tools/isac/Knowledge/Diff.thy Sun Jul 18 21:19:25 2021 +0200
5.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Mon Jul 19 15:34:54 2021 +0200
5.3 @@ -96,7 +96,7 @@
5.4 | primed t = raise ERROR ("primed called with arg = '"^ UnparseC.term t ^"'");
5.5
5.6 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
5.7 -fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
5.8 +fun eval_primed _ _ (p as (Const (\<^const_name>\<open>Diff.primed\<close>,_) $ t)) _ =
5.9 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (primed t),
5.10 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
5.11 | eval_primed _ _ _ _ = NONE;
6.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Sun Jul 18 21:19:25 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Mon Jul 19 15:34:54 2021 +0200
6.3 @@ -69,7 +69,7 @@
6.4 (*("occur_exactly_in", ("EqSystem.occur_exactly_in",
6.5 eval_occur_exactly_in "#eval_occur_exactly_in_") )*)
6.6 fun eval_occur_exactly_in _ "EqSystem.occur_exactly_in"
6.7 - (p as (Const ("EqSystem.occur_exactly_in",_)
6.8 + (p as (Const (\<^const_name>\<open>EqSystem.occur_exactly_in\<close>,_)
6.9 $ vs $ all $ t)) _ =
6.10 if occur_exactly_in (TermC.isalist2list vs) (TermC.isalist2list all) t
6.11 then SOME ((UnparseC.term p) ^ " = True",
7.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Sun Jul 18 21:19:25 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Mon Jul 19 15:34:54 2021 +0200
7.3 @@ -71,7 +71,7 @@
7.4
7.5 (*WN080222
7.6 (*("new_c", ("Integrate.new_c", eval_new_c "#new_c_"))*)
7.7 -fun eval_new_c _ _ (p as (Const ("Integrate.new_c",_) $ t)) _ =
7.8 +fun eval_new_c _ _ (p as (Const (\<^const_name>\<open>Integrate.new_c\<close>,_) $ t)) _ =
7.9 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (new_c p),
7.10 Trueprop $ (mk_equality (p, new_c p)))
7.11 | eval_new_c _ _ _ _ = NONE;
7.12 @@ -93,7 +93,7 @@
7.13
7.14
7.15 (*("is_f_x", ("Integrate.is_f_x", eval_is_f_x "is_f_x_"))*)
7.16 -fun eval_is_f_x _ _(p as (Const ("Integrate.is_f_x", _)
7.17 +fun eval_is_f_x _ _(p as (Const (\<^const_name>\<open>Integrate.is_f_x\<close>, _)
7.18 $ arg)) _ =
7.19 if TermC.is_f_x arg
7.20 then SOME ((UnparseC.term p) ^ " = True",
8.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Sun Jul 18 21:19:25 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Mon Jul 19 15:34:54 2021 +0200
8.3 @@ -59,7 +59,7 @@
8.4 eval_factors_from_solution ""))
8.5 this code is limited (max 3 solutions) AND has too little checks *)
8.6 fun eval_factors_from_solution (thmid:string) _
8.7 - (t as Const ("Partial_Fractions.factors_from_solution", _) $ sol) thy =
8.8 + (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) thy =
8.9 let val prod = factors_from_solution sol
8.10 in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
8.11 HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
9.1 --- a/src/Tools/isac/Knowledge/Poly.thy Sun Jul 18 21:19:25 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Poly.thy Mon Jul 19 15:34:54 2021 +0200
9.3 @@ -199,11 +199,11 @@
9.4 if (1) then degree 0
9.5 if (2) then v is a factor on the very right, casually with exponent.*)
9.6 fun factor_right_deg (*case 2*)
9.7 - (Const ("Groups.times_class.times", _) $
9.8 - t1 $ (Const ("Transcendental.powr",_) $ vv $ num)) v =
9.9 + (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $
9.10 + t1 $ (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ vv $ num)) v =
9.11 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))
9.12 else NONE
9.13 - | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ num) v =
9.14 + | factor_right_deg (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ vv $ num) v =
9.15 if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE
9.16
9.17 | factor_right_deg (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ vv) v =
9.18 @@ -279,15 +279,15 @@
9.19
9.20 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
9.21 fun get_basStr (Const (\<^const_name>\<open>powr\<close>,_) $ Free (str, _) $ _) = str
9.22 - | get_basStr (Const ("Transcendental.powr",_) $ n $ _) = TermC.to_string n
9.23 + | get_basStr (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ n $ _) = TermC.to_string n
9.24 | get_basStr (Free (str, _)) = str
9.25 | get_basStr t =
9.26 if TermC.is_num t then TermC.to_string t
9.27 else "|||"; (* gross gewichtet; für Brüche ect. *)
9.28
9.29 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
9.30 -fun get_potStr (Const ("Transcendental.powr", _) $ Free _ $ Free (str, _)) = str
9.31 - | get_potStr (Const ("Transcendental.powr", _) $ Free _ $ t) =
9.32 +fun get_potStr (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ Free (str, _)) = str
9.33 + | get_potStr (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ t) =
9.34 if TermC.is_num t then TermC.to_string t else "|||"
9.35 | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)
9.36 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
9.37 @@ -354,11 +354,11 @@
9.38 if (is_nums x) then counter (n, xs)
9.39 else
9.40 (case x of
9.41 - (Const ("Transcendental.powr", _) $ Free _ $ t) =>
9.42 + (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ Free _ $ t) =>
9.43 if TermC.is_num t
9.44 then counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs)
9.45 else counter (n + 1000, xs) (*FIXME.MG?!*)
9.46 - | (Const ("Num.numeral_class.numeral", _) $ num) =>
9.47 + | (Const (\<^const_name>\<open>numeral\<close>, _) $ num) =>
9.48 counter (n + 1 + HOLogic.dest_numeral num, xs)
9.49 | _ => counter (n + 1, xs)) (*FIXME.MG?! ... Brüche ect.*)
9.50 (**)in(**)
9.51 @@ -575,33 +575,33 @@
9.52 this is weaker than 'is_polynomial' !.*)
9.53 fun is_polyexp (Free _) = true
9.54 | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)
9.55 - | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ num) =
9.56 + | is_polyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ num) =
9.57 if TermC.is_num num then true
9.58 else if TermC.is_variable num then true
9.59 else is_polyexp num
9.60 - | is_polyexp (Const ("Groups.plus_class.plus",_) $ num $ Free _) =
9.61 + | is_polyexp (Const (\<^const_name>\<open>plus\<close>, _) $ num $ Free _) =
9.62 if TermC.is_num num then true
9.63 else if TermC.is_variable num then true
9.64 else is_polyexp num
9.65 - | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ num) =
9.66 + | is_polyexp (Const (\<^const_name>\<open>minus\<close>, _) $ Free _ $ num) =
9.67 if TermC.is_num num then true
9.68 else if TermC.is_variable num then true
9.69 else is_polyexp num
9.70 - | is_polyexp (Const ("Groups.times_class.times",_) $ num $ Free _) =
9.71 + | is_polyexp (Const (\<^const_name>\<open>times\<close>, _) $ num $ Free _) =
9.72 if TermC.is_num num then true
9.73 else if TermC.is_variable num then true
9.74 else is_polyexp num
9.75 - | is_polyexp (Const ("Transcendental.powr",_) $ Free _ $ num) =
9.76 + | is_polyexp (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ Free _ $ num) =
9.77 if TermC.is_num num then true
9.78 else if TermC.is_variable num then true
9.79 else is_polyexp num
9.80 - | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
9.81 + | is_polyexp (Const (\<^const_name>\<open>plus_class.plus\<close>,_) $ t1 $ t2) =
9.82 ((is_polyexp t1) andalso (is_polyexp t2))
9.83 - | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
9.84 + | is_polyexp (Const (\<^const_name>\<open>Groups.minus_class.minus\<close>,_) $ t1 $ t2) =
9.85 ((is_polyexp t1) andalso (is_polyexp t2))
9.86 - | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
9.87 + | is_polyexp (Const (\<^const_name>\<open>Groups.times_class.times\<close>,_) $ t1 $ t2) =
9.88 ((is_polyexp t1) andalso (is_polyexp t2))
9.89 - | is_polyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
9.90 + | is_polyexp (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $ t1 $ t2) =
9.91 ((is_polyexp t1) andalso (is_polyexp t2))
9.92 | is_polyexp num = TermC.is_num num;
9.93 \<close>
9.94 @@ -618,7 +618,7 @@
9.95 subsection \<open>evaluations functions\<close>
9.96 subsubsection \<open>for predicates\<close>
9.97 ML \<open>
9.98 -fun eval_is_polyrat_in _ _(p as (Const ("Poly.is_polyrat_in",_) $ t $ v)) _ =
9.99 +fun eval_is_polyrat_in _ _(p as (Const (\<^const_name>\<open>Poly.is_polyrat_in\<close>, _) $ t $ v)) _ =
9.100 if is_polyrat_in t v
9.101 then SOME ((UnparseC.term p) ^ " = True",
9.102 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
9.103 @@ -628,7 +628,7 @@
9.104
9.105 (*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)
9.106 fun eval_is_expanded_in _ _
9.107 - (p as (Const ("Poly.is_expanded_in",_) $ t $ v)) _ =
9.108 + (p as (Const (\<^const_name>\<open>Poly.is_expanded_in\<close>, _) $ t $ v)) _ =
9.109 if is_expanded_in t v
9.110 then SOME ((UnparseC.term p) ^ " = True",
9.111 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
9.112 @@ -638,7 +638,7 @@
9.113
9.114 (*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)
9.115 fun eval_is_poly_in _ _
9.116 - (p as (Const ("Poly.is_poly_in",_) $ t $ v)) _ =
9.117 + (p as (Const (\<^const_name>\<open>Poly.is_poly_in\<close>, _) $ t $ v)) _ =
9.118 if is_poly_in t v
9.119 then SOME ((UnparseC.term p) ^ " = True",
9.120 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
9.121 @@ -648,7 +648,7 @@
9.122
9.123 (*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)
9.124 fun eval_has_degree_in _ _
9.125 - (p as (Const ("Poly.has_degree_in",_) $ t $ v)) _ =
9.126 + (p as (Const (\<^const_name>\<open>Poly.has_degree_in\<close>, _) $ t $ v)) _ =
9.127 let val d = has_degree_in t v
9.128 val d' = TermC.term_of_num HOLogic.realT d
9.129 in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),
9.130 @@ -658,7 +658,7 @@
9.131
9.132 (*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)
9.133 fun eval_is_polyexp (thmid:string) _
9.134 - (t as (Const("Poly.is_polyexp", _) $ arg)) thy =
9.135 + (t as (Const (\<^const_name>\<open>Poly.is_polyexp\<close>, _) $ arg)) thy =
9.136 if is_polyexp arg
9.137 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
9.138 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.139 @@ -672,7 +672,7 @@
9.140 (*WN.18.6.03 *)
9.141 (*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)
9.142 fun eval_is_addUnordered (thmid:string) _
9.143 - (t as (Const("Poly.is_addUnordered", _) $ arg)) thy =
9.144 + (t as (Const (\<^const_name>\<open>Poly.is_addUnordered\<close>, _) $ arg)) thy =
9.145 if is_addUnordered arg
9.146 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
9.147 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.148 @@ -681,7 +681,7 @@
9.149 | eval_is_addUnordered _ _ _ _ = NONE;
9.150
9.151 fun eval_is_multUnordered (thmid:string) _
9.152 - (t as (Const("Poly.is_multUnordered", _) $ arg)) thy =
9.153 + (t as (Const (\<^const_name>\<open>Poly.is_multUnordered\<close>, _) $ arg)) thy =
9.154 if is_multUnordered arg
9.155 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
9.156 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
10.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Sun Jul 18 21:19:25 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Mon Jul 19 15:34:54 2021 +0200
10.3 @@ -1169,8 +1169,8 @@
10.4 | dest_hd' _ (Abs (_, T, _)) = ((("", 0), T), 4)
10.5 | dest_hd' _ _ = raise ERROR "dest_hd': uncovered case in fun.def.";
10.6
10.7 -fun size_of_term' x (Const ("Transcendental.powr",_) $
10.8 - Free (var, _) $ Const ("Num.numeral_class.numeral", _) $ pot) =
10.9 +fun size_of_term' x (Const (\<^const_name>\<open>Transcendental.powr\<close>,_) $
10.10 + Free (var, _) $ Const (\<^const_name>\<open>numeral\<close>, _) $ pot) =
10.11 (case x of (*WN*)
10.12 (Free (xstr, _)) =>
10.13 (if xstr = var then 1000 * (HOLogic.dest_numeral pot) else 3)
11.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Sun Jul 18 21:19:25 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Mon Jul 19 15:34:54 2021 +0200
11.3 @@ -113,20 +113,20 @@
11.4 fun identifier (Free (id, _)) = id (* //2, a *)
11.5 (*TOODOO*)
11.6 | identifier (* 3*a*b *)
11.7 - (Const ("Groups.times_class.times", _) $ (Const ("Groups.times_class.times", _) $
11.8 + (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $
11.9 num $ t) $ Free (id, _)) =
11.10 if TermC.is_num num andalso TermC.is_atom t then id
11.11 else "|||||||||||||"
11.12
11.13 | identifier (* 2*a, a*b *)
11.14 - (Const ("Groups.times_class.times", _) $ num $ Free (id, _)) =
11.15 + (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ num $ Free (id, _)) =
11.16 if TermC.is_atom num then id
11.17 else "|||||||||||||"
11.18 | identifier _ = "|||||||||||||"(*the "largest" string*);
11.19
11.20 (*("kleiner", ("PolyMinus.kleiner", eval_kleiner ""))*)
11.21 (* order "by alphabet" w.r.t. var: num < (var | num*var) > (var*var | ..) *)
11.22 -fun eval_kleiner _ _ (p as (Const ("PolyMinus.kleiner",_) $ a $ b)) _ =
11.23 +fun eval_kleiner _ _ (p as (Const (\<^const_name>\<open>PolyMinus.kleiner\<close>,_) $ a $ b)) _ =
11.24 if TermC.is_num b then
11.25 if TermC.is_num a then (*123 kleiner 32 = True !!!*)
11.26 if TermC.num_of_term a < TermC.num_of_term b then
11.27 @@ -149,15 +149,15 @@
11.28 if TermC.is_atom t then true
11.29 else
11.30 case t of
11.31 - Const ("Groups.times_class.times", _) $ t1 $ t2 =>
11.32 + Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $ t1 $ t2 =>
11.33 ist_monom t1 andalso ist_monom t2
11.34 - | Const ("Transcendental.powr", _) $ t1 $ t2 =>
11.35 + | Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ t1 $ t2 =>
11.36 ist_monom t1 andalso ist_monom t2
11.37 | _ => false
11.38
11.39 (* is this a univariate monomial ? *)
11.40 (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
11.41 -fun eval_ist_monom _ _ (p as (Const ("PolyMinus.ist_monom",_) $ a)) _ =
11.42 +fun eval_ist_monom _ _ (p as (Const (\<^const_name>\<open>PolyMinus.ist_monom\<close>,_) $ a)) _ =
11.43 if ist_monom a then
11.44 SOME ((UnparseC.term p) ^ " = True",
11.45 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
12.1 --- a/src/Tools/isac/Knowledge/RatEq.thy Sun Jul 18 21:19:25 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/RatEq.thy Mon Jul 19 15:34:54 2021 +0200
12.3 @@ -67,7 +67,7 @@
12.4
12.5 subsection \<open>evaluations functions\<close>
12.6 ML \<open>
12.7 -fun eval_is_ratequation_in _ _ (p as (Const ("RatEq.is_ratequation_in",_) $ t $ v)) _ =
12.8 +fun eval_is_ratequation_in _ _ (p as (Const (\<^const_name>\<open>RatEq.is_ratequation_in\<close>, _) $ t $ v)) _ =
12.9 if is_rateqation_in t v
12.10 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
12.11 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
13.1 --- a/src/Tools/isac/Knowledge/Rational.thy Sun Jul 18 21:19:25 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Jul 19 15:34:54 2021 +0200
13.3 @@ -41,7 +41,7 @@
13.4
13.5 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
13.6 fun eval_is_ratpolyexp (thmid:string) _
13.7 - (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
13.8 + (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
13.9 if is_ratpolyexp arg
13.10 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
13.11 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
13.12 @@ -51,7 +51,7 @@
13.13
13.14 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
13.15 fun eval_get_denominator (thmid:string) _
13.16 - (t as Const ("Rational.get_denominator", _) $
13.17 + (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
13.18 (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
13.19 denom)) thy =
13.20 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "",
13.21 @@ -60,7 +60,7 @@
13.22
13.23 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
13.24 fun eval_get_numerator (thmid:string) _
13.25 - (t as Const ("Rational.get_numerator", _) $
13.26 + (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
13.27 (Const (\<^const_name>\<open>divide\<close>, _) $num
13.28 $denom )) thy =
13.29 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
13.30 @@ -123,17 +123,17 @@
13.31 ML \<open>
13.32 fun monom_of_term vs (c, es) (t as Const _) =
13.33 (c, list_update es (find_index (curry op = t) vs) 1)
13.34 - | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
13.35 + | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
13.36 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
13.37 - | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
13.38 + | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
13.39 (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
13.40 | monom_of_term vs (c, es) (t as Free _) =
13.41 (c, list_update es (find_index (curry op = t) vs) 1)
13.42 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
13.43 - (e as Const ("Num.numeral_class.numeral", _) $ _)) =
13.44 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
13.45 + (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
13.46 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
13.47 - | monom_of_term vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
13.48 - (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
13.49 + | monom_of_term vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
13.50 + (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
13.51 (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
13.52
13.53 | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
13.54 @@ -144,9 +144,9 @@
13.55 (*-------v------*)
13.56 fun monoms_of_term vs (t as Const _) =
13.57 [monom_of_term vs (1, replicate (length vs) 0) t]
13.58 - | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
13.59 + | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
13.60 [monom_of_term vs (1, replicate (length vs) 0) t]
13.61 - | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
13.62 + | monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
13.63 [monom_of_term vs (1, replicate (length vs) 0) t]
13.64 | monoms_of_term vs (t as Free _) =
13.65 [monom_of_term vs (1, replicate (length vs) 0) t]
13.66 @@ -191,7 +191,7 @@
13.67 | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
13.68 | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
13.69 | term_of_es baseT expT (v :: vs) (e :: es) =
13.70 - Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
13.71 + Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
13.72 :: term_of_es baseT expT vs es
13.73 | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
13.74
13.75 @@ -215,8 +215,8 @@
13.76 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
13.77 ML \<open>
13.78 fun mk_noteq_0 baseT t =
13.79 - Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $
13.80 - (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
13.81 + Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $
13.82 + (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
13.83
13.84 fun mk_asms baseT ts =
13.85 let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
13.86 @@ -464,7 +464,7 @@
13.87
13.88 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
13.89 fun eval_is_expanded (thmid:string) _
13.90 - (t as (Const("Rational.is_expanded", _) $ arg)) thy =
13.91 + (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy =
13.92 if is_expanded arg
13.93 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
13.94 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
14.1 --- a/src/Tools/isac/Knowledge/Root.thy Sun Jul 18 21:19:25 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/Root.thy Mon Jul 19 15:34:54 2021 +0200
14.3 @@ -46,7 +46,7 @@
14.4 (*evaluation square-root over the integers*)
14.5 fun eval_sqrt (_ : string) (_ : string) (t as (Const (op0, _) $ arg)) _(*thy*) =
14.6 (case arg of
14.7 - (Const ("Num.numeral_class.numeral", T) $ num) =>
14.8 + (Const (\<^const_name>\<open>numeral\<close>, T) $ num) =>
14.9 let val ni = HOLogic.dest_numeral num
14.10 in
14.11 if ni < 0 then NONE
15.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Sun Jul 18 21:19:25 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Mon Jul 19 15:34:54 2021 +0200
15.3 @@ -112,7 +112,7 @@
15.4 let
15.5 fun findroot (t as (_ $ _ $ _ $ _)) _ = raise TERM ( "is_rootTerm_in", [t])
15.6 (* at the moment there is no term like this, but ....*)
15.7 - | findroot (Const ("Root.nroot",_) $ _ $ t3) v = Prog_Expr.occurs_in v t3
15.8 + | findroot (Const (\<^const_name>\<open>nroot\<close>, _) $ _ $ t3) v = Prog_Expr.occurs_in v t3
15.9 | findroot (_ $ t2 $ t3) v = findroot t2 v orelse findroot t3 v
15.10 | findroot (Const (\<^const_name>\<open>sqrt\<close>, _) $ t2) v = Prog_Expr.occurs_in v t2
15.11 | findroot (_ $ t2) v = findroot t2 v
15.12 @@ -151,19 +151,19 @@
15.13 isnorm t v
15.14 end;
15.15
15.16 -fun eval_is_rootTerm_in _ _ (p as (Const ("RootEq.is_rootTerm_in",_) $ t $ v)) _ =
15.17 +fun eval_is_rootTerm_in _ _ (p as (Const (\<^const_name>\<open>RootEq.is_rootTerm_in\<close>,_) $ t $ v)) _ =
15.18 if is_rootTerm_in t v
15.19 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
15.20 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
15.21 | eval_is_rootTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
15.22
15.23 -fun eval_is_sqrtTerm_in _ _ (p as (Const ("RootEq.is_sqrtTerm_in",_) $ t $ v)) _ =
15.24 +fun eval_is_sqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_sqrtTerm_in\<close>,_) $ t $ v)) _ =
15.25 if is_sqrtTerm_in t v
15.26 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
15.27 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
15.28 | eval_is_sqrtTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
15.29
15.30 -fun eval_is_normSqrtTerm_in _ _ (p as (Const ("RootEq.is_normSqrtTerm_in",_) $ t $ v)) _ =
15.31 +fun eval_is_normSqrtTerm_in _ _ (p as (Const (\<^const_name>\<open>is_normSqrtTerm_in\<close>,_) $ t $ v)) _ =
15.32 if is_normSqrtTerm_in t v
15.33 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
15.34 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
16.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy Sun Jul 18 21:19:25 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy Mon Jul 19 15:34:54 2021 +0200
16.3 @@ -55,7 +55,7 @@
16.4 findrootrat t v
16.5 end;
16.6
16.7 -fun eval_is_rootRatAddTerm_in _ _ (p as (Const ("RootRatEq.is_rootRatAddTerm_in",_) $ t $ v)) _ =
16.8 +fun eval_is_rootRatAddTerm_in _ _ (p as (Const (\<^const_name>\<open>is_rootRatAddTerm_in\<close>,_) $ t $ v)) _ =
16.9 if is_rootRatAddTerm_in t v
16.10 then SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
16.11 else SOME ((UnparseC.term p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
17.1 --- a/src/Tools/isac/Knowledge/Test.thy Sun Jul 18 21:19:25 2021 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Test.thy Mon Jul 19 15:34:54 2021 +0200
17.3 @@ -56,10 +56,10 @@
17.4 fun atom (Const (_, Type (_,[]))) = true
17.5 | atom (Free (_, Type (_,[]))) = true
17.6 | atom (Var (_, Type (_,[]))) = true
17.7 - | atom((Const ("Bin.integ_of_bin",_)) $ _) = true
17.8 + | atom((Const ("Bin.integ_of_bin", _)) $ _) = true
17.9 | atom _ = false;
17.10
17.11 -fun varids (Const ("Num.numeral_class.numeral", _) $ _) = []
17.12 +fun varids (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = []
17.13 | varids (Const (s, Type (_,[]))) = [strip_thy s]
17.14 | varids (Free (s, Type (_,[]))) = [strip_thy s]
17.15 | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
17.16 @@ -253,7 +253,7 @@
17.17
17.18 (*does a term contain a root ?*)
17.19 fun eval_contains_root (thmid:string) _
17.20 - (t as (Const("Test.contains_root", _) $ arg)) thy =
17.21 + (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) thy =
17.22 if member op = (ids_of arg) "sqrt"
17.23 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
17.24 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
17.25 @@ -262,13 +262,13 @@
17.26 | eval_contains_root _ _ _ _ = NONE;
17.27
17.28 (*dummy precondition for root-met of x+1=2*)
17.29 -fun eval_precond_rootmet (thmid:string) _ (t as (Const ("Test.precond_rootmet", _) $ arg)) thy =
17.30 +fun eval_precond_rootmet (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)) thy =
17.31 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
17.32 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
17.33 | eval_precond_rootmet _ _ _ _ = NONE;
17.34
17.35 (*dummy precondition for root-pbl of x+1=2*)
17.36 -fun eval_precond_rootpbl (thmid:string) _ (t as (Const ("Test.precond_rootpbl", _) $ arg)) thy =
17.37 +fun eval_precond_rootpbl (thmid:string) _ (t as (Const (\<^const_name>\<open>Test.precond_rootpbl\<close>, _) $ arg)) thy =
17.38 SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
17.39 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
17.40 | eval_precond_rootpbl _ _ _ _ = NONE;
18.1 --- a/src/Tools/isac/ProgLang/Auto_Prog.thy Sun Jul 18 21:19:25 2021 +0200
18.2 +++ b/src/Tools/isac/ProgLang/Auto_Prog.thy Mon Jul 19 15:34:54 2021 +0200
18.3 @@ -74,28 +74,28 @@
18.4 fun stacpbls (_ $ body) =
18.5 let
18.6 fun scan (Const (\<^const_name>\<open>Let\<close>, _) $ e $ (Abs (_, _, b))) = (scan e) @ (scan b)
18.7 - | scan (Const ("Tactical.If", _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
18.8 - | scan (Const ("Tactical.While", _) $ _ $ e $ _) = scan e
18.9 - | scan (Const ("Tactical.While", _) $ _ $ e) = scan e
18.10 - | scan (Const ("Tactical.Repeat", _) $ e $ _) = scan e
18.11 - | scan (Const ("Tactical.Repeat", _) $ e) = scan e
18.12 - | scan (Const ("Tactical.Try", _) $ e $ _) = scan e
18.13 - | scan (Const ("Tactical.Try", _) $ e) = scan e
18.14 - | scan (Const ("Tactical.Or", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
18.15 - | scan (Const ("Tactical.Or", _) $ e1 $ e2) = (scan e1) @ (scan e2)
18.16 - | scan (Const ("Tactical.Chain", _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
18.17 - | scan (Const ("Tactical.Chain", _) $ e1 $ e2) = (scan e1) @ (scan e2)
18.18 + | scan (Const (\<^const_name>\<open>Tactical.If\<close>, _) $ _ $ e1 $ e2) = (scan e1) @ (scan e2)
18.19 + | scan (Const (\<^const_name>\<open>Tactical.While\<close>, _) $ _ $ e $ _) = scan e
18.20 + | scan (Const (\<^const_name>\<open>Tactical.While\<close>, _) $ _ $ e) = scan e
18.21 + | scan (Const (\<^const_name>\<open>Tactical.Repeat\<close>, _) $ e $ _) = scan e
18.22 + | scan (Const (\<^const_name>\<open>Tactical.Repeat\<close>, _) $ e) = scan e
18.23 + | scan (Const (\<^const_name>\<open>Tactical.Try\<close>, _) $ e $ _) = scan e
18.24 + | scan (Const (\<^const_name>\<open>Tactical.Try\<close>, _) $ e) = scan e
18.25 + | scan (Const (\<^const_name>\<open>Tactical.Or\<close>, _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
18.26 + | scan (Const (\<^const_name>\<open>Tactical.Or\<close>, _) $ e1 $ e2) = (scan e1) @ (scan e2)
18.27 + | scan (Const (\<^const_name>\<open>Tactical.Chain\<close>, _) $ e1 $ e2 $ _) = (scan e1) @ (scan e2)
18.28 + | scan (Const (\<^const_name>\<open>Tactical.Chain\<close>, _) $ e1 $ e2) = (scan e1) @ (scan e2)
18.29 | scan t = case Prog_Tac.eval_leaf [] NONE TermC.empty t of
18.30 (Program.Tac _, _) => [t] | (Program.Expr _, _) => []
18.31 in ((distinct op =) o scan) body end
18.32 | stacpbls t = raise ERROR ("fun stacpbls not applicable to '" ^ UnparseC.term t ^ "'")
18.33
18.34 (* get operators out of a program *)
18.35 -fun is_calc (Const ("Prog_Tac.Calculate",_) $ _) = true
18.36 - | is_calc (Const ("Prog_Tac.Calculate",_) $ _ $ _) = true
18.37 +fun is_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _) = true
18.38 + | is_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ _) = true
18.39 | is_calc _ = false;
18.40 -fun op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_) = HOLogic.dest_string op_
18.41 - | op_of_calc (Const ("Prog_Tac.Calculate",_) $ op_ $ _) = HOLogic.dest_string op_
18.42 +fun op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_) = HOLogic.dest_string op_
18.43 + | op_of_calc (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ op_ $ _) = HOLogic.dest_string op_
18.44 | op_of_calc t = raise ERROR ("op_of_calc called with " ^ UnparseC.term t);
18.45 fun get_calcs thy sc =
18.46 sc
19.1 --- a/src/Tools/isac/ProgLang/Isabelle-isac-conflicts Sun Jul 18 21:19:25 2021 +0200
19.2 +++ b/src/Tools/isac/ProgLang/Isabelle-isac-conflicts Mon Jul 19 15:34:54 2021 +0200
19.3 @@ -8,8 +8,8 @@
19.4 (2) numerals in (terms and) thms are stored differently:
19.5 string Isabelle term isac term
19.6 123 Bin.... Free("123",_)
19.7 - 0 Const("0",_) Free("0",_)
19.8 - 0 Const("1",_) Free("1",_)
19.9 + 0 Const ("0",_) Free("0",_)
19.10 + 0 Const ("1",_) Free("1",_)
19.11
19.12 (3) overwritteln functions
19.13 find_first see isac/ROOT.ML
20.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Jul 18 21:19:25 2021 +0200
20.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Mon Jul 19 15:34:54 2021 +0200
20.3 @@ -124,7 +124,7 @@
20.4
20.5 (*. evaluate the predicate matches (match on whole term only) .*)
20.6 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
20.7 -fun eval_matches (_:string) "Prog_Expr.matches" (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy =
20.8 +fun eval_matches (_:string) "Prog_Expr.matches" (t as Const (\<^const_name>\<open>Prog_Expr.matches\<close>, _) $ pat $ tst) thy =
20.9 if TermC.matches thy tst pat
20.10 then
20.11 let
20.12 @@ -204,7 +204,7 @@
20.13
20.14 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
20.15 fun eval_matchsub (_:string) "Prog_Expr.matchsub"
20.16 - (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy =
20.17 + (t as Const (\<^const_name>\<open>Prog_Expr.matchsub\<close>, _) $ pat $ tst) thy =
20.18 if matchsub thy tst pat
20.19 then
20.20 let val prop = HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True}))
20.21 @@ -227,7 +227,7 @@
20.22 fun lhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _) = l
20.23 | lhs t = raise ERROR("lhs called with (" ^ UnparseC.term t ^ ")");
20.24 (*("lhs" ,("Prog_Expr.lhs" , eval_lhs "")):calc*)
20.25 -fun eval_lhs _ "Prog_Expr.lhs" (t as (Const ("Prog_Expr.lhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
20.26 +fun eval_lhs _ "Prog_Expr.lhs" (t as (Const (\<^const_name>\<open>lhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ l $ _))) _ =
20.27 SOME ((UnparseC.term t) ^ " = " ^ (UnparseC.term l),
20.28 HOLogic.Trueprop $ (TermC.mk_equality (t, l)))
20.29 | eval_lhs _ _ _ _ = NONE;
20.30 @@ -242,7 +242,7 @@
20.31 fun rhs (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r) = r
20.32 | rhs t = raise ERROR("rhs called with (" ^ UnparseC.term t ^ ")");
20.33 (*("rhs" ,("Prog_Expr.rhs" , eval_rhs "")):calc*)
20.34 -fun eval_rhs _ "Prog_Expr.rhs" (t as (Const ("Prog_Expr.rhs",_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
20.35 +fun eval_rhs _ "Prog_Expr.rhs" (t as (Const (\<^const_name>\<open>rhs\<close>,_) $ (Const (\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ r))) _ =
20.36 SOME (UnparseC.term t ^ " = " ^ UnparseC.term r,
20.37 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
20.38 | eval_rhs _ _ _ _ = NONE;
20.39 @@ -252,7 +252,7 @@
20.40 fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
20.41
20.42 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
20.43 -fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const ("Prog_Expr.occurs_in",_) $ v $ t)) _ =
20.44 +fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
20.45 ((*tracing("#>@ eval_occurs_in: v= "^(UnparseC.term v));
20.46 tracing("#>@ eval_occurs_in: t= "^(UnparseC.term t));*)
20.47 if occurs_in v t
20.48 @@ -270,7 +270,7 @@
20.49 (*("some_occur_in", ("Prog_Expr.some_occur_in",
20.50 eval_some_occur_in "#eval_some_occur_in_"))*)
20.51 fun eval_some_occur_in _ "Prog_Expr.some_occur_in"
20.52 - (p as (Const ("Prog_Expr.some_occur_in",_) $ vs $ t)) _ =
20.53 + (p as (Const (\<^const_name>\<open>some_occur_in\<close>,_) $ vs $ t)) _ =
20.54 if some_occur_in (TermC.isalist2list vs) t
20.55 then SOME ((UnparseC.term p) ^ " = True",
20.56 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
20.57 @@ -305,14 +305,14 @@
20.58 | eval_is_even _ _ _ _ = NONE;
20.59
20.60 (*("is_const",("Prog_Expr.is_const", Prog_Expr.eval_const "#is_const_"))*)
20.61 -fun eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const ("Partial_Fractions.AA", _))) _ =
20.62 +fun eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const ("Partial_Fractions.AA", _))) _ =
20.63 (*TODO get rid of this special case*)
20.64 SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
20.65 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
20.66 - | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ Const _)) _ =
20.67 + | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ Const _)) _ =
20.68 SOME (TermC.mk_thmid thmid (UnparseC.term t) "",
20.69 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
20.70 - | eval_const thmid _ (t as (Const ("Prog_Expr.is_const", _) $ n)) _ =
20.71 + | eval_const thmid _ (t as (Const (\<^const_name>\<open>is_const\<close>, _) $ n)) _ =
20.72 if TermC.is_num n
20.73 then SOME (TermC.mk_thmid thmid (TermC.string_of_num n) "",
20.74 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
21.1 --- a/src/Tools/isac/ProgLang/Prog_Tac.thy Sun Jul 18 21:19:25 2021 +0200
21.2 +++ b/src/Tools/isac/ProgLang/Prog_Tac.thy Mon Jul 19 15:34:54 2021 +0200
21.3 @@ -1,6 +1,8 @@
21.4 (* Title: tactics, tacticals etc. for scripts
21.5 Author: Walther Neuper 000224
21.6 (c) due to copyright terms
21.7 +
21.8 +TOODOO: rearrange thy dependency such that "Tactical.Chain" etc are known const_name
21.9 *)
21.10
21.11 theory Prog_Tac
21.12 @@ -84,34 +86,34 @@
21.13 (case get_t e1 a of NONE => get_t e2 a | la => la)
21.14 | get_t (Const ("Tactical.Try",_) $ e) a = get_t e a
21.15 | get_t (Const ("Tactical.Try",_) $ e $ a) _ = get_t e a
21.16 - | get_t (Const ("Tactical.Repeat",_) $ e) a = get_t e a
21.17 + | get_t (Const ("Tactical.Repeat", _) $ e) a = get_t e a
21.18 | get_t (Const ("Tactical.Repeat",_) $ e $ a) _ = get_t e a
21.19 | get_t (Const ("Tactical.Or",_) $e1 $ e2) a =
21.20 (case get_t e1 a of NONE => get_t e2 a | la => la)
21.21 | get_t (Const ("Tactical.Or",_) $e1 $ e2 $ a) _ =
21.22 (case get_t e1 a of NONE => get_t e2 a | la => la)
21.23 | get_t (Const ("Tactical.While",_) $ _ $ e) a = get_t e a
21.24 - | get_t (Const ("Tactical.While",_) $ _ $ e $ a) _ = get_t e a
21.25 - | get_t (Const ("Tactical.Letpar",_) $ e1 $ Abs (_, _, e2)) a =
21.26 + | get_t (Const ("Tactical.While", _) $ _ $ e $ a) _ = get_t e a
21.27 + | get_t (Const ("Tactical.Letpar", _) $ e1 $ Abs (_, _, e2)) a =
21.28 (case get_t e1 a of NONE => get_t e2 a | la => la)
21.29 - | get_t (Const (\<^const_name>\<open>Let\<close>,_) $ e1 $ Abs (_, _, _)) a =
21.30 + | get_t (Const (\<^const_name>\<open>Let\<close>, _) $ e1 $ Abs (_, _, _)) a =
21.31 get_t e1 a (* don't go deeper without evaluation *)
21.32 | get_t (Const ("If", _) $ _ $ _ $ _) _ = NONE
21.33
21.34 - | get_t (Const ("Prog_Tac.Rewrite",_) $ _ $ a) _ = SOME a
21.35 - | get_t (Const ("Prog_Tac.Rewrite",_) $ _ ) a = SOME a
21.36 - | get_t (Const ("Prog_Tac.Rewrite_Inst",_) $ _ $ _ $ a) _ = SOME a
21.37 - | get_t (Const ("Prog_Tac.Rewrite_Inst",_) $ _ $ _ ) a = SOME a
21.38 - | get_t (Const ("Prog_Tac.Rewrite_Set",_) $ _ $ a) _ = SOME a
21.39 - | get_t (Const ("Prog_Tac.Rewrite_Set",_) $ _ ) a = SOME a
21.40 - | get_t (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ _ $a)_ =SOME a
21.41 - | get_t (Const ("Prog_Tac.Rewrite_Set_Inst",_) $ _ $ _ ) a =SOME a
21.42 - | get_t (Const ("Prog_Tac.Calculate",_) $ _ $ a) _ = SOME a
21.43 - | get_t (Const ("Prog_Tac.Calculate",_) $ _ ) a = SOME a
21.44 - | get_t (Const ("Prog_Tac.Substitute",_) $ _ $ a) _ = SOME a
21.45 - | get_t (Const ("Prog_Tac.Substitute",_) $ _ ) a = SOME a
21.46 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ $ a) _ = SOME a
21.47 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite\<close>,_) $ _ ) a = SOME a
21.48 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ $ a) _ = SOME a
21.49 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Inst\<close>,_) $ _ $ _ ) a = SOME a
21.50 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ $ a) _ = SOME a
21.51 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set\<close>,_) $ _ ) a = SOME a
21.52 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ $a)_ =SOME a
21.53 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Rewrite_Set_Inst\<close>,_) $ _ $ _ ) a =SOME a
21.54 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ $ a) _ = SOME a
21.55 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Calculate\<close>,_) $ _ ) a = SOME a
21.56 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ $ a) _ = SOME a
21.57 + | get_t (Const (\<^const_name>\<open>Prog_Tac.Substitute\<close>,_) $ _ ) a = SOME a
21.58
21.59 - | get_t (Const ("Prog_Tac.SubProblem",_) $ _ $ _) _ = NONE
21.60 + | get_t (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>,_) $ _ $ _) _ = NONE
21.61
21.62 | get_t _ _ = ((*tracing ("### get_t yac: list-expr "^(term2str x));*) NONE)
21.63 in get_t body TermC.empty end
21.64 @@ -172,9 +174,9 @@
21.65 case a of SOME a' => subst_atomic E (t $ a')
21.66 | NONE => ((subst_atomic E t) $ v)),
21.67 a)
21.68 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.SubProblem", _) $ _ $ _)) =
21.69 + | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.SubProblem\<close>, _) $ _ $ _)) =
21.70 (Program.Tac (subst_atomic E t), NONE)
21.71 - | eval_leaf E _ _ (t as (Const ("Prog_Tac.Take", _) $ _)) =
21.72 + | eval_leaf E _ _ (t as (Const (\<^const_name>\<open>Prog_Tac.Take\<close>, _) $ _)) =
21.73 (Program.Tac (subst_atomic E t), NONE)
21.74 | eval_leaf E _ _ (t as (Const ("Prog_Tac.Substitute"(*1*), _) $ _ $ _)) =
21.75 (Program.Tac (subst_atomic E t), NONE)
22.1 --- a/src/Tools/isac/ProgLang/evaluate.sml Sun Jul 18 21:19:25 2021 +0200
22.2 +++ b/src/Tools/isac/ProgLang/evaluate.sml Mon Jul 19 15:34:54 2021 +0200
22.3 @@ -227,10 +227,10 @@
22.4 (*** handle numerals in eval_binop ***)
22.5
22.6 (* preliminary HACK *)
22.7 -fun int_of_numeral (Const ("Groups.zero_class.zero", _)) = 0
22.8 - | int_of_numeral (Const ("Groups.one_class.one", _)) = 1
22.9 - | int_of_numeral (Const ("Groups.uminus_class.uminus", _) $ t) = ~1 * int_of_numeral t
22.10 - | int_of_numeral (Const ("Num.numeral_class.numeral", _) $ n) = HOLogic.dest_numeral n
22.11 +fun int_of_numeral (Const (\<^const_name>\<open>zero_class.zero\<close>, _)) = 0
22.12 + | int_of_numeral (Const (\<^const_name>\<open>one_class.one\<close>, _)) = 1
22.13 + | int_of_numeral (Const (\<^const_name>\<open>uminus\<close>, _) $ t) = ~1 * int_of_numeral t
22.14 + | int_of_numeral (Const (\<^const_name>\<open>numeral\<close>, _) $ n) = HOLogic.dest_numeral n
22.15 | int_of_numeral t = raise TERM ("int_of_numeral", [t]);
22.16
22.17 fun calcul op_ (t1, t2) =
23.1 --- a/src/Tools/isac/Specify/i-model.sml Sun Jul 18 21:19:25 2021 +0200
23.2 +++ b/src/Tools/isac/Specify/i-model.sml Mon Jul 19 15:34:54 2021 +0200
23.3 @@ -157,7 +157,7 @@
23.4 [] => raise ERROR ("penv_value: no values in '" ^ UnparseC.term id)
23.5 | [v] => (id, v)
23.6 | (v1 :: v2 :: _) => (case v1 of
23.7 - Const ("Program.Arbfix",_) => (id, v2)
23.8 + Const (\<^const_name>\<open>Program.Arbfix\<close>, _) => (id, v2)
23.9 | _ => (id, v1));
23.10
23.11 (* find the variant with most items already input *)
24.1 --- a/test/Tools/isac/BaseDefinitions/termC.sml Sun Jul 18 21:19:25 2021 +0200
24.2 +++ b/test/Tools/isac/BaseDefinitions/termC.sml Mon Jul 19 15:34:54 2021 +0200
24.3 @@ -570,7 +570,7 @@
24.4 then () else error "TermC.scala_of_term aaa::real";
24.5
24.6 val t = @{term "aaa + bbb"};
24.7 -if TermC.scala_of_term t = "App(App(Const(\"Groups.plus_class.plus\", Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), TFree(\"'a\", List(\"Groups.plus\"))))))), Free(\"aaa\", TFree(\"'a\", List(\"Groups.plus\")))), Free(\"bbb\", TFree(\"'a\", List(\"Groups.plus\"))))"
24.8 +if TermC.scala_of_term t = "App(App(Const (\"Groups.plus_class.plus\", Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), Type(\"fun\", List(TFree(\"'a\", List(\"Groups.plus\")), TFree(\"'a\", List(\"Groups.plus\"))))))), Free(\"aaa\", TFree(\"'a\", List(\"Groups.plus\")))), Free(\"bbb\", TFree(\"'a\", List(\"Groups.plus\"))))"
24.9 then () else error "TermC.scala_of_term aaa + bbb";
24.10
24.11 "----------- fun TermC.contains_Var ------------------------------------------------------------------";