1.1 --- a/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Wed Feb 08 08:59:37 2023 +0100
1.2 +++ b/src/Tools/isac/BaseDefinitions/BaseDefinitions.thy Sun Feb 12 12:44:25 2023 +0100
1.3 @@ -56,25 +56,14 @@
1.4 apply (simp_all add: realpow_def even_real_def odd_real_def inv_real_eq)
1.5 by (simp add: powr_minus_divide)
1.6
1.7 +ML_file thmC.sml
1.8 ML_file termC.sml
1.9 ML_file substitution.sml
1.10 ML_file contextC.sml
1.11 ML_file environment.sml
1.12
1.13 ML \<open>
1.14 -open ThyC
1.15 \<close> ML \<open>
1.16 -cut_longid "Simplify.assoc"
1.17 -\<close> ML \<open>
1.18 -fun strip_thy str =
1.19 - let fun strip bdVar [] = implode (rev bdVar)
1.20 - | strip bdVar ("." :: _) = implode (rev bdVar)
1.21 - | strip bdVar (c :: cs) = strip (bdVar @ [c]) cs
1.22 - in strip [] (rev (Symbol.explode str)) end;
1.23 -\<close> ML \<open>
1.24 -strip_thy "Simplify.assoc"
1.25 -\<close> ML \<open>
1.26 -strip_thy: string -> string
1.27 \<close> ML \<open>
1.28 \<close>
1.29 end
2.1 --- a/src/Tools/isac/BaseDefinitions/libraryC.sml Wed Feb 08 08:59:37 2023 +0100
2.2 +++ b/src/Tools/isac/BaseDefinitions/libraryC.sml Sun Feb 12 12:44:25 2023 +0100
2.3 @@ -68,7 +68,10 @@
2.4 val strs2str': string list -> string
2.5 val strs2str_: string list -> string (* duplicates in Rule *)
2.6 val strslist2strs: string list list -> string
2.7 +(*///------------------------------>>> Subst ----------------------------------------------\\\*)
2.8 type subst = (term * term) list
2.9 + val subs2str: string list -> string (*? type input ?*)
2.10 +(*\\\------------------------------>>> Subst ----------------------------------------------///*)
2.11
2.12 val take: int * 'a list -> 'a list (*conflict with Library.take: int -> 'a list -> 'a list *)
2.13 val take_fromto: int -> int -> 'a list -> 'a list
2.14 @@ -82,19 +85,12 @@
2.15
2.16 val linefeed: string -> string
2.17 val dropwhile' : ('a -> 'b -> bool) -> 'a list -> 'b list -> 'a list * 'b list
2.18 +
2.19 \<^isac_test>\<open>
2.20 val enumerate_strings: string list -> string list
2.21 val quad2pair: 'a * 'b * 'c * 'd -> 'a * 'b
2.22 \<close>
2.23
2.24 -(*///------------------------------>>> thy ------------------------------------------------\\\*)
2.25 - val strip_thy: string -> string
2.26 -(*\\\------------------------------>>> thy ------------------------------------------------///*)
2.27 -(*///------------------------------>>> term -----------------------------------------------\\\*)
2.28 - val subs2str: string list -> string
2.29 - val id_of: term -> string
2.30 - val ids_of: term -> string list
2.31 -(*\\\------------------------------>>> term -----------------------------------------------///*)
2.32 end;
2.33
2.34 (**)
2.35 @@ -169,7 +165,6 @@
2.36 val nos = space_implode "#";
2.37 fun strs2str_ strl = "#" ^ (nos strl) ^ "#";
2.38 fun strslist2strs strslist = map strs2str strslist |> strs2str';
2.39 -type subst = (term * term) list;
2.40
2.41 fun spair2str (s1, s2) = "(" ^ quote s1 ^ ", " ^ quote s2 ^ ")";
2.42 fun pair2str_ (s1, s2) = s1 ^ "#" ^ s2;
2.43 @@ -251,33 +246,13 @@
2.44 | aaa xys (x :: xs) (y :: ys) = aaa (xys @ [(x, y)]) xs ys
2.45 in aaa [] xs ys end;
2.46
2.47 -(*///------------------------------>>> thy ------------------------------------------------\\\*)
2.48 -fun strip_thy str =
2.49 - let fun strip bdVar [] = implode (rev bdVar)
2.50 - | strip bdVar ("." :: _) = implode (rev bdVar)
2.51 - | strip bdVar (c :: cs) = strip (bdVar @ [c]) cs
2.52 - in strip [] (rev (Symbol.explode str)) end;
2.53 -(*\\\------------------------------>>> thy ------------------------------------------------///*)
2.54 -
2.55 -(*///------------------------------>>> term ----------------------------------------------\\\*)
2.56 -fun id_of (Var ((id,ix),_)) = if ix=0 then id else id^(string_of_int ix)
2.57 - | id_of (Free (id ,_)) = id
2.58 - | id_of (Const(id ,_)) = id
2.59 - | id_of _ = ""; (* never such an identifier *)
2.60 -
2.61 -fun ids_of t =
2.62 - let fun con ss (Const (s,_)) = s::ss
2.63 - | con ss (Free (s,_)) = s::ss
2.64 - | con ss (Abs (s,_,b)) = s::(con ss b)
2.65 - | con ss (t1 $ t2) = (con ss t1) @ (con ss t2)
2.66 - | con ss _ = ss
2.67 - in map strip_thy (((distinct op =) o (con [])) t) end;
2.68 -
2.69 +(*///------------------------------>>> Subst ----------------------------------------------\\\*)
2.70 +type subst = (term * term) list;
2.71 fun subs2str (subs: string list) = list2str subs;
2.72 (*> val sss = ["(''bdv'',x)", "(err,#0)"];
2.73 > subs2str sss;
2.74 val it = "[(bdv,x),(err,#0)]" : string*)
2.75 -(*\\\------------------------------>>> term ----------------------------------------------///*)
2.76 +(*\\\------------------------------>>> Subst ----------------------------------------------///*)
2.77
2.78 fun termless tu = (Term_Ord.term_ord tu = LESS);
2.79
3.1 --- a/src/Tools/isac/BaseDefinitions/termC.sml Wed Feb 08 08:59:37 2023 +0100
3.2 +++ b/src/Tools/isac/BaseDefinitions/termC.sml Sun Feb 12 12:44:25 2023 +0100
3.3 @@ -21,8 +21,16 @@
3.4 val contains_Var: term -> bool
3.5 val dest_binop_typ: typ -> typ * typ * typ
3.6 val dest_equals: term -> term * term
3.7 +
3.8 + type id
3.9 + val cut_longid: string -> id
3.10 val free2str: term -> string
3.11 - val ids2str: term -> string list
3.12 + val str_of_free_opt: term -> string option
3.13 + val str_of_int: int -> string
3.14 + val id_of: term -> string
3.15 + val ids_of: term -> string list
3.16 + val ids2str: term -> string list (*double?*)
3.17 +
3.18 val ins_concl: term -> term -> term
3.19 val inst_abs: term -> term
3.20 val inst_bdv: LibraryC.subst -> term -> term
3.21 @@ -72,8 +80,6 @@
3.22
3.23 val matches: theory -> term -> term -> bool
3.24
3.25 - val str_of_free_opt: term -> string option
3.26 - val str_of_int: int -> string
3.27 val strip_imp_prems': term -> term option
3.28 val subst_atomic_all: LibraryC.subst -> term -> bool * term
3.29
3.30 @@ -339,10 +345,24 @@
3.31 (* this shall be improved due to future requirements *)
3.32 fun guess_bdv_typ t = t |> vars |> hd |> type_of
3.33
3.34 +type id = string (*the shortest significant*)
3.35 +val cut_longid = ThmC.cut_longid
3.36 fun free2str (Free (s, _)) = s
3.37 | free2str t = raise TERM ("free2str not for ", [t]);
3.38 fun str_of_free_opt (Free (s, _)) = SOME s
3.39 | str_of_free_opt _ = NONE
3.40 +fun id_of (Var ((id,ix),_)) = if ix= 0 then id else id ^ string_of_int ix
3.41 + | id_of (Free (id ,_)) = id
3.42 + | id_of (Const(id ,_)) = id
3.43 + | id_of _ = ""; (* never such an identifier *)
3.44 +
3.45 +fun ids_of t =
3.46 + let fun con ss (Const (s,_)) = s::ss
3.47 + | con ss (Free (s,_)) = s::ss
3.48 + | con ss (Abs (s,_,b)) = s::(con ss b)
3.49 + | con ss (t1 $ t2) = (con ss t1) @ (con ss t2)
3.50 + | con ss _ = ss
3.51 + in map cut_longid (((distinct op =) o (con [])) t) end;
3.52
3.53 (* compare Logic.unvarify_global, which rejects Free *)
3.54 fun var2free (t as Const _) = t
3.55 @@ -468,7 +488,7 @@
3.56 fun mk_num_op_num T1 T2 (op_, Top) n1 n2 =
3.57 Const (op_, Top) $ HOLogic.mk_number T1 n1 $ HOLogic.mk_number T2 n2;
3.58 fun mk_thmid thmid n1 n2 =
3.59 - thmid ^ (strip_thy n1) ^ "_" ^ (strip_thy n2);
3.60 + thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
3.61 fun mk_add t1 t2 =
3.62 let
3.63 val (T1, T2) = (type_of t1, type_of t2)
3.64 @@ -543,7 +563,7 @@
3.65
3.66 fun var_for vs (t as Const (str, _)) id =
3.67 if is_num t then vs
3.68 - else if id = strip_thy str then t :: vs else vs
3.69 + else if id = cut_longid str then t :: vs else vs
3.70 | var_for vs (t as Free (str, _)) id = if id = str then t :: vs else vs
3.71 | var_for vs (t as Var (idn, _)) id = if id = Term.string_of_vname idn then t :: vs else vs
3.72 | var_for vs (Bound _) _ = vs
3.73 @@ -557,7 +577,7 @@
3.74 (* treat Free, Const, Var as vars_of in polynomials *)
3.75 fun vars_of t =
3.76 let
3.77 - val var_ids = t |> ids2str |> subtract op = poly_consts |> map strip_thy |> sort string_ord
3.78 + val var_ids = t |> ids2str |> subtract op = poly_consts |> map cut_longid |> sort string_ord
3.79 in (map (var_for [] t) var_ids) |> flat |> distinct op = end
3.80
3.81 (* this may decompose an object-language isa-list;
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Tools/isac/BaseDefinitions/thmC.sml Sun Feb 12 12:44:25 2023 +0100
4.3 @@ -0,0 +1,205 @@
4.4 +(* Title: BaseDefinitions/thmC.sml
4.5 + Author: Walther Neuper
4.6 + (c) due to copyright terms
4.7 +
4.8 +This structure could be dropped due to improved reflection in Isabelle;
4.9 +but ThmC.sym_thm requires still an identifying string thm_id.
4.10 +*)
4.11 +signature THEOREM_ISAC =
4.12 +sig
4.13 + type T = ThmC_Def.T
4.14 + type id = ThmC_Def.id (* shortest possible *)
4.15 + type long_id (* e.g. "Test.radd_left_commute"*)
4.16 +
4.17 + val cut_longid: string -> id
4.18 + val long_id: T -> long_id
4.19 +
4.20 + val string_of_thm: Proof.context -> thm -> string
4.21 + val string_of_thms: Proof.context -> thm list -> string
4.22 +
4.23 + val id_of_thm: thm -> id
4.24 + val of_thm: thm -> T
4.25 + val from_rule : Proof.context -> Rule.rule -> T
4.26 + val member': id list -> Rule.rule -> bool
4.27 +
4.28 + val is_sym: id -> bool
4.29 + val thm_from_thy: theory -> id -> thm
4.30 +
4.31 + val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule
4.32 + val make_sym_rule: Proof.context -> Rule.rule -> Rule.rule
4.33 + val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
4.34 + val sym_thm: thm -> thm
4.35 +
4.36 +\<^isac_test>\<open>
4.37 + val dest_eq_concl: thm -> term * term
4.38 + val string_of_thm_in_thy: theory -> thm -> string
4.39 + val id_drop_sym: id -> id
4.40 + val revert_sym_rule: theory -> Rule.rule -> Rule.rule
4.41 +\<close>
4.42 +end
4.43 +
4.44 +(**)
4.45 +structure ThmC(**): THEOREM_ISAC(**) =
4.46 +struct
4.47 +(**)
4.48 +
4.49 +(** types and conversions **)
4.50 +
4.51 +type T = ThmC_Def.T;
4.52 +type id = ThmC_Def.id;
4.53 +type long_id = string;
4.54 +
4.55 +fun long_id (thmID, _) =
4.56 + thmID
4.57 + |> Global_Theory.get_thm (Know_Store.get_via_last_thy "Isac_Knowledge")
4.58 + |> Thm.get_name_hint
4.59 +fun cut_longid "" = "" (* case required in fun eval_* *)
4.60 + | cut_longid dn = last_elem (space_explode "." dn); (*the cut_longid is the key into Know_Store*)
4.61 +
4.62 +val string_of_thm = ThmC_Def.string_of_thm;
4.63 +val string_of_thms = ThmC_Def.string_of_thms;
4.64 +
4.65 +fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_longid;
4.66 +fun of_thm thm = (id_of_thm thm, thm);
4.67 +fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
4.68 + | from_rule ctxt r =
4.69 + raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r);
4.70 +
4.71 +\<^isac_test>\<open>
4.72 +fun string_of_thm_in_thy thy thm =
4.73 + UnparseC.term (Proof_Context.init_global thy) (Thm.prop_of thm);
4.74 +\<close>
4.75 +fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
4.76 + handle ERROR _ => false
4.77 +
4.78 +
4.79 +(** handle symmetric equalities, generated by deriving input terms **)
4.80 +
4.81 +fun is_sym id =
4.82 + case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
4.83 + | _ => false;
4.84 +
4.85 +\<^isac_test>\<open>
4.86 +fun id_drop_sym id =
4.87 + case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
4.88 + | _ => id
4.89 +\<close>
4.90 +
4.91 +(* get the theorem associated with the xstring-identifier;
4.92 + if the identifier starts with "sym_" then swap "lhs = rhs" around "=";
4.93 + in case identifiers starting with "#" come from Eval and
4.94 + get an ad-hoc theorem (containing numerals only) -- rejected here
4.95 +*)
4.96 +fun thm_from_thy thy thmid =
4.97 + case Symbol.explode thmid of
4.98 + "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
4.99 + raise ERROR ("thm_from_thy not impl.for " ^ thmid)
4.100 + | "s" :: "y" :: "m" :: "_" :: id =>
4.101 + ((Global_Theory.get_thm thy) (implode id)) RS sym
4.102 + | "#" :: _ =>
4.103 + raise ERROR ("thm_from_thy not impl.for " ^ thmid)
4.104 + | _ =>
4.105 + thmid |> Global_Theory.get_thm thy
4.106 +
4.107 +fun dest_eq_concl thm =
4.108 + (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
4.109 + NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm])
4.110 + | SOME eq => eq);
4.111 +
4.112 +(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
4.113 +(*NB: careful instantiation avoids shifting of schematic variables*)
4.114 +fun sym_thm thm =
4.115 + let
4.116 + val thy = Thm.theory_of_thm thm;
4.117 + val certT = Thm.global_ctyp_of thy;
4.118 + val cert = Thm.global_cterm_of thy;
4.119 +
4.120 + val (lhs, rhs) = dest_eq_concl thm |> apply2 cert;
4.121 + val A = Thm.typ_of_cterm lhs;
4.122 +
4.123 + val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
4.124 + val (t, s) = dest_eq_concl sym_rule;
4.125 +
4.126 + val instT = TVars.map (K (K A)) (TVars.build (TVars.add_tvars t));
4.127 + val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, Vars.empty));
4.128 +
4.129 + val cinstT = TVars.map (K certT) instT;
4.130 + val cinst = Vars.make [(s', lhs), (t', rhs)];
4.131 + in
4.132 + thm
4.133 + |> Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule)
4.134 + |> Thm.put_name_hint (Thm.get_name_hint thm)
4.135 + end;
4.136 +
4.137 +fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
4.138 + | make_sym_rule_set (Rule_Def.Repeat {id, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =
4.139 + Rule_Def.Repeat {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls,
4.140 + rules = rules, rew_ord = rew_ord, preconds = preconds}
4.141 + | make_sym_rule_set (Rule_Set.Sequence {id, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =
4.142 + Rule_Set.Sequence {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls,
4.143 + rules = rules, rew_ord = rew_ord, preconds = preconds}
4.144 + | make_sym_rule_set (Rule_Set.Rrls {id, program, calc, errpatts, asm_rls, prepat, rew_ord}) =
4.145 + Rule_Set.Rrls {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls,
4.146 + prepat = prepat, rew_ord = rew_ord}
4.147 +
4.148 +(* toggles sym_* and keeps "#:" for ad-hoc theorems *)
4.149 +fun make_sym_rule ctxt (Rule.Thm (thmID, thm)) =
4.150 + let
4.151 + val thm' = sym_thm thm
4.152 + val thmID' = case Symbol.explode thmID of
4.153 + "s" :: "y" :: "m" :: "_" :: id => implode id
4.154 + | "#" :: ":" :: _ => "#: " ^ string_of_thm ctxt thm'
4.155 + | _ => "sym_" ^ thmID
4.156 + in Rule.Thm (thmID', thm') end
4.157 + | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
4.158 + | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string ctxt r)
4.159 +
4.160 +\<^isac_test>\<open>
4.161 +(* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
4.162 +fun revert_sym_rule thy (Rule.Thm (id, thm)) =
4.163 + (*this ^^ might come from the user, who doesn't care about thy*)
4.164 + if is_sym (cut_longid id)
4.165 + then
4.166 + let
4.167 + val id' = id_drop_sym id
4.168 + val thm' = thm_from_thy thy id'
4.169 + val id'' = Thm.get_name_hint thm' (*recover the thy the thm comes from*)
4.170 + in Rule.Thm (id'', thm') end
4.171 + else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
4.172 + | revert_sym_rule thy rule =
4.173 + raise ERROR ("ThmC.revert_sym_rule: NOT for " ^
4.174 + Rule.to_string (Proof_Context.init_global thy) rule)
4.175 +\<close>
4.176 +
4.177 +
4.178 +(* ML antiquotations *)
4.179 +
4.180 +val sym_prefix = "sym_";
4.181 +
4.182 +fun make_rule ctxt symmetric (xname, pos) =
4.183 + let
4.184 + val _ =
4.185 + if String.isPrefix sym_prefix xname
4.186 + then error ("Bad theorem name with sym-prefix " ^ quote xname ^ Position.here pos) else ();
4.187 +
4.188 + val context = Context.Proof ctxt;
4.189 + val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
4.190 + val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos);
4.191 + val thm =
4.192 + if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
4.193 + else Facts.the_single (name, pos) thms;
4.194 + val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
4.195 + in Rule.Thm (xname', thm') end;
4.196 +
4.197 +fun antiquotation binding sym =
4.198 + ML_Antiquotation.value_embedded binding
4.199 + (Scan.lift Parse.embedded_position >> (fn name =>
4.200 + "ThmC.make_rule ML_context " ^ Bool.toString sym ^
4.201 + ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position name));
4.202 +
4.203 +val _ =
4.204 + Theory.setup
4.205 + (antiquotation \<^binding>\<open>rule_thm\<close> false #>
4.206 + antiquotation \<^binding>\<open>rule_thm_sym\<close> true);
4.207 +
4.208 +(**)end(**)
5.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Feb 08 08:59:37 2023 +0100
5.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Sun Feb 12 12:44:25 2023 +0100
5.3 @@ -51,7 +51,7 @@
5.4 fun new_c term =
5.5 let
5.6 fun selc var =
5.7 - case (Symbol.explode o LibraryC.id_of) var of
5.8 + case (Symbol.explode o TermC.id_of) var of
5.9 "c"::[] => true
5.10 | "c" :: "_":: is =>
5.11 (case (TermC.int_opt_of_string o implode) is of
5.12 @@ -59,7 +59,7 @@
5.13 | NONE => false)
5.14 | _ => false;
5.15 fun get_coeff c =
5.16 - case (Symbol.explode o LibraryC.id_of) c of
5.17 + case (Symbol.explode o TermC.id_of) c of
5.18 "c"::"_"::is => (the o TermC.int_opt_of_string o implode) is
5.19 | _ => 0;
5.20 val cs = filter selc (TermC.vars term);
5.21 @@ -71,7 +71,6 @@
5.22 let val max_coeff = maxl (map get_coeff cs)
5.23 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
5.24 end;
5.25 -\<close> ML \<open>
5.26
5.27 (*WN080222:*)
5.28 (*("add_new_c", ("Integrate.add_new_c", eval_add_new_c "#add_new_c_"))
5.29 @@ -305,4 +304,4 @@
5.30 \<close> ML \<open>
5.31 \<close>
5.32
5.33 -end
5.34 \ No newline at end of file
5.35 +end
6.1 --- a/src/Tools/isac/Knowledge/Test.thy Wed Feb 08 08:59:37 2023 +0100
6.2 +++ b/src/Tools/isac/Knowledge/Test.thy Sun Feb 12 12:44:25 2023 +0100
6.3 @@ -60,9 +60,9 @@
6.4 | atom _ = false;
6.5
6.6 fun varids (Const (\<^const_name>\<open>numeral\<close>, _) $ _) = []
6.7 - | varids (Const (s, Type (_,[]))) = [strip_thy s]
6.8 - | varids (Free (s, Type (_,[]))) = [strip_thy s]
6.9 - | varids (Var((s, _),Type (_,[]))) = [strip_thy s]
6.10 + | varids (Const (s, Type (_,[]))) = [ThmC.cut_longid s]
6.11 + | varids (Free (s, Type (_,[]))) = [ThmC.cut_longid s]
6.12 + | varids (Var((s, _),Type (_,[]))) = [ThmC.cut_longid s]
6.13 (*| varids (_ (s,"?DUMMY" )) = ..ML-error *)
6.14 | varids((Const ("Bin.integ_of_bin",_)) $ _)= [](*8.01: superfluous?*)
6.15 | varids (Abs (a, _, t)) = union op = [a] (varids t)
6.16 @@ -86,9 +86,9 @@
6.17
6.18 fun degree addl mul bdVar t =
6.19 let
6.20 -fun deg _ _ v (Const (s, Type (_, []))) = if v=strip_thy s then 1 else 0
6.21 - | deg _ _ v (Free (s, Type (_, []))) = if v=strip_thy s then 1 else 0
6.22 - | deg _ _ v (Var((s, _), Type (_, []))) = if v=strip_thy s then 1 else 0
6.23 +fun deg _ _ v (Const (s, Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
6.24 + | deg _ _ v (Free (s, Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
6.25 + | deg _ _ v (Var((s, _), Type (_, []))) = if v=ThmC.cut_longid s then 1 else 0
6.26 (*| deg _ _ v (_ (s,"?DUMMY" )) = ..ML-error *)
6.27 | deg _ _ _ ((Const ("Bin.integ_of_bin", _)) $ _ ) = 0
6.28 | deg addl mul v (h $ t1 $ t2) =
6.29 @@ -98,7 +98,7 @@
6.30 | deg _ _ _ t = raise ERROR ("deg: t = " ^ UnparseC.term @{context} t)
6.31 in
6.32 if polynomial (addl @ [mul]) t bdVar
6.33 - then SOME (deg addl mul (id_of bdVar) t)
6.34 + then SOME (deg addl mul (TermC.id_of bdVar) t)
6.35 else (NONE:int option)
6.36 end;
6.37 fun degree_ addl mul bdVar t = (* do not export *)
6.38 @@ -119,21 +119,21 @@
6.39 else false;
6.40 (* strip_thy op_ before *)
6.41 fun is_div_op (dv, (Const (op_,
6.42 - (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) ) = (dv = strip_thy op_)
6.43 + (Type (\<^type_name>\<open>fun\<close>, [Type (_, []), Type (\<^type_name>\<open>fun\<close>, [Type _, Type _])])))) ) = (dv = ThmC.cut_longid op_)
6.44 | is_div_op _ = false;
6.45
6.46 fun is_denom bdVar div_op t =
6.47 let
6.48 - fun is bool [v] _ (Const (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
6.49 - | is bool [v] _ (Free (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
6.50 - | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
6.51 + fun is bool [v] _ (Const (s,Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
6.52 + | is bool [v] _ (Free (s,Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
6.53 + | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = ThmC.cut_longid s then true else false)
6.54 | is _ [_] _ ((Const ("Bin.integ_of_bin",_)) $ _) = false
6.55 | is bool [v] dv (h$n$d) =
6.56 if is_div_op (dv, h)
6.57 then (is false [v] dv n) orelse(is true [v] dv d)
6.58 else (is bool [v] dv n) orelse(is bool [v] dv d)
6.59 | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."
6.60 - in is false (varids bdVar) (strip_thy div_op) t end;
6.61 + in is false (varids bdVar) (ThmC.cut_longid div_op) t end;
6.62
6.63
6.64 fun rational t div_op bdVar =
6.65 @@ -254,7 +254,7 @@
6.66 (*does a term contain a root ?*)
6.67 fun eval_contains_root (thmid:string) _
6.68 (t as (Const (\<^const_name>\<open>Test.contains_root\<close>, _) $ arg)) ctxt =
6.69 - if member op = (ids_of arg) "sqrt"
6.70 + if member op = (TermC.ids_of arg) "sqrt"
6.71 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg)"",
6.72 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
6.73 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg)"",
7.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Wed Feb 08 08:59:37 2023 +0100
7.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Sun Feb 12 12:44:25 2023 +0100
7.3 @@ -19,7 +19,6 @@
7.4 and "Author" "Theory_Ref" "Problem_Ref" "Method_Ref"
7.5 "CAS" "Program" "Given" "Where" "Find" "Relate"
7.6 begin
7.7 - ML_file thmC.sml
7.8 ML_file "model-def.sml"
7.9 ML_file problem.sml
7.10 ML_file method.sml
8.1 --- a/src/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 08:59:37 2023 +0100
8.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
8.3 @@ -1,204 +0,0 @@
8.4 -(* Title: BaseDefinitions/thmC.sml
8.5 - Author: Walther Neuper
8.6 - (c) due to copyright terms
8.7 -
8.8 -This structure could be dropped due to improved reflection in Isabelle;
8.9 -but ThmC.sym_thm requires still an identifying string thm_id.
8.10 -*)
8.11 -signature THEOREM_ISAC =
8.12 -sig
8.13 - type T = ThmC_Def.T
8.14 - type id = ThmC_Def.id (* shortest possible *)
8.15 - type long_id (* e.g. "Test.radd_left_commute"*)
8.16 -
8.17 - val cut_longid: string -> id
8.18 - val long_id: T -> long_id
8.19 -
8.20 - val string_of_thm: Proof.context -> thm -> string
8.21 - val string_of_thms: Proof.context -> thm list -> string
8.22 -
8.23 - val id_of_thm: thm -> id
8.24 - val of_thm: thm -> T
8.25 - val from_rule : Proof.context -> Rule.rule -> T
8.26 - val member': id list -> Rule.rule -> bool
8.27 -
8.28 - val is_sym: id -> bool
8.29 - val thm_from_thy: theory -> id -> thm
8.30 -
8.31 - val make_rule: Proof.context -> bool -> string * Position.T -> Rule_Def.rule
8.32 - val make_sym_rule: Proof.context -> Rule.rule -> Rule.rule
8.33 - val make_sym_rule_set: Rule_Set.T -> Rule_Set.T
8.34 - val sym_thm: thm -> thm
8.35 -
8.36 -\<^isac_test>\<open>
8.37 - val dest_eq_concl: thm -> term * term
8.38 - val string_of_thm_in_thy: theory -> thm -> string
8.39 - val id_drop_sym: id -> id
8.40 - val revert_sym_rule: theory -> Rule.rule -> Rule.rule
8.41 -\<close>
8.42 -end
8.43 -
8.44 -(**)
8.45 -structure ThmC(**): THEOREM_ISAC(**) =
8.46 -struct
8.47 -(**)
8.48 -
8.49 -(** types and conversions **)
8.50 -
8.51 -type T = ThmC_Def.T;
8.52 -type id = ThmC_Def.id;
8.53 -type long_id = string;
8.54 -
8.55 -fun long_id (thmID, _) =
8.56 - thmID
8.57 - |> Global_Theory.get_thm (Know_Store.get_via_last_thy "Isac_Knowledge")
8.58 - |> Thm.get_name_hint
8.59 -fun cut_longid dn = last_elem (space_explode "." dn); (*the cut_longid is the key into Know_Store*)
8.60 -
8.61 -val string_of_thm = ThmC_Def.string_of_thm;
8.62 -val string_of_thms = ThmC_Def.string_of_thms;
8.63 -
8.64 -fun id_of_thm thm = thm |> Thm.get_name_hint |> cut_longid;
8.65 -fun of_thm thm = (id_of_thm thm, thm);
8.66 -fun from_rule _ (Rule.Thm (id, thm)) = (id, thm)
8.67 - | from_rule ctxt r =
8.68 - raise ERROR ("ThmC.from_rule: not defined for " ^ Rule.to_string ctxt r);
8.69 -
8.70 -\<^isac_test>\<open>
8.71 -fun string_of_thm_in_thy thy thm =
8.72 - UnparseC.term (Proof_Context.init_global thy) (Thm.prop_of thm);
8.73 -\<close>
8.74 -fun member' thmIDs thm = (member op = thmIDs (Rule.thm_id thm))
8.75 - handle ERROR _ => false
8.76 -
8.77 -
8.78 -(** handle symmetric equalities, generated by deriving input terms **)
8.79 -
8.80 -fun is_sym id =
8.81 - case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: _ => true
8.82 - | _ => false;
8.83 -
8.84 -\<^isac_test>\<open>
8.85 -fun id_drop_sym id =
8.86 - case Symbol.explode id of "s" :: "y" :: "m" :: "_" :: id => implode id
8.87 - | _ => id
8.88 -\<close>
8.89 -
8.90 -(* get the theorem associated with the xstring-identifier;
8.91 - if the identifier starts with "sym_" then swap "lhs = rhs" around "=";
8.92 - in case identifiers starting with "#" come from Eval and
8.93 - get an ad-hoc theorem (containing numerals only) -- rejected here
8.94 -*)
8.95 -fun thm_from_thy thy thmid =
8.96 - case Symbol.explode thmid of
8.97 - "s" :: "y" :: "m" :: "_" :: "#" :: _ =>
8.98 - raise ERROR ("thm_from_thy not impl.for " ^ thmid)
8.99 - | "s" :: "y" :: "m" :: "_" :: id =>
8.100 - ((Global_Theory.get_thm thy) (implode id)) RS sym
8.101 - | "#" :: _ =>
8.102 - raise ERROR ("thm_from_thy not impl.for " ^ thmid)
8.103 - | _ =>
8.104 - thmid |> Global_Theory.get_thm thy
8.105 -
8.106 -fun dest_eq_concl thm =
8.107 - (case try (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl o Thm.prop_of) thm of
8.108 - NONE => raise THM ("dest_eq_concl: conclusion needs to be HOL equality", 0, [thm])
8.109 - | SOME eq => eq);
8.110 -
8.111 -(* A1==>...==> An ==> (Lhs = Rhs) goes to A1 ==>...==> An ==> (Rhs = Lhs) *)
8.112 -(*NB: careful instantiation avoids shifting of schematic variables*)
8.113 -fun sym_thm thm =
8.114 - let
8.115 - val thy = Thm.theory_of_thm thm;
8.116 - val certT = Thm.global_ctyp_of thy;
8.117 - val cert = Thm.global_cterm_of thy;
8.118 -
8.119 - val (lhs, rhs) = dest_eq_concl thm |> apply2 cert;
8.120 - val A = Thm.typ_of_cterm lhs;
8.121 -
8.122 - val sym_rule = Thm.lift_rule (Thm.cprop_of thm) @{thm sym};
8.123 - val (t, s) = dest_eq_concl sym_rule;
8.124 -
8.125 - val instT = TVars.map (K (K A)) (TVars.build (TVars.add_tvars t));
8.126 - val (t', s') = (t, s) |> apply2 (dest_Var o Term_Subst.instantiate (instT, Vars.empty));
8.127 -
8.128 - val cinstT = TVars.map (K certT) instT;
8.129 - val cinst = Vars.make [(s', lhs), (t', rhs)];
8.130 - in
8.131 - thm
8.132 - |> Thm.implies_elim (Thm.instantiate (cinstT, cinst) sym_rule)
8.133 - |> Thm.put_name_hint (Thm.get_name_hint thm)
8.134 - end;
8.135 -
8.136 -fun make_sym_rule_set Rule_Set.Empty = Rule_Set.Empty
8.137 - | make_sym_rule_set (Rule_Def.Repeat {id, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =
8.138 - Rule_Def.Repeat {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls,
8.139 - rules = rules, rew_ord = rew_ord, preconds = preconds}
8.140 - | make_sym_rule_set (Rule_Set.Sequence {id, program, calc, errpatts, asm_rls, prog_rls, rules, rew_ord, preconds}) =
8.141 - Rule_Set.Sequence {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls, prog_rls = prog_rls,
8.142 - rules = rules, rew_ord = rew_ord, preconds = preconds}
8.143 - | make_sym_rule_set (Rule_Set.Rrls {id, program, calc, errpatts, asm_rls, prepat, rew_ord}) =
8.144 - Rule_Set.Rrls {id = "sym_" ^ id, program = program, calc = calc, errpatts = errpatts, asm_rls = asm_rls,
8.145 - prepat = prepat, rew_ord = rew_ord}
8.146 -
8.147 -(* toggles sym_* and keeps "#:" for ad-hoc theorems *)
8.148 -fun make_sym_rule ctxt (Rule.Thm (thmID, thm)) =
8.149 - let
8.150 - val thm' = sym_thm thm
8.151 - val thmID' = case Symbol.explode thmID of
8.152 - "s" :: "y" :: "m" :: "_" :: id => implode id
8.153 - | "#" :: ":" :: _ => "#: " ^ string_of_thm ctxt thm'
8.154 - | _ => "sym_" ^ thmID
8.155 - in Rule.Thm (thmID', thm') end
8.156 - | make_sym_rule _ (Rule.Rls_ rls) = Rule.Rls_ (make_sym_rule_set rls)
8.157 - | make_sym_rule ctxt r = raise ERROR ("ThmC.make_sym_rule: not for " ^ Rule.to_string ctxt r)
8.158 -
8.159 -\<^isac_test>\<open>
8.160 -(* revert a thm RS @{thm sym} back to original thm, in case it ML\<open>is_sym\<close> *)
8.161 -fun revert_sym_rule thy (Rule.Thm (id, thm)) =
8.162 - (*this ^^ might come from the user, who doesn't care about thy*)
8.163 - if is_sym (cut_longid id)
8.164 - then
8.165 - let
8.166 - val id' = id_drop_sym id
8.167 - val thm' = thm_from_thy thy id'
8.168 - val id'' = Thm.get_name_hint thm' (*recover the thy the thm comes from*)
8.169 - in Rule.Thm (id'', thm') end
8.170 - else Rule.Thm (Thm.get_name_hint thm, thm) (*recover the thy the thm comes from*)
8.171 - | revert_sym_rule thy rule =
8.172 - raise ERROR ("ThmC.revert_sym_rule: NOT for " ^
8.173 - Rule.to_string (Proof_Context.init_global thy) rule)
8.174 -\<close>
8.175 -
8.176 -
8.177 -(* ML antiquotations *)
8.178 -
8.179 -val sym_prefix = "sym_";
8.180 -
8.181 -fun make_rule ctxt symmetric (xname, pos) =
8.182 - let
8.183 - val _ =
8.184 - if String.isPrefix sym_prefix xname
8.185 - then error ("Bad theorem name with sym-prefix " ^ quote xname ^ Position.here pos) else ();
8.186 -
8.187 - val context = Context.Proof ctxt;
8.188 - val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
8.189 - val {name, dynamic, thms, ...} = Facts.retrieve context facts (xname, pos);
8.190 - val thm =
8.191 - if dynamic then error ("Bad dynamic fact " ^ quote name ^ Position.here pos)
8.192 - else Facts.the_single (name, pos) thms;
8.193 - val (xname', thm') = if symmetric then (sym_prefix ^ xname, thm RS sym) else (xname, thm);
8.194 - in Rule.Thm (xname', thm') end;
8.195 -
8.196 -fun antiquotation binding sym =
8.197 - ML_Antiquotation.value_embedded binding
8.198 - (Scan.lift Parse.embedded_position >> (fn name =>
8.199 - "ThmC.make_rule ML_context " ^ Bool.toString sym ^
8.200 - ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position name));
8.201 -
8.202 -val _ =
8.203 - Theory.setup
8.204 - (antiquotation \<^binding>\<open>rule_thm\<close> false #>
8.205 - antiquotation \<^binding>\<open>rule_thm_sym\<close> true);
8.206 -
8.207 -(**)end(**)
9.1 --- a/src/Tools/isac/ProgLang/Prog_Expr.thy Wed Feb 08 08:59:37 2023 +0100
9.2 +++ b/src/Tools/isac/ProgLang/Prog_Expr.thy Sun Feb 12 12:44:25 2023 +0100
9.3 @@ -160,8 +160,7 @@
9.4 HOLogic.Trueprop $ (TermC.mk_equality (t, r)))
9.5 | eval_rhs _ _ _ _ = NONE;
9.6
9.7 -
9.8 -fun occurs_in v t = member op = (((map strip_thy) o TermC.ids2str) t) (Term.term_name v);
9.9 +fun occurs_in v t = member op = (((map ThmC.cut_longid) o TermC.ids2str) t) (Term.term_name v);
9.10 (*("occurs_in", ("Prog_Expr.occurs_in", Prog_Expr.eval_occurs_in ""))*)
9.11 fun eval_occurs_in _ "Prog_Expr.occurs_in" (p as (Const (\<^const_name>\<open>occurs_in\<close>, _) $ v $ t)) _ =
9.12 ((*tracing("#>@ eval_occurs_in: v= " ^ UnparseC.term @{context} v);
9.13 @@ -249,7 +248,7 @@
9.14 val n1 = t1 |> HOLogic.dest_number |> snd
9.15 val n2 = t2 |> HOLogic.dest_number |> snd
9.16 in
9.17 - if Eval.calc_equ (strip_thy op0) (n1, n2)
9.18 + if Eval.calc_equ (ThmC.cut_longid op0) (n1, n2)
9.19 then SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
9.20 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
9.21 else SOME (TermC.mk_thmid thmid (string_of_int n1) (string_of_int n2),
10.1 --- a/src/Tools/isac/Specify/sub-problem.sml Wed Feb 08 08:59:37 2023 +0100
10.2 +++ b/src/Tools/isac/Specify/sub-problem.sml Sun Feb 12 12:44:25 2023 +0100
10.3 @@ -43,7 +43,7 @@
10.4 case cas of
10.5 NONE => Auto_Prog.pblterm dI pI
10.6 | SOME t => subst_atomic ((Model_Pattern.variables model) ~~~ vals) t
10.7 - val f = Auto_Prog.subpbl (strip_thy dI) pI
10.8 + val f = Auto_Prog.subpbl (ThmC.cut_longid dI) pI
10.9 in
10.10 (Tactic.Subproblem (dI, pI), Tactic.Subproblem' ((dI, pI, mI), pors, hdl, fmz_, ctxt, f))
10.11 end
11.1 --- a/test/Tools/isac/MathEngBasic/thmC.sml Wed Feb 08 08:59:37 2023 +0100
11.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Sun Feb 12 12:44:25 2023 +0100
11.3 @@ -50,7 +50,7 @@
11.4
11.5 if id = "sym_real_mult_minus1" andalso ThmC.string_of_thm ctxt thm = "- ?z1 = - 1 * ?z1" then ()
11.6 else error "input to revert_sym_rule CHANGED";
11.7 -
11.8 +
11.9 (*if*) is_sym (ThmC.cut_longid id) (*then*);
11.10 val id' = id_drop_sym id
11.11 val thm' = thm_from_thy thy id'
12.1 --- a/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Wed Feb 08 08:59:37 2023 +0100
12.2 +++ b/test/Tools/isac/Minisubpbl/200-start-method-NEXT_STEP.sml Sun Feb 12 12:44:25 2023 +0100
12.3 @@ -18,11 +18,101 @@
12.4 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Model_Problem*)
12.5 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Theory "Test"*)
12.6 (*[], Pbl*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Problem ["sqroot-test", "univariate", "equation", "test"*)
12.7 -(*[], Met*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
12.8 +
12.9 +(*[], Met*)val return_Step_do_next_Specify_Problem = Step.do_next p ((pt, e_pos'), []);(*Specify_Method ["Test", "squ-equ-test-subpbl1"]*)
12.10 +(*/------------------- step into Step.do_next_Specify_Problem ------------------------------\\*)
12.11 +"~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis)) =
12.12 + (p, ((pt, e_pos'), []));
12.13 + (*if*) Pos.on_calc_end ip (*else*);
12.14 + val (_, probl_id, _) = Calc.references (pt, p);
12.15 +val _ =
12.16 + (*case*) tacis (*of*);
12.17 + (*if*) probl_id = Problem.id_empty (*else*);
12.18 +
12.19 + Step.switch_specify_solve p_ (pt, ip);
12.20 +"~~~~~ fun switch_specify_solve , args:"; val (state_pos, (pt, input_pos)) = (p_, (pt, ip));
12.21 + (*if*) Pos.on_specification ([], state_pos) (*then*);
12.22 +
12.23 + Step.specify_do_next (pt, input_pos);
12.24 +"~~~~~ fun specify_do_next , args:"; val ((ptp as (pt, (p, p_)))) = ((pt, input_pos));
12.25 + val (_, (p_', tac)) = Specify.find_next_step ptp
12.26 + val ist_ctxt = Ctree.get_loc pt (p, p_)
12.27 +val _ =
12.28 + (*case*) tac (*of*);
12.29 +
12.30 +Step_Specify.by_tactic_input tac (pt, (p, p_'));
12.31 +"~~~~~ fun by_tactic_input , args:"; val ((Tactic.Specify_Method id), (pt, pos)) =
12.32 + (tac, (pt, (p, p_')));
12.33 +
12.34 + val (o_model, ctxt, i_model) =
12.35 +Specify_Step.complete_for id (pt, pos);
12.36 +"~~~~~ fun complete_for , args:"; val (mID, (ctree, pos)) = (id, (pt, pos));
12.37 + val {origin = (o_model, _, _), probl = i_prob, ctxt,
12.38 + ...} = Calc.specify_data (ctree, pos);
12.39 + val {model = m_patt, where_, where_rls, ...} = MethodC.from_store ctxt mID
12.40 + val {origin = (root_model, _, _), ...} = Calc.specify_data (ctree, ([], Pos.Und))
12.41 + val (o_model', ctxt') = O_Model.complete_for m_patt root_model (o_model, ctxt)
12.42 +
12.43 + val (_, (i_model, _)) =
12.44 + M_Match.match_itms_oris ctxt i_prob (m_patt, where_, where_rls) o_model';
12.45 +"~~~~~ fun match_itms_oris , args:"; val (ctxt, pbl, (pbt, where_, where_rls), oris) =
12.46 + (ctxt, i_prob, (m_patt, where_, where_rls), o_model');
12.47 + (*0*)val mv = I_Model.max_variant pbl;
12.48 +
12.49 + fun eqdsc_pbt_itm ((_,(d,_))) (_, _, _, _, itm_) = d = I_Model.descriptor itm_;
12.50 + fun notmem pbl pbt1 = case find_first (eqdsc_pbt_itm pbt1) pbl of
12.51 + SOME _ => false | NONE => true;
12.52 + (*1*)val mis = (filter (notmem pbl)) pbt;
12.53 + fun eqdsc_ori (_,(d,_)) (_, _, _, d', _) = d = d';
12.54 + fun ori2itmMis (f, (d, pid)) (i, v, _, _, _) = (i, v, false, f, I_Model.Mis (d, pid));
12.55 + (*2*)fun oris2itms oris mis1 = ((map (ori2itmMis mis1)) o (filter (eqdsc_ori mis1))) oris;
12.56 + val news = (flat o (map (oris2itms oris))) mis;
12.57 + (*3*)fun mem_vat (_, vats, _, _, _) = member op = vats mv;
12.58 + val newitms = filter mem_vat news;
12.59 + (*4*)val itms' = pbl @ newitms;
12.60 +
12.61 + val (pb, where_') =
12.62 + Pre_Conds.check ctxt where_rls where_ itms' mv;
12.63 +"~~~~~ fun check , args:"; val (ctxt, where_rls, pres, pbl, (_)) =
12.64 + (ctxt, where_rls, where_, itms', mv);
12.65 + val env = I_Model.environment pbl;
12.66 + val pres' = map (TermC.subst_atomic_all env) pres;
12.67 +
12.68 +(*+*)val "Test" = ctxt |> Proof_Context.theory_of |> ThyC.id_of
12.69 +(*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls
12.70 +(*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = pres'
12.71 +
12.72 +(*+*)val ctxt = Config.put rewrite_trace true ctxt;
12.73 + val evals = map (
12.74 + Pre_Conds.eval ctxt where_rls) pres';
12.75 +(*
12.76 +@## rls: prls_met_test_squ_sub on: precond_rootmet x
12.77 +@### try calc: "Test.precond_rootmet"
12.78 +@#### eval asms: "(precond_rootmet x) = True"
12.79 +@### calc. to: True
12.80 +@### try calc: "Test.precond_rootmet"
12.81 +@### try calc: "Test.precond_rootmet"
12.82 +*)
12.83 +(*+*)val ctxt = Config.put rewrite_trace false ctxt;
12.84 +
12.85 +"~~~~~ fun eval_precond_rootmet , args:"; val ((thmid:string), _, (t as (Const (\<^const_name>\<open>Test.precond_rootmet\<close>, _) $ arg)), ctxt) =
12.86 + ("aaa", "bbb", tTEST, ctxt);
12.87 + SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
12.88 + HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
12.89 +;
12.90 + (TermC.mk_thmid thmid (UnparseC.term ctxt arg)) "";
12.91 +"~~~~~ fun mk_thmid , args:"; val (thmid, n1, n2) = (thmid, (UnparseC.term ctxt arg), "");
12.92 + thmid ^ (cut_longid n1) ^ "_" ^ (cut_longid n2);
12.93 +
12.94 + (cut_longid n2);
12.95 +"~~~~~ fun cut_longid , args:"; val (dn) = (n2);
12.96 +(*\------------------- step into Step.do_next_Specify_Problem ------------------------------//*)
12.97 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Specify_Problem
12.98 +
12.99 (*[1], Frm*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Apply_Method ["Test", "squ-equ-test-subpbl1"]*)
12.100 -(*[1], Res*)val (_, ([(tac''', _, _)], _, (pt''', p'''))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
12.101 +(*[1], Res*)val return_Step_do_next_Apply_Method = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "norm_equation"*)
12.102
12.103 -(*//------------------ step into Apply_Method ----------------------------------------------\\*)
12.104 +(*/------------------- step into Apply_Method ----------------------------------------------\\*)
12.105 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
12.106 = (p ,((pt, e_pos'), []));
12.107 (*if*) Pos.on_calc_end ip (*else*);
12.108 @@ -40,8 +130,15 @@
12.109 "~~~~~ and do_next , args:"; val (ptp as (pt, pos as (p, p_))) = (pt, input_pos);
12.110 (*if*) MethodC.id_empty = get_obj g_metID pt (par_pblobj pt p) (*else*);
12.111 val ((ist, ctxt), sc) = LItool.resume_prog (p,p_) pt;
12.112 -val LI.Next_Step (ist, ctxt, tac) =
12.113 - (*case*) LI.find_next_step sc (pt, pos) ist ctxt (*of*);
12.114 +
12.115 +val return_LI_find_next_step = (*case*)
12.116 + LI.find_next_step sc (pt, pos) ist ctxt (*of*);
12.117 +(*//------------------ step into LI.find_next_step -----------------------------------------\\*)
12.118 +"~~~~~ fun find_next_step , args:"; val ((Rule.Prog prog), (ptp as (pt, pos as (p, _))), (Istate.Pstate ist), ctxt) =
12.119 + (sc, (pt, pos), ist, ctxt);
12.120 +(*.. this showed that we have ContextC.empty*)
12.121 +(*\\------------------ step into XXXXX -----------------------------------------------------//*)
12.122 +val LI.Next_Step (ist, ctxt, tac) = return_LI_find_next_step;
12.123
12.124 LI.by_tactic tac (ist, Tactic.insert_assumptions tac ctxt) ptp;
12.125 "~~~~~ fun by_tactic , args:"; val (tac_, ic, (pt, pos))
12.126 @@ -63,14 +160,14 @@
12.127
12.128 val return =
12.129 ((p, Pos.Res), c, Test_Out.FormKF (UnparseC.term ctxt f'), pt)
12.130 -(*-------------------- stop step into Apply_Method -------------------------------------------*)
12.131 -(*\\------------------ step into Apply_Method ----------------------------------------------//*)
12.132 +(*\------------------- step into Apply_Method ----------------------------------------------//*)
12.133 +val (_, ([(tac, _, _)], _, (pt, p))) = return_Step_do_next_Apply_Method
12.134
12.135 -(*[2], Res*)val (_, ([(tac''''', _, _)], _, (pt''''', p'''''))) = Step.do_next p''' ((pt''', e_pos'), []);(*Rewrite_Set "Test_simplify"*)
12.136 +(*[2], Res*)val (_, ([(tac, _, _)], _, (pt, p))) = Step.do_next p ((pt, e_pos'), []);(*Rewrite_Set "Test_simplify"*)
12.137
12.138 (* final test ... ----------------------------------------------------------------------------*)
12.139 -(*+*)val ([2], Res) = p''''';
12.140 -Test_Tool.show_pt_tac pt'''''; (*[
12.141 +(*+*)val ([2], Res) = p;
12.142 +Test_Tool.show_pt_tac pt; (*[
12.143 ([], Frm), solve (x + 1 = 2, x)
12.144 . . . . . . . . . . Apply_Method ["Test", "squ-equ-test-subpbl1"],
12.145 ([1], Frm), x + 1 = 2
13.1 --- a/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml Wed Feb 08 08:59:37 2023 +0100
13.2 +++ b/test/Tools/isac/Minisubpbl/250-Rewrite_Set-from-method-NEXT_STEP.sml Sun Feb 12 12:44:25 2023 +0100
13.3 @@ -1,6 +1,5 @@
13.4 -(* Title: "Minisubpbl/200-start-method-NEXT_STEP.sml"
13.5 - Author: Walther Neuper 1105
13.6 - (c) copyright due to lincense terms.
13.7 +(* Title: Minisubpbl/250-Rewrite_Set-from_method-NEXT_STEP.sml
13.8 + Author: Walther Neuper
13.9 *)
13.10
13.11 open Rewrite;
13.12 @@ -10,7 +9,6 @@
13.13 "----------- Minisubplb/250-Rewrite_Set-from_method-NEXT_STEP.sml ----------------------------";
13.14 "----------- Minisubplb/250-Rewrite_Set-from_method-NEXT_STEP.sml ----------------------------";
13.15 "----------- Minisubplb/250-Rewrite_Set-from_method-NEXT_STEP.sml ----------------------------";
13.16 -"----------- Minisubplb/250-Rewrite_Set-from_method-NEXT_STEP.sml ----------------------------";
13.17 val fmz = ["equality (x+1=(2::real))", "solveFor x", "solutions L"];
13.18 val (dI',pI',mI') =
13.19 ("Test", ["sqroot-test", "univariate", "equation", "test"],
13.20 @@ -26,7 +24,7 @@
13.21
13.22 (*//------------------ step into Rewrite_Set "norm_equation" -------------------------------\\*)
13.23 "~~~~~ fun do_next , args:"; val ((ip as (_, p_)), (ptp as (pt, p), tacis))
13.24 - = (p''', ((pt''', e_pos'), []));
13.25 + = (p, ((pt, e_pos'), []));
13.26 (*if*) Pos.on_calc_end ip (*else*);
13.27 val (_, probl_id, _) = Calc.references (pt, p);
13.28 val _ =
14.1 --- a/test/Tools/isac/Test_Theory.thy Wed Feb 08 08:59:37 2023 +0100
14.2 +++ b/test/Tools/isac/Test_Theory.thy Sun Feb 12 12:44:25 2023 +0100
14.3 @@ -17,14 +17,14 @@
14.4 (*\\------------------ adhoc inserted n ----------------------------------------------------//*)
14.5 \<close> ML \<open> (*\\----------- adhoc inserted n ----------------------------------------------------//*)
14.6
14.7 +val return_XXXXX = "XXXXX"
14.8 \<close> ML \<open> (*//----------- step into XXXXX -----------------------------------------------------\\*)
14.9 (*//------------------ step into XXXXX -----------------------------------------------------\\*)
14.10 -(*keep for continuing YYYYY*)
14.11 \<close> ML \<open> (*------------- continuing XXXXX ------------------------------------------------------*)
14.12 (*-------------------- continuing XXXXX ------------------------------------------------------*)
14.13 -(*kept for continuing YYYYY*)
14.14 (*\\------------------ step into XXXXX -----------------------------------------------------//*)
14.15 \<close> ML \<open> (*\\----------- step into XXXXX -----------------------------------------------------//*)
14.16 +val "XXXXX" = return_XXXXX
14.17
14.18 (*/------------------- check entry to XXXXX -------------------------------------------------\*)
14.19 (*\------------------- check entry to XXXXX -------------------------------------------------/*)