funpack: rename xxx' to xxxX preparing ''xxxX'' (''xxx''' not accepted by funpack)
1.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Nov 29 18:09:44 2018 +0100
1.2 +++ b/src/Tools/isac/Knowledge/Test.thy Fri Nov 30 12:27:18 2018 +0100
1.3 @@ -964,7 +964,7 @@
1.4 " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
1.5 " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
1.6 " (L_L::bool list) = " ^
1.7 - " (SubProblem (Test', " ^
1.8 + " (SubProblem (TestX, " ^
1.9 " [LINEAR,univariate,equation,test]," ^
1.10 " [Test,solve_linear]) " ^
1.11 " [BOOL e_e, REAL v_v]) " ^
2.1 --- a/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Thu Nov 29 18:09:44 2018 +0100
2.2 +++ b/test/Tools/isac/ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform.thy Fri Nov 30 12:27:18 2018 +0100
2.3 @@ -463,7 +463,7 @@
2.4
2.5 text\<open>\noindent First we isolate the difficulty in the program as follows:
2.6 \begin{verbatim}
2.7 - " (L_L::bool list) = (SubProblem (PolyEq', " ^
2.8 + " (L_L::bool list) = (SubProblem (PolyEqX, " ^
2.9 " [abcFormula, degree_2, polynomial, " ^
2.10 " univariate,equation], " ^
2.11 " [no_met]) " ^
2.12 @@ -1024,7 +1024,7 @@
2.13 (*
2.14 * simplify
2.15 *)
2.16 - " X' = (SubProblem (Isac',[pqFormula,degree_2, "^
2.17 + " X' = (SubProblem (IsacX,[pqFormula,degree_2, "^
2.18 " polynomial,univariate,equation], "^
2.19 " [no_met]) "^
2.20 " [BOOL e_e, REAL v_v]) "^
2.21 @@ -1067,7 +1067,7 @@
2.22 *)
2.23 " (equ::bool) = (denom = (0::real)); "^
2.24 " (L_L::bool list) = "^
2.25 - " (SubProblem (Test', "^
2.26 + " (SubProblem (TestX, "^
2.27 " [LINEAR,univariate,equation,test], "^
2.28 " [Test,solve_linear]) "^
2.29 " [BOOL equ, REAL z]) "^
2.30 @@ -1147,7 +1147,7 @@
2.31 " (num::real) = get_numerator funterm; "^
2.32 (*get_numerator*)
2.33 " (equ::bool) = (denom = (0::real)); "^
2.34 - " (L_L::bool list) = (SubProblem (PolyEq', "^
2.35 + " (L_L::bool list) = (SubProblem (PolyEqX, "^
2.36 " [abcFormula,degree_2,polynomial,univariate,equation], "^
2.37 " [no_met]) "^
2.38 " [BOOL equ, REAL zzz]); "^
2.39 @@ -1172,7 +1172,7 @@
2.40 " eq_a = (Substitute [zzz=z1]) eq; "^
2.41 " eq_a = (Rewrite_Set norm_Rational False) eq_a; "^
2.42 " (sol_a::bool list) = "^
2.43 - " (SubProblem (Isac', "^
2.44 + " (SubProblem (IsacX, "^
2.45 " [univariate,equation],[no_met]) "^
2.46 " [BOOL eq_a, REAL (A::real)]); "^
2.47 " (a::real) = (rhs(NTH 1 sol_a)); "^
2.48 @@ -1181,7 +1181,7 @@
2.49 " eq_b = (Substitute [zzz=z2]) eq_b; "^
2.50 " eq_b = (Rewrite_Set norm_Rational False) eq_b; "^
2.51 " (sol_b::bool list) = "^
2.52 - " (SubProblem (Isac', "^
2.53 + " (SubProblem (IsacX, "^
2.54 " [univariate,equation],[no_met]) "^
2.55 " [BOOL eq_b, REAL (B::real)]); "^
2.56 " (b::real) = (rhs(NTH 1 sol_b)); "^
3.1 --- a/test/Tools/isac/Interpret/calchead.sml Thu Nov 29 18:09:44 2018 +0100
3.2 +++ b/test/Tools/isac/Interpret/calchead.sml Fri Nov 30 12:27:18 2018 +0100
3.3 @@ -334,7 +334,7 @@
3.4 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.5 (*...copied from stac2tac_*)
3.6 str2term (
3.7 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.8 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.9 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.10 " REAL_LIST [c, c_2]]");
3.11 val ags = isalist2list ags';
3.12 @@ -359,7 +359,7 @@
3.13 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.14 (*...copied from stac2tac_*)
3.15 str2term (
3.16 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.17 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.18 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.19 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
3.20 val ags = isalist2list ags';
3.21 @@ -385,7 +385,7 @@
3.22 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.23 (*...copied from stac2tac_*)
3.24 str2term (
3.25 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.26 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.27 " [REAL_LIST [c, c_2]]");
3.28 val ags = isalist2list ags';
3.29 val pI = ["LINEAR","system"];
3.30 @@ -425,7 +425,7 @@
3.31 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.32 (*...copied from stac2tac_*)
3.33 str2term (
3.34 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.35 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.36 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.37 " REAL_LIST [c, c_2]]");
3.38 val ags = isalist2list ags';
3.39 @@ -450,7 +450,7 @@
3.40 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.41 (*...copied from stac2tac_*)
3.42 str2term (
3.43 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.44 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.45 " [BOOL_LIST [c_2 = 0, L * c + c_2 = q_0 * L ^^^ 2 / 2]," ^
3.46 " REAL_LIST [c, c_2], BOOL_LIST ss''']");
3.47 val ags = isalist2list ags';
3.48 @@ -476,7 +476,7 @@
3.49 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.50 (*...copied from stac2tac_*)
3.51 str2term (
3.52 - "SubProblem (EqSystem', [LINEAR, system], [no_met]) " ^
3.53 + "SubProblem (EqSystemX, [LINEAR, system], [no_met]) " ^
3.54 " [REAL_LIST [c, c_2]]");
3.55 val ags = isalist2list ags';
3.56 val pI = ["LINEAR","system"];
3.57 @@ -521,7 +521,7 @@
3.58 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.59 (*...copied from stac2tac_*)
3.60 str2term (
3.61 - "SubProblem (Test',[univariate,equation,test]," ^
3.62 + "SubProblem (TestX,[univariate,equation,test]," ^
3.63 " [no_met]) [BOOL (x+1=2), REAL x]");
3.64 val AGS = isalist2list ags';
3.65 val pI = ["univariate","equation","test"];
3.66 @@ -539,7 +539,7 @@
3.67 (Const ("Product_Type.Pair",_) $ pI' $ mI')) $ ags' =
3.68 (*...copied from stac2tac_*)
3.69 str2term (
3.70 - "SubProblem (Test',[univariate,equation,test]," ^
3.71 + "SubProblem (TestX,[univariate,equation,test]," ^
3.72 " [no_met]) [BOOL (x+1=2), REAL x]");
3.73 val AGS = isalist2list ags';
3.74 val pI = ["univariate","equation","test"];
4.1 --- a/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Thu Nov 29 18:09:44 2018 +0100
4.2 +++ b/test/Tools/isac/Knowledge/Inverse_Z_Transform/inverse_z_transform.sml Fri Nov 30 12:27:18 2018 +0100
4.3 @@ -34,7 +34,7 @@
4.4 " (zzz::real) = argument_in X'_z; "^(* z *)
4.5 " (funterm::real) = rhs X'; "^(* 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))*)
4.6
4.7 - " (pbz::real) = (SubProblem (Isac', "^(**)
4.8 + " (pbz::real) = (SubProblem (IsacX, "^(**)
4.9 " [partial_fraction,rational,simplification], "^
4.10 " [simplification,of_rationals,to_partial_fraction]) "^
4.11 " [REAL funterm, REAL zzz]); "^(*([2], Res), 4 / (z - 1 / 2) + -4 / (z - -1 / 4)*)
5.1 --- a/test/Tools/isac/Knowledge/diffapp.sml Thu Nov 29 18:09:44 2018 +0100
5.2 +++ b/test/Tools/isac/Knowledge/diffapp.sml Fri Nov 30 12:27:18 2018 +0100
5.3 @@ -775,7 +775,7 @@
5.4 \ [BOOL e_2, REAL v_2])";
5.5 val s = subst_atomic env t;
5.6 term2str s;
5.7 -"SubProblem (Reals_, [univar, equation], [no_met])\
5.8 +"SubProblem (Reals_s, [univar, equation], [no_met])\
5.9 \ [BOOL (b / 2 = r * cos alpha), REAL b]";
5.10 val s_2 = str2term "[b = 2*r*cos alpha]";
5.11 val env = env @ [(str2term "s_2::bool list", s_2)];
6.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Thu Nov 29 18:09:44 2018 +0100
6.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri Nov 30 12:27:18 2018 +0100
6.3 @@ -361,7 +361,7 @@
6.4 " (numer::real) = get_numerator f_f; " ^(*numer: 24*)
6.5 " (denom::real) = get_denominator f_f; " ^(*denom: -1 + -2 * z + 8 * z ^^^ 2*)
6.6 " (equ::bool) = (denom = (0::real)); " ^(*equ: -1 + -2 * z + 8 * z ^^^ 2 = 0*)
6.7 - " (L_L::bool list) = (SubProblem (PolyEq', " ^
6.8 + " (L_L::bool list) = (SubProblem (PolyEqX, " ^
6.9 " [abcFormula, degree_2, polynomial, univariate, equation], " ^
6.10 " [no_met]) [BOOL equ, REAL zzz]); " ^(*L_L: [z = 1 / 2, z = -1 / 4]*)
6.11 " (facs::real) = factors_from_solution L_L; " ^(*facs: (z - 1 / 2) * (z - -1 / 4)*)
6.12 @@ -381,14 +381,14 @@
6.13 " eq_a = (Substitute [zzz = z1]) eq; " ^(*eq_a: 3 = A * (1 / 2 - -1 / 4) + B * (1 / 2 - 1 / 2)*)
6.14 " eq_a = (Rewrite_Set norm_Rational False) eq_a; " ^(*eq_a: 3 = 3 * A / 4*)
6.15 " (sol_a::bool list) = " ^
6.16 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
6.17 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
6.18 " [BOOL eq_a, REAL (A::real)]); " ^(*sol_a: [A = 4]*)
6.19 " (a::real) = (rhs (NTH 1 sol_a)); " ^(*a: 4*)
6.20 " (eq_b::bool) = Take eq; " ^(*eq_b: 3 = A * (z - -1 / 4) + B * (z - 1 / 2)*)
6.21 " eq_b = (Substitute [zzz = z2]) eq_b; " ^(*eq_b: *)
6.22 " eq_b = (Rewrite_Set norm_Rational False) eq_b; " ^(*eq_b: *)
6.23 " (sol_b::bool list) = " ^
6.24 - " (SubProblem (Isac', [univariate,equation], [no_met]) " ^
6.25 + " (SubProblem (IsacX, [univariate,equation], [no_met]) " ^
6.26 " [BOOL eq_b, REAL (B::real)]); " ^(*sol_b: [B = -4]*)
6.27 " (b::real) = (rhs (NTH 1 sol_b)); " ^(*b: -4*)
6.28 " eqr = drop_questionmarks eqr; " ^(*eqr: A / (z - 1 / 2) + B / (z - -1 / 4)*)
7.1 --- a/test/Tools/isac/Knowledge/rateq.sml Thu Nov 29 18:09:44 2018 +0100
7.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Fri Nov 30 12:27:18 2018 +0100
7.3 @@ -311,7 +311,7 @@
7.4 "~~~~~ fun nxt_up, args:"; val (thy, ptp, scr, E, l, ay,
7.5 (t as Const ("HOL.Let",_) $ e $ (Abs (i,T,b))), a, v) = (thy, ptp, (Prog sc), E, up, ay, (go up sc), a, v);
7.6
7.7 -term2str t = "let L_La =\n SubProblem (RatEq', [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
7.8 +term2str t = "let L_La =\n SubProblem (RatEqX, [univariate, equation], [no_met])\n [BOOL e_e, REAL v_v]\nin Check_elementwise L_L {v_v. Assumptions}";
7.9
7.10 (* comment from BEFORE Isabelle2002 --> 2011:
7.11 nxt_up thy ptp (Prog sc) E up ay (go up sc) a v;
8.1 --- a/test/Tools/isac/OLDTESTS/script.sml Thu Nov 29 18:09:44 2018 +0100
8.2 +++ b/test/Tools/isac/OLDTESTS/script.sml Fri Nov 30 12:27:18 2018 +0100
8.3 @@ -43,13 +43,13 @@
8.4 \ (v_::real) (itv_::real set) (err_::bool) = \
8.5 \ (let e_e = (hd o (filterVar m_)) rs_; \
8.6 \ t_ = (if 1 < length_ rs_ \
8.7 - \ then (SubProblem (Reals_,[make,function],[no_met])\
8.8 + \ then (SubProblem (Reals_s,[make,function],[no_met])\
8.9 \ [REAL m_, REAL v_v, BOOL_LIST rs_])\
8.10 \ else (hd rs_)); \
8.11 - \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
8.12 + \ (mx_::real) = SubProblem (Reals_s,[on_interval,max_of,function], \
8.13 \ [Isac,maximum_on_interval])\
8.14 \ [BOOL t_, REAL v_v, REAL_SET itv_]\
8.15 - \ in ((SubProblem (Reals_,[find_values,tool],[Isac,find_values]) \
8.16 + \ in ((SubProblem (Reals_s,[find_values,tool],[Isac,find_values]) \
8.17 \ [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, \
8.18 \ BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list))";
8.19
8.20 @@ -68,9 +68,9 @@
8.21 \ v_2 = nth_ 2 vs_; \
8.22 \ e_1 = (hd o (filterVar v_1)) es_; \
8.23 \ e_2 = (hd o (filterVar v_2)) es_; \
8.24 - \ (s_1::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
8.25 + \ (s_1::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
8.26 \ [BOOL e_1, REAL v_1]);\
8.27 - \ (s_2::bool list) = (SubProblem (Reals_,[univar,equation],[no_met])\
8.28 + \ (s_2::bool list) = (SubProblem (Reals_s,[univar,equation],[no_met])\
8.29 \ [BOOL e_2, REAL v_2])\
8.30 \in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)";
8.31
8.32 @@ -148,7 +148,7 @@
8.33 \ e_1 = hd (dropWhile (ident h_) eqs_); \
8.34 \ vs_ = dropWhile (ident f_) (Vars h_); \
8.35 \ v_1 = hd (dropWhile (ident v_v) vs_); \
8.36 - \ (s_1::bool list)=(SubProblem(Reals_,[univar,equation],[no_met])\
8.37 + \ (s_1::bool list)=(SubProblem(Reals_s,[univar,equation],[no_met])\
8.38 \ [BOOL e_1, REAL v_1])\
8.39 \ in Substitute [(v_1 = (rhs o hd) s_1)] h_)";
8.40
9.1 --- a/test/Tools/isac/OLDTESTS/script_if.sml Thu Nov 29 18:09:44 2018 +0100
9.2 +++ b/test/Tools/isac/OLDTESTS/script_if.sml Fri Nov 30 12:27:18 2018 +0100
9.3 @@ -87,9 +87,9 @@
9.4 asm_rls=[],asm_thm=[]},
9.5 "Script Solve_univar_err (e_e::bool) (v_::real) (err_::bool) = \
9.6 \ (if (is_rootequation_in e_e v_v)\
9.7 - \ then ((SubProblem (Isac_,[squareroot,univariate,equation],\
9.8 + \ then ((SubProblem (IsacX,[squareroot,univariate,equation],\
9.9 \ (SqRoot_,square_equation)) [BOOL e_e, REAL v_v, BOOL err_]))\
9.10 - \ else ((SubProblem (Isac_,[linear,univariate,equation],\
9.11 + \ else ((SubProblem (IsacX,[linear,univariate,equation],\
9.12 \ (RatArith_,solve_linear)) [BOOL e_e, REAL v_])))"
9.13 )]);
9.14
10.1 --- a/test/Tools/isac/OLDTESTS/scriptnew.sml Thu Nov 29 18:09:44 2018 +0100
10.2 +++ b/test/Tools/isac/OLDTESTS/scriptnew.sml Fri Nov 30 12:27:18 2018 +0100
10.3 @@ -486,7 +486,7 @@
10.4 val scr = Prog ((inst_abs o Thm.term_of o the o (parse thy))
10.5 "Script Biquadrat_poly (e_e::bool) (v_::real) = \
10.6 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
10.7 - \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \
10.8 + \ L_0_ = (SubProblem (PolyEqX,[univariate,equation], [no_met]) \
10.9 \ [BOOL e_e, REAL v_0_]); \
10.10 \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \
10.11 \ ((Rewrite real_root_positive False) Or \
11.1 --- a/test/Tools/isac/ProgLang/scrtools.sml Thu Nov 29 18:09:44 2018 +0100
11.2 +++ b/test/Tools/isac/ProgLang/scrtools.sml Fri Nov 30 12:27:18 2018 +0100
11.3 @@ -334,7 +334,7 @@
11.4 val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
11.5 case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
11.6
11.7 -@{term "(SubProblem (Biegelinie',[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
11.8 +@{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
11.9 case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
11.10
11.11 (* --- fun subst_stacexpr *)