1.1 --- a/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 12:28:47 2020 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 14:46:55 2020 +0200
1.3 @@ -48,7 +48,7 @@
1.4 val tac2xml : int -> Tactic.input -> Celem.xml
1.5 val tacs2xml : int -> Tactic.input list -> Celem.xml
1.6 val theref2xml : int -> ThyC.thyID -> string -> xstring -> string
1.7 - val thm'2xml : int -> ThmC.thm' -> Celem.xml
1.8 + val thm'2xml : int -> ThmC_Def.thm' -> Celem.xml
1.9 val thm''2xml : int -> thm -> Celem.xml
1.10 val thmstr2xml : int -> string -> Celem.xml
1.11 end
1.12 @@ -97,9 +97,9 @@
1.13 | rule2xml j _ (Rule.Thm (thmDeriv, _)) =
1.14 indt j ^ "<RULE>\n" ^
1.15 indt (j+i) ^ "<TAG> Theorem </TAG>\n" ^
1.16 - indt (j+i) ^ "<STRING> " ^ ThmC.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
1.17 + indt (j+i) ^ "<STRING> " ^ ThmC_Def.thmID_of_derivation_name thmDeriv ^ " </STRING>\n" ^
1.18 indt (j+i) ^ "<GUH> " ^
1.19 - Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
1.20 + Celem.thm2guh (Rtools.thy_containing_thm thmDeriv) (ThmC_Def.thmID_of_derivation_name thmDeriv) ^ " </GUH>\n" ^
1.21 indt j ^ "</RULE>\n"
1.22 | rule2xml _ _ (Rule.Num_Calc (_(*termop*), _)) = ""
1.23 (*FIXXXXXXXME.WN060714 in rls make Num_Calc : calc -> rule [add scriptop!]
1.24 @@ -467,7 +467,7 @@
1.25
1.26 fun thm''2xml j (thm : thm) =
1.27 indt j ^ "<THEOREM>\n" ^
1.28 - indt (j+i) ^ "<ID> " ^ ThmC.thmID_of_derivation_name' thm ^ " </ID>\n"^
1.29 + indt (j+i) ^ "<ID> " ^ ThmC_Def.thmID_of_derivation_name' thm ^ " </ID>\n"^
1.30 term2xml j (Thm.prop_of thm) ^ "\n" ^
1.31 indt j ^ "</THEOREM>\n";
1.32 fun xml_of_thm' (ID, form) =
2.1 --- a/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Apr 10 12:28:47 2020 +0200
2.2 +++ b/src/Tools/isac/BridgeLibisabelle/interface.sml Fri Apr 10 14:46:55 2020 +0200
2.3 @@ -11,7 +11,7 @@
2.4
2.5 signature KERNEL =
2.6 sig
2.7 - val appendFormula : Celem.calcID -> UnparseC.cterm' -> XML.tree (*unit future*)
2.8 + val appendFormula : Celem.calcID -> TermC.as_string -> XML.tree (*unit future*)
2.9 val autoCalculate : Celem.calcID -> Solve.auto -> XML.tree (*unit future*)
2.10 val applyTactic : Celem.calcID -> Pos.pos' -> Tactic.input -> XML.tree
2.11 val CalcTree : Selem.fmz list -> XML.tree
2.12 @@ -48,7 +48,7 @@
2.13 val moveUp : Celem.calcID -> Pos.pos' -> XML.tree
2.14 val refFormula : Celem.calcID -> Pos.pos' -> XML.tree
2.15 val refineProblem : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
2.16 - val replaceFormula : Celem.calcID -> UnparseC.cterm' -> XML.tree
2.17 + val replaceFormula : Celem.calcID -> TermC.as_string -> XML.tree
2.18 val requestFillformula : Celem.calcID -> Error_Fill_Def.errpatID * Error_Fill_Def.fillpatID -> XML.tree
2.19 val resetCalcHead : Celem.calcID -> XML.tree
2.20 val setContext : Celem.calcID -> Pos.pos' -> Celem.guh -> XML.tree
2.21 @@ -439,7 +439,7 @@
2.22 handle _ => sysERROR2xml cI "error in kernel 16";
2.23
2.24 (* append a formula to the calculation *)
2.25 -fun appendFormula' cI (ifo: UnparseC.cterm') =
2.26 +fun appendFormula' cI (ifo: TermC.as_string) =
2.27 (let
2.28 val cs = get_calc cI
2.29 val pos = get_pos cI 1
2.30 @@ -679,7 +679,7 @@
2.31 (#1: (Error_Fill_Def.fillpatID * term * thm * (Selem.subs option) -> Error_Fill_Def.fillpatID))) fillforms of
2.32 (_, fillform, thm, sube_opt) :: _ =>
2.33 let
2.34 - val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC.thm''_of_thm thm)
2.35 + val (pt, pos') = Generate.generate_inconsistent_rew (sube_opt, ThmC_Def.thm''_of_thm thm)
2.36 fillform (get_loc pt pos) pos pt
2.37 in
2.38 (upd_calc cI ((pt, pos'), []); (*upd_ipos cI 1 pos';*)
3.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Fri Apr 10 12:28:47 2020 +0200
3.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Fri Apr 10 14:46:55 2020 +0200
3.3 @@ -14,14 +14,14 @@
3.4 ad(2) decode "<" ---> "<", decode ">" ---> ">"
3.5 decode "&" ---> "&"
3.6 called for term2xml; + see "fun encode" below*)
3.7 -fun decode (str: UnparseC.cterm') =
3.8 +fun decode (str: TermC.as_string) =
3.9 let fun dec [] = []
3.10 | dec ("^"::"^"::"^"::cs) = "^"::(dec cs)
3.11 | dec ("&"::cs) = "&"::"a"::"m"::"p"::";"::(dec cs)
3.12 | dec ("<"::cs) = "&"::"l"::"t"::";"::(dec cs)
3.13 | dec (">"::cs) = "&"::"g"::"t"::";"::(dec cs)
3.14 | dec (c::cs) = c::(dec cs)
3.15 - in (implode o dec o Symbol.explode) str: UnparseC.cterm' end;
3.16 + in (implode o dec o Symbol.explode) str: TermC.as_string end;
3.17
3.18 fun dop_leading _ [] = []
3.19 | dop_leading c (c' :: cs) =
3.20 @@ -33,7 +33,7 @@
3.21 let val cs' = dop_leading "^" cs
3.22 in rm_doublets c (singled @ [c']) cs' end
3.23 else rm_doublets c (singled @ [c']) cs
3.24 -fun encode (str : UnparseC.cterm') =
3.25 +fun encode (str : TermC.as_string) =
3.26 let fun enc [] = []
3.27 | enc ("^" :: cs) = "^" :: "^" :: "^" :: (enc cs)
3.28 | enc (c :: cs) = c :: (enc cs)
4.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 12:28:47 2020 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 14:46:55 2020 +0200
4.3 @@ -13,7 +13,7 @@
4.4 in
4.5 filter (fn thm => Context.theory_name (Thm.theory_of_thm thm) = Context.theory_name thy
4.6 andalso not (thm contains_one_of fun_ids)
4.7 - andalso not (ThmC.thmID_of_derivation_name' thm = "mono"))
4.8 + andalso not (ThmC_Def.thmID_of_derivation_name' thm = "mono"))
4.9 (* created in Biegelinie by partial_function ^^^^^^*)
4.10 (map snd (Global_Theory.all_thms_of thy false))
4.11 end
4.12 @@ -21,7 +21,7 @@
4.13 (* wrap theory-data into the uniform type thydata *)
4.14
4.15 fun makeHthm (part : string, thyID : ThyC.thyID) (thm : thm) =
4.16 - let val theID = [part, thyID, "Theorems"] @ [ThmC.thmID_of_derivation_name' thm] : Celem.theID
4.17 + let val theID = [part, thyID, "Theorems"] @ [ThmC_Def.thmID_of_derivation_name' thm] : Celem.theID
4.18 in (theID, Celem.Hthm {guh = Celem.theID2guh theID, coursedesign = [],
4.19 mathauthors = ["isac-team"], fillpats = [], thm = thm})
4.20 end;
4.21 @@ -42,7 +42,7 @@
4.22 end;
4.23
4.24 fun revert_sym thy (Rule.Thm (thmID, thm)) =
4.25 - if (Rtools.is_sym o ThmC.thmID_of_derivation_name) thmID
4.26 + if (Rtools.is_sym o ThmC_Def.thmID_of_derivation_name) thmID
4.27 then
4.28 let
4.29 val thmID' = Rtools.sym_drop thmID
4.30 @@ -58,7 +58,7 @@
4.31 |> map (revert_sym thy)
4.32 |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
4.33 |> gen_distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
4.34 - : (ThmC.thmID * thm) list
4.35 + : (ThmC_Def.thmID * thm) list
4.36
4.37 (* collect all thydata defined in in a theory *)
4.38
4.39 @@ -83,7 +83,7 @@
4.40 (* collect theorems defined in Isabelle *)
4.41 fun collect_isab isa (thmDeriv, thm) =
4.42 let val theID =
4.43 - [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
4.44 + [isa, ThyC.thyID_of_derivation_name thmDeriv, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
4.45 in
4.46 (theID: Celem.theID, Celem.Hthm {guh = Celem.theID2guh theID,
4.47 mathauthors = ["Isabelle team, TU Munich"],
4.48 @@ -211,7 +211,7 @@
4.49 val the = Celem.Html {guh = guh, coursedesign = [], mathauthors = mathauthors, html = ""}
4.50 in (the, theID) end
4.51
4.52 -fun make_thm thy part (thmID : ThmC.thmID, thm) (mathauthors : Celem.authors) =
4.53 +fun make_thm thy part (thmID : ThmC_Def.thmID, thm) (mathauthors : Celem.authors) =
4.54 let
4.55 val guh = Celem.thm2guh (part, ThyC.theory2thyID thy) thmID
4.56 val theID = Rtools.guh2theID guh
5.1 --- a/src/Tools/isac/Build_Isac.thy Fri Apr 10 12:28:47 2020 +0200
5.2 +++ b/src/Tools/isac/Build_Isac.thy Fri Apr 10 14:46:55 2020 +0200
5.3 @@ -15,12 +15,13 @@
5.4 imports
5.5 (* theory KEStore imports Complex_Main
5.6 ML_file libraryC.sml
5.7 + ML_file theoryC.sml
5.8 + ML_file unparseC.sml
5.9 ML_file "rule-def.sml"
5.10 + ML_file thmC.sml
5.11 ML_file "exec-def.sml"
5.12 ML_file "rewrite-order.sml"
5.13 - ML_file theoryC.sml
5.14 ML_file rule.sml
5.15 - ML_file thmC.sml
5.16 ML_file "error-fill-def.sml"
5.17 ML_file "rule-set.sml"
5.18 ML_file calcelems.sml
5.19 @@ -40,11 +41,11 @@
5.20 theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
5.21 theory Auto_Prog imports Program Prog_Tac Tactical begin
5.22 theory ProgLang imports Prog_Expr Auto_Prog
5.23 - ML_file rewrite.sml
5.24 *) "ProgLang/ProgLang"
5.25 (*
5.26 theory MathEngBasic imports
5.27 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
5.28 + ML_file rewrite.sml
5.29 ML_file "calc-tree-elem.sml"
5.30 ML_file model.sml
5.31 ML_file mstools.sml
6.1 --- a/src/Tools/isac/CalcElements/KEStore.thy Fri Apr 10 12:28:47 2020 +0200
6.2 +++ b/src/Tools/isac/CalcElements/KEStore.thy Fri Apr 10 14:46:55 2020 +0200
6.3 @@ -7,9 +7,9 @@
6.4 begin
6.5 ML_file libraryC.sml
6.6 ML_file theoryC.sml
6.7 -ML_file "unparseC.sml"
6.8 +ML_file unparseC.sml
6.9 ML_file "rule-def.sml"
6.10 -ML_file thmC.sml
6.11 +ML_file "thmC-def.sml"
6.12 ML_file "exec-def.sml"
6.13 ML_file "rewrite-order.sml"
6.14 ML_file rule.sml
7.1 --- a/src/Tools/isac/CalcElements/calcelems.sml Fri Apr 10 12:28:47 2020 +0200
7.2 +++ b/src/Tools/isac/CalcElements/calcelems.sml Fri Apr 10 14:46:55 2020 +0200
7.3 @@ -71,7 +71,7 @@
7.4 val lim_deriv: int Unsynchronized.ref
7.5 val isabthys: unit -> theory list
7.6 val partID': ThyC.theory' -> string
7.7 - val thm2guh: string * ThyC.thyID -> ThmC.thmID -> guh
7.8 + val thm2guh: string * ThyC.thyID -> ThmC_Def.thmID -> guh
7.9 val rls2guh: string * ThyC.thyID -> Rule_Set.identifier -> guh
7.10 val theID2guh: theID -> guh
7.11 type pbt_ = string * (term * term)
8.1 --- a/src/Tools/isac/CalcElements/error-fill-def.sml Fri Apr 10 12:28:47 2020 +0200
8.2 +++ b/src/Tools/isac/CalcElements/error-fill-def.sml Fri Apr 10 14:46:55 2020 +0200
8.3 @@ -33,7 +33,7 @@
8.4 do not match (which reflects student's error).
8.5 fillpatterns are stored with these thms. *)
8.6 fun errpat2str (id, tms, thms) =
8.7 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms2str tms ^ ",\n" ^ ThmC.thms2str thms
8.8 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms2str tms ^ ",\n" ^ ThmC_Def.thms2str thms
8.9 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
8.10
8.11 (* for (at least) 2 kinds of access:
9.1 --- a/src/Tools/isac/CalcElements/rule.sml Fri Apr 10 12:28:47 2020 +0200
9.2 +++ b/src/Tools/isac/CalcElements/rule.sml Fri Apr 10 14:46:55 2020 +0200
9.3 @@ -57,7 +57,7 @@
9.4 | eq_rule _ = false;
9.5
9.6 fun rule2str Rule_Def.Erule = "Erule"
9.7 - | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC.string_of_thmI thm ^ ")"
9.8 + | rule2str (Rule_Def.Thm (str, thm)) = "Thm (\"" ^ str ^ "\"," ^ ThmC_Def.string_of_thmI thm ^ ")"
9.9 | rule2str (Rule_Def.Num_Calc (str, _)) = "Num_Calc (\"" ^ str ^ "\",fn)"
9.10 | rule2str (Rule_Def.Cal1 (str, _)) = "Cal1 (\"" ^ str ^ "\",fn)"
9.11 | rule2str (Rule_Def.Rls_ rls) = "Rls_ (\"" ^ id_rls rls ^ "\")";
10.1 --- a/src/Tools/isac/CalcElements/termC.sml Fri Apr 10 12:28:47 2020 +0200
10.2 +++ b/src/Tools/isac/CalcElements/termC.sml Fri Apr 10 14:46:55 2020 +0200
10.3 @@ -8,6 +8,8 @@
10.4 signature TERM_ISAC =
10.5 sig
10.6 val empty: term
10.7 + type as_string
10.8 +
10.9 datatype lrd = D | L | R
10.10 type path
10.11 val string_of_path: path -> string
10.12 @@ -111,6 +113,7 @@
10.13 (**)
10.14
10.15 val empty = UnparseC.e_term
10.16 +type as_string = UnparseC.term_as_string
10.17
10.18 datatype lrd = L (*t1 in "t1$t2"*)
10.19 | R (*t2 in "t1$t2"*) | D; (*b in Abs(_,_,b*)
11.1 --- a/src/Tools/isac/CalcElements/theoryC.sml Fri Apr 10 12:28:47 2020 +0200
11.2 +++ b/src/Tools/isac/CalcElements/theoryC.sml Fri Apr 10 14:46:55 2020 +0200
11.3 @@ -2,8 +2,7 @@
11.4 Author: Walther Neuper
11.5 (c) due to copyright terms
11.6
11.7 -TODO: use "ThyC" for renaming identifiers.
11.8 -Probably this structure can be dropped due to improvements of Isabelle.
11.9 +Probably this structure can be dropped due to improved reflection in Isabelle.
11.10 *)
11.11 signature THEORY_ISAC =
11.12 sig
11.13 @@ -39,16 +38,10 @@
11.14 (* Since Isabelle2017 sessions in theory identifiers are enforced.
11.15 However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
11.16 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
11.17 +
11.18 fun thy2ctxt' thy' = Proof_Context.init_global (Thy_Info_get_theory thy');(*FIXXXME thy-ctxt*)
11.19 fun thy2ctxt thy = Proof_Context.init_global thy;(*FIXXXME thy-ctxt*)
11.20 fun Isac _ = Proof_Context.theory_of (thy2ctxt' "Isac_Knowledge"); (*@{theory "Isac_Knowledge"}*)
11.21 -(*ad thm':
11.22 - there are two kinds of theorems ...
11.23 - (1) known by isabelle
11.24 - (2) not known, eg. calc_thm, instantiated rls
11.25 - the latter have a thmid "#..."
11.26 - and thus outside isa we ALWAYS transport both (thmID, ThmC.string_of_thmI)
11.27 - and have a special assoc_thm / assoc_rls in this interface *)
11.28 type thyID = string; (* WN.3.11.03 TODO: replace domID with thyID*)
11.29 type domID = string; (* domID ^".thy" = theory' WN.101011 replace by thyID*)
11.30 type theory' = string; (* = domID ^".thy" WN.101011 ABOLISH !*)
11.31 @@ -62,7 +55,6 @@
11.32 fun thyID2theory' (thyID:thyID) = thyID;
11.33 fun theory'2thyID (theory':theory') = theory';
11.34
11.35 -
11.36 fun thyID_of_derivation_name dn = hd (space_explode "." dn);
11.37
11.38 (**)end(**)
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/Tools/isac/CalcElements/thmC-def.sml Fri Apr 10 14:46:55 2020 +0200
12.3 @@ -0,0 +1,96 @@
12.4 +(* Title: CalcElements/thmC-def.sml
12.5 + Author: Walther Neuper
12.6 + (c) due to copyright terms
12.7 +
12.8 +Probably this structure can be dropped due to improved reflection in Isabelle.
12.9 +*)
12.10 +signature THEOREM_ISAC_DEF =
12.11 +sig
12.12 + type thm'
12.13 + type thm''
12.14 + eqtype thmID
12.15 +
12.16 + val id_of_thm: Rule_Def.rule -> string
12.17 + val string_of_thmI: thm -> string
12.18 + val thmID_of_derivation_name: string -> string
12.19 + val thmID_of_derivation_name': thm -> string
12.20 + val thm''_of_thm: thm -> thm''
12.21 + val thm_of_thm: Rule_Def.rule -> thm
12.22 +
12.23 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
12.24 + val thm2str: thm -> string
12.25 + val thms2str : thm list -> string
12.26 + val string_of_thm': theory -> thm -> string
12.27 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
12.28 + val string_of_thm: thm -> string
12.29 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
12.30 +end
12.31 +
12.32 +(**)
12.33 +structure ThmC_Def(**): THEOREM_ISAC_DEF(**) =
12.34 +struct
12.35 +(**)
12.36 +
12.37 +(* TODO CLEANUP Thm:
12.38 +Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
12.39 + (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC_Def.string_of_thmI
12.40 +thmID : type for data from user input + program
12.41 +thmDeriv : type for thy_hierarchy ONLY
12.42 +obsolete types : thm' (SEE "ad thm'"), thm''.
12.43 +revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
12.44 +activate : thmID_of_derivation_name'
12.45 +*)
12.46 +type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
12.47 +(*
12.48 + ad thm': there are two kinds of theorems ...
12.49 + (1) defined in isabelle
12.50 + (2) not known, eg. calc_thm, instantiated rls
12.51 + the latter have a thmid "#..."
12.52 + and thus outside isa we ALWAYS transport both (thmID, ThmC_Def.string_of_thmI)
12.53 + and have a special assoc_thm / assoc_rls in this interface
12.54 +*)
12.55 +type thm' = thmID * UnparseC.term_as_string;(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
12.56 +val thm'2xml : int -> ThmC_Def.thm' -> Celem.xml
12.57 +val assoc_thm': theory -> ThmC_Def.thm' -> thm
12.58 +| Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
12.59 +*)
12.60 +(* tricky combination of (string, term) for theorems in Isac:
12.61 + * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
12.62 + by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
12.63 + * case 2 "sym_..": Global_Theory.get_thm..RS sym
12.64 + * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
12.65 + from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
12.66 +*)
12.67 +type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
12.68 +
12.69 +fun thm2str thm =
12.70 + let
12.71 + val t = Thm.prop_of thm
12.72 + val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
12.73 + val ctxt' = Config.put show_markup false ctxt
12.74 + in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
12.75 +fun thms2str thms = (strs2str o (map thm2str)) thms
12.76 +
12.77 +(*check for [.] as caused by "fun assoc_thm'"*)
12.78 +fun string_of_thm thm = UnparseC.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
12.79 +fun string_of_thm' thy thm = UnparseC.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)
12.80 +fun string_of_thmI thm =
12.81 + let
12.82 + val str = (de_quote o string_of_thm) thm
12.83 + val (a, b) = split_nlast (5, Symbol.explode str)
12.84 + in
12.85 + case b of
12.86 + [" ", " ","[", ".", "]"] => implode a
12.87 + | _ => str
12.88 + end
12.89 +
12.90 +fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
12.91 + | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
12.92 +
12.93 +fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
12.94 +fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
12.95 +fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
12.96 + | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
12.97 +fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
12.98 +
12.99 +(**)end(**)
13.1 --- a/src/Tools/isac/CalcElements/thmC.sml Fri Apr 10 12:28:47 2020 +0200
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,97 +0,0 @@
13.4 -(* Title: CalcElements/thmC.sml
13.5 - Author: Walther Neuper
13.6 - (c) due to copyright terms
13.7 -
13.8 -TODO: use "ThmC" for renaming identifiers.
13.9 -Probably this structure can be dropped due to improvements of Isabelle.
13.10 -*)
13.11 -signature THEOREM_ISAC =
13.12 -sig
13.13 -(*datatype T = Rule_Def.Thm ..ERROR: cannot get out from Rule_Def.rule*)
13.14 -
13.15 -(*/------- to ThmC.sml ------\*)
13.16 - eqtype thmID
13.17 - type thm'
13.18 - type thm''
13.19 -
13.20 - val thmID_of_derivation_name: string -> string
13.21 - val thmID_of_derivation_name': thm -> string
13.22 - val thm''_of_thm: thm -> thm''
13.23 - val thm_of_thm: Rule_Def.rule -> thm
13.24 -
13.25 - val string_of_thmI: thm -> string
13.26 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
13.27 - val thm2str: thm -> string
13.28 - val thms2str : thm list -> string
13.29 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
13.30 - val string_of_thm: thm -> string
13.31 - val string_of_thm': theory -> thm -> string
13.32 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
13.33 -(*/------- to ThmC.sml ------\*)
13.34 - val id_of_thm: Rule_Def.rule -> string
13.35 -(*\------- to ThmC.sml ------/*)
13.36 -end
13.37 -
13.38 -(**)
13.39 -structure ThmC(**): THEOREM_ISAC(**) =
13.40 -struct
13.41 -(**)
13.42 -
13.43 -(*datatype T = Rule_Def.Thm ..ERROR: cannot get out from Rule_Def.rule*)
13.44 -
13.45 -(* TODO CLEANUP Thm:
13.46 -Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
13.47 - (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI
13.48 -thmID : type for data from user input + program
13.49 -thmDeriv : type for thy_hierarchy ONLY
13.50 -obsolete types : thm' (SEE "ad thm'"), thm''.
13.51 -revise funs : id_of_thm, thm_of_thm, rep_thm_G', eq_thmI, eq_thmI', thm''_of_thm thm.
13.52 -activate : thmID_of_derivation_name'
13.53 -*)
13.54 -type thmID = string; (* identifier for a thm (the shortest possible identifier) *)
13.55 -type thm' = thmID * UnparseC.cterm';(*WN060610 deprecated in favour of thm''; WN180324: used in TODO review:
13.56 -val thm'2xml : int -> ThmC.thm' -> Celem.xml
13.57 -val assoc_thm': theory -> ThmC.thm' -> thm
13.58 -| Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
13.59 -*)
13.60 -(* tricky combination of (string, term) for theorems in Isac:
13.61 - * case 1 general: frontend + lucin, e.g. applicable_in..Rewrite: (thmID, _) --> (thmID, thm)
13.62 - by Global_Theory.get_thm, special cases ("add_commute",..) see convert_metaview_to_thmid.
13.63 - * case 2 "sym_..": Global_Theory.get_thm..RS sym
13.64 - * case 3 ad-hoc thm "#..." mk_thm from ad-hoc term (numerals only) in calculate_:
13.65 - from applicable_in..Calculate: opstr --calculate_/adhoc_thm--> (thmID, thm)
13.66 -*)
13.67 -type thm'' = thmID * thm; (* only for transport via libisabelle isac-java <--- ME *)
13.68 -
13.69 -fun thm2str thm =
13.70 - let
13.71 - val t = Thm.prop_of thm
13.72 - val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))
13.73 - val ctxt' = Config.put show_markup false ctxt
13.74 - in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
13.75 -fun thms2str thms = (strs2str o (map thm2str)) thms
13.76 -
13.77 -(*check for [.] as caused by "fun assoc_thm'"*)
13.78 -fun string_of_thm thm = UnparseC.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)
13.79 -fun string_of_thm' thy thm = UnparseC.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)
13.80 -fun string_of_thmI thm =
13.81 - let
13.82 - val str = (de_quote o string_of_thm) thm
13.83 - val (a, b) = split_nlast (5, Symbol.explode str)
13.84 - in
13.85 - case b of
13.86 - [" ", " ","[", ".", "]"] => implode a
13.87 - | _ => str
13.88 - end
13.89 -
13.90 -fun id_of_thm (Rule_Def.Thm (id, _)) = id (* TODO re-arrange code for rule2str *)
13.91 - | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
13.92 -
13.93 -fun thmID_of_derivation_name dn = last_elem (space_explode "." dn);
13.94 -fun thmID_of_derivation_name' thm = (thmID_of_derivation_name o Thm.get_name_hint) thm
13.95 -fun thyID_of_derivation_name dn = hd (space_explode "." dn);
13.96 -fun thm_of_thm (Rule_Def.Thm (_, thm)) = thm (* TODO re-arrange code for rule2str *)
13.97 - | thm_of_thm _ = raise ERROR ("thm_of_thm: uncovered case " (* ^ rule2str r *))
13.98 -fun thm''_of_thm thm = (thmID_of_derivation_name' thm, thm) : thm''
13.99 -
13.100 -(**)end(**)
14.1 --- a/src/Tools/isac/CalcElements/unparseC.sml Fri Apr 10 12:28:47 2020 +0200
14.2 +++ b/src/Tools/isac/CalcElements/unparseC.sml Fri Apr 10 14:46:55 2020 +0200
14.3 @@ -8,7 +8,7 @@
14.4
14.5 signature UNPARSE_ISAC =
14.6 sig
14.7 - eqtype cterm'
14.8 + eqtype term_as_string
14.9 type subst = (term * term) list
14.10 val e_term: term
14.11 (**)
14.12 @@ -47,7 +47,7 @@
14.13 struct
14.14 (**)
14.15
14.16 -type cterm' = string;
14.17 +type term_as_string = string;
14.18 type subst = (term * term) list;
14.19
14.20 fun term_to_string' ctxt t =
15.1 --- a/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 12:28:47 2020 +0200
15.2 +++ b/src/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 14:46:55 2020 +0200
15.3 @@ -21,7 +21,7 @@
15.4 val check_for :
15.5 term * term ->
15.6 term * (term * term) list -> (Error_Fill_Def.errpatID * term list * 'a list) list * Rule_Set.T -> Error_Fill_Def.errpatID option
15.7 - val rule2thm'' : Rule.rule -> ThmC.thm''
15.8 + val rule2thm'' : Rule.rule -> ThmC_Def.thm''
15.9 val rule2rls' : Rule.rule -> string
15.10 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
15.11 (* NONE *)
15.12 @@ -153,7 +153,7 @@
15.13 let
15.14 val thmDeriv = Thm.get_name_hint thm
15.15 val (part, thyID) = Rtools.thy_containing_thm thmDeriv
15.16 - val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
15.17 + val theID = [part, thyID, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
15.18 val fillpats = case Specify.get_the theID of
15.19 Celem.Hthm {fillpats, ...} => fillpats
15.20 | _ => error "get_fillpats: uncovered case of get_the"
15.21 @@ -228,7 +228,7 @@
15.22 do not match (which reflects student's error).
15.23 fillpatterns are stored with these thms. *)
15.24 fun errpat2str (id, tms, thms) =
15.25 - "(\"" ^ id ^ "\",\n" ^ UnparseC.terms2str tms ^ ",\n" ^ ThmC.thms2str thms
15.26 + "(\"" ^ id ^ "\",\n" ^ UnparseC.terms2str tms ^ ",\n" ^ ThmC_Def.thms2str thms
15.27 fun errpats2str errpats = (strs2str' o (map errpat2str)) errpats
15.28
15.29 (**)end(**)
15.30 \ No newline at end of file
16.1 --- a/src/Tools/isac/Interpret/rewtools.sml Fri Apr 10 12:28:47 2020 +0200
16.2 +++ b/src/Tools/isac/Interpret/rewtools.sml Fri Apr 10 14:46:55 2020 +0200
16.3 @@ -25,8 +25,8 @@
16.4 rhs: term * term, thm: Celem.guh, thminst: term, thyID: ThyC.thyID}
16.5 | EContThy
16.6 val guh2filename : Celem.guh -> Celem.filename
16.7 - val is_sym : ThmC.thmID -> bool
16.8 - val sym_drop : ThmC.thmID -> ThmC.thmID
16.9 + val is_sym : ThmC_Def.thmID -> bool
16.10 + val sym_drop : ThmC_Def.thmID -> ThmC_Def.thmID
16.11 val sym_rls : Rule_Set.T -> Rule_Set.T
16.12 val sym_rule : Rule.rule -> Rule.rule
16.13 val thms_of_rls : Rule_Set.T -> Rule.rule list
16.14 @@ -51,7 +51,7 @@
16.15 val trtas2str : (term * Rule.rule * (term * term list)) list -> string
16.16 val eq_Thm : Rule.rule * Rule.rule -> bool
16.17 val deriv2str : (term * Rule.rule * (term * term list)) list -> string
16.18 - val deriv_of_thm'' : ThmC.thm'' -> string
16.19 + val deriv_of_thm'' : ThmC_Def.thm'' -> string
16.20 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
16.21
16.22 (*----- unused code, kept as hints to design ideas ---------------------------------------------*)
16.23 @@ -218,7 +218,7 @@
16.24 val thm' = sym_thm thm
16.25 val thmID' = case Symbol.explode thmID of
16.26 "s" :: "y" :: "m" :: "_" :: id => implode id
16.27 - | "#" :: ":" :: _ => "#: " ^ ThmC.string_of_thmI thm'
16.28 + | "#" :: ":" :: _ => "#: " ^ ThmC_Def.string_of_thmI thm'
16.29 | _ => "sym_" ^ thmID
16.30 in Rule.Thm (thmID', thm') end
16.31 | sym_rule (Rule.Rls_ rls) = Rule.Rls_ (sym_rls rls) (* TODO? handle with interSteps ? *)
16.32 @@ -236,7 +236,7 @@
16.33 | eq_Thm (r1, r2) = error ("eq_Thm: called with '" ^ Rule.rule2str r1 ^ "' '" ^ Rule.rule2str r2 ^ "'")
16.34 fun distinct_Thm r = gen_distinct eq_Thm r
16.35
16.36 -fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC.id_of_thm thm))
16.37 +fun eq_Thms thmIDs thm = (member op = thmIDs (ThmC_Def.id_of_thm thm))
16.38 handle ERROR _ => false
16.39
16.40 fun thy_containing_thm thmDeriv =
16.41 @@ -349,7 +349,7 @@
16.42 Applicable.Appl (Tactic.Rewrite' (thy', ord', erls, _, _, f, (res,asm))) =>
16.43 ContThm
16.44 {thyID = ThyC.theory'2thyID thy',
16.45 - thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
16.46 + thm = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
16.47 applto = f, applat = TermC.empty, reword = ord',
16.48 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
16.49 result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
16.50 @@ -365,7 +365,7 @@
16.51 ContNOrew
16.52 {thyID = ThyC.theory'2thyID thy',
16.53 thm_rls =
16.54 - Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
16.55 + Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
16.56 applto = f}
16.57 end
16.58 | _ => error "context_thy..Rewrite: uncovered case 2")
16.59 @@ -382,7 +382,7 @@
16.60 ContThmInst
16.61 {thyID = ThyC.theory'2thyID thy',
16.62 thm =
16.63 - Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
16.64 + Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
16.65 bdvs = subst, thminst = thminst, applto = f, applat = TermC.empty, reword = ord',
16.66 asms = [](*asms ~~ asms'*), lhs = (TermC.empty, TermC.empty)(*(lhs, lhs')*), rhs = (TermC.empty, TermC.empty)(*(rhs, rhs')*),
16.67 result = res, resasms = asm, asmrls = Rule_Set.rls2str erls}
16.68 @@ -402,7 +402,7 @@
16.69 in
16.70 ContNOrewInst
16.71 {thyID = ThyC.theory'2thyID thy',
16.72 - thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv),
16.73 + thm_rls = Celem.thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv),
16.74 bdvs = subst, thminst = thminst, applto = f}
16.75 end
16.76 | _ => error "context_thy..Rewrite_Inst: uncovered case 4")
17.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Apr 10 12:28:47 2020 +0200
17.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Fri Apr 10 14:46:55 2020 +0200
17.3 @@ -50,12 +50,12 @@
17.4 subsubsection \<open>From rule-sets collect theorems, which have been taken from Isabelle\<close>
17.5 ML \<open>
17.6 val isacrlsthms = (*length = 460*)
17.7 - thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC.thmID * thm) list
17.8 + thms_of_rlss @{theory} (KEStore_Elems.get_rlss knowledge_parent) : (ThmC_Def.thmID * thm) list
17.9
17.10 val rlsthmsNOTisac = isacrlsthms (*length = 36*)
17.11 |> filter (fn (deriv, _) =>
17.12 member op= (map Context.theory_name isabthys') (ThyC.thyID_of_derivation_name deriv))
17.13 - : (ThmC.thmID * thm) list
17.14 + : (ThmC_Def.thmID * thm) list
17.15 \<close>
17.16
17.17 subsubsection \<open>Collect data in a (key, data) list and insert data into the tree\<close>
18.1 --- a/src/Tools/isac/Knowledge/Rational-WN.sml Fri Apr 10 12:28:47 2020 +0200
18.2 +++ b/src/Tools/isac/Knowledge/Rational-WN.sml Fri Apr 10 14:46:55 2020 +0200
18.3 @@ -195,7 +195,7 @@
18.4 case rul of
18.5 Rule.Thm (thmid, thm) =>
18.6 (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
18.7 - rls put_asm (ThmC.thm_of_thm rul) ct of
18.8 + rls put_asm (ThmC_Def.thm_of_thm rul) ct of
18.9 NONE => rew_once ruls asm ct apno thms
18.10 | SOME (ct',asm') =>
18.11 rew_once ruls (asm union asm') ct' Appl (rul::thms))
18.12 @@ -209,7 +209,7 @@
18.13 rls put_asm thm' ct;
18.14 val _ = if pairopt <> NONE then ()
18.15 else error("rewrite_set_, rewrite_ \""^
18.16 - (ThmC.string_of_thmI thm')^"\" \""^
18.17 + (ThmC_Def.string_of_thmI thm')^"\" \""^
18.18 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
18.19 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
18.20 val ruls = (#rules o Rule_Set.rep) ruless;
18.21 @@ -231,7 +231,7 @@
18.22 case rul of
18.23 Rule.Thm (thmid, thm) =>
18.24 (case rewrite_ thy ((snd o #rew_ord o Rule_Set.rep) ruless)
18.25 - rls put_asm (ThmC.thm_of_thm rul) ct of
18.26 + rls put_asm (ThmC_Def.thm_of_thm rul) ct of
18.27 NONE => rew_once ruls asm ct apno thms
18.28 | SOME (ct',asm') =>
18.29 rew_once ruls (asm union asm') ct' Appl (rul::thms))
18.30 @@ -245,7 +245,7 @@
18.31 rls put_asm thm' ct;
18.32 val _ = if pairopt <> NONE then ()
18.33 else error("rewrite_set_, rewrite_ \""^
18.34 - (ThmC.string_of_thmI thm')^"\" \""^
18.35 + (ThmC_Def.string_of_thmI thm')^"\" \""^
18.36 (Syntax.string_of_term (ThyC.thy2ctxt thy) ct)^"\" = NONE")
18.37 in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
18.38 val ruls = (#rules o Rule_Set.rep) ruless;
19.1 --- a/src/Tools/isac/Knowledge/Rational.thy Fri Apr 10 12:28:47 2020 +0200
19.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Fri Apr 10 14:46:55 2020 +0200
19.3 @@ -485,15 +485,15 @@
19.4 in (t, t'', [rs(*one in order to ease locate_rule*)], der) end;
19.5
19.6 fun locate_rule thy eval_rls ro [rs] t r =
19.7 - if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
19.8 + if member op = ((map (ThmC_Def.id_of_thm)) rs) (ThmC_Def.id_of_thm r)
19.9 then
19.10 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
19.11 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC_Def.thm_of_thm r) t;
19.12 in
19.13 case ropt of SOME ta => [(r, ta)]
19.14 | NONE => ((*tracing
19.15 - ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*) [])
19.16 + ("### locate_rule: rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*) [])
19.17 end
19.18 - else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
19.19 + else ((*tracing ("### locate_rule: " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
19.20 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
19.21
19.22 fun next_rule thy eval_rls ro [rs] t =
19.23 @@ -546,16 +546,16 @@
19.24 in (t, t'', [rs(*here only _ONE_*)], der) end;
19.25
19.26 fun locate_rule thy eval_rls ro [rs] t r =
19.27 - if member op = ((map (ThmC.id_of_thm)) rs) (ThmC.id_of_thm r)
19.28 + if member op = ((map (ThmC_Def.id_of_thm)) rs) (ThmC_Def.id_of_thm r)
19.29 then
19.30 - let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC.thm_of_thm r) t;
19.31 + let val ropt = Rewrite.rewrite_ thy ro eval_rls true (ThmC_Def.thm_of_thm r) t;
19.32 in
19.33 case ropt of
19.34 SOME ta => [(r, ta)]
19.35 | NONE =>
19.36 - ((*tracing ("### locate_rule: rewrite " ^ ThmC.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*)
19.37 + ((*tracing ("### locate_rule: rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*)
19.38 []) end
19.39 - else ((*tracing ("### locate_rule: " ^ ThmC.id_of_thm r ^ " not mem rrls");*) [])
19.40 + else ((*tracing ("### locate_rule: " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
19.41 | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
19.42
19.43 fun next_rule thy eval_rls ro [rs] t =
20.1 --- a/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri Apr 10 12:28:47 2020 +0200
20.2 +++ b/src/Tools/isac/MathEngBasic/MathEngBasic.thy Fri Apr 10 14:46:55 2020 +0200
20.3 @@ -7,6 +7,8 @@
20.4 imports "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript"
20.5 begin
20.6 (* removed all warnings here, only "handle _" remains *)
20.7 + ML_file thmC.sml
20.8 + ML_file rewrite.sml
20.9 ML_file "calc-tree-elem.sml"
20.10 ML_file model.sml
20.11 ML_file mstools.sml
21.1 --- a/src/Tools/isac/MathEngBasic/model.sml Fri Apr 10 12:28:47 2020 +0200
21.2 +++ b/src/Tools/isac/MathEngBasic/model.sml Fri Apr 10 14:46:55 2020 +0200
21.3 @@ -12,11 +12,11 @@
21.4 val oris2str : ori list -> string
21.5 val e_ori : ori
21.6 datatype item
21.7 - = Correct of UnparseC.cterm' | False of UnparseC.cterm' | Incompl of UnparseC.cterm' | Missing of UnparseC.cterm' | Superfl of string
21.8 + = Correct of TermC.as_string | False of TermC.as_string | Incompl of TermC.as_string | Missing of TermC.as_string | Superfl of string
21.9 | SyntaxE of string | TypeE of string
21.10 datatype itm_ = Cor of (term * (term list)) * (term * (term list))
21.11 - | Syn of UnparseC.cterm' | Typ of UnparseC.cterm' | Inc of (term * (term list)) * (term * (term list))
21.12 - | Sup of (term * (term list)) | Mis of (term * term) | Par of UnparseC.cterm'
21.13 + | Syn of TermC.as_string | Typ of TermC.as_string | Inc of (term * (term list)) * (term * (term list))
21.14 + | Sup of (term * (term list)) | Mis of (term * term) | Par of TermC.as_string
21.15 val itm_2str : itm_ -> string
21.16 val itm_2str_ : Proof.context -> itm_ -> string
21.17 type itm
21.18 @@ -255,13 +255,13 @@
21.19 Cor of (term * (* description *)
21.20 (term list)) * (* for list: elem-wise input *)
21.21 (term * (term list)) (* elem of penv ---- penv delayed to future *)
21.22 -| Syn of UnparseC.cterm'
21.23 -| Typ of UnparseC.cterm'
21.24 +| Syn of TermC.as_string
21.25 +| Typ of TermC.as_string
21.26 | Inc of (term * (term list)) * (term * (term list)) (*lists,
21.27 + init_pbl WN.11.03 FIXXME: empty penv .. bad; init_pbl should return Mis !!! *)
21.28 | Sup of (term * (term list)) (* user-input not found in pbt(+?oris?11.03)*)
21.29 | Mis of (term * term) (* after re-specification pbt-item not found in pbl: only dsc, pid_*)
21.30 -| Par of UnparseC.cterm'; (* internal state from fun parsitm *)
21.31 +| Par of TermC.as_string; (* internal state from fun parsitm *)
21.32
21.33 type vats = int list; (* variants in formalizations *)
21.34
21.35 @@ -374,13 +374,13 @@
21.36
21.37 (* for _output_ of the items of a Model *)
21.38 datatype item =
21.39 - Correct of UnparseC.cterm' (* labels a correct formula (type cterm') *)
21.40 + Correct of TermC.as_string (* labels a correct formula (type cterm') *)
21.41 | SyntaxE of string (**)
21.42 | TypeE of string (**)
21.43 - | False of UnparseC.cterm' (* WN050618 notexistent in itm_: only used in Where *)
21.44 - | Incompl of UnparseC.cterm' (**)
21.45 + | False of TermC.as_string (* WN050618 notexistent in itm_: only used in Where *)
21.46 + | Incompl of TermC.as_string (**)
21.47 | Superfl of string (**)
21.48 - | Missing of UnparseC.cterm';
21.49 + | Missing of TermC.as_string;
21.50 fun item2str (Correct s) ="Correct " ^ s
21.51 | item2str (SyntaxE s) ="SyntaxE " ^ s
21.52 | item2str (TypeE s) ="TypeE " ^ s
22.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
22.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 14:46:55 2020 +0200
22.3 @@ -0,0 +1,342 @@
22.4 +(* isac's rewriter
22.5 + (c) Walther Neuper 2000
22.6 +*)
22.7 +
22.8 +signature REWRITE =
22.9 + sig
22.10 +(*/------- to ThmC_Def -------\*)
22.11 + val assoc_thm': theory -> ThmC_Def.thm' -> thm
22.12 + val assoc_thm'': theory -> ThmC_Def.thmID -> thm
22.13 +(*\------- to ThmC_Def -------/*)
22.14 + val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
22.15 + val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
22.16 + val eval_prog_expr: theory -> Rule_Set.T -> term -> term
22.17 + val eval_true_: theory -> Rule_Set.T -> term -> bool
22.18 + val eval_true: theory -> term list -> Rule_Set.T -> bool
22.19 + val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
22.20 + -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
22.21 + val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
22.22 + term -> (term * term list) option
22.23 + val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
22.24 + -> (term * term) list -> thm -> term -> (term * term list) option
22.25 + val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
22.26 + val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
22.27 + val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
22.28 + -> term -> (term * term list) option
22.29 +(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
22.30 + (* NONE *)
22.31 +(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
22.32 + val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
22.33 + Rule_Set.T -> bool -> thm -> term -> (term * term list) option
22.34 + val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
22.35 + val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
22.36 + val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
22.37 + val mk_thm: theory -> string -> thm
22.38 + val trace1: int -> string -> unit
22.39 +( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
22.40 + end
22.41 +
22.42 +(**)
22.43 +structure Rewrite(**): REWRITE(**) =
22.44 +struct
22.45 +(**)
22.46 +
22.47 +exception NO_REWRITE;
22.48 +exception STOP_REW_SUB; (*WN050820 quick and dirty*)
22.49 +
22.50 +fun trace i str =
22.51 + if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
22.52 +fun trace1 i str =
22.53 + if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
22.54 +
22.55 +fun rewrite__ thy i bdv tless rls put_asm thm ct =
22.56 + let
22.57 + val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
22.58 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct
22.59 + in if rew then SOME (t', distinct asms) else NONE end
22.60 + (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
22.61 +and rew_sub thy i bdv tless rls put_asm lrd r t =
22.62 + (let
22.63 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
22.64 + (*?alternative Unify.matchers:
22.65 + http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
22.66 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
22.67 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
22.68 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
22.69 + val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
22.70 + then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.t2str thy r') else ()
22.71 + val (t'', p'') = (*conditional rewriting*)
22.72 + let
22.73 + val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
22.74 + in
22.75 + if nofalse
22.76 + then
22.77 + (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
22.78 + then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.ts2str thy p' ^
22.79 + " stored: " ^ UnparseC.ts2str thy simpl_p')
22.80 + else();
22.81 + (t',simpl_p')) (* uncond.rew. from above*)
22.82 + else
22.83 + (if ! Celem.trace_rewrite andalso i < ! Celem.depth
22.84 + then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.ts2str thy p')
22.85 + else();
22.86 + raise STOP_REW_SUB (* don't go into subterms of cond *))
22.87 + end
22.88 + in
22.89 + if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
22.90 + then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
22.91 + then tracing (idt"#"i ^ " not: \"" ^ UnparseC.t2str thy t ^ "\" > \"" ^ UnparseC.t2str thy t' ^ "\"")
22.92 + else ();
22.93 + raise NO_REWRITE)
22.94 + else (t'', p'', [], true)
22.95 + end
22.96 + ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
22.97 + (case t of
22.98 + Const(s,T) => (Const(s,T),[],lrd,false)
22.99 + | Free(s,T) => (Free(s,T),[],lrd,false)
22.100 + | Var(n,T) => (Var(n,T),[],lrd,false)
22.101 + | Bound i => (Bound i,[],lrd,false)
22.102 + | Abs(s,T,body) =>
22.103 + let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
22.104 + in (Abs(s, T, t'), asms, [], rew) end
22.105 + | t1 $ t2 =>
22.106 + let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
22.107 + in
22.108 + if rew2 then (t1 $ t2', asm2, lrd, true)
22.109 + else
22.110 + let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
22.111 + in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
22.112 + end)
22.113 +and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
22.114 + if asms = [@{term True}] orelse asms = [] then ([], true)
22.115 + else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
22.116 + if asms = [@{term False}] then ([], false)
22.117 + else
22.118 + let
22.119 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
22.120 + | chk indets (a :: asms) =
22.121 + (case rewrite__set_ thy (i + 1) false bdv rls a of
22.122 + NONE => (chk (indets @ [a]) asms)
22.123 + | SOME (t, a') =>
22.124 + if t = @{term True} then (chk (indets @ a') asms)
22.125 + else if t = @{term False} then ([], false)
22.126 + (*asm false .. thm not applied ^^^; continue until False vvv*)
22.127 + else chk (indets @ [t] @ a') asms);
22.128 + in chk [] asms end
22.129 +and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
22.130 + error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.t2str thy t ^ "'")
22.131 + | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
22.132 + let
22.133 + val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.t2str thy t)
22.134 + val (t', asm, rew) = app_rev thy (i + 1) rrls t
22.135 + in if rew then SOME (t', distinct asm) else NONE end
22.136 + | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
22.137 + let
22.138 + (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
22.139 + datatype switch = Appl | Noap;
22.140 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
22.141 + | rew_once ruls asm ct Appl [] =
22.142 + (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
22.143 + | Rule_Set.Seqence _ => (ct, asm)
22.144 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rls2str rls ^ "\""))
22.145 + | rew_once ruls asm ct apno (rul :: thms) =
22.146 + case rul of
22.147 + Rule.Thm (thmid, thm) =>
22.148 + (trace1 i (" try thm: \"" ^ thmid ^ "\"");
22.149 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
22.150 + ((#erls o Rule_Set.rep) rls) put_asm thm ct of
22.151 + NONE => rew_once ruls asm ct apno thms
22.152 + | SOME (ct', asm') =>
22.153 + (trace1 i (" rewrites to: \"" ^ UnparseC.t2str thy ct' ^ "\"");
22.154 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
22.155 + (* once again try the same rule, e.g. associativity against "()"*)
22.156 + | Rule.Num_Calc (cc as (op_, _)) =>
22.157 + let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
22.158 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
22.159 + in case Num_Calc.adhoc_thm thy cc ct of
22.160 + NONE => rew_once ruls asm ct apno thms
22.161 + | SOME (_, thm') =>
22.162 + let
22.163 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
22.164 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
22.165 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
22.166 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
22.167 + val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
22.168 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
22.169 + end
22.170 + | Rule.Cal1 (cc as (op_, _)) =>
22.171 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
22.172 + val ct = TermC.uminus_to_string ct
22.173 + in case Num_Calc.adhoc_thm1_ thy cc ct of
22.174 + NONE => (ct, asm)
22.175 + | SOME (_, thm') =>
22.176 + let
22.177 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
22.178 + ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
22.179 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
22.180 + ThmC_Def.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
22.181 + val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
22.182 + in the pairopt end
22.183 + end
22.184 + | Rule.Rls_ rls' =>
22.185 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
22.186 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
22.187 + | NONE => rew_once ruls asm ct apno thms)
22.188 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
22.189 + val ruls = (#rules o Rule_Set.rep) rls;
22.190 + val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
22.191 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
22.192 + in if ct = ct' then NONE else SOME (ct', distinct asm') end
22.193 +(*-------------------------------------------------------------*)
22.194 +and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
22.195 + let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
22.196 + fun chk_prepat _ _ [] _ = true
22.197 + | chk_prepat thy erls prepat t =
22.198 + let
22.199 + fun chk (pres, pat) =
22.200 + (let
22.201 + val subst: Type.tyenv * Envir.tenv =
22.202 + Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
22.203 + in
22.204 + snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
22.205 + end) handle _ (*TODO Pattern.MATCH*) => false
22.206 + fun scan_ _ [] = false
22.207 + | scan_ f (pp :: pps) =
22.208 + if f pp then true else scan_ f pps;
22.209 + in scan_ chk prepat end;
22.210 + (* apply the normal_form of a rev-set *)
22.211 + fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
22.212 + if chk_prepat thy erls prepat t then normal_form t else NONE
22.213 + | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.rls2str r ^ "\"");
22.214 + val opt = app_rev' thy rrls t
22.215 + in
22.216 + case opt of
22.217 + SOME (t', asm) => (t', asm, true)
22.218 + | NONE => app_sub thy i rrls t
22.219 + end
22.220 +and app_sub thy i rrls t = (* apply an Rrls to subterms *)
22.221 + case t of
22.222 + Const (s, T) => (Const(s, T), [], false)
22.223 + | Free (s, T) => (Free(s, T), [], false)
22.224 + | Var (n, T) => (Var(n, T), [], false)
22.225 + | Bound i => (Bound i, [], false)
22.226 + | Abs (s, T, body) =>
22.227 + let val (t', asm, rew) = app_rev thy i rrls body
22.228 + in (Abs(s, T, t'), asm, rew) end
22.229 + | t1 $ t2 =>
22.230 + let val (t2', asm2, rew2) = app_rev thy i rrls t2
22.231 + in
22.232 + if rew2 then (t1 $ t2', asm2, true)
22.233 + else
22.234 + let val (t1', asm1, rew1) = app_rev thy i rrls t1
22.235 + in if rew1 then (t1' $ t2, asm1, true)
22.236 + else (t1 $ t2, [], false)
22.237 + end
22.238 + end;
22.239 +
22.240 +(* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
22.241 +fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
22.242 +
22.243 +(* rewriting without internal argument [] *)
22.244 +fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
22.245 +fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
22.246 +
22.247 +(* variants of rewrite; TODO del. put_asm *)
22.248 +fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
22.249 + rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
22.250 +fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
22.251 +
22.252 +(* given a list of equalities (lhs = rhs) and a term,
22.253 + replace all occurrences of lhs in the term with rhs;
22.254 + thus the order or equalities matters: put variables in lhs first. *)
22.255 +fun rewrite_terms_ thy ord erls equs t =
22.256 + let
22.257 + fun rew_ (t', asm') [] _ = (t', asm')
22.258 + | rew_ (t', asm') (rules as r::rs) t =
22.259 + let
22.260 + val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
22.261 + in
22.262 + if rew
22.263 + then rew_ (t'', asm' @ asm'') rules t''
22.264 + else rew_ (t', asm') rs t'
22.265 + end
22.266 + val (t'', asm'') = rew_ (TermC.empty, []) equs t
22.267 + in if t'' = TermC.empty then NONE else SOME (t'', asm'')
22.268 + end;
22.269 +
22.270 +(* search ct for adjacent numerals and calculate them by operator isa_fn *)
22.271 +fun calculate_ thy isa_fn ct =
22.272 + let val ct = TermC.uminus_to_string ct
22.273 + in case Num_Calc.adhoc_thm thy isa_fn ct of
22.274 + NONE => NONE
22.275 + | SOME (thmID, thm) =>
22.276 + (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
22.277 + SOME (rew, _) => rew
22.278 + | NONE => raise ERROR ""
22.279 + in SOME (rew, (thmID, thm)) end)
22.280 + handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
22.281 + end;
22.282 +
22.283 +(* Thm.make_thm added to Pure/thm.ML *)
22.284 +fun mk_thm thy str =
22.285 + let
22.286 + val t = (Thm.term_of o the o (TermC.parse thy)) str
22.287 + val t' = case t of
22.288 + Const ("Pure.imp", _) $ _ $ _ => t
22.289 + | _ => HOLogic.Trueprop $ t
22.290 + in Thm.make_thm (Thm.global_cterm_of thy t') end;
22.291 +
22.292 +(*/------- to ThmC_Def -------\*)
22.293 +(*
22.294 + "metaview" as seen from programs and from user input;
22.295 + both are parsed as terms by the function package.
22.296 +*)
22.297 +fun convert_metaview_to_thmid thy thmid =
22.298 + let val thmid' = case thmid of
22.299 + "add_commute" => "add.commute"
22.300 + | "mult_commute" => "mult.commute"
22.301 + | "add_left_commute" => "add.left_commute"
22.302 + | "mult_left_commute" => "mult.left_commute"
22.303 + | "add_assoc" => "add.assoc"
22.304 + | "mult_assoc" => "mult.assoc"
22.305 + | _ => thmid
22.306 + in (Global_Theory.get_thm thy) thmid' end;
22.307 +
22.308 +(* get the theorem associated with the xstring-identifier;
22.309 + if the identifier starts with "sym_" then swap lhs = rhs around =
22.310 + (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC_Def.string_of_thmI);
22.311 + identifiers starting with "#" come from Num_Calc and
22.312 + get a hand-made theorem (containing numerals only) *)
22.313 +fun assoc_thm'' thy thmid =
22.314 + case Symbol.explode thmid of
22.315 + "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
22.316 + | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
22.317 + | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
22.318 + | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str
22.319 +fun assoc_thm' thy (thmid, ct') =
22.320 + (case Symbol.explode thmid of
22.321 + "s"::"y"::"m"::"_"::id =>
22.322 + if hd id = "#"
22.323 + then mk_thm thy ct'
22.324 + else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
22.325 + | id =>
22.326 + if hd id = "#"
22.327 + then mk_thm thy ct'
22.328 + else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
22.329 + ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
22.330 + raise ERROR
22.331 + ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
22.332 +(*\------- to ThmC_Def -------/*)
22.333 +
22.334 +
22.335 +fun eval_prog_expr thy srls t =
22.336 + let val rew = rewrite_set_ thy false srls t;
22.337 + in case rew of SOME (res,_) => res | NONE => t end;
22.338 +
22.339 +fun eval_true_ _ _ (Const ("HOL.True",_)) = true
22.340 + | eval_true_ thy rls t =
22.341 + case rewrite_set_ thy false rls t of
22.342 + SOME (Const ("HOL.True",_),_) => true
22.343 + | _ => false;
22.344 +
22.345 +end
22.346 \ No newline at end of file
23.1 --- a/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 10 12:28:47 2020 +0200
23.2 +++ b/src/Tools/isac/MathEngBasic/specification-elems.sml Fri Apr 10 14:46:55 2020 +0200
23.3 @@ -16,21 +16,21 @@
23.4 type subst' (* substitution in isac-programs; rename subst_prog [(bdv, x)] *)
23.5 (*type subst for rewriting, in Rule (+?Isabelle); rename subst_rew [(bools, x)] *)
23.6 (* TODO use these types in functions below and elsewhere; rename below according to types *)
23.7 - val subst'_to_sube : subst' -> UnparseC.cterm' list (* e.g. rename to subst_user_of_prog *)
23.8 + val subst'_to_sube : subst' -> TermC.as_string list (* e.g. rename to subst_user_of_prog *)
23.9 val subst_to_subst' : UnparseC.subst -> subst'
23.10 val subst'_to_subst : subst' -> (term * term) list
23.11 - val sube2str : UnparseC.cterm' list -> string
23.12 - val sube2subst : theory -> UnparseC.cterm' list -> (term * term) list
23.13 - val sube2subte : UnparseC.cterm' list -> term list
23.14 - val subs2subst : theory -> UnparseC.cterm' list -> (term * term) list
23.15 - val subst2sube : (term * term) list -> UnparseC.cterm' list (* for datatypes.sml *)
23.16 - val subst2subs : (term * term) list -> UnparseC.cterm' list
23.17 + val sube2str : TermC.as_string list -> string
23.18 + val sube2subst : theory -> TermC.as_string list -> (term * term) list
23.19 + val sube2subte : TermC.as_string list -> term list
23.20 + val subs2subst : theory -> TermC.as_string list -> (term * term) list
23.21 + val subst2sube : (term * term) list -> TermC.as_string list (* for datatypes.sml *)
23.22 + val subst2subs : (term * term) list -> TermC.as_string list
23.23 val subst2subs' : (term * term) list -> (string * string) list
23.24 - val subte2sube : term list -> UnparseC.cterm' list
23.25 + val subte2sube : term list -> TermC.as_string list
23.26
23.27 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
23.28 val e_fmz : fmz_ * Celem.spec (* for datatypes.sml *)
23.29 - val e_sube : UnparseC.cterm' list
23.30 + val e_sube : TermC.as_string list
23.31 val e_subs : string list
23.32 val subte2subst : term list -> (term * term) list
23.33 (*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
23.34 @@ -49,7 +49,7 @@
23.35 (strs2str o
23.36 (map (
23.37 Celem.linefeed o pair2str o (apsnd UnparseC.term2str) o (apfst UnparseC.term2str)))) s;
23.38 -type fmz_ = UnparseC.cterm' list;
23.39 +type fmz_ = TermC.as_string list;
23.40 (* a formalization of an example contains data
23.41 sufficient for mechanically finding the solution for the example.
23.42 FIXME.WN051014: dont store fmz = (_,spec) in the PblObj, this is done in origin *)
23.43 @@ -59,13 +59,13 @@
23.44 type result = term * term list
23.45 fun res2str (t, ts) = pair2str (UnparseC.term2str t, UnparseC.terms2str ts); (* for tests only *)
23.46
23.47 -type subs = UnparseC.cterm' list; (* substitution as seen by learner in tactics, in programs, etc.
23.48 +type subs = TermC.as_string list; (* substitution as seen by learner in tactics, in programs, etc.
23.49 questionable design. rename to stubst_user *)
23.50 val e_subs = ["(''bdv'', x)"]; (* for tests only *)
23.51
23.52 (* argument type of tac Rewrite_Inst *)
23.53 -type sube = UnparseC.cterm' list; (* = subs. delete *)
23.54 -val e_sube = []: UnparseC.cterm' list; (* for tests only *)
23.55 +type sube = TermC.as_string list; (* = subs. delete *)
23.56 +val e_sube = []: TermC.as_string list; (* for tests only *)
23.57 fun sube2str s = strs2str s;
23.58
23.59 type subte = term list; (* _sub_stitution as _t_erms of _e_qualities: revise ! *)
23.60 @@ -77,7 +77,7 @@
23.61 |> HOLogic.dest_list
23.62 |> map HOLogic.dest_prod
23.63 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term2str e2))
23.64 - |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): UnparseC.cterm' list)
23.65 + |> map (fn (e1, e2) => "(''" ^ e1 ^ "'', " ^ e2 ^ ")"): TermC.as_string list)
23.66 handle TERM _ => raise TERM ("subst'_to_sube: wrong argument ", [sub])
23.67 fun subst_to_subst' subst = subst
23.68 |> map (apfst TermC.free2str)
24.1 --- a/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 12:28:47 2020 +0200
24.2 +++ b/src/Tools/isac/MathEngBasic/tactic.sml Fri Apr 10 14:46:55 2020 +0200
24.3 @@ -10,8 +10,8 @@
24.4 signature TACTIC =
24.5 sig
24.6 datatype T =
24.7 - Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
24.8 - | Add_Relation' of UnparseC.cterm' * Model.itm list
24.9 + Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
24.10 + | Add_Relation' of TermC.as_string * Model.itm list
24.11 | Apply_Method' of Celem.metID * term option * Istate_Def.T * Proof.context
24.12
24.13 | Begin_Sequ' | Begin_Trans' of term
24.14 @@ -21,10 +21,10 @@
24.15 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
24.16
24.17 | CAScmd' of term
24.18 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
24.19 + | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
24.20 | Check_Postcond' of Celem.pblID * term
24.21 - | Check_elementwise' of term * UnparseC.cterm' * Selem.result
24.22 - | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
24.23 + | Check_elementwise' of term * TermC.as_string * Selem.result
24.24 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
24.25
24.26 | Derive' of Rule_Set.T
24.27 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
24.28 @@ -34,14 +34,14 @@
24.29 | Empty_Tac_
24.30 | Free_Solve'
24.31
24.32 - | Init_Proof' of UnparseC.cterm' list * Celem.spec
24.33 + | Init_Proof' of TermC.as_string list * Celem.spec
24.34 | Model_Problem' of Celem.pblID * Model.itm list * Model.itm list
24.35 | Or_to_List' of term * term
24.36 | Refine_Problem' of Celem.pblID * (Model.itm list * (bool * term) list)
24.37 | Refine_Tacitly' of Celem.pblID * Celem.pblID * ThyC.domID * Celem.metID * Model.itm list
24.38
24.39 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
24.40 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
24.41 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
24.42 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
24.43 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
24.44 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
24.45
24.46 @@ -61,8 +61,8 @@
24.47 val string_of: T -> string
24.48
24.49 datatype input =
24.50 - Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
24.51 - | Apply_Assumption of UnparseC.cterm' list
24.52 + Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
24.53 + | Apply_Assumption of TermC.as_string list
24.54 | Apply_Method of Celem.metID
24.55 (*/--- TODO: re-design ? -----------------------------------------------------------------\*)
24.56 | Begin_Sequ | Begin_Trans
24.57 @@ -71,11 +71,11 @@
24.58 | End_Sequ | End_Trans
24.59 | End_Ruleset | End_Subproblem | End_Intersect | End_Proof'
24.60 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
24.61 - | CAScmd of UnparseC.cterm'
24.62 + | CAScmd of TermC.as_string
24.63 | Calculate of string
24.64 | Check_Postcond of Celem.pblID
24.65 - | Check_elementwise of UnparseC.cterm'
24.66 - | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
24.67 + | Check_elementwise of TermC.as_string
24.68 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
24.69
24.70 | Derive of Rule_Set.identifier
24.71 | Detail_Set of Rule_Set.identifier
24.72 @@ -85,14 +85,14 @@
24.73 | Empty_Tac
24.74 | Free_Solve
24.75
24.76 - | Init_Proof of UnparseC.cterm' list * Celem.spec
24.77 + | Init_Proof of TermC.as_string list * Celem.spec
24.78 | Model_Problem
24.79 | Or_to_List
24.80 | Refine_Problem of Celem.pblID
24.81 | Refine_Tacitly of Celem.pblID
24.82
24.83 - | Rewrite of ThmC.thm''
24.84 - | Rewrite_Inst of Selem.subs * ThmC.thm''
24.85 + | Rewrite of ThmC_Def.thm''
24.86 + | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
24.87 | Rewrite_Set of Rule_Set.identifier
24.88 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
24.89
24.90 @@ -103,7 +103,7 @@
24.91
24.92 | Substitute of Selem.sube
24.93 | Tac of string
24.94 - | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
24.95 + | Take of TermC.as_string | Take_Inst of TermC.as_string
24.96 val input_to_string : input -> string
24.97 val tac2IDstr : input -> string
24.98 val is_empty : input -> bool
24.99 @@ -144,8 +144,8 @@
24.100 see 'type tac_' for the internal representation of tactics
24.101 *)
24.102 datatype input =
24.103 - Add_Find of UnparseC.cterm' | Add_Given of UnparseC.cterm' | Add_Relation of UnparseC.cterm'
24.104 - | Apply_Assumption of UnparseC.cterm' list
24.105 + Add_Find of TermC.as_string | Add_Given of TermC.as_string | Add_Relation of TermC.as_string
24.106 + | Apply_Assumption of TermC.as_string list
24.107 | Apply_Method of Celem.metID
24.108 (* creates an "istate" in PblObj.env; in case of "implicit_take"
24.109 creates a formula at ((lev_on o lev_dn) p, Frm) and in this "ppobj.loc"
24.110 @@ -159,11 +159,11 @@
24.111 | End_Sequ | End_Trans
24.112 | End_Ruleset | End_Subproblem (* WN0509 drop *) | End_Intersect | End_Proof'
24.113 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
24.114 - | CAScmd of UnparseC.cterm'
24.115 + | CAScmd of TermC.as_string
24.116 | Calculate of string
24.117 | Check_Postcond of Celem.pblID
24.118 - | Check_elementwise of UnparseC.cterm'
24.119 - | Del_Find of UnparseC.cterm' | Del_Given of UnparseC.cterm' | Del_Relation of UnparseC.cterm'
24.120 + | Check_elementwise of TermC.as_string
24.121 + | Del_Find of TermC.as_string | Del_Given of TermC.as_string | Del_Relation of TermC.as_string
24.122
24.123 | Derive of Rule_Set.identifier (* WN0509 drop *)
24.124 | Detail_Set of Rule_Set.identifier (* WN0509 drop *)
24.125 @@ -173,7 +173,7 @@
24.126 | Empty_Tac
24.127 | Free_Solve
24.128
24.129 - | Init_Proof of UnparseC.cterm' list * Celem.spec
24.130 + | Init_Proof of TermC.as_string list * Celem.spec
24.131 | Model_Problem
24.132 | Or_to_List
24.133 | Refine_Problem of Celem.pblID
24.134 @@ -183,8 +183,8 @@
24.135 because there all the thms are present with both (thmID, thm)
24.136 (where user-views can show both or only one of (thmID, thm)),
24.137 and thm is created from ThmID by assoc_thm'' when entering isabisac *)
24.138 - | Rewrite of ThmC.thm''
24.139 - | Rewrite_Inst of Selem.subs * ThmC.thm''
24.140 + | Rewrite of ThmC_Def.thm''
24.141 + | Rewrite_Inst of Selem.subs * ThmC_Def.thm''
24.142 | Rewrite_Set of Rule_Set.identifier
24.143 | Rewrite_Set_Inst of Selem.subs * Rule_Set.identifier
24.144
24.145 @@ -195,7 +195,7 @@
24.146
24.147 | Substitute of Selem.sube
24.148 | Tac of string (* WN0509 drop *)
24.149 - | Take of UnparseC.cterm' | Take_Inst of UnparseC.cterm'
24.150 + | Take of TermC.as_string | Take_Inst of TermC.as_string
24.151
24.152 fun input_to_string ma = case ma of
24.153 Init_Proof (ppc, spec) =>
24.154 @@ -334,8 +334,8 @@
24.155 TODO.WN161219: replace *every* cterm' by term
24.156 *)
24.157 datatype T =
24.158 - Add_Find' of UnparseC.cterm' * Model.itm list | Add_Given' of UnparseC.cterm' * Model.itm list
24.159 - | Add_Relation' of UnparseC.cterm' * Model.itm list
24.160 + Add_Find' of TermC.as_string * Model.itm list | Add_Given' of TermC.as_string * Model.itm list
24.161 + | Add_Relation' of TermC.as_string * Model.itm list
24.162 | Apply_Method' of (* creates the 1st step visible in a (sub-) comprising
24.163 * tactic Apply_Method metID
24.164 * formula term *)
24.165 @@ -351,14 +351,14 @@
24.166 | End_Ruleset' of term | End_Intersect' of term | End_Proof''
24.167 (*\--- TODO: re-design ? -----------------------------------------------------------------/*)
24.168 | CAScmd' of term
24.169 - | Calculate' of ThyC.theory' * string * term * (term * ThmC.thm')
24.170 + | Calculate' of ThyC.theory' * string * term * (term * ThmC_Def.thm')
24.171 | Check_Postcond' of Celem.pblID *
24.172 term (* returnvalue of program in solve *)
24.173 | Check_elementwise' of (* DEPRECATED, made idle for Calc.T in df00a2b5c4cc *)
24.174 term * (* (1) the current formula: [x=1,x=...] *)
24.175 string * (* (2) the pred from Check_elementwise *)
24.176 Selem.result (* (3) composed from (1) and (2): {x. pred} *)
24.177 - | Del_Find' of UnparseC.cterm' | Del_Given' of UnparseC.cterm' | Del_Relation' of UnparseC.cterm'
24.178 + | Del_Find' of TermC.as_string | Del_Given' of TermC.as_string | Del_Relation' of TermC.as_string
24.179
24.180 | Derive' of Rule_Set.T
24.181 | Detail_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
24.182 @@ -368,7 +368,7 @@
24.183 | Empty_Tac_
24.184 | Free_Solve'
24.185
24.186 - | Init_Proof' of UnparseC.cterm' list * Celem.spec
24.187 + | Init_Proof' of TermC.as_string list * Celem.spec
24.188 | Model_Problem' of (* first step in specifying *)
24.189 Celem.pblID * (* key into KEStore *)
24.190 Model.itm list * (* the 'untouched' pbl *)
24.191 @@ -381,8 +381,8 @@
24.192 ThyC.domID * (* from new pbt?! filled in specify *)
24.193 Celem.metID * (* from new pbt?! filled in specify *)
24.194 Model.itm list (* drop ! 9.03: remains [] for Model_Problem recognizing its activation *)
24.195 - | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC.thm'' * term * Selem.result
24.196 - | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC.thm'' * term * Selem.result
24.197 + | Rewrite' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * ThmC_Def.thm'' * term * Selem.result
24.198 + | Rewrite_Inst' of ThyC.theory' * Rewrite_Ord.rew_ord' * Rule_Set.T * bool * UnparseC.subst * ThmC_Def.thm'' * term * Selem.result
24.199 | Rewrite_Set' of ThyC.theory' * bool * Rule_Set.T * term * Selem.result
24.200 | Rewrite_Set_Inst' of ThyC.theory' * bool * UnparseC.subst * Rule_Set.T * term * Selem.result
24.201
25.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
25.2 +++ b/src/Tools/isac/MathEngBasic/thmC.sml Fri Apr 10 14:46:55 2020 +0200
25.3 @@ -0,0 +1,18 @@
25.4 +(* Title: CalcElements/thmC.sml
25.5 + Author: Walther Neuper
25.6 + (c) due to copyright terms
25.7 +
25.8 +Probably this structure can be dropped due to improved reflection in Isabelle.
25.9 +*)
25.10 +signature THEOREM_ISAC =
25.11 +sig
25.12 +
25.13 +end
25.14 +
25.15 +(**)
25.16 +structure ThmC(**): THEOREM_ISAC(**) =
25.17 +struct
25.18 +(**)
25.19 +
25.20 +
25.21 +end
26.1 --- a/src/Tools/isac/ProgLang/ProgLang.thy Fri Apr 10 12:28:47 2020 +0200
26.2 +++ b/src/Tools/isac/ProgLang/ProgLang.thy Fri Apr 10 14:46:55 2020 +0200
26.3 @@ -9,11 +9,7 @@
26.4 text \<open>Abstract:
26.5 The imported theories define the language, which extends Isabelle's functions to
26.6 Isac's programs for Lucas-Interpretation.
26.7 - The language is interpreted by use of Isac's rewrite engine, defined in the ML-file below.
26.8 \<close>
26.9 -
26.10 -ML_file rewrite.sml
26.11 -
26.12 ML \<open>
26.13 \<close> ML \<open>
26.14 \<close> ML \<open>
27.1 --- a/src/Tools/isac/ProgLang/rewrite.sml Fri Apr 10 12:28:47 2020 +0200
27.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
27.3 @@ -1,334 +0,0 @@
27.4 -(* isac's rewriter
27.5 - (c) Walther Neuper 2000
27.6 -*)
27.7 -
27.8 -signature REWRITE =
27.9 - sig
27.10 - val assoc_thm': theory -> ThmC.thm' -> thm
27.11 - val assoc_thm'': theory -> ThmC.thmID -> thm
27.12 - val calculate_: theory -> string * Exec_Def.eval_fn -> term -> (term * (string * thm)) option
27.13 - val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
27.14 - val eval_prog_expr: theory -> Rule_Set.T -> term -> term
27.15 - val eval_true_: theory -> Rule_Set.T -> term -> bool
27.16 - val eval_true: theory -> term list -> Rule_Set.T -> bool
27.17 - val rew_sub: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool)
27.18 - -> Rule_Set.T -> bool -> TermC.path -> term -> term -> term * term list * TermC.path * bool
27.19 - val rewrite_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool -> thm ->
27.20 - term -> (term * term list) option
27.21 - val rewrite_inst_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> bool
27.22 - -> (term * term) list -> thm -> term -> (term * term list) option
27.23 - val rewrite_set_: theory -> bool -> Rule_Set.T -> term -> (term * term list) option
27.24 - val rewrite_set_inst_: theory -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
27.25 - val rewrite_terms_: theory -> ((term * term) list -> term * term -> bool) -> Rule_Set.T -> term list
27.26 - -> term -> (term * term list) option
27.27 -(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
27.28 - (* NONE *)
27.29 -(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )
27.30 - val rewrite__: theory -> int -> (term * term) list -> ((term * term) list -> term * term -> bool) ->
27.31 - Rule_Set.T -> bool -> thm -> term -> (term * term list) option
27.32 - val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
27.33 - val app_rev: theory -> int -> Rule_Set.T -> term -> term * term list * bool
27.34 - val app_sub: theory -> int -> Rule_Set.T -> term -> term * term list * bool
27.35 - val mk_thm: theory -> string -> thm
27.36 - val trace1: int -> string -> unit
27.37 -( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
27.38 - end
27.39 -
27.40 -(**)
27.41 -structure Rewrite(**): REWRITE(**) =
27.42 -struct
27.43 -(**)
27.44 -
27.45 -exception NO_REWRITE;
27.46 -exception STOP_REW_SUB; (*WN050820 quick and dirty*)
27.47 -
27.48 -fun trace i str =
27.49 - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" i ^ str) else ()
27.50 -fun trace1 i str =
27.51 - if ! Celem.trace_rewrite andalso i < ! Celem.depth then tracing (idt "#" (i + 1) ^ str) else ()
27.52 -
27.53 -fun rewrite__ thy i bdv tless rls put_asm thm ct =
27.54 - let
27.55 - val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
27.56 - (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct
27.57 - in if rew then SOME (t', distinct asms) else NONE end
27.58 - (* one rewrite (possibly conditional, ordered) EXOR exn EXOR go into subterms *)
27.59 -and rew_sub thy i bdv tless rls put_asm lrd r t =
27.60 - (let
27.61 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
27.62 - (*?alternative Unify.matchers:
27.63 - http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2017/src/Pure/more_unify.ML*)
27.64 - val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
27.65 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
27.66 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
27.67 - val _ = if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
27.68 - then tracing (idt "#" (i + 1) ^ " eval asms: " ^ UnparseC.t2str thy r') else ()
27.69 - val (t'', p'') = (*conditional rewriting*)
27.70 - let
27.71 - val (simpl_p', nofalse) = eval__true thy (i + 1) p' bdv rls
27.72 - in
27.73 - if nofalse
27.74 - then
27.75 - (if ! Celem.trace_rewrite andalso i < ! Celem.depth andalso p' <> []
27.76 - then tracing (idt "#" (i + 1) ^ " asms accepted: " ^ UnparseC.ts2str thy p' ^
27.77 - " stored: " ^ UnparseC.ts2str thy simpl_p')
27.78 - else();
27.79 - (t',simpl_p')) (* uncond.rew. from above*)
27.80 - else
27.81 - (if ! Celem.trace_rewrite andalso i < ! Celem.depth
27.82 - then tracing (idt "#" (i + 1) ^ " asms false: " ^ UnparseC.ts2str thy p')
27.83 - else();
27.84 - raise STOP_REW_SUB (* don't go into subterms of cond *))
27.85 - end
27.86 - in
27.87 - if TermC.perm lhs rhs andalso not (tless bdv (t', t)) (*ordered rewriting*)
27.88 - then (if ! Celem.trace_rewrite andalso i < ! Celem.depth
27.89 - then tracing (idt"#"i ^ " not: \"" ^ UnparseC.t2str thy t ^ "\" > \"" ^ UnparseC.t2str thy t' ^ "\"")
27.90 - else ();
27.91 - raise NO_REWRITE)
27.92 - else (t'', p'', [], true)
27.93 - end
27.94 - ) handle _ (*TODO Pattern.MATCH when tests are ready: ERROR 364ce4699452 *) =>
27.95 - (case t of
27.96 - Const(s,T) => (Const(s,T),[],lrd,false)
27.97 - | Free(s,T) => (Free(s,T),[],lrd,false)
27.98 - | Var(n,T) => (Var(n,T),[],lrd,false)
27.99 - | Bound i => (Bound i,[],lrd,false)
27.100 - | Abs(s,T,body) =>
27.101 - let val (t', asms, _ (*lrd*), rew) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.D]) r body
27.102 - in (Abs(s, T, t'), asms, [], rew) end
27.103 - | t1 $ t2 =>
27.104 - let val (t2', asm2, lrd, rew2) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.R]) r t2
27.105 - in
27.106 - if rew2 then (t1 $ t2', asm2, lrd, true)
27.107 - else
27.108 - let val (t1', asm1, lrd, rew1) = rew_sub thy i bdv tless rls put_asm (lrd @ [TermC.L]) r t1
27.109 - in if rew1 then (t1' $ t2, asm1, lrd, true) else (t1 $ t2,[], lrd, false) end
27.110 - end)
27.111 -and eval__true thy i asms bdv rls = (* simplify asumptions until one evaluates to false *)
27.112 - if asms = [@{term True}] orelse asms = [] then ([], true)
27.113 - else (* this allows to check Rrls with prepat = ([@{term True}], pat) *)
27.114 - if asms = [@{term False}] then ([], false)
27.115 - else
27.116 - let
27.117 - fun chk indets [] = (indets, true) (*return asms<>True until false*)
27.118 - | chk indets (a :: asms) =
27.119 - (case rewrite__set_ thy (i + 1) false bdv rls a of
27.120 - NONE => (chk (indets @ [a]) asms)
27.121 - | SOME (t, a') =>
27.122 - if t = @{term True} then (chk (indets @ a') asms)
27.123 - else if t = @{term False} then ([], false)
27.124 - (*asm false .. thm not applied ^^^; continue until False vvv*)
27.125 - else chk (indets @ [t] @ a') asms);
27.126 - in chk [] asms end
27.127 -and rewrite__set_ thy _ __ Rule_Set.Empty t = (* rewrite with a rule set *)
27.128 - error ("rewrite__set_ called with 'Erls' for '" ^ UnparseC.t2str thy t ^ "'")
27.129 - | rewrite__set_ thy i _ _ (rrls as Rule_Set.Rrls _) t = (* rewrite with a 'reverse rule set' *)
27.130 - let
27.131 - val _= trace i (" rls: " ^ Rule_Set.rls2str rrls ^ " on: " ^ UnparseC.t2str thy t)
27.132 - val (t', asm, rew) = app_rev thy (i + 1) rrls t
27.133 - in if rew then SOME (t', distinct asm) else NONE end
27.134 - | rewrite__set_ thy i put_asm bdv rls ct = (* Rls, Seq containing Thms or Num_Calc, Cal1 *)
27.135 - let
27.136 - (* attention with cp to test/..: unbound thy, i, bdv, rls; TODO1803? pull out to rewrite__*)
27.137 - datatype switch = Appl | Noap;
27.138 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
27.139 - | rew_once ruls asm ct Appl [] =
27.140 - (case rls of Rule_Def.Repeat _ => rew_once ruls asm ct Noap ruls
27.141 - | Rule_Set.Seqence _ => (ct, asm)
27.142 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule_Set.rls2str rls ^ "\""))
27.143 - | rew_once ruls asm ct apno (rul :: thms) =
27.144 - case rul of
27.145 - Rule.Thm (thmid, thm) =>
27.146 - (trace1 i (" try thm: \"" ^ thmid ^ "\"");
27.147 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
27.148 - ((#erls o Rule_Set.rep) rls) put_asm thm ct of
27.149 - NONE => rew_once ruls asm ct apno thms
27.150 - | SOME (ct', asm') =>
27.151 - (trace1 i (" rewrites to: \"" ^ UnparseC.t2str thy ct' ^ "\"");
27.152 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
27.153 - (* once again try the same rule, e.g. associativity against "()"*)
27.154 - | Rule.Num_Calc (cc as (op_, _)) =>
27.155 - let val _= trace1 i (" try calc: \"" ^ op_ ^ "\"")
27.156 - val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
27.157 - in case Num_Calc.adhoc_thm thy cc ct of
27.158 - NONE => rew_once ruls asm ct apno thms
27.159 - | SOME (_, thm') =>
27.160 - let
27.161 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
27.162 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
27.163 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
27.164 - ThmC.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
27.165 - val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
27.166 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
27.167 - end
27.168 - | Rule.Cal1 (cc as (op_, _)) =>
27.169 - let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
27.170 - val ct = TermC.uminus_to_string ct
27.171 - in case Num_Calc.adhoc_thm1_ thy cc ct of
27.172 - NONE => (ct, asm)
27.173 - | SOME (_, thm') =>
27.174 - let
27.175 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule_Set.rep) rls)
27.176 - ((#erls o Rule_Set.rep) rls) put_asm thm' ct;
27.177 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
27.178 - ThmC.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
27.179 - val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
27.180 - in the pairopt end
27.181 - end
27.182 - | Rule.Rls_ rls' =>
27.183 - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
27.184 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
27.185 - | NONE => rew_once ruls asm ct apno thms)
27.186 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
27.187 - val ruls = (#rules o Rule_Set.rep) rls;
27.188 - val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)
27.189 - val (ct', asm') = rew_once ruls [] ct Noap ruls;
27.190 - in if ct = ct' then NONE else SOME (ct', distinct asm') end
27.191 -(*------------------------
27.192 --------------------------------------*)
27.193 -and app_rev thy i rrls t = (* apply an Rrls; if not applicable proceed with subterms *)
27.194 - let (* check a (precond, pattern) of a rev-set; stops with 1st true *)
27.195 - fun chk_prepat _ _ [] _ = true
27.196 - | chk_prepat thy erls prepat t =
27.197 - let
27.198 - fun chk (pres, pat) =
27.199 - (let
27.200 - val subst: Type.tyenv * Envir.tenv =
27.201 - Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
27.202 - in
27.203 - snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
27.204 - end) handle _ (*TODO Pattern.MATCH*) => false
27.205 - fun scan_ _ [] = false
27.206 - | scan_ f (pp :: pps) =
27.207 - if f pp then true else scan_ f pps;
27.208 - in scan_ chk prepat end;
27.209 - (* apply the normal_form of a rev-set *)
27.210 - fun app_rev' thy (Rule_Set.Rrls {erls, prepat, scr = Rule.Rfuns {normal_form, ...}, ...}) t =
27.211 - if chk_prepat thy erls prepat t then normal_form t else NONE
27.212 - | app_rev' _ r _ = raise ERROR ("app_rev' not appl. to \"" ^ Rule_Set.rls2str r ^ "\"");
27.213 - val opt = app_rev' thy rrls t
27.214 - in
27.215 - case opt of
27.216 - SOME (t', asm) => (t', asm, true)
27.217 - | NONE => app_sub thy i rrls t
27.218 - end
27.219 -and app_sub thy i rrls t = (* apply an Rrls to subterms *)
27.220 - case t of
27.221 - Const (s, T) => (Const(s, T), [], false)
27.222 - | Free (s, T) => (Free(s, T), [], false)
27.223 - | Var (n, T) => (Var(n, T), [], false)
27.224 - | Bound i => (Bound i, [], false)
27.225 - | Abs (s, T, body) =>
27.226 - let val (t', asm, rew) = app_rev thy i rrls body
27.227 - in (Abs(s, T, t'), asm, rew) end
27.228 - | t1 $ t2 =>
27.229 - let val (t2', asm2, rew2) = app_rev thy i rrls t2
27.230 - in
27.231 - if rew2 then (t1 $ t2', asm2, true)
27.232 - else
27.233 - let val (t1', asm1, rew1) = app_rev thy i rrls t1
27.234 - in if rew1 then (t1' $ t2, asm1, true)
27.235 - else (t1 $ t2, [], false)
27.236 - end
27.237 - end;
27.238 -
27.239 -(* rewriting without argument [] for rew_ord; WN110603: shouldnt asm<>[] lead to false? *)
27.240 -fun eval_true thy terms rls = (snd o (eval__true thy 1 terms [])) rls;
27.241 -
27.242 -(* rewriting without internal argument [] *)
27.243 -fun rewrite_ thy rew_ord erls bool thm term = rewrite__ thy 1 [] rew_ord erls bool thm term;
27.244 -fun rewrite_set_ thy bool rls term = rewrite__set_ thy 1 bool [] rls term;
27.245 -
27.246 -(* variants of rewrite; TODO del. put_asm *)
27.247 -fun rewrite_inst_ thy rew_ord rls put_asm subst thm ct =
27.248 - rewrite__ thy 1 subst rew_ord rls put_asm thm ct;
27.249 -fun rewrite_set_inst_ thy put_asm subst rls ct = rewrite__set_ thy 1 put_asm subst rls ct;
27.250 -
27.251 -(* given a list of equalities (lhs = rhs) and a term,
27.252 - replace all occurrences of lhs in the term with rhs;
27.253 - thus the order or equalities matters: put variables in lhs first. *)
27.254 -fun rewrite_terms_ thy ord erls equs t =
27.255 - let
27.256 - fun rew_ (t', asm') [] _ = (t', asm')
27.257 - | rew_ (t', asm') (rules as r::rs) t =
27.258 - let
27.259 - val (t'', asm'', _(*lrd*), rew) = rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t
27.260 - in
27.261 - if rew
27.262 - then rew_ (t'', asm' @ asm'') rules t''
27.263 - else rew_ (t', asm') rs t'
27.264 - end
27.265 - val (t'', asm'') = rew_ (TermC.empty, []) equs t
27.266 - in if t'' = TermC.empty then NONE else SOME (t'', asm'')
27.267 - end;
27.268 -
27.269 -(* search ct for adjacent numerals and calculate them by operator isa_fn *)
27.270 -fun calculate_ thy isa_fn ct =
27.271 - let val ct = TermC.uminus_to_string ct
27.272 - in case Num_Calc.adhoc_thm thy isa_fn ct of
27.273 - NONE => NONE
27.274 - | SOME (thmID, thm) =>
27.275 - (let val rew = case rewrite_ thy Rewrite_Ord.dummy_ord Rule_Set.empty false thm ct of
27.276 - SOME (rew, _) => rew
27.277 - | NONE => raise ERROR ""
27.278 - in SOME (rew, (thmID, thm)) end)
27.279 - handle _ (*TODO Pattern.MATCH ?del?*)=> error ("calculate_: " ^ thmID ^ " does not rewrite")
27.280 - end;
27.281 -
27.282 -(* Thm.make_thm added to Pure/thm.ML *)
27.283 -fun mk_thm thy str =
27.284 - let
27.285 - val t = (Thm.term_of o the o (TermC.parse thy)) str
27.286 - val t' = case t of
27.287 - Const ("Pure.imp", _) $ _ $ _ => t
27.288 - | _ => HOLogic.Trueprop $ t
27.289 - in Thm.make_thm (Thm.global_cterm_of thy t') end;
27.290 -
27.291 -(* "metaview" as seen from programs and from user input (both are parsed like terms presently) *)
27.292 -fun convert_metaview_to_thmid thy thmid =
27.293 - let val thmid' = case thmid of
27.294 - "add_commute" => "add.commute"
27.295 - | "mult_commute" => "mult.commute"
27.296 - | "add_left_commute" => "add.left_commute"
27.297 - | "mult_left_commute" => "mult.left_commute"
27.298 - | "add_assoc" => "add.assoc"
27.299 - | "mult_assoc" => "mult.assoc"
27.300 - | _ => thmid
27.301 - in (Global_Theory.get_thm thy) thmid' end;
27.302 -
27.303 -(* get the theorem associated with the xstring-identifier;
27.304 - if the identifier starts with "sym_" then swap lhs = rhs around =
27.305 - (ATTENTION: "RS sym" attaches a [.] -- remove it with ThmC.string_of_thmI);
27.306 - identifiers starting with "#" come from Num_Calc and
27.307 - get a hand-made theorem (containing numerals only) *)
27.308 -fun assoc_thm'' thy thmid =
27.309 - case Symbol.explode thmid of
27.310 - "s"::"y"::"m"::"_"::"#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
27.311 - | "s"::"y"::"m"::"_"::id => ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
27.312 - | "#"::_ => error ("assoc_thm'' not impl.for " ^ thmid)
27.313 - | _ => thmid |> convert_metaview_to_thmid thy |> TermC.num_str
27.314 -fun assoc_thm' thy (thmid, ct') =
27.315 - (case Symbol.explode thmid of
27.316 - "s"::"y"::"m"::"_"::id =>
27.317 - if hd id = "#"
27.318 - then mk_thm thy ct'
27.319 - else ((TermC.num_str o (Global_Theory.get_thm thy)) (implode id)) RS sym
27.320 - | id =>
27.321 - if hd id = "#"
27.322 - then mk_thm thy ct'
27.323 - else thmid |> convert_metaview_to_thmid thy |> TermC.num_str
27.324 - ) handle _ (*TODO: find exn behind ERROR: Undefined fact: "add_commute"*) =>
27.325 - error ("assoc_thm': \"" ^ thmid ^ "\" not in \"" ^ ThyC.theory2domID thy ^ "\" (and parents)")
27.326 -
27.327 -fun eval_prog_expr thy srls t =
27.328 - let val rew = rewrite_set_ thy false srls t;
27.329 - in case rew of SOME (res,_) => res | NONE => t end;
27.330 -
27.331 -fun eval_true_ _ _ (Const ("HOL.True",_)) = true
27.332 - | eval_true_ thy rls t =
27.333 - case rewrite_set_ thy false rls t of
27.334 - SOME (Const ("HOL.True",_),_) => true
27.335 - | _ => false;
27.336 -
27.337 -end
27.338 \ No newline at end of file
28.1 --- a/src/Tools/isac/Specify/appl.sml Fri Apr 10 12:28:47 2020 +0200
28.2 +++ b/src/Tools/isac/Specify/appl.sml Fri Apr 10 14:46:55 2020 +0200
28.3 @@ -377,7 +377,7 @@
28.4 then
28.5 case Rewrite.calculate_ (Celem.assoc_thy thy') isa_fn f of
28.6 SOME (f', (id, thm))
28.7 - => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, ThmC.string_of_thmI thm))))
28.8 + => Appl (Tactic.Calculate' (thy', op_, f, (f', (id, ThmC_Def.string_of_thmI thm))))
28.9 | NONE => Notappl ("'calculate "^op_^"' not applicable")
28.10 else Notappl msg
28.11 end
29.1 --- a/src/Tools/isac/Specify/calchead.sml Fri Apr 10 12:28:47 2020 +0200
29.2 +++ b/src/Tools/isac/Specify/calchead.sml Fri Apr 10 14:46:55 2020 +0200
29.3 @@ -100,13 +100,13 @@
29.4 -> string * Model.itm
29.5 val ppc2list : 'a Model.ppc -> 'a list
29.6 val mk_delete: theory -> string -> Model.itm_ -> Tactic.input
29.7 - val mk_additem: string -> UnparseC.cterm' -> Tactic.input
29.8 + val mk_additem: string -> TermC.as_string -> Tactic.input
29.9 val nxt_add: theory -> Model.ori list -> (string * (term * 'a)) list -> (int * Model.vats * bool * string * Model.itm_) list -> (string * string) option
29.10 val is_error: Model.itm_ -> bool
29.11 val complete_mod_: (int * int list * string * term * term list) list * ('a * (term * term)) list * ('b * (term * term)) list * Model.itm list -> Model.itm list * Model.itm list
29.12 - val nxt_specif_additem: string -> UnparseC.cterm' -> Calc.T -> calcstate'
29.13 + val nxt_specif_additem: string -> TermC.as_string -> Calc.T -> calcstate'
29.14 val vals_of_oris : Model.ori list -> term list
29.15 - val specify_additem: string -> UnparseC.cterm' -> Calc.T -> string * calcstate'
29.16 + val specify_additem: string -> TermC.as_string -> Calc.T -> string * calcstate'
29.17 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
29.18 val e_calcstate : Calc.T * Generate.taci list
29.19 val e_calcstate' : calcstate'
29.20 @@ -123,7 +123,7 @@
29.21 val cpy_nam : Celem.pat list -> Model.preori list -> Celem.pat -> Model.preori
29.22 datatype additm = Add of Model.itm | Err of string
29.23 val appl_add: Proof.context -> string -> Model.ori list ->
29.24 - Model.itm list -> (string * (term * term)) list -> UnparseC.cterm' -> additm
29.25 + Model.itm list -> (string * (term * term)) list -> TermC.as_string -> additm
29.26 val seek_oridts: Proof.context -> ''a -> term * term list -> (int * 'b list * ''a * term * term list) list -> string * (int * 'b list * ''a * term * term list) * term list
29.27 ( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
29.28
30.1 --- a/src/Tools/isac/Specify/generate.sml Fri Apr 10 12:28:47 2020 +0200
30.2 +++ b/src/Tools/isac/Specify/generate.sml Fri Apr 10 14:46:55 2020 +0200
30.3 @@ -11,7 +11,7 @@
30.4 datatype mout =
30.5 EmptyMout
30.6 | Error' of string
30.7 - | FormKF of UnparseC.cterm'
30.8 + | FormKF of TermC.as_string
30.9 | PpcKF of pblmet * Model.item Model.ppc
30.10 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
30.11 val generate1 : Tactic.T -> Istate_Def.T * Proof.context -> Calc.T
30.12 @@ -24,7 +24,7 @@
30.13 theory -> Tactic.T -> Pos.pos' -> Ctree.ctree -> Pos.pos' * Pos.pos' list * mout * Ctree.ctree
30.14 val generate : (Tactic.input * Tactic.T * (Pos.pos' * (Istate_Def.T * Proof.context))) list ->
30.15 Ctree.ctree * Pos.pos' list * Pos.pos' -> Ctree.ctree * Pos.pos' list * Pos.pos' (* for mathengine.sml *)
30.16 - val generate_inconsistent_rew : Selem.subs option * ThmC.thm'' -> term -> Istate_Def.T * Proof.context ->
30.17 + val generate_inconsistent_rew : Selem.subs option * ThmC_Def.thm'' -> term -> Istate_Def.T * Proof.context ->
30.18 Pos.pos' -> Ctree.ctree -> Calc.T (* for interface.sml *)
30.19 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
30.20 val tacis2str : taci list -> string
30.21 @@ -96,8 +96,8 @@
30.22 (*3.5.00: TODO: foppFK eliminated in interface FE-KE !!!*)
30.23 datatype foppFK = (* in DG cases div 2 *)
30.24 EmptyFoppFK (*DG internal*)
30.25 -| FormFK of UnparseC.cterm'
30.26 -| PpcFK of UnparseC.cterm' Model.ppc
30.27 +| FormFK of TermC.as_string
30.28 +| PpcFK of TermC.as_string Model.ppc
30.29 fun foppFK2str (FormFK ct') ="FormFK " ^ ct'
30.30 | foppFK2str (PpcFK ppc) ="PpcFK " ^ Model.ppc2str ppc
30.31 | foppFK2str EmptyFoppFK ="EmptyFoppFK"
30.32 @@ -118,7 +118,7 @@
30.33
30.34 datatype inout = (*FIXME.WN1105 drop this: was required for proto0 with dialog in sml*)
30.35 Error_ of string (*<--*)
30.36 -| FormKF of cellID * edit * indent * nest * UnparseC.cterm' (*<--*)
30.37 +| FormKF of cellID * edit * indent * nest * TermC.as_string (*<--*)
30.38 | PpcKF of cellID * edit * indent * nest * (pblmet * Model.item Model.ppc) (*<--*)
30.39 | RefineKF of Stool.match list (*<--*)
30.40 | RefinedKF of (Celem.pblID * ((Model.itm list) * ((bool * term) list))) (*<--*)
30.41 @@ -127,7 +127,7 @@
30.42 datatype mout = EmptyMout | Error' of inout | Form' of inout | Problems of inout
30.43 *)
30.44 datatype mout =
30.45 - FormKF of UnparseC.cterm'
30.46 + FormKF of TermC.as_string
30.47 | PpcKF of (pblmet * Model.item Model.ppc)
30.48 | RefinedKF of Celem.pblID * (Model.itm list * (bool * term) list)
30.49 | Error' of string
31.1 --- a/src/Tools/isac/Specify/input-calchead.sml Fri Apr 10 12:28:47 2020 +0200
31.2 +++ b/src/Tools/isac/Specify/input-calchead.sml Fri Apr 10 14:46:55 2020 +0200
31.3 @@ -5,9 +5,9 @@
31.4
31.5 signature INPUT_CALCHEAD =
31.6 sig
31.7 - datatype iitem = Find of UnparseC.cterm' list | Given of UnparseC.cterm' list | Relate of UnparseC.cterm' list
31.8 + datatype iitem = Find of TermC.as_string list | Given of TermC.as_string list | Relate of TermC.as_string list
31.9 type imodel = iitem list
31.10 - type icalhd = Pos.pos' * UnparseC.cterm' * imodel * Pos.pos_ * Celem.spec
31.11 + type icalhd = Pos.pos' * TermC.as_string * imodel * Pos.pos_ * Celem.spec
31.12 val input_icalhd : Ctree.ctree -> icalhd -> Ctree.ctree * Ctree.ocalhd
31.13 val cas_input : term -> (Ctree.ctree * Ctree.ocalhd) option
31.14 (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
31.15 @@ -87,23 +87,23 @@
31.16 (*** handle an input calc-head ***)
31.17
31.18 datatype iitem =
31.19 - Given of UnparseC.cterm' list
31.20 + Given of TermC.as_string list
31.21 (*Where is never input*)
31.22 -| Find of UnparseC.cterm' list
31.23 -| Relate of UnparseC.cterm' list
31.24 +| Find of TermC.as_string list
31.25 +| Relate of TermC.as_string list
31.26
31.27 type imodel = iitem list
31.28
31.29 (*calc-head as input*)
31.30 type icalhd =
31.31 Pos.pos' * (*the position of the calc-head in the calc-tree*)
31.32 - UnparseC.cterm' * (*the headline*)
31.33 + TermC.as_string * (*the headline*)
31.34 imodel * (*the model (without Find) of the calc-head*)
31.35 Pos.pos_ * (*model belongs to Pbl or Met*)
31.36 Celem.spec; (*specification: domID, pblID, metID*)
31.37 val e_icalhd = (Pos.e_pos', "", [Given [""]], Pos.Pbl, Celem.e_spec)
31.38
31.39 -fun is_casinput (hdf : UnparseC.cterm') ((fmz_, spec) : Selem.fmz) =
31.40 +fun is_casinput (hdf : TermC.as_string) ((fmz_, spec) : Selem.fmz) =
31.41 hdf <> "" andalso fmz_ = [] andalso spec = Celem.e_spec
31.42
31.43 (* re-parse itms with a new thy and prepare for checking with ori list *)
32.1 --- a/src/Tools/isac/TODO.thy Fri Apr 10 12:28:47 2020 +0200
32.2 +++ b/src/Tools/isac/TODO.thy Fri Apr 10 14:46:55 2020 +0200
32.3 @@ -39,7 +39,7 @@
32.4 \item see "TODO CLEANUP Thm" in code
32.5 (* TODO CLEANUP Thm:
32.6 Thm (string, thm): (a) needs string to identify sym_thmID for handling in front-end;
32.7 - (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC.string_of_thmI
32.8 + (b) investigate if ""RS sym" attaches a [.]" still occurs: ThmC_Def.string_of_thmI
32.9 thmID : type for data from user input + program
32.10 thmDeriv : type for thy_hierarchy ONLY
32.11 obsolete types : thm' (SEE "ad thm'"), thm''.
33.1 --- a/src/Tools/isac/Test_Code/test-code.sml Fri Apr 10 12:28:47 2020 +0200
33.2 +++ b/src/Tools/isac/Test_Code/test-code.sml Fri Apr 10 14:46:55 2020 +0200
33.3 @@ -7,7 +7,7 @@
33.4 signature TEST_CODE =
33.5 sig
33.6 type NEW (* TODO: refactor "fun me" with calcstate and remove *)
33.7 - val f2str : Generate.mout -> UnparseC.cterm'
33.8 + val f2str : Generate.mout -> TermC.as_string
33.9 val TESTg_form : Calc.T -> Generate.mout
33.10 val CalcTreeTEST : Selem.fmz list -> Pos.pos' * NEW * Generate.mout * Tactic.input * Telem.safe * Ctree.ctree
33.11 val me : Tactic.input -> Pos.pos' -> NEW -> Ctree.ctree ->
34.1 --- a/test/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 12:28:47 2020 +0200
34.2 +++ b/test/Tools/isac/BridgeLibisabelle/datatypes.sml Fri Apr 10 14:46:55 2020 +0200
34.3 @@ -227,14 +227,14 @@
34.4 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
34.5 "----------- fun xml_of_tac: SimpleTacic: is not properly abstracted in Java -------------------";
34.6
34.7 -"----------- these are : cterm' -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";
34.8 -Add_Given: cterm' -> Tactic.input;
34.9 -Add_Find: cterm' -> Tactic.input;
34.10 -Add_Relation: cterm' -> Tactic.input;
34.11 -Check_elementwise: cterm' -> Tactic.input;
34.12 -Take: cterm' -> Tactic.input;
34.13 +"----------- these are : TermC.as_string -> tac: WN150814 THESE WELL BECOME TermTactic TERMTACTIC";
34.14 +Add_Given: TermC.as_string -> Tactic.input;
34.15 +Add_Find: TermC.as_string -> Tactic.input;
34.16 +Add_Relation: TermC.as_string -> Tactic.input;
34.17 +Check_elementwise: TermC.as_string -> Tactic.input;
34.18 +Take: TermC.as_string -> Tactic.input;
34.19
34.20 -Add_Given: cterm' -> Tactic.input;
34.21 +Add_Given: TermC.as_string -> Tactic.input;
34.22 val tac = Add_Given("equality (x + 1 = 2)");
34.23 xml_of_tac tac;(*
34.24 <FORMTACTIC name="Add_Given">
34.25 @@ -268,7 +268,7 @@
34.26 Refine_Tacitly: pblID -> Tactic.input;
34.27 Specify_Problem: pblID -> Tactic.input;
34.28 Specify_Method: metID -> Tactic.input;
34.29 -Substitute: sube -> Tactic.input;; (* Substitute: sube -> tac; e_sube: cterm' list; UNCLEAR HOW TO INPUT *)
34.30 +Substitute: sube -> Tactic.input;; (* Substitute: sube -> tac; e_sube: TermC.as_string list; UNCLEAR HOW TO INPUT *)
34.31 Check_Postcond: pblID -> Tactic.input;
34.32
34.33 Apply_Method: metID -> Tactic.input;
34.34 @@ -292,9 +292,9 @@
34.35 Rewrite_Inst: subs * thm'' -> Tactic.input;
34.36 Substitute : sube -> Tactic.input;
34.37
34.38 -e_subs: cterm' list;
34.39 +e_subs: TermC.as_string list;
34.40 e_subs: subs;
34.41 -val subs = ["(''bdv_1'', xxx)","(''bdv_2'', yyy)"]: cterm' list;
34.42 +val subs = ["(''bdv_1'', xxx)","(''bdv_2'', yyy)"]: TermC.as_string list;
34.43 xml_of_subs subs;(*
34.44 <SUBSTITUTION>
34.45 <PAIR>
34.46 @@ -333,7 +333,7 @@
34.47 then () else error "xml_to_tac Rewrite_Inst CHANGED";
34.48
34.49 val sube = ["(bdv_1 = xxx)", "(bdv_2 = yyy)"]: sube;
34.50 -e_sube: cterm' list;
34.51 +e_sube: TermC.as_string list;
34.52 e_sube: sube;
34.53 xml_of_sube sube;(*
34.54 <SUBSTITUTION>
35.1 --- a/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 12:28:47 2020 +0200
35.2 +++ b/test/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Fri Apr 10 14:46:55 2020 +0200
35.3 @@ -41,13 +41,13 @@
35.4 (*val it =
35.5 ["Q' ?x = - qq ?x", "- qq ?x = Q' ?x", "\<not> ?a =!= 0 \<Longrightarrow> (?a * ?f ?x = ?b) = (?f ?x = 1 / ?a * ?b)",
35.6 "Q ?x = M_b' ?x", "M_b' ?x = Q ?x", "y'' ?x = - M_b ?x / EI", "M_b ?x = - EI * y'' ?x"]*)
35.7 -map ThmC.thmID_of_derivation_name' (thms_of thy) =
35.8 +map ThmC_Def.thmID_of_derivation_name' (thms_of thy) =
35.9 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit",
35.10 "Querkraft_Moment", "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"]
35.11 *)
35.12 val thy = @{theory Biegelinie};
35.13 val thms = thms_of thy;
35.14 -if map ThmC.thmID_of_derivation_name' thms =
35.15 +if map ThmC_Def.thmID_of_derivation_name' thms =
35.16 ["Querkraft_Belastung", "Belastung_Querkraft", "make_fun_explicit", "Querkraft_Moment",
35.17 "Moment_Querkraft", "Neigung_Moment", "Moment_Neigung"] then ()
35.18 else error "fun thms_of ...changed";
36.1 --- a/test/Tools/isac/CalcElements/calcelems.sml Fri Apr 10 12:28:47 2020 +0200
36.2 +++ b/test/Tools/isac/CalcElements/calcelems.sml Fri Apr 10 14:46:55 2020 +0200
36.3 @@ -43,7 +43,7 @@
36.4 if dn = "Test.radd_0" then ()
36.5 else error "calcelems.sml Thm.derivation_name changed 1";
36.6
36.7 -val thmID = ThmC.thmID_of_derivation_name dn;
36.8 +val thmID = ThmC_Def.thmID_of_derivation_name dn;
36.9 val thyID = ThyC.thyID_of_derivation_name dn;
36.10 if thmID = "radd_0" andalso thyID = "Test" then ()
36.11 else error "calcelems.sml Thm.derivation_name changed 2";
36.12 @@ -94,7 +94,7 @@
36.13 if long_id = "Groups.monoid_mult_class.mult_1_left" then ()
36.14 else error "fun Thm.get_name_hint or @{thm mult_1_left} changed";
36.15
36.16 -if ThmC.thmID_of_derivation_name long_id = "mult_1_left" then ()
36.17 +if ThmC_Def.thmID_of_derivation_name long_id = "mult_1_left" then ()
36.18 else error "fun thmID_of_derivation_name broken";
36.19
36.20 if ThyC.thyID_of_derivation_name long_id = "Groups" then ()
37.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
37.2 +++ b/test/Tools/isac/CalcElements/thmC-def.sml Fri Apr 10 14:46:55 2020 +0200
37.3 @@ -0,0 +1,17 @@
37.4 +(* Title: "CalcElements/thmC.sml"
37.5 + Author: Walther Neuper
37.6 + (c) due to copyright terms
37.7 +*)
37.8 +
37.9 +"-----------------------------------------------------------------------------------------------";
37.10 +"table of contents -----------------------------------------------------------------------------";
37.11 +"-----------------------------------------------------------------------------------------------";
37.12 +"----------- TODO ------------------------------------------------------------------------------";
37.13 +"-----------------------------------------------------------------------------------------------";
37.14 +"-----------------------------------------------------------------------------------------------";
37.15 +"-----------------------------------------------------------------------------------------------";
37.16 +
37.17 +
37.18 +"----------- TODO ------------------------------------------------------------------------------";
37.19 +"----------- TODO ------------------------------------------------------------------------------";
37.20 +"----------- TODO ------------------------------------------------------------------------------";
38.1 --- a/test/Tools/isac/CalcElements/thmC.sml Fri Apr 10 12:28:47 2020 +0200
38.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
38.3 @@ -1,17 +0,0 @@
38.4 -(* Title: "CalcElements/thmC.sml"
38.5 - Author: Walther Neuper
38.6 - (c) due to copyright terms
38.7 -*)
38.8 -
38.9 -"-----------------------------------------------------------------------------------------------";
38.10 -"table of contents -----------------------------------------------------------------------------";
38.11 -"-----------------------------------------------------------------------------------------------";
38.12 -"----------- TODO ------------------------------------------------------------------------------";
38.13 -"-----------------------------------------------------------------------------------------------";
38.14 -"-----------------------------------------------------------------------------------------------";
38.15 -"-----------------------------------------------------------------------------------------------";
38.16 -
38.17 -
38.18 -"----------- TODO ------------------------------------------------------------------------------";
38.19 -"----------- TODO ------------------------------------------------------------------------------";
38.20 -"----------- TODO ------------------------------------------------------------------------------";
39.1 --- a/test/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 12:28:47 2020 +0200
39.2 +++ b/test/Tools/isac/Interpret/error-fill-pattern.sml Fri Apr 10 14:46:55 2020 +0200
39.3 @@ -1010,8 +1010,8 @@
39.4 autoCalculate 1 (Steps 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
39.5 (*autoCalculate 1 (Steps 1);([2], Res), d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x (x ^^^ 4)*)
39.6
39.7 -"~~~~~ fun appendFormula , args:"; val (cI, (ifo:cterm')) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
39.8 -"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: UnparseC.cterm')) = (cI, ifo);
39.9 +"~~~~~ fun appendFormula , args:"; val (cI, (ifo:TermC.as_string)) = (1, "d_d x (x ^ 2) + cos (4 * x ^ 3)");
39.10 +"~~~~~ fun appendFormula' , args:"; val (cI, (ifo: UnparseC.term_as_string)) = (cI, ifo);
39.11 val cs = get_calc cI
39.12 val pos = get_pos cI 1;
39.13 (*+*)if pos = ([1], Res) then () else error "inform with (positive) Error_Pattern.check_for broken 1";
39.14 @@ -1099,7 +1099,7 @@
39.15 (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
39.16 val thmDeriv = Thm.get_name_hint thm
39.17 val (part, thyID) = thy_containing_thm thmDeriv
39.18 - val theID = [part, thyID, "Theorems", ThmC.thmID_of_derivation_name thmDeriv]
39.19 + val theID = [part, thyID, "Theorems", ThmC_Def.thmID_of_derivation_name thmDeriv]
39.20 val Hthm {fillpats, ...} = get_the theID
39.21 val some = map (get_fillform subst (thm, form) errpatID) fillpats;
39.22
40.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Apr 10 12:28:47 2020 +0200
40.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml Fri Apr 10 14:46:55 2020 +0200
40.3 @@ -513,7 +513,7 @@
40.4 ([1], Res), x + 1 + -1 * 2 = 0 ///Check_Postcond..ERROR*)
40.5
40.6 (*//---------- appendFormula 1 "x = 1" \<longrightarrow> Step_Solve.inform \<longrightarrow> LI.locate_input_term ----------\\*)
40.7 -"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: UnparseC.cterm') = ((**) "x = 1");
40.8 +"~~~~~ fun appendFormula , args:"; val ((*cI, *) ifo: UnparseC.term_as_string) = ((**) "x = 1");
40.9 val cs = (*get_calc cI*) ((pt, p), [(*nxt, nxt_, (pos, (ist, ctxt))*)])
40.10 val pos = (*get_pos cI 1*) p
40.11
41.1 --- a/test/Tools/isac/Interpret/rewtools.sml Fri Apr 10 12:28:47 2020 +0200
41.2 +++ b/test/Tools/isac/Interpret/rewtools.sml Fri Apr 10 14:46:55 2020 +0200
41.3 @@ -139,7 +139,7 @@
41.4 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
41.5 val thm_deriv = Thm.get_name_hint thm;
41.6
41.7 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv)
41.8 +if thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv)
41.9 = "thy_isac_Test-thm-radd_left_commute" then ()
41.10 else error "context_thy mini-subpbl ([2,4], Res) changed";
41.11 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-radd_left_commute*
41.12 @@ -161,7 +161,7 @@
41.13 applicable_in pos pt tac
41.14 val thm = Global_Theory.get_thm (Isac ()(*WN141021 assoc_thy thy' ERROR*)) thmID
41.15 val thm_deriv = Thm.get_name_hint thm;
41.16 -if thm2guh (thy_containing_thm thm_deriv) (ThmC.thmID_of_derivation_name thm_deriv) =
41.17 +if thm2guh (thy_containing_thm thm_deriv) (ThmC_Def.thmID_of_derivation_name thm_deriv) =
41.18 "thy_isac_Test-thm-risolate_bdv_add" then ()
41.19 else error "context_thy mini-subpbl ([3,1,1], Frm) changed";
41.20 (*~/proto3/kbase/thy$ ls -l thy_isac_Test-thm-risolate_bdv_add*
42.1 --- a/test/Tools/isac/Knowledge/rational.sml Fri Apr 10 12:28:47 2020 +0200
42.2 +++ b/test/Tools/isac/Knowledge/rational.sml Fri Apr 10 14:46:55 2020 +0200
42.3 @@ -806,7 +806,7 @@
42.4
42.5 if length (hd revsets) = 11 then () else error "length of revset changed";
42.6 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
42.7 - (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC.thmID_of_derivation_name)
42.8 + (@{thm realpow_twoI} |> Thm.get_name_hint |> ThmC_Def.thmID_of_derivation_name)
42.9 then () else error "first element of revset changed";
42.10 if
42.11 (revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",?r1 ^^^ 2 = ?r1 * ?r1)" andalso
43.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
43.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml Fri Apr 10 14:46:55 2020 +0200
43.3 @@ -0,0 +1,805 @@
43.4 +(* Title: "ProgLang/rewrite.sml"
43.5 + Author: Walther Neuper 050908
43.6 + (c) copyright due to lincense terms.
43.7 +*)
43.8 +
43.9 +"--------------------------------------------------------";
43.10 +"table of contents --------------------------------------";
43.11 +"--------------------------------------------------------";
43.12 +"----------- assemble rewrite ---------------------------";
43.13 +"----------- test rewriting without Isac session --------";
43.14 +"----------- conditional rewriting without Isac session -";
43.15 +"----------- step through 'and rew_sub': ----------------";
43.16 +"----------- step through 'fun rewrite_terms_' ---------";
43.17 +"----------- rewrite_inst_ bdvs -------------------------";
43.18 +"----------- check diff 2002--2009-3 --------------------";
43.19 +"----------- compare all prepat's existing 2010 ---------";
43.20 +"----------- fun app_rev, Rrls, -------------------------";
43.21 +"----------- 2011 thms with axclasses -------------------";
43.22 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
43.23 +"----------- fun assoc_thm' -----------------------------";
43.24 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
43.25 +"----------- fun mk_thm ------------------------------------------------------------------------";
43.26 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
43.27 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
43.28 +"--------------------------------------------------------";
43.29 +"--------------------------------------------------------";
43.30 +"--------------------------------------------------------";
43.31 +
43.32 +
43.33 +"----------- assemble rewrite ---------------------------";
43.34 +"----------- assemble rewrite ---------------------------";
43.35 +"----------- assemble rewrite ---------------------------";
43.36 +"===== rewriting by thm with 'a";
43.37 +(*show_types := true;*)
43.38 +
43.39 +val thy = @{theory Complex_Main};
43.40 +val ctxt = @{context};
43.41 +val thm = @{thm add.commute};
43.42 +val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
43.43 +"----- from old: fun rewrite__";
43.44 +val bdv = [];
43.45 +val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
43.46 +"----- from old: and rew_sub";
43.47 +val (LHS,RHS) = (dest_equals o strip_trueprop
43.48 + o Logic.strip_imp_concl) r;
43.49 +(* old
43.50 +val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
43.51 +"----- fun match_rew in Pure/pattern.ML";
43.52 +val rtm = the_default RHS (Term.rename_abs LHS t RHS);
43.53 +
43.54 +writeln(Syntax.string_of_term ctxt rtm);
43.55 +writeln(Syntax.string_of_term ctxt LHS);
43.56 +writeln(Syntax.string_of_term ctxt t);
43.57 +
43.58 +(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
43.59 +val (rew, RHS) = (Envir.subst_term
43.60 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
43.61 +(*lookup in isabelle?trace?response...*)
43.62 +writeln(Syntax.string_of_term ctxt rew);
43.63 +writeln(Syntax.string_of_term ctxt RHS);
43.64 +"===== rewriting: prep insertion into rew_sub";
43.65 +val thy = @{theory Complex_Main};
43.66 +val ctxt = @{context};
43.67 +val thm = @{thm nonzero_divide_mult_cancel_right};
43.68 +val r = Thm.prop_of thm;
43.69 +val tm = @{term "x / (2 * x)::real"};
43.70 +"----- and rew_sub";
43.71 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
43.72 + o Logic.strip_imp_concl) r;
43.73 +val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
43.74 + (Vartab.empty, Vartab.empty)) r;
43.75 +val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
43.76 +val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
43.77 + o Logic.strip_imp_concl) r';
43.78 +
43.79 +(*is displayed on top of <response> buffer...*)
43.80 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
43.81 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
43.82 +(**)
43.83 +
43.84 +"----------- test rewriting without Isac's thys ---------";
43.85 +"----------- test rewriting without Isac's thys ---------";
43.86 +"----------- test rewriting without Isac's thys ---------";
43.87 +
43.88 +"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
43.89 +val thy = @{theory Complex_Main};
43.90 +val ctxt = @{context};
43.91 +val thm = @{thm add.commute};
43.92 +val tm = @{term "x + y*z::real"};
43.93 +
43.94 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
43.95 + handle _ => error "rewrite.sml diff.behav. in rewriting";
43.96 +(*is displayed on _TOP_ of <response> buffer...*)
43.97 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
43.98 +if r = @{term "y*z + x::real"}
43.99 +then () else error "rewrite.sml diff.result in rewriting";
43.100 +
43.101 +"----- rewriting a subterm";
43.102 +val tm = @{term "w*(x + y*z)::real"};
43.103 +
43.104 +val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
43.105 + handle _ => error "rewrite.sml diff.behav. in rew_sub";
43.106 +
43.107 +"----- ordered rewriting";
43.108 +fun tord (_:subst) pp = LibraryC.termless pp;
43.109 +if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
43.110 +else error "rewrite.sml diff.behav. in ord.rewr.";
43.111 +
43.112 +val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
43.113 + handle _ => error "rewrite.sml diff.behav. in rewriting";
43.114 +(*is displayed on _TOP_ of <response> buffer...*)
43.115 +Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
43.116 +
43.117 +val tm = @{term "x*y + z::real"};
43.118 +val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
43.119 + handle _ => error "rewrite.sml diff.behav. in rewriting";
43.120 +
43.121 +
43.122 +"----------- conditional rewriting without Isac's thys --";
43.123 +"----------- conditional rewriting without Isac's thys --";
43.124 +"----------- conditional rewriting without Isac's thys --";
43.125 +
43.126 +"===== prepr cond.rew. with Pattern.match";
43.127 +val thy = @{theory Complex_Main};
43.128 +val ctxt = @{context};
43.129 +val thm = @{thm nonzero_divide_mult_cancel_right};
43.130 +val rule = Thm.prop_of thm;
43.131 +val tm = @{term "x / (2 * x)::real"};
43.132 +
43.133 +val prem = Logic.strip_imp_prems rule;
43.134 +val nps = Logic.count_prems rule;
43.135 +val prems = Logic.strip_prems (nps, [], rule);
43.136 +
43.137 +val eq = Logic.strip_imp_concl rule;
43.138 +val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
43.139 +
43.140 +val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
43.141 +val rule' = Envir.subst_term mtcs rule;
43.142 +
43.143 +val prems' = (fst o Logic.strip_prems)
43.144 + (Logic.count_prems rule', [], rule');
43.145 +val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
43.146 + o Logic.strip_imp_concl) rule';
43.147 +
43.148 +"----- conditional rewriting creating an assumption";
43.149 +"----- conditional rewriting creating an assumption";
43.150 +val thm = @{thm nonzero_divide_mult_cancel_right};
43.151 +val tm = @{term "x / (2 * x)::real"};
43.152 +val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
43.153 + handle _ => error "rewrite.sml diff.behav. in cond.rew.";
43.154 +
43.155 +if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
43.156 +else error "rewrite.sml diff.result in cond.rew.";
43.157 +
43.158 +if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
43.159 +then () else error "rewrite.sml diff.asm in cond.rew.";
43.160 +"----- conditional rewriting immediately: can only be done with ";
43.161 +"------Isabelle numerals, because erls cannot handle them yet.";
43.162 +
43.163 +
43.164 +"----------- step through 'and rew_sub': ----------------";
43.165 +"----------- step through 'and rew_sub': ----------------";
43.166 +"----------- step through 'and rew_sub': ----------------";
43.167 +(*and make asms without Trueprop, beginning with the result:*)
43.168 +val tm = @{term "x / (2 * x)::real"};
43.169 +val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
43.170 +(*show_types := false;*)
43.171 +"----- evaluate arguments";
43.172 +val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
43.173 + (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
43.174 +"----- step 1: LHS, RHS of rule";
43.175 + val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
43.176 + o Logic.strip_imp_concl) r;
43.177 +UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
43.178 +UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
43.179 +"----- step 2: the rule instantiated";
43.180 + val r' = Envir.subst_term
43.181 + (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
43.182 +UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
43.183 +"----- step 3: get the (instantiated) assumption(s)";
43.184 + val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
43.185 +UnparseC.term2str (hd p') = "x \<noteq> 0";
43.186 +"=====vvv make asms without Trueprop ---vvv";
43.187 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
43.188 + (Logic.count_prems r', [], r'));
43.189 +case p' of
43.190 + [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
43.191 + $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
43.192 + | _ => error "rewrite.sml assumption changed";
43.193 +"=====^^^ make asms without Trueprop ---^^^";
43.194 +"----- step 4: get the (instantiated) RHS";
43.195 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
43.196 + o Logic.strip_imp_concl) r';
43.197 +UnparseC.term2str t' = "1 / 2";
43.198 +
43.199 +"----------- step through 'fun rewrite_terms_' ---------";
43.200 +"----------- step through 'fun rewrite_terms_' ---------";
43.201 +"----------- step through 'fun rewrite_terms_' ---------";
43.202 +"----- step 0: args for rewrite_terms_, local fun";
43.203 +val (thy, ord, erls, equs, t) =
43.204 + (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
43.205 + str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
43.206 +"----- step 1: args for rew_";
43.207 +val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
43.208 +"----- step 2: rew_sub";
43.209 +rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
43.210 +"----- step 3: step through rew_sub -- inefficient: goes into subterms";
43.211 +
43.212 +
43.213 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
43.214 +writeln "----------- rewrite_terms_ 1---------------------------";
43.215 +if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
43.216 +else error "rewrite.sml rewrite_terms_ [x = 0]";
43.217 +
43.218 +val equs = [str2term "M_b 0 = 0"];
43.219 +val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
43.220 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
43.221 +writeln "----------- rewrite_terms_ 2---------------------------";
43.222 +if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
43.223 +else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
43.224 +
43.225 +val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
43.226 +val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
43.227 +val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
43.228 +writeln "----------- rewrite_terms_ 3---------------------------";
43.229 +if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
43.230 +else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
43.231 +
43.232 +
43.233 +"----------- rewrite_inst_ bdvs -------------------------";
43.234 +"----------- rewrite_inst_ bdvs -------------------------";
43.235 +"----------- rewrite_inst_ bdvs -------------------------";
43.236 +(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
43.237 +val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
43.238 +val bdvs = [(str2term"bdv_1",str2term"c"),
43.239 + (str2term"bdv_2",str2term"c_2"),
43.240 + (str2term"bdv_3",str2term"c_3"),
43.241 + (str2term"bdv_4",str2term"c_4")];
43.242 +(*------------ outcommented WN071210, after inclusion into ROOT.ML
43.243 +val SOME (t,_) =
43.244 + rewrite_inst_ thy e_rew_ord
43.245 + (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
43.246 + [(Num_Calc ("EqSystem.occur'_exactly'_in",
43.247 + eval_occur_exactly_in
43.248 + "#eval_occur_exactly_in_"))
43.249 + ])
43.250 + false bdvs (num_str @{separate_bdvs_add) t;
43.251 +(writeln o UnparseC.term2str) t;
43.252 +if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
43.253 +then () else error "rewrite.sml rewrite_inst_ bdvs";
43.254 +> trace_rewrite:=true;
43.255 +trace_rewrite:=false;--------------------------------------------*)
43.256 +
43.257 +
43.258 +"----------- check diff 2002--2009-3 --------------------";
43.259 +"----------- check diff 2002--2009-3 --------------------";
43.260 +"----------- check diff 2002--2009-3 --------------------";
43.261 +(*----- 2002 -------------------------------------------------------------------
43.262 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
43.263 +q_0 * x ^^^ 2 / 2)
43.264 +## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
43.265 +/ 2)
43.266 +### try thm: real_diff_minus
43.267 +### try thm: sym_real_mult_minus1
43.268 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
43.269 +/ 2)
43.270 +### try thm: rat_mult_poly_l
43.271 +### try thm: rat_mult_poly_r
43.272 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
43.273 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
43.274 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
43.275 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
43.276 +is_polyexp
43.277 +###### try calc: Poly.is'_polyexp'
43.278 +====== calc. to: False
43.279 +###### try calc: Poly.is'_polyexp'
43.280 +###### try calc: Poly.is'_polyexp'
43.281 +#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
43.282 +----- 2002 NONE rewrite --------------------------------------------------------
43.283 +----- 2009 should maintain this behaviour, but: --------------------------------
43.284 +# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
43.285 +## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
43.286 +### try thm: real_diff_minus
43.287 +### try thm: sym_real_mult_minus1
43.288 +## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
43.289 +### try thm: rat_mult_poly_l
43.290 +### try thm: rat_mult_poly_r
43.291 +#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
43.292 +==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
43.293 + 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
43.294 +##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
43.295 +###### try calc: Poly.is'_polyexp'
43.296 +====== calc. to: False
43.297 +###### try calc: Poly.is'_polyexp'
43.298 +###### try calc: Poly.is'_polyexp'
43.299 +#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
43.300 +=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
43.301 +----- 2009 -------------------------------------------------------------------*)
43.302 +
43.303 +(*the situation as was before repair (asm without Trueprop) is outcommented*)
43.304 +val thy = @{theory "Isac_Knowledge"};
43.305 +"===== example which raised the problem =================";
43.306 +val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
43.307 +"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
43.308 +val subs = [(@{term "bdv"}, @{term "x"})];
43.309 +val rls = norm_Rational_noadd_fractions;
43.310 +val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
43.311 +if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
43.312 + UnparseC.terms2str asms = "[]" then {}
43.313 +else error "this was NONE with Isabelle2013-2 ?!?"
43.314 +"----- rewrite_ rat_mult_poly_r--------------------------";
43.315 +val thm = @{thm rat_mult_poly_r};
43.316 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
43.317 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
43.318 + [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
43.319 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
43.320 +(*t' = t''; (*false because of further rewrites in t'*)*)
43.321 +"----- rew_sub --------------------------------";
43.322 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
43.323 +(*t'' = t'''; (*true*)*)
43.324 +"----- rewrite_set_ erls --------------------------------";
43.325 +val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
43.326 +val NONE = rewrite_set_ thy true erls cond;
43.327 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
43.328 +
43.329 +writeln "===== maximally simplified example =====================";
43.330 +val t = @{term "a / b * (x / x ^^^ 2)"};
43.331 + "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
43.332 +writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
43.333 +val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
43.334 +UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
43.335 +(*checked visually: trace_rewrite looks like above for 2009*)
43.336 +
43.337 +writeln "----- rewrite_ rat_mult_poly_r--------------------------";
43.338 +val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
43.339 +(*t' = t''; (*false because of further rewrites in t'*)*)
43.340 +writeln "----- rew_sub --------------------------------";
43.341 +val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
43.342 +(*t'' = t'''; (*true*)*)
43.343 +writeln "----- rewrite_set_ erls --------------------------------";
43.344 +val cond = @{term "(x / x ^^^ 2)"};
43.345 +val NONE = rewrite_set_ thy true erls cond;
43.346 +(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
43.347 +
43.348 +
43.349 +"----------- compare all prepat's existing 2010 ---------";
43.350 +"----------- compare all prepat's existing 2010 ---------";
43.351 +"----------- compare all prepat's existing 2010 ---------";
43.352 +val thy = @{theory "Isac_Knowledge"};
43.353 +val t = @{term "a + b * x = (0 ::real)"};
43.354 +val pat = parse_patt thy "?l = (?r ::real)";
43.355 +val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
43.356 +val precond = parse_patt thy "(?l::real) is_expanded";
43.357 +
43.358 +val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
43.359 +val preinst = Envir.subst_term inst precond;
43.360 +UnparseC.term2str preinst;
43.361 +
43.362 +"===== Rational.thy: cancel ===";
43.363 +(* pat matched with the current term gives an environment
43.364 + (or not: hen the Rrls not applied);
43.365 + if pre1 and pre2 evaluate to @{term True} in this environment,
43.366 + then the Rrls is applied. *)
43.367 +val t = str2term "(a + b) / c ::real";
43.368 +val pat = parse_patt thy "?r / ?s ::real";
43.369 +val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
43.370 +val prepat = [(pres, pat)];
43.371 +val erls = rational_erls;
43.372 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
43.373 +
43.374 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
43.375 +val asms = map (Envir.subst_term subst) pres;
43.376 +if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
43.377 +then () else error "rewrite.sml: prepat cancel subst";
43.378 +if ([], true) = eval__true thy 0 asms [] erls
43.379 +then () else error "rewrite.sml: prepat cancel eval__true";
43.380 +
43.381 +"===== Rational.thy: add_fractions_p ===";
43.382 +(* if each pat* matches with the current term, the Rrls is applied
43.383 + (there are no preconditions to be checked, they are @{term True}) *)
43.384 +val t = str2term "a / b + 1 / 2";
43.385 +val pat = parse_patt thy "?r / ?s + ?u / ?v";
43.386 +val pres = [@{term True}];
43.387 +val prepat = [(pres, pat)];
43.388 +val erls = rational_erls;
43.389 +(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
43.390 +
43.391 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
43.392 +if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
43.393 +then () else error "rewrite.sml: prepat add_fractions_p";
43.394 +
43.395 +"===== Poly.thy: order_mult_ ===";
43.396 + (* ?p matched with the current term gives an environment,
43.397 + which evaluates (the instantiated) "p is_multUnordered" to true*)
43.398 +val t = str2term "x^^^2 * x";
43.399 +val pat = parse_patt thy "?p :: real"
43.400 +val pres = [parse_patt thy "?p is_multUnordered"];
43.401 +val prepat = [(pres, pat)];
43.402 +val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
43.403 + [Num_Calc ("Poly.is'_multUnordered",
43.404 + eval_is_multUnordered "")];
43.405 +
43.406 +val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
43.407 +val asms = map (Envir.subst_term subst) pres;
43.408 +if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
43.409 +then () else error "rewrite.sml: prepat order_mult_ subst";
43.410 +if ([], true) = eval__true thy 0 asms [] erls
43.411 +then () else error "rewrite.sml: prepat order_mult_ eval__true";
43.412 +
43.413 +
43.414 +"----------- fun app_rev, Rrls, -------------------------";
43.415 +"----------- fun app_rev, Rrls, -------------------------";
43.416 +"----------- fun app_rev, Rrls, -------------------------";
43.417 +val t = str2term "x^^^2 * x";
43.418 +
43.419 +if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
43.420 +val tm = str2term "(x^^^2 * x) is_multUnordered";
43.421 +eval_is_multUnordered "testid" "" tm thy;
43.422 +
43.423 +case eval_is_multUnordered "testid" "" tm thy of
43.424 + SOME (_, Const ("HOL.Trueprop", _) $
43.425 + (Const ("HOL.eq", _) $
43.426 + (Const ("Poly.is'_multUnordered", _) $ _) $
43.427 + Const ("HOL.True", _))) => ()
43.428 + | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
43.429 +
43.430 +tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
43.431 +val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
43.432 +tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
43.433 +if UnparseC.term2str t' = "x * x ^^^ 2" then ()
43.434 +else error "rewrite.sml Poly.is'_multUnordered doesn't work";
43.435 +
43.436 +(* for achieving the previous result, the following code was taken apart *)
43.437 +"----- rewrite__set_ ---";
43.438 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
43.439 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
43.440 +"----- app_rev ---";
43.441 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
43.442 + fun chk_prepat thy erls [] t = true
43.443 + | chk_prepat thy erls prepat t =
43.444 + let fun chk (pres, pat) =
43.445 + (let val subst: Type.tyenv * Envir.tenv =
43.446 + Pattern.match thy (pat, t)
43.447 + (Vartab.empty, Vartab.empty)
43.448 + in snd (eval__true thy (i+1)
43.449 + (map (Envir.subst_term subst) pres)
43.450 + [] erls)
43.451 + end)
43.452 + handle _ => false
43.453 + fun scan_ f [] = false (*scan_ NEVER called by []*)
43.454 + | scan_ f (pp::pps) = if f pp then true
43.455 + else scan_ f pps;
43.456 + in scan_ chk prepat end;
43.457 +
43.458 + (*.apply the normal_form of a rev-set.*)
43.459 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
43.460 + if chk_prepat thy erls prepat t
43.461 + then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
43.462 + normal_form t)
43.463 + else NONE;
43.464 +(*fixme val NONE = app_rev' thy rrls t;*)
43.465 +"----- app_rev' ---";
43.466 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
43.467 +(*fixme false*) chk_prepat thy erls prepat t;
43.468 +"----- chk_prepat ---";
43.469 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
43.470 + fun chk (pres, pat) =
43.471 + (let val subst: Type.tyenv * Envir.tenv =
43.472 + Pattern.match thy (pat, t)
43.473 + (Vartab.empty, Vartab.empty)
43.474 + in snd (eval__true thy (i+1)
43.475 + (map (Envir.subst_term subst) pres)
43.476 + [] erls)
43.477 + end)
43.478 + handle _ => false;
43.479 + fun scan_ f [] = false (*scan_ NEVER called by []*)
43.480 + | scan_ f (pp::pps) = if f pp then true
43.481 + else scan_ f pps;
43.482 +tracing "=== poly.sml: scan_ chk prepat begin";
43.483 +scan_ chk prepat;
43.484 +tracing "=== poly.sml: scan_ chk prepat end";
43.485 +
43.486 +"----- chk ---";
43.487 +(*reestablish...*) val t = str2term "x ^^^ 2 * x";
43.488 +val [(pres, pat)] = prepat;
43.489 + val subst: Type.tyenv * Envir.tenv =
43.490 + Pattern.match thy (pat, t)
43.491 + (Vartab.empty, Vartab.empty);
43.492 +
43.493 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
43.494 +"----- eval__true ---";
43.495 +val asms = (map (Envir.subst_term subst) pres);
43.496 +if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
43.497 +else error "rewrite.sml: diff. is_multUnordered, asms";
43.498 +val (thy, i, asms, bdv, rls) =
43.499 + (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
43.500 + [] : (term * term) list, erls);
43.501 +case eval__true thy i asms bdv rls of
43.502 + ([], true) => ()
43.503 + | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
43.504 +
43.505 +"----------- 2011 thms with axclasses -------------------";
43.506 +"----------- 2011 thms with axclasses -------------------";
43.507 +"----------- 2011 thms with axclasses -------------------";
43.508 +val thm = num_str @{thm div_by_1};
43.509 +val prop = Thm.prop_of thm;
43.510 +atomty prop; (*Type 'a*)
43.511 +val t = str2term "(2*x)/1"; (*Type real*)
43.512 +
43.513 +val (thy, ro, er, inst) =
43.514 + (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
43.515 +val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
43.516 +
43.517 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
43.518 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
43.519 +"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
43.520 +val thy = @{theory RatEq};
43.521 +val ctxt = Proof_Context.init_global thy;
43.522 +val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
43.523 +val rls = assoc_rls "RatEq_eliminate"
43.524 +
43.525 +val SOME (t''''', asm''''') =
43.526 + rewrite_set_ thy true rls t;
43.527 +"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
43.528 + rewrite__set_ thy 1 bool [] rls term;
43.529 +"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
43.530 + = (thy, 1, bool, []:(term * term) list, rls, term);
43.531 +
43.532 +(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
43.533 + datatype switch = Appl | Noap;
43.534 + fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
43.535 + | rew_once ruls asm ct Appl [] =
43.536 + (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
43.537 + | Rule_Set.Seqence _ => (ct, asm)
43.538 + | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
43.539 + | rew_once ruls asm ct apno (rul :: thms) =
43.540 + case rul of
43.541 + Rule.Thm (thmid, thm) =>
43.542 + (trace1 i (" try thm: " ^ thmid);
43.543 + case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
43.544 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
43.545 + NONE => rew_once ruls asm ct apno thms
43.546 + | SOME (ct', asm') =>
43.547 + (trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
43.548 + rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
43.549 + (* once again try the same rule, e.g. associativity against "()"*)
43.550 + | Rule.Num_Calc (cc as (op_, _)) =>
43.551 + let val _= trace1 i (" try calc: " ^ op_ ^ "'")
43.552 + val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
43.553 + in case Num_Calc.adhoc_thm thy cc ct of
43.554 + NONE => rew_once ruls asm ct apno thms
43.555 + | SOME (_, thm') =>
43.556 + let
43.557 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
43.558 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
43.559 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
43.560 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
43.561 + val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
43.562 + in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
43.563 + end
43.564 + | Rule.Cal1 (cc as (op_, _)) =>
43.565 + let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
43.566 + val ct = TermC.uminus_to_string ct
43.567 + in case Num_Calc.adhoc_thm1_ thy cc ct of
43.568 + NONE => (ct, asm)
43.569 + | SOME (_, thm') =>
43.570 + let
43.571 + val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
43.572 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
43.573 + val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
43.574 + Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
43.575 + val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
43.576 + in the pairopt end
43.577 + end
43.578 + | Rule.Rls_ rls' =>
43.579 + (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
43.580 + SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
43.581 + | NONE => rew_once ruls asm ct apno thms)
43.582 + | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
43.583 + val ruls = (#rules o Rule.Rule_Set.rep) rls;
43.584 +(* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
43.585 + val (ct', asm') = rew_once ruls [] ct Noap ruls;
43.586 +"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
43.587 + = (ruls, []:term list, ct, Noap, ruls);
43.588 + val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
43.589 +
43.590 + val SOME (ct', asm') = (*case*)
43.591 + rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
43.592 + ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
43.593 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
43.594 + = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
43.595 + ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
43.596 +
43.597 + val (t', asms, _ (*lrd*), rew) =
43.598 + rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
43.599 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
43.600 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
43.601 + = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
43.602 + (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
43.603 + val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
43.604 + val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
43.605 +;
43.606 +(*+*)if UnparseC.term2str r' =
43.607 +(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
43.608 +(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
43.609 +(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
43.610 +(*+*) " 1 / x) =\n" ^
43.611 +(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
43.612 +(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
43.613 +(*+*)then () else error "instantiated rule CHANGED";
43.614 +
43.615 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
43.616 +;
43.617 +(*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
43.618 +(*+*)then () else error "stored assumptions CHANGED";
43.619 +
43.620 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
43.621 +;
43.622 +(*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
43.623 +(*+*)then () else error "rewritten term (an equality) CHANGED";
43.624 +
43.625 + val (simpl_p', nofalse) =
43.626 + eval__true thy (i + 1) p' bdv rls;
43.627 +"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
43.628 + (*if*) asms = [@{term True}] orelse asms = [] (*else*);
43.629 +
43.630 +(*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
43.631 +(*+*)then () else error "asms before chk CHANGED";
43.632 +
43.633 + fun chk indets [] = (indets, true) (*return asms<>True until false*)
43.634 + | chk indets (a :: asms) =
43.635 + (case rewrite__set_ thy (i + 1) false bdv rls a of
43.636 + NONE => (chk (indets @ [a]) asms)
43.637 + | SOME (t, a') =>
43.638 + if t = @{term True} then (chk (indets @ a') asms)
43.639 + else if t = @{term False} then ([], false)
43.640 + (*asm false .. thm not applied ^^^; continue until False vvv*)
43.641 + else chk (indets @ [t] @ a') asms);
43.642 +
43.643 + val (xxx, true) =
43.644 + chk [] asms; (*return from eval__true*);
43.645 +"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
43.646 +
43.647 +(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
43.648 +(*+*)(*val rules =
43.649 +(*+*) [Num_Calc ("Rings.divide_class.divide", fn),
43.650 +(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
43.651 +(*+*) :
43.652 +(*+*) Num_Calc ("HOL.eq", fn),
43.653 +(*+*) Thm ("not_true", "(\<not> True) = False"),
43.654 +(*+*) Thm ("not_false", "(\<not> False) = True"),
43.655 +(*+*) :
43.656 +(*+*) Num_Calc ("Prog_Expr.pow", fn),
43.657 +(*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
43.658 +(*+*) rule list*)
43.659 +(*+*)chk: term list -> term list -> term list * bool
43.660 +
43.661 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
43.662 +
43.663 +(*+*)trace_rewrite := true;
43.664 +
43.665 + (*this was False; vvvv--- means: indeterminate*)
43.666 + val (* SOME (t, a') *)NONE = (*case*)
43.667 + rewrite__set_ thy (i + 1) false bdv rls a (*of*);
43.668 +
43.669 +(*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
43.670 +(*
43.671 + :
43.672 + #### rls: rateq_erls on: x \<noteq> 0
43.673 + :
43.674 + ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
43.675 + ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
43.676 + ##### try calc: HOL.eq'
43.677 + ##### try thm: not_true
43.678 + ##### try thm: not_false
43.679 + ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
43.680 + and True, False are NOT stored ...
43.681 + :
43.682 + ### asms accepted: [x \<noteq> 0] stored: []
43.683 + : *)
43.684 +trace_rewrite := false;
43.685 +( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
43.686 +
43.687 +
43.688 +"----------- fun assoc_thm' -----------------------------";
43.689 +"----------- fun assoc_thm' -----------------------------";
43.690 +"----------- fun assoc_thm' -----------------------------";
43.691 +val thy = @{theory ProgLang}
43.692 +
43.693 +val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
43.694 +if string_of_thm' thy tth = "6 = 2 * 3" then ()
43.695 +else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
43.696 +
43.697 +val tth = assoc_thm' thy ("add_0_left","");
43.698 +if string_of_thm' thy tth = "0 + ?a = ?a" then ()
43.699 +else error "assoc_thm' (add_0_left,\"\") changed";
43.700 +
43.701 +val tth = assoc_thm' thy ("sym_add_0_left","");
43.702 +if string_of_thm' thy tth = "?t = 0 + ?t" then ()
43.703 +else error "assoc_thm' (sym_add_0_left,\"\") changed";
43.704 +
43.705 +val tth = assoc_thm' thy ("add_commute","");
43.706 +if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
43.707 +else error "assoc_thm' (add_commute,\"\") changed"
43.708 +
43.709 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
43.710 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
43.711 +"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
43.712 +"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
43.713 + (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
43.714 +"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
43.715 + (thy, 1, [], rew_ord, erls, bool, thm, term);
43.716 +"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
43.717 + (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
43.718 + val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
43.719 + val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
43.720 + val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
43.721 + val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
43.722 +;
43.723 +if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
43.724 +else error "ARGS FOR Pattern.match CHANGED";
43.725 +val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
43.726 +if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
43.727 + else error "Pattern.match CHANGED";
43.728 +
43.729 +"----------- fun mk_thm ------------------------------------------------------------------------";
43.730 +"----------- fun mk_thm ------------------------------------------------------------------------";
43.731 +"----------- fun mk_thm ------------------------------------------------------------------------";
43.732 +val thy = @{theory Isac_Knowledge}
43.733 +
43.734 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
43.735 +val thm = @{thm realpow_twoI};
43.736 +val patt_str = "?r ^^^ 2 = ?r * ?r";
43.737 +val term_str = "r ^^^ 2 = r * r";
43.738 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
43.739 +case parse_patt thy patt_str of
43.740 + Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
43.741 + (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
43.742 +| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
43.743 +case parse thy term_str of
43.744 + NONE => ()
43.745 +| _ => writeln "parse does NOT take patterns with '?'";
43.746 +
43.747 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
43.748 +if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
43.749 +
43.750 +val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
43.751 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
43.752 +
43.753 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
43.754 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
43.755 + gives a strange thm*);
43.756 +(*while this..*)
43.757 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
43.758 + ..gives another strange thm; but it is used and works with rewriting: *);
43.759 +
43.760 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
43.761 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
43.762 +
43.763 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
43.764 +val thm = @{thm real_mult_div_cancel2};
43.765 +val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
43.766 +val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
43.767 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
43.768 +case parse_patt thy patt_str of
43.769 + Const ("Pure.imp", _) $
43.770 + (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
43.771 + (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
43.772 + (Const ("HOL.Trueprop", _) $
43.773 + (Const ("HOL.eq", _) $ _ $ _ )) => ()
43.774 +| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
43.775 +case parse thy term_str of
43.776 + NONE => ()
43.777 +| _ => writeln "parse does NOT take patterns with '?'";
43.778 +
43.779 +val t1 = (#prop o Thm.rep_thm) (num_str thm);
43.780 +if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
43.781 +
43.782 +val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
43.783 +if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
43.784 +
43.785 +(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
43.786 +(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
43.787 + gives a strange thm*);
43.788 +(*while this*)
43.789 +val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
43.790 + gives another strange thm; but it is used and words with rewriting: *);
43.791 +
43.792 +val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
43.793 +if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
43.794 +
43.795 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
43.796 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
43.797 +"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
43.798 +(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
43.799 +val thy = @{theory};
43.800 +val rls = norm_equation;
43.801 +val term = str2term "x + 1 = 2";
43.802 +
43.803 +val SOME (t, asm) = rewrite_set_ thy false rls term;
43.804 +if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
43.805 +
43.806 +"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
43.807 +"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
43.808 +
44.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
44.2 +++ b/test/Tools/isac/MathEngBasic/thmC.sml Fri Apr 10 14:46:55 2020 +0200
44.3 @@ -0,0 +1,17 @@
44.4 +(* Title: "CalcElements/thmC.sml"
44.5 + Author: Walther Neuper
44.6 + (c) due to copyright terms
44.7 +*)
44.8 +
44.9 +"-----------------------------------------------------------------------------------------------";
44.10 +"table of contents -----------------------------------------------------------------------------";
44.11 +"-----------------------------------------------------------------------------------------------";
44.12 +"----------- TODO ------------------------------------------------------------------------------";
44.13 +"-----------------------------------------------------------------------------------------------";
44.14 +"-----------------------------------------------------------------------------------------------";
44.15 +"-----------------------------------------------------------------------------------------------";
44.16 +
44.17 +
44.18 +"----------- TODO ------------------------------------------------------------------------------";
44.19 +"----------- TODO ------------------------------------------------------------------------------";
44.20 +"----------- TODO ------------------------------------------------------------------------------";
45.1 --- a/test/Tools/isac/Minisubpbl/150-add-given.sml Fri Apr 10 12:28:47 2020 +0200
45.2 +++ b/test/Tools/isac/Minisubpbl/150-add-given.sml Fri Apr 10 14:46:55 2020 +0200
45.3 @@ -82,7 +82,7 @@
45.4 (thy, ori, (hd icl));
45.5 "~~~~~ to return val:"; val xxx =
45.6 ( fd,
45.7 - ((UnparseC.term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : cterm'
45.8 + ((UnparseC.term_to_string''' thy) o comp_dts) (d, subtract op = (ts_in itm_) ts) : TermC.as_string
45.9 );
45.10 if xxx = ("#Given", "equality (x + 1 = 2)") then () else error "";
45.11
46.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml Fri Apr 10 12:28:47 2020 +0200
46.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml Fri Apr 10 14:46:55 2020 +0200
46.3 @@ -77,11 +77,11 @@
46.4 if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();
46.5
46.6 (*
46.7 -val ct = "x = (-12) / 5" : cterm'
46.8 +val ct = "x = (-12) / 5" : TermC.as_string
46.9 > asm;
46.10 val it =
46.11 ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
46.12 - "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list
46.13 + "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : TermC.as_string list
46.14 *)
46.15
46.16
47.1 --- a/test/Tools/isac/ProgLang/rewrite.sml Fri Apr 10 12:28:47 2020 +0200
47.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
47.3 @@ -1,805 +0,0 @@
47.4 -(* Title: "ProgLang/rewrite.sml"
47.5 - Author: Walther Neuper 050908
47.6 - (c) copyright due to lincense terms.
47.7 -*)
47.8 -
47.9 -"--------------------------------------------------------";
47.10 -"table of contents --------------------------------------";
47.11 -"--------------------------------------------------------";
47.12 -"----------- assemble rewrite ---------------------------";
47.13 -"----------- test rewriting without Isac session --------";
47.14 -"----------- conditional rewriting without Isac session -";
47.15 -"----------- step through 'and rew_sub': ----------------";
47.16 -"----------- step through 'fun rewrite_terms_' ---------";
47.17 -"----------- rewrite_inst_ bdvs -------------------------";
47.18 -"----------- check diff 2002--2009-3 --------------------";
47.19 -"----------- compare all prepat's existing 2010 ---------";
47.20 -"----------- fun app_rev, Rrls, -------------------------";
47.21 -"----------- 2011 thms with axclasses -------------------";
47.22 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
47.23 -"----------- fun assoc_thm' -----------------------------";
47.24 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
47.25 -"----------- fun mk_thm ------------------------------------------------------------------------";
47.26 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
47.27 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
47.28 -"--------------------------------------------------------";
47.29 -"--------------------------------------------------------";
47.30 -"--------------------------------------------------------";
47.31 -
47.32 -
47.33 -"----------- assemble rewrite ---------------------------";
47.34 -"----------- assemble rewrite ---------------------------";
47.35 -"----------- assemble rewrite ---------------------------";
47.36 -"===== rewriting by thm with 'a";
47.37 -(*show_types := true;*)
47.38 -
47.39 -val thy = @{theory Complex_Main};
47.40 -val ctxt = @{context};
47.41 -val thm = @{thm add.commute};
47.42 -val t = (Thm.term_of o the) (parse thy "((r + u) + t) + s");
47.43 -"----- from old: fun rewrite__";
47.44 -val bdv = [];
47.45 -val r = (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm);
47.46 -"----- from old: and rew_sub";
47.47 -val (LHS,RHS) = (dest_equals o strip_trueprop
47.48 - o Logic.strip_imp_concl) r;
47.49 -(* old
47.50 -val insts = Pattern.match thy (LHS,t) (Vartab.empty, Vartab.empty);*)
47.51 -"----- fun match_rew in Pure/pattern.ML";
47.52 -val rtm = the_default RHS (Term.rename_abs LHS t RHS);
47.53 -
47.54 -writeln(Syntax.string_of_term ctxt rtm);
47.55 -writeln(Syntax.string_of_term ctxt LHS);
47.56 -writeln(Syntax.string_of_term ctxt t);
47.57 -
47.58 -(Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty));
47.59 -val (rew, RHS) = (Envir.subst_term
47.60 - (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) rtm, rtm);
47.61 -(*lookup in isabelle?trace?response...*)
47.62 -writeln(Syntax.string_of_term ctxt rew);
47.63 -writeln(Syntax.string_of_term ctxt RHS);
47.64 -"===== rewriting: prep insertion into rew_sub";
47.65 -val thy = @{theory Complex_Main};
47.66 -val ctxt = @{context};
47.67 -val thm = @{thm nonzero_divide_mult_cancel_right};
47.68 -val r = Thm.prop_of thm;
47.69 -val tm = @{term "x / (2 * x)::real"};
47.70 -"----- and rew_sub";
47.71 -val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
47.72 - o Logic.strip_imp_concl) r;
47.73 -val r' = Envir.subst_term (Pattern.match thy (LHS, tm)
47.74 - (Vartab.empty, Vartab.empty)) r;
47.75 -val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
47.76 -val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
47.77 - o Logic.strip_imp_concl) r';
47.78 -
47.79 -(*is displayed on top of <response> buffer...*)
47.80 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r');
47.81 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} t');
47.82 -(**)
47.83 -
47.84 -"----------- test rewriting without Isac's thys ---------";
47.85 -"----------- test rewriting without Isac's thys ---------";
47.86 -"----------- test rewriting without Isac's thys ---------";
47.87 -
47.88 -"===== rewriting with Isabelle2009-1 only, i.e without isac-hacks";
47.89 -val thy = @{theory Complex_Main};
47.90 -val ctxt = @{context};
47.91 -val thm = @{thm add.commute};
47.92 -val tm = @{term "x + y*z::real"};
47.93 -
47.94 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
47.95 - handle _ => error "rewrite.sml diff.behav. in rewriting";
47.96 -(*is displayed on _TOP_ of <response> buffer...*)
47.97 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
47.98 -if r = @{term "y*z + x::real"}
47.99 -then () else error "rewrite.sml diff.result in rewriting";
47.100 -
47.101 -"----- rewriting a subterm";
47.102 -val tm = @{term "w*(x + y*z)::real"};
47.103 -
47.104 -val SOME (r,_) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
47.105 - handle _ => error "rewrite.sml diff.behav. in rew_sub";
47.106 -
47.107 -"----- ordered rewriting";
47.108 -fun tord (_:subst) pp = LibraryC.termless pp;
47.109 -if tord [] (@{term "x + y*z::real"}, @{term "y*z + x::real"}) then ()
47.110 -else error "rewrite.sml diff.behav. in ord.rewr.";
47.111 -
47.112 -val NONE = (rewrite_ thy tord Rule_Set.empty false thm tm)
47.113 - handle _ => error "rewrite.sml diff.behav. in rewriting";
47.114 -(*is displayed on _TOP_ of <response> buffer...*)
47.115 -Pretty.writeln (Proof_Context.pretty_term_abbrev @{context} r);
47.116 -
47.117 -val tm = @{term "x*y + z::real"};
47.118 -val SOME (r,_) = (rewrite_ thy tord Rule_Set.empty false thm tm)
47.119 - handle _ => error "rewrite.sml diff.behav. in rewriting";
47.120 -
47.121 -
47.122 -"----------- conditional rewriting without Isac's thys --";
47.123 -"----------- conditional rewriting without Isac's thys --";
47.124 -"----------- conditional rewriting without Isac's thys --";
47.125 -
47.126 -"===== prepr cond.rew. with Pattern.match";
47.127 -val thy = @{theory Complex_Main};
47.128 -val ctxt = @{context};
47.129 -val thm = @{thm nonzero_divide_mult_cancel_right};
47.130 -val rule = Thm.prop_of thm;
47.131 -val tm = @{term "x / (2 * x)::real"};
47.132 -
47.133 -val prem = Logic.strip_imp_prems rule;
47.134 -val nps = Logic.count_prems rule;
47.135 -val prems = Logic.strip_prems (nps, [], rule);
47.136 -
47.137 -val eq = Logic.strip_imp_concl rule;
47.138 -val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
47.139 -
47.140 -val mtcs = Pattern.match thy (LHS, tm) (Vartab.empty, Vartab.empty);
47.141 -val rule' = Envir.subst_term mtcs rule;
47.142 -
47.143 -val prems' = (fst o Logic.strip_prems)
47.144 - (Logic.count_prems rule', [], rule');
47.145 -val RHS' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
47.146 - o Logic.strip_imp_concl) rule';
47.147 -
47.148 -"----- conditional rewriting creating an assumption";
47.149 -"----- conditional rewriting creating an assumption";
47.150 -val thm = @{thm nonzero_divide_mult_cancel_right};
47.151 -val tm = @{term "x / (2 * x)::real"};
47.152 -val SOME (rew, asm) = (rewrite_ thy dummy_ord Rule_Set.empty false thm tm)
47.153 - handle _ => error "rewrite.sml diff.behav. in cond.rew.";
47.154 -
47.155 -if rew = @{term "1 / 2::real"} then () (* the rewrite is _NO_ Trueprop *)
47.156 -else error "rewrite.sml diff.result in cond.rew.";
47.157 -
47.158 -if hd asm = @{term "x \<noteq> (0::real)"} (* dropped Trueprop $ ...*)
47.159 -then () else error "rewrite.sml diff.asm in cond.rew.";
47.160 -"----- conditional rewriting immediately: can only be done with ";
47.161 -"------Isabelle numerals, because erls cannot handle them yet.";
47.162 -
47.163 -
47.164 -"----------- step through 'and rew_sub': ----------------";
47.165 -"----------- step through 'and rew_sub': ----------------";
47.166 -"----------- step through 'and rew_sub': ----------------";
47.167 -(*and make asms without Trueprop, beginning with the result:*)
47.168 -val tm = @{term "x / (2 * x)::real"};
47.169 -val (t', asm, _, _) = rew_sub thy 0 [] dummy_ord Rule_Set.empty true [] (Thm.prop_of thm) tm;
47.170 -(*show_types := false;*)
47.171 -"----- evaluate arguments";
47.172 -val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
47.173 - (thy, 0, [], dummy_ord, Rule_Set.empty, true, [], (Thm.prop_of thm), tm);
47.174 -"----- step 1: LHS, RHS of rule";
47.175 - val (LHS, RHS) = (HOLogic.dest_eq o HOLogic.dest_Trueprop
47.176 - o Logic.strip_imp_concl) r;
47.177 -UnparseC.term2str r = "?b \<noteq> (0::?'a) \<Longrightarrow> ?b / (?a * ?b) = (1::?'a) / ?a";
47.178 -UnparseC.term2str LHS = "?b / (?a * ?b)"; UnparseC.term2str RHS = "(1::?'a) / ?a";
47.179 -"----- step 2: the rule instantiated";
47.180 - val r' = Envir.subst_term
47.181 - (Pattern.match thy (LHS, t) (Vartab.empty, Vartab.empty)) r;
47.182 -UnparseC.term2str r' = "x \<noteq> 0 \<Longrightarrow> x / (2 * x) = 1 / 2";
47.183 -"----- step 3: get the (instantiated) assumption(s)";
47.184 - val p' = (fst o Logic.strip_prems) (Logic.count_prems r', [], r');
47.185 -UnparseC.term2str (hd p') = "x \<noteq> 0";
47.186 -"=====vvv make asms without Trueprop ---vvv";
47.187 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems)
47.188 - (Logic.count_prems r', [], r'));
47.189 -case p' of
47.190 - [Const ("HOL.Not", _) $ (Const ("HOL.eq", _)
47.191 - $ Free ("x", _) $ Const ("Groups.zero_class.zero", _))] => ()
47.192 - | _ => error "rewrite.sml assumption changed";
47.193 -"=====^^^ make asms without Trueprop ---^^^";
47.194 -"----- step 4: get the (instantiated) RHS";
47.195 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
47.196 - o Logic.strip_imp_concl) r';
47.197 -UnparseC.term2str t' = "1 / 2";
47.198 -
47.199 -"----------- step through 'fun rewrite_terms_' ---------";
47.200 -"----------- step through 'fun rewrite_terms_' ---------";
47.201 -"----------- step through 'fun rewrite_terms_' ---------";
47.202 -"----- step 0: args for rewrite_terms_, local fun";
47.203 -val (thy, ord, erls, equs, t) =
47.204 - (@{theory "Biegelinie"}, dummy_ord, Rule_Set.Empty, [str2term "x = 0"],
47.205 - str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2");
47.206 -"----- step 1: args for rew_";
47.207 -val ((t', asm'), (rules as r::rs), t) = ((TermC.empty, []), equs, t);
47.208 -"----- step 2: rew_sub";
47.209 -rew_sub thy 1 [] ord erls false [] (HOLogic.Trueprop $ r) t;
47.210 -"----- step 3: step through rew_sub -- inefficient: goes into subterms";
47.211 -
47.212 -
47.213 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
47.214 -writeln "----------- rewrite_terms_ 1---------------------------";
47.215 -if UnparseC.term2str t' = "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
47.216 -else error "rewrite.sml rewrite_terms_ [x = 0]";
47.217 -
47.218 -val equs = [str2term "M_b 0 = 0"];
47.219 -val t = str2term "M_b 0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2";
47.220 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
47.221 -writeln "----------- rewrite_terms_ 2---------------------------";
47.222 -if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
47.223 -else error "rewrite.sml rewrite_terms_ [M_b 0 = 0]";
47.224 -
47.225 -val equs = [str2term "x = 0", str2term"M_b 0 = 0"];
47.226 -val t = str2term "M_b x = -1 * q_0 * x ^^^ 2 / 2 + x * c + c_2";
47.227 -val SOME (t', _) = rewrite_terms_ thy dummy_ord Rule_Set.Empty equs t;
47.228 -writeln "----------- rewrite_terms_ 3---------------------------";
47.229 -if UnparseC.term2str t' = "0 = -1 * q_0 * 0 ^^^ 2 / 2 + 0 * c + c_2" then ()
47.230 -else error "rewrite.sml rewrite_terms_ [x = 0, M_b 0 = 0]";
47.231 -
47.232 -
47.233 -"----------- rewrite_inst_ bdvs -------------------------";
47.234 -"----------- rewrite_inst_ bdvs -------------------------";
47.235 -"----------- rewrite_inst_ bdvs -------------------------";
47.236 -(*see smltest/Scripts/term_G.sml: inst_bdv 2*)
47.237 -val t = str2term"-1 * (q_0 * L ^^^ 2) / 2 + (L * c_3 + c_4) = 0";
47.238 -val bdvs = [(str2term"bdv_1",str2term"c"),
47.239 - (str2term"bdv_2",str2term"c_2"),
47.240 - (str2term"bdv_3",str2term"c_3"),
47.241 - (str2term"bdv_4",str2term"c_4")];
47.242 -(*------------ outcommented WN071210, after inclusion into ROOT.ML
47.243 -val SOME (t,_) =
47.244 - rewrite_inst_ thy e_rew_ord
47.245 - (Rule_Set.append_rules "erls_isolate_bdvs" Rule_Set.empty
47.246 - [(Num_Calc ("EqSystem.occur'_exactly'_in",
47.247 - eval_occur_exactly_in
47.248 - "#eval_occur_exactly_in_"))
47.249 - ])
47.250 - false bdvs (num_str @{separate_bdvs_add) t;
47.251 -(writeln o UnparseC.term2str) t;
47.252 -if UnparseC.term2str t = "L * c_3 + c_4 = 0 + -1 * (-1 * (q_0 * L ^^^ 2) / 2)"
47.253 -then () else error "rewrite.sml rewrite_inst_ bdvs";
47.254 -> trace_rewrite:=true;
47.255 -trace_rewrite:=false;--------------------------------------------*)
47.256 -
47.257 -
47.258 -"----------- check diff 2002--2009-3 --------------------";
47.259 -"----------- check diff 2002--2009-3 --------------------";
47.260 -"----------- check diff 2002--2009-3 --------------------";
47.261 -(*----- 2002 -------------------------------------------------------------------
47.262 -# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 *
47.263 -q_0 * x ^^^ 2 / 2)
47.264 -## rls: discard_minus_ on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
47.265 -/ 2)
47.266 -### try thm: real_diff_minus
47.267 -### try thm: sym_real_mult_minus1
47.268 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2
47.269 -/ 2)
47.270 -### try thm: rat_mult_poly_l
47.271 -### try thm: rat_mult_poly_r
47.272 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
47.273 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
47.274 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
47.275 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2
47.276 -is_polyexp
47.277 -###### try calc: Poly.is'_polyexp'
47.278 -====== calc. to: False
47.279 -###### try calc: Poly.is'_polyexp'
47.280 -###### try calc: Poly.is'_polyexp'
47.281 -#### asms false: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"]
47.282 ------ 2002 NONE rewrite --------------------------------------------------------
47.283 ------ 2009 should maintain this behaviour, but: --------------------------------
47.284 -# rls: norm_Rational_noadd_fractions on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
47.285 -## rls: discard_minus on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
47.286 -### try thm: real_diff_minus
47.287 -### try thm: sym_real_mult_minus1
47.288 -## rls: rat_mult_poly on: 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)
47.289 -### try thm: rat_mult_poly_l
47.290 -### try thm: rat_mult_poly_r
47.291 -#### eval asms: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
47.292 -==> 1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) =
47.293 - 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
47.294 -##### rls: Rule_Set.empty-is_polyexp on: L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp
47.295 -###### try calc: Poly.is'_polyexp'
47.296 -====== calc. to: False
47.297 -###### try calc: Poly.is'_polyexp'
47.298 -###### try calc: Poly.is'_polyexp'
47.299 -#### asms accepted: ["L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2 is_polyexp"] stored: ["False"]
47.300 -=== rewrites to: 1 * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI
47.301 ------ 2009 -------------------------------------------------------------------*)
47.302 -
47.303 -(*the situation as was before repair (asm without Trueprop) is outcommented*)
47.304 -val thy = @{theory "Isac_Knowledge"};
47.305 -"===== example which raised the problem =================";
47.306 -val t = @{term "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
47.307 -"----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
47.308 -val subs = [(@{term "bdv"}, @{term "x"})];
47.309 -val rls = norm_Rational_noadd_fractions;
47.310 -val SOME (t', asms) = rewrite_set_inst_ thy true subs rls t;
47.311 -if UnparseC.term2str t' = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * 1 * x ^^^ 2 / 2)" andalso
47.312 - UnparseC.terms2str asms = "[]" then {}
47.313 -else error "this was NONE with Isabelle2013-2 ?!?"
47.314 -"----- rewrite_ rat_mult_poly_r--------------------------";
47.315 -val thm = @{thm rat_mult_poly_r};
47.316 - "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
47.317 -val erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
47.318 - [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp "")];
47.319 -val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
47.320 -(*t' = t''; (*false because of further rewrites in t'*)*)
47.321 -"----- rew_sub --------------------------------";
47.322 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
47.323 -(*t'' = t'''; (*true*)*)
47.324 -"----- rewrite_set_ erls --------------------------------";
47.325 -val cond = @{term "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)"};
47.326 -val NONE = rewrite_set_ thy true erls cond;
47.327 -(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
47.328 -
47.329 -writeln "===== maximally simplified example =====================";
47.330 -val t = @{term "a / b * (x / x ^^^ 2)"};
47.331 - "?c::real is_polyexp ==> (?a::real) / (?b::real) * ?c = ?a * ?c / ?b";
47.332 -writeln "----- rewrite_set_inst_ norm_Rational_noadd_fractions--";
47.333 -val (*NONE*) SOME (t', asm) = rewrite_set_inst_ thy true subs rls t;
47.334 -UnparseC.term2str t' = "a * x / (b * x ^^^ 2)"; (*rew. by thm outside test case*)
47.335 -(*checked visually: trace_rewrite looks like above for 2009*)
47.336 -
47.337 -writeln "----- rewrite_ rat_mult_poly_r--------------------------";
47.338 -val NONE (*SOME (t'', _)*) = rewrite_ thy dummy_ord erls true thm t;
47.339 -(*t' = t''; (*false because of further rewrites in t'*)*)
47.340 -writeln "----- rew_sub --------------------------------";
47.341 -val (t''', _, _, _) = rew_sub thy 0 [] dummy_ord erls true [] (Thm.prop_of thm) t;
47.342 -(*t'' = t'''; (*true*)*)
47.343 -writeln "----- rewrite_set_ erls --------------------------------";
47.344 -val cond = @{term "(x / x ^^^ 2)"};
47.345 -val NONE = rewrite_set_ thy true erls cond;
47.346 -(* ^^^^^ goes with '====== calc. to: False' above from beginning*)
47.347 -
47.348 -
47.349 -"----------- compare all prepat's existing 2010 ---------";
47.350 -"----------- compare all prepat's existing 2010 ---------";
47.351 -"----------- compare all prepat's existing 2010 ---------";
47.352 -val thy = @{theory "Isac_Knowledge"};
47.353 -val t = @{term "a + b * x = (0 ::real)"};
47.354 -val pat = parse_patt thy "?l = (?r ::real)";
47.355 -val precond = parse_patt thy "is_polynomial (?l::real)";(*no infix def*)
47.356 -val precond = parse_patt thy "(?l::real) is_expanded";
47.357 -
47.358 -val inst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
47.359 -val preinst = Envir.subst_term inst precond;
47.360 -UnparseC.term2str preinst;
47.361 -
47.362 -"===== Rational.thy: cancel ===";
47.363 -(* pat matched with the current term gives an environment
47.364 - (or not: hen the Rrls not applied);
47.365 - if pre1 and pre2 evaluate to @{term True} in this environment,
47.366 - then the Rrls is applied. *)
47.367 -val t = str2term "(a + b) / c ::real";
47.368 -val pat = parse_patt thy "?r / ?s ::real";
47.369 -val pres = [parse_patt thy "?r is_expanded", parse_patt thy "?s is_expanded"];
47.370 -val prepat = [(pres, pat)];
47.371 -val erls = rational_erls;
47.372 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
47.373 -
47.374 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
47.375 -val asms = map (Envir.subst_term subst) pres;
47.376 -if UnparseC.terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"
47.377 -then () else error "rewrite.sml: prepat cancel subst";
47.378 -if ([], true) = eval__true thy 0 asms [] erls
47.379 -then () else error "rewrite.sml: prepat cancel eval__true";
47.380 -
47.381 -"===== Rational.thy: add_fractions_p ===";
47.382 -(* if each pat* matches with the current term, the Rrls is applied
47.383 - (there are no preconditions to be checked, they are @{term True}) *)
47.384 -val t = str2term "a / b + 1 / 2";
47.385 -val pat = parse_patt thy "?r / ?s + ?u / ?v";
47.386 -val pres = [@{term True}];
47.387 -val prepat = [(pres, pat)];
47.388 -val erls = rational_erls;
47.389 -(* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)
47.390 -
47.391 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
47.392 -if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls
47.393 -then () else error "rewrite.sml: prepat add_fractions_p";
47.394 -
47.395 -"===== Poly.thy: order_mult_ ===";
47.396 - (* ?p matched with the current term gives an environment,
47.397 - which evaluates (the instantiated) "p is_multUnordered" to true*)
47.398 -val t = str2term "x^^^2 * x";
47.399 -val pat = parse_patt thy "?p :: real"
47.400 -val pres = [parse_patt thy "?p is_multUnordered"];
47.401 -val prepat = [(pres, pat)];
47.402 -val erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
47.403 - [Num_Calc ("Poly.is'_multUnordered",
47.404 - eval_is_multUnordered "")];
47.405 -
47.406 -val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);
47.407 -val asms = map (Envir.subst_term subst) pres;
47.408 -if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]"
47.409 -then () else error "rewrite.sml: prepat order_mult_ subst";
47.410 -if ([], true) = eval__true thy 0 asms [] erls
47.411 -then () else error "rewrite.sml: prepat order_mult_ eval__true";
47.412 -
47.413 -
47.414 -"----------- fun app_rev, Rrls, -------------------------";
47.415 -"----------- fun app_rev, Rrls, -------------------------";
47.416 -"----------- fun app_rev, Rrls, -------------------------";
47.417 -val t = str2term "x^^^2 * x";
47.418 -
47.419 -if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
47.420 -val tm = str2term "(x^^^2 * x) is_multUnordered";
47.421 -eval_is_multUnordered "testid" "" tm thy;
47.422 -
47.423 -case eval_is_multUnordered "testid" "" tm thy of
47.424 - SOME (_, Const ("HOL.Trueprop", _) $
47.425 - (Const ("HOL.eq", _) $
47.426 - (Const ("Poly.is'_multUnordered", _) $ _) $
47.427 - Const ("HOL.True", _))) => ()
47.428 - | _ => error "rewrite.sml diff. eval_is_multUnordered 2b";
47.429 -
47.430 -tracing "----- begin rewrite x^^^2 * x ---"; trace_rewrite := false;
47.431 -val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
47.432 -tracing "----- end rewrite x^^^2 * x ---"; trace_rewrite := false;
47.433 -if UnparseC.term2str t' = "x * x ^^^ 2" then ()
47.434 -else error "rewrite.sml Poly.is'_multUnordered doesn't work";
47.435 -
47.436 -(* for achieving the previous result, the following code was taken apart *)
47.437 -"----- rewrite__set_ ---";
47.438 -val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
47.439 - val (t', asm, rew) = app_rev thy (i+1) rrls t;
47.440 -"----- app_rev ---";
47.441 -val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
47.442 - fun chk_prepat thy erls [] t = true
47.443 - | chk_prepat thy erls prepat t =
47.444 - let fun chk (pres, pat) =
47.445 - (let val subst: Type.tyenv * Envir.tenv =
47.446 - Pattern.match thy (pat, t)
47.447 - (Vartab.empty, Vartab.empty)
47.448 - in snd (eval__true thy (i+1)
47.449 - (map (Envir.subst_term subst) pres)
47.450 - [] erls)
47.451 - end)
47.452 - handle _ => false
47.453 - fun scan_ f [] = false (*scan_ NEVER called by []*)
47.454 - | scan_ f (pp::pps) = if f pp then true
47.455 - else scan_ f pps;
47.456 - in scan_ chk prepat end;
47.457 -
47.458 - (*.apply the normal_form of a rev-set.*)
47.459 - fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
47.460 - if chk_prepat thy erls prepat t
47.461 - then ((*tracing("### app_rev': t = "^(UnparseC.term2str t));*)
47.462 - normal_form t)
47.463 - else NONE;
47.464 -(*fixme val NONE = app_rev' thy rrls t;*)
47.465 -"----- app_rev' ---";
47.466 -val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
47.467 -(*fixme false*) chk_prepat thy erls prepat t;
47.468 -"----- chk_prepat ---";
47.469 -val (thy, erls, prepat, t) = (thy, erls, prepat, t);
47.470 - fun chk (pres, pat) =
47.471 - (let val subst: Type.tyenv * Envir.tenv =
47.472 - Pattern.match thy (pat, t)
47.473 - (Vartab.empty, Vartab.empty)
47.474 - in snd (eval__true thy (i+1)
47.475 - (map (Envir.subst_term subst) pres)
47.476 - [] erls)
47.477 - end)
47.478 - handle _ => false;
47.479 - fun scan_ f [] = false (*scan_ NEVER called by []*)
47.480 - | scan_ f (pp::pps) = if f pp then true
47.481 - else scan_ f pps;
47.482 -tracing "=== poly.sml: scan_ chk prepat begin";
47.483 -scan_ chk prepat;
47.484 -tracing "=== poly.sml: scan_ chk prepat end";
47.485 -
47.486 -"----- chk ---";
47.487 -(*reestablish...*) val t = str2term "x ^^^ 2 * x";
47.488 -val [(pres, pat)] = prepat;
47.489 - val subst: Type.tyenv * Envir.tenv =
47.490 - Pattern.match thy (pat, t)
47.491 - (Vartab.empty, Vartab.empty);
47.492 -
47.493 -(*fixme: asms = ["p is_multUnordered"]...instantiate*)
47.494 -"----- eval__true ---";
47.495 -val asms = (map (Envir.subst_term subst) pres);
47.496 -if UnparseC.terms2str asms = "[\"x ^^^ 2 * x is_multUnordered\"]" then ()
47.497 -else error "rewrite.sml: diff. is_multUnordered, asms";
47.498 -val (thy, i, asms, bdv, rls) =
47.499 - (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
47.500 - [] : (term * term) list, erls);
47.501 -case eval__true thy i asms bdv rls of
47.502 - ([], true) => ()
47.503 - | _ => error "rewrite.sml: diff. is_multUnordered, eval__true";
47.504 -
47.505 -"----------- 2011 thms with axclasses -------------------";
47.506 -"----------- 2011 thms with axclasses -------------------";
47.507 -"----------- 2011 thms with axclasses -------------------";
47.508 -val thm = num_str @{thm div_by_1};
47.509 -val prop = Thm.prop_of thm;
47.510 -atomty prop; (*Type 'a*)
47.511 -val t = str2term "(2*x)/1"; (*Type real*)
47.512 -
47.513 -val (thy, ro, er, inst) =
47.514 - (@{theory "Isac_Knowledge"}, tless_true, eval_rls, [(@{term "bdv::real"}, @{term "x::real"})]);
47.515 -val SOME (t, _) = rewrite_ thy ro er true thm t; (*real matches 'a ?via ring? etc*)
47.516 -
47.517 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
47.518 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
47.519 -"----------- fun rewrite_set_ .. RatEq_eliminate step into to fun chk --------------------------";
47.520 -val thy = @{theory RatEq};
47.521 -val ctxt = Proof_Context.init_global thy;
47.522 -val SOME t = parseNEW ctxt "(3 + -1 * x + x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + x ^^^ 3) = 1 / x";
47.523 -val rls = assoc_rls "RatEq_eliminate"
47.524 -
47.525 -val SOME (t''''', asm''''') =
47.526 - rewrite_set_ thy true rls t;
47.527 -"~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, true, rls, t);
47.528 - rewrite__set_ thy 1 bool [] rls term;
47.529 -"~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct)
47.530 - = (thy, 1, bool, []:(term * term) list, rls, term);
47.531 -
47.532 -(*/------- outcomment this code: otherwise the re-definition could infect tests lateron ------\ * )
47.533 - datatype switch = Appl | Noap;
47.534 - fun rew_once _ asm ct Noap [] = (ct, asm) (* ?TODO unify with Prog_Expr.rew_once? *)
47.535 - | rew_once ruls asm ct Appl [] =
47.536 - (case rls of Rule_Set.Repeat _ => rew_once ruls asm ct Noap ruls
47.537 - | Rule_Set.Seqence _ => (ct, asm)
47.538 - | rls => raise ERROR ("rew_once not appl. to \"" ^ Rule.rls2str rls ^ "\""))
47.539 - | rew_once ruls asm ct apno (rul :: thms) =
47.540 - case rul of
47.541 - Rule.Thm (thmid, thm) =>
47.542 - (trace1 i (" try thm: " ^ thmid);
47.543 - case rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
47.544 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct of
47.545 - NONE => rew_once ruls asm ct apno thms
47.546 - | SOME (ct', asm') =>
47.547 - (trace1 i (" rewrites to: " ^ UnparseC.t2str thy ct');
47.548 - rew_once ruls (union (op =) asm asm') ct' Appl (rul :: thms)))
47.549 - (* once again try the same rule, e.g. associativity against "()"*)
47.550 - | Rule.Num_Calc (cc as (op_, _)) =>
47.551 - let val _= trace1 i (" try calc: " ^ op_ ^ "'")
47.552 - val ct = TermC.uminus_to_string ct (*WN190312: superfluous?*)
47.553 - in case Num_Calc.adhoc_thm thy cc ct of
47.554 - NONE => rew_once ruls asm ct apno thms
47.555 - | SOME (_, thm') =>
47.556 - let
47.557 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
47.558 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
47.559 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
47.560 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
47.561 - val _ = trace1 i (" calc. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
47.562 - in rew_once ruls asm ((fst o the) pairopt) Appl (rul :: thms) end
47.563 - end
47.564 - | Rule.Cal1 (cc as (op_, _)) =>
47.565 - let val _= trace1 i (" try cal1: " ^ op_ ^ "'");
47.566 - val ct = TermC.uminus_to_string ct
47.567 - in case Num_Calc.adhoc_thm1_ thy cc ct of
47.568 - NONE => (ct, asm)
47.569 - | SOME (_, thm') =>
47.570 - let
47.571 - val pairopt = rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
47.572 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm' ct;
47.573 - val _ = if pairopt <> NONE then () else error ("rewrite_set_, rewrite_ \"" ^
47.574 - Rule.string_of_thmI thm' ^ "\" " ^ UnparseC.t2str thy ct ^ " = NONE")
47.575 - val _ = trace1 i (" cal1. to: " ^ UnparseC.t2str thy ((fst o the) pairopt))
47.576 - in the pairopt end
47.577 - end
47.578 - | Rule.Rls_ rls' =>
47.579 - (case rewrite__set_ thy (i + 1) put_asm bdv rls' ct of
47.580 - SOME (t', asm') => rew_once ruls (union (op =) asm asm') t' Appl thms
47.581 - | NONE => rew_once ruls asm ct apno thms)
47.582 - | r => raise ERROR ("rew_once not appl. to \"" ^ Rule.rule2str r ^ "\"");
47.583 - val ruls = (#rules o Rule.Rule_Set.rep) rls;
47.584 -(* val _ = trace i (" rls: " ^ Rule_Set.rls2str rls ^ " on: " ^ UnparseC.t2str thy ct)*)
47.585 - val (ct', asm') = rew_once ruls [] ct Noap ruls;
47.586 -"~~~~~ fun rew_once , args:"; val (ruls, asm, ct, apno, (rul :: thms))
47.587 - = (ruls, []:term list, ct, Noap, ruls);
47.588 - val Rule.Thm (thmid, thm) = (*case*) rul (*of*);
47.589 -
47.590 - val SOME (ct', asm') = (*case*)
47.591 - rewrite__ thy (i + 1) bdv ((snd o #rew_ord o Rule.Rule_Set.rep) rls)
47.592 - ((#erls o Rule.Rule_Set.rep) rls) put_asm thm ct (*of*);
47.593 -"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct)
47.594 - = (thy, (i + 1), bdv, ((snd o #rew_ord o Rule.Rule_Set.rep) rls),
47.595 - ((#erls o Rule.Rule_Set.rep) rls), put_asm, thm, ct);
47.596 -
47.597 - val (t', asms, _ (*lrd*), rew) =
47.598 - rew_sub thy i bdv tless rls put_asm ([(*root of the term*)]: TermC.path)
47.599 - (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm) ct;
47.600 -"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t)
47.601 - = (thy, i, bdv, tless, rls, put_asm, ([(*root of the term*)]: TermC.path),
47.602 - (((TermC.inst_bdv bdv) o Num_Calc.norm o #prop o Thm.rep_thm) thm), ct);
47.603 - val (lhs, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
47.604 - val r' = Envir.subst_term (Pattern.match thy (lhs, t) (Vartab.empty, Vartab.empty)) r
47.605 -;
47.606 -(*+*)if UnparseC.term2str r' =
47.607 -(*+*) "\<lbrakk>9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0; x \<noteq> 0\<rbrakk>\n" ^
47.608 -(*+*) "\<Longrightarrow> ((3 + -1 * x + x ^^^ 2) /\n" ^
47.609 -(*+*) " (9 * x + -6 * x ^^^ 2 + x ^^^ 3) =\n" ^
47.610 -(*+*) " 1 / x) =\n" ^
47.611 -(*+*) " ((3 + -1 * x + x ^^^ 2) * x =\n" ^
47.612 -(*+*) " 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3))"
47.613 -(*+*)then () else error "instantiated rule CHANGED";
47.614 -
47.615 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
47.616 -;
47.617 -(*+*)if map UnparseC.term2str p' = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
47.618 -(*+*)then () else error "stored assumptions CHANGED";
47.619 -
47.620 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
47.621 -;
47.622 -(*+*)if UnparseC.term2str t' = "(3 + -1 * x + x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + x ^^^ 3)"
47.623 -(*+*)then () else error "rewritten term (an equality) CHANGED";
47.624 -
47.625 - val (simpl_p', nofalse) =
47.626 - eval__true thy (i + 1) p' bdv rls;
47.627 -"~~~~~ and eval__true , args:"; val (thy, i, asms, bdv, rls) = (thy, (i + 1), p', bdv, rls);
47.628 - (*if*) asms = [@{term True}] orelse asms = [] (*else*);
47.629 -
47.630 -(*+*)if map UnparseC.term2str asms = ["x \<noteq> 0", "9 * x + -6 * x ^^^ 2 + x ^^^ 3 \<noteq> 0"]
47.631 -(*+*)then () else error "asms before chk CHANGED";
47.632 -
47.633 - fun chk indets [] = (indets, true) (*return asms<>True until false*)
47.634 - | chk indets (a :: asms) =
47.635 - (case rewrite__set_ thy (i + 1) false bdv rls a of
47.636 - NONE => (chk (indets @ [a]) asms)
47.637 - | SOME (t, a') =>
47.638 - if t = @{term True} then (chk (indets @ a') asms)
47.639 - else if t = @{term False} then ([], false)
47.640 - (*asm false .. thm not applied ^^^; continue until False vvv*)
47.641 - else chk (indets @ [t] @ a') asms);
47.642 -
47.643 - val (xxx, true) =
47.644 - chk [] asms; (*return from eval__true*);
47.645 -"~~~~~ fun chk , args:"; val (indets, (a :: asms)) = ([], asms);
47.646 -
47.647 -(*+*)val Rule_Set.Repeat {id = "rateq_erls", rules, ...} = rls;
47.648 -(*+*)(*val rules =
47.649 -(*+*) [Num_Calc ("Rings.divide_class.divide", fn),
47.650 -(*+*) Thm ("minus_divide_left", "- ?a1 / ?b1 = - (?a1 / ?b1)"),
47.651 -(*+*) :
47.652 -(*+*) Num_Calc ("HOL.eq", fn),
47.653 -(*+*) Thm ("not_true", "(\<not> True) = False"),
47.654 -(*+*) Thm ("not_false", "(\<not> False) = True"),
47.655 -(*+*) :
47.656 -(*+*) Num_Calc ("Prog_Expr.pow", fn),
47.657 -(*+*) Num_Calc ("RatEq.is'_ratequation'_in", fn)]:
47.658 -(*+*) rule list*)
47.659 -(*+*)chk: term list -> term list -> term list * bool
47.660 -
47.661 - rewrite__set_ thy (i + 1) false bdv rls a (*of*);
47.662 -
47.663 -(*+*)trace_rewrite := true;
47.664 -
47.665 - (*this was False; vvvv--- means: indeterminate*)
47.666 - val (* SOME (t, a') *)NONE = (*case*)
47.667 - rewrite__set_ thy (i + 1) false bdv rls a (*of*);
47.668 -
47.669 -(*+*)UnparseC.term2str a = "x \<noteq> 0"; (* rewrite__set_ \<rightarrow> @{term True} ----------------- SHOULD BE indet !*)
47.670 -(*
47.671 - :
47.672 - #### rls: rateq_erls on: x \<noteq> 0
47.673 - :
47.674 - ##### try calc: HOL.eq' <<<------------------------------- here the error comes from
47.675 - ===== calc. to: ~ False <<<------------------------------- \<not> x = 0 is NOT False
47.676 - ##### try calc: HOL.eq'
47.677 - ##### try thm: not_true
47.678 - ##### try thm: not_false
47.679 - ===== rewrites to: True <<<------------------------------- so x \<noteq> 0 is NOT True
47.680 - and True, False are NOT stored ...
47.681 - :
47.682 - ### asms accepted: [x \<noteq> 0] stored: []
47.683 - : *)
47.684 -trace_rewrite := false;
47.685 -( *\------- outcomment this code: otherwise the re-definition could infect tests lateron ------/*)
47.686 -
47.687 -
47.688 -"----------- fun assoc_thm' -----------------------------";
47.689 -"----------- fun assoc_thm' -----------------------------";
47.690 -"----------- fun assoc_thm' -----------------------------";
47.691 -val thy = @{theory ProgLang}
47.692 -
47.693 -val tth = assoc_thm' thy ("sym_#mult_2_3","6 = 2 * 3");
47.694 -if string_of_thm' thy tth = "6 = 2 * 3" then ()
47.695 -else error "assoc_thm' (sym_#mult_2_3, 6 = 2 * 3) changed";
47.696 -
47.697 -val tth = assoc_thm' thy ("add_0_left","");
47.698 -if string_of_thm' thy tth = "0 + ?a = ?a" then ()
47.699 -else error "assoc_thm' (add_0_left,\"\") changed";
47.700 -
47.701 -val tth = assoc_thm' thy ("sym_add_0_left","");
47.702 -if string_of_thm' thy tth = "?t = 0 + ?t" then ()
47.703 -else error "assoc_thm' (sym_add_0_left,\"\") changed";
47.704 -
47.705 -val tth = assoc_thm' thy ("add_commute","");
47.706 -if string_of_thm' thy tth = "?a + ?b = ?b + ?a" then ()
47.707 -else error "assoc_thm' (add_commute,\"\") changed"
47.708 -
47.709 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
47.710 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
47.711 -"----------- fun rewrite_ down to Pattern.match ------------------------------------------------";
47.712 -"~~~~~ fun rewrite_ , args:"; val (thy, rew_ord, erls, bool, thm, term) =
47.713 - (@{theory}, dummy_ord, Rule_Set.empty, false, @{thm distrib_left}, @{term "x * (y + z) :: int"});
47.714 -"~~~~~ fun rewrite__ , args:"; val (thy, i, bdv, tless, rls, put_asm, thm, ct) =
47.715 - (thy, 1, [], rew_ord, erls, bool, thm, term);
47.716 -"~~~~~ and rew_sub , args:"; val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) =
47.717 - (thy, i, bdv, tless, rls, put_asm, [], (((inst_bdv bdv) o norm o #prop o Thm.rep_thm) thm), ct)
47.718 - val (lhss, rhss) = (HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r
47.719 - val r' = Envir.subst_term (Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty)) r
47.720 - val p' = map HOLogic.dest_Trueprop ((fst o Logic.strip_prems) (Logic.count_prems r', [], r'))
47.721 - val t' = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o Logic.strip_imp_concl) r'
47.722 -;
47.723 -if UnparseC.term2str lhss = "?a * (?b + ?c)" andalso UnparseC.term2str t = "x * (y + z)" then ()
47.724 -else error "ARGS FOR Pattern.match CHANGED";
47.725 -val match = Pattern.match thy (lhss, t) (Vartab.empty, Vartab.empty);
47.726 -if (Envir.subst_term match r |> UnparseC.term2str) = "x * (y + z) = x * y + x * z" then ()
47.727 - else error "Pattern.match CHANGED";
47.728 -
47.729 -"----------- fun mk_thm ------------------------------------------------------------------------";
47.730 -"----------- fun mk_thm ------------------------------------------------------------------------";
47.731 -"----------- fun mk_thm ------------------------------------------------------------------------";
47.732 -val thy = @{theory Isac_Knowledge}
47.733 -
47.734 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
47.735 -val thm = @{thm realpow_twoI};
47.736 -val patt_str = "?r ^^^ 2 = ?r * ?r";
47.737 -val term_str = "r ^^^ 2 = r * r";
47.738 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
47.739 -case parse_patt thy patt_str of
47.740 - Const ("HOL.eq", _) $ (Const ("Prog_Expr.pow", _) $ Var (("r", 0), _) $ Free ("2", _)) $
47.741 - (Const ("Groups.times_class.times", _) $ Var (("r", 0), _) $ Var (("r", 0), _)) => ()
47.742 -| _ => error "parse_patt ?r ^^^ 2 = ?r * ?r changed";
47.743 -case parse thy term_str of
47.744 - NONE => ()
47.745 -| _ => writeln "parse does NOT take patterns with '?'";
47.746 -
47.747 -val t1 = (#prop o Thm.rep_thm) (num_str thm);
47.748 -if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
47.749 -
47.750 -val t2 = HOLogic.Trueprop $ (((parse_patt thy)) patt_str) : term;
47.751 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
47.752 -
47.753 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
47.754 -(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
47.755 - gives a strange thm*);
47.756 -(*while this..*)
47.757 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
47.758 - ..gives another strange thm; but it is used and works with rewriting: *);
47.759 -
47.760 -val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
47.761 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
47.762 -
47.763 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
47.764 -val thm = @{thm real_mult_div_cancel2};
47.765 -val patt_str = "?k \<noteq> 0 \<Longrightarrow> ?m * ?k / (?n * ?k) = ?m / ?n";
47.766 -val term_str = "k \<noteq> 0 \<Longrightarrow> m * k / (n * k) = m / n";
47.767 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
47.768 -case parse_patt thy patt_str of
47.769 - Const ("Pure.imp", _) $
47.770 - (Const ("HOL.Trueprop", _) $ (Const ("HOL.Not", _) $
47.771 - (Const ("HOL.eq", _) $ Var (("k", 0), _) $ Free ("0", _)))) $
47.772 - (Const ("HOL.Trueprop", _) $
47.773 - (Const ("HOL.eq", _) $ _ $ _ )) => ()
47.774 -| _ => error "parse_patt ?k \<noteq> 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n changed";
47.775 -case parse thy term_str of
47.776 - NONE => ()
47.777 -| _ => writeln "parse does NOT take patterns with '?'";
47.778 -
47.779 -val t1 = (#prop o Thm.rep_thm) (num_str thm);
47.780 -if UnparseC.term2str t1 = patt_str then () else error "realpow_twoI (\<rightarrow> string) NOT equal to given string";
47.781 -
47.782 -val t2 = (*Trueprop $*) (((parse_patt thy)) patt_str) : term;
47.783 -if t1 = t2 then () else error "prop of realpow_twoI NOT equal to parsed string";
47.784 -
47.785 -(mk_thm thy patt_str) handle _ => mk_thm thy "mk_thm = does NOT handle patterns";
47.786 -(*and this*) mk_thm thy term_str (* = "r ^^^ 2 = r * r" [.]: thm
47.787 - gives a strange thm*);
47.788 -(*while this*)
47.789 -val thm_made = Thm.make_thm (Thm.global_cterm_of thy t2) (* = "?r ^^^ 2 = ?r * ?r" [.]: thm
47.790 - gives another strange thm; but it is used and words with rewriting: *);
47.791 -
47.792 -val t1' = (#prop o Thm.rep_thm) (num_str thm_made);
47.793 -if t1 = t1' then () else error "prop of realpow_twoI NOT equal to thm_made from string";
47.794 -
47.795 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
47.796 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
47.797 -"----------- fun rewrite_set_ .. norm_equation -------------------------------------------------";
47.798 -(* norm_equation is defined in Test.thy, other rls see Knowledg/**)
47.799 -val thy = @{theory};
47.800 -val rls = norm_equation;
47.801 -val term = str2term "x + 1 = 2";
47.802 -
47.803 -val SOME (t, asm) = rewrite_set_ thy false rls term;
47.804 -if UnparseC.term2str t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
47.805 -
47.806 -"~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
47.807 -"~~~~~ fun rewrite__set_, args:"; val (thy, i, put_asm, bdv, rls, ct) = (thy, 1, bool, [], rls, term);
47.808 -
48.1 --- a/test/Tools/isac/Test_Isac.thy Fri Apr 10 12:28:47 2020 +0200
48.2 +++ b/test/Tools/isac/Test_Isac.thy Fri Apr 10 14:46:55 2020 +0200
48.3 @@ -131,8 +131,10 @@
48.4 open Rule_Set
48.5 open Exec_Def
48.6 open ThyC
48.7 + open ThmC_Def
48.8 open ThmC
48.9 open Rewrite_Ord
48.10 + open UnparseC
48.11 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
48.12 \<close>
48.13
48.14 @@ -177,7 +179,14 @@
48.15 subsection \<open>basic code first\<close>
48.16 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
48.17 ML_file "CalcElements/libraryC.sml"
48.18 + ML_file "CalcElements/rule-def.sml"
48.19 + ML_file "CalcElements/exec-def.sml"
48.20 + ML_file "CalcElements/rewrite-order.sml"
48.21 + ML_file "CalcElements/theoryC.sml"
48.22 ML_file "CalcElements/rule.sml"
48.23 + ML_file "CalcElements/thmC-def.sml"
48.24 + ML_file "CalcElements/error-fill-def.sml"
48.25 + ML_file "CalcElements/rule-set.sml"
48.26 ML_file "CalcElements/calcelems.sml"
48.27 ML_file "CalcElements/termC.sml"
48.28 ML_file "CalcElements/contextC.sml"
48.29 @@ -192,7 +201,6 @@
48.30 ML_file "ProgLang/prog_tac.sml"
48.31 ML_file "ProgLang/tactical.sml"
48.32 ML_file "ProgLang/auto_prog.sml"
48.33 - ML_file "ProgLang/rewrite.sml"
48.34 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
48.35 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
48.36
48.37 @@ -220,6 +228,8 @@
48.38 ML_file "Minisubpbl/800-append-on-Frm.sml"
48.39
48.40 subsection \<open>further functionality alongside batch build sequence\<close>
48.41 + ML_file "MathEngBasic/thmC.sml"
48.42 + ML_file "MathEngBasic/rewrite.sml"
48.43 ML_file "MathEngBasic/model.sml"
48.44 ML_file "MathEngBasic/mstools.sml"
48.45 ML_file "MathEngBasic/specification-elems.sml"
48.46 @@ -235,6 +245,7 @@
48.47 ML_file "Specify/step-specify.sml"
48.48 ML_file "Specify/specify.sml"
48.49
48.50 + ML_file "Interpret/istate.sml"
48.51 ML_file "Interpret/sub-problem.sml"
48.52 ML_file "Interpret/rewtools.sml"
48.53 ML_file "Interpret/error-pattern.sml"
49.1 --- a/test/Tools/isac/Test_Isac_Short.thy Fri Apr 10 12:28:47 2020 +0200
49.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Fri Apr 10 14:46:55 2020 +0200
49.3 @@ -131,6 +131,7 @@
49.4 open Rule_Set
49.5 open Exec_Def
49.6 open ThyC
49.7 + open ThmC_Def
49.8 open ThmC
49.9 open Rewrite_Ord
49.10 open UnparseC
49.11 @@ -183,7 +184,7 @@
49.12 ML_file "CalcElements/rewrite-order.sml"
49.13 ML_file "CalcElements/theoryC.sml"
49.14 ML_file "CalcElements/rule.sml"
49.15 - ML_file "CalcElements/thmC.sml"
49.16 + ML_file "CalcElements/thmC-def.sml"
49.17 ML_file "CalcElements/error-fill-def.sml"
49.18 ML_file "CalcElements/rule-set.sml"
49.19 ML_file "CalcElements/calcelems.sml"
49.20 @@ -200,7 +201,6 @@
49.21 ML_file "ProgLang/prog_tac.sml"
49.22 ML_file "ProgLang/tactical.sml"
49.23 ML_file "ProgLang/auto_prog.sml"
49.24 - ML_file "ProgLang/rewrite.sml"
49.25 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
49.26 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
49.27
49.28 @@ -228,6 +228,8 @@
49.29 ML_file "Minisubpbl/800-append-on-Frm.sml"
49.30
49.31 subsection \<open>further functionality alongside batch build sequence\<close>
49.32 + ML_file "MathEngBasic/thmC.sml"
49.33 + ML_file "MathEngBasic/rewrite.sml"
49.34 ML_file "MathEngBasic/model.sml"
49.35 ML_file "MathEngBasic/mstools.sml"
49.36 ML_file "MathEngBasic/specification-elems.sml"
50.1 --- a/test/Tools/isac/Test_Some.thy Fri Apr 10 12:28:47 2020 +0200
50.2 +++ b/test/Tools/isac/Test_Some.thy Fri Apr 10 14:46:55 2020 +0200
50.3 @@ -51,8 +51,10 @@
50.4 open Rule_Set
50.5 open Exec_Def
50.6 open ThyC
50.7 + open ThmC_Def
50.8 open ThmC
50.9 open Rewrite_Ord
50.10 + open UnparseC
50.11 (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
50.12 \<close>
50.13 ML_file "CalcElements/libraryC.sml"