1.1 --- a/test/Tools/isac/Interpret/script.sml Thu Oct 27 10:48:24 2016 +0200
1.2 +++ b/test/Tools/isac/Interpret/script.sml Sat Nov 12 17:21:43 2016 +0100
1.3 @@ -14,6 +14,12 @@
1.4 "----------- 'trace_script' from outside 'fun me '----------------";
1.5 "----------- fun sel_rules ---------------------------------------";
1.6 "----------- fun sel_appl_atomic_tacs ----------------------------";
1.7 +"----------- fun de_esc_underscore -------------------------------";
1.8 +"----------- fun go ----------------------------------------------";
1.9 +"----------- fun formal_args -------------------------------------";
1.10 +"----------- fun dsc_valT ----------------------------------------";
1.11 +"----------- fun itms2args ---------------------------------------";
1.12 +"----------- fun rep_tac_ ----------------------------------------";
1.13 "-----------------------------------------------------------------";
1.14 "-----------------------------------------------------------------";
1.15 "-----------------------------------------------------------------";
1.16 @@ -570,7 +576,7 @@
1.17 val f =
1.18 case p_ of
1.19 Frm => get_obj g_form pt p
1.20 - | Res => (fst o (get_obj g_result pt)) p
1.21 + | Res => (fst o (get_obj g_result pt)) p;
1.22 (*WN120611 stopped and took version 1 again for fetchApplicableTactics !
1.23 (distinct o flat o (map (atomic_appl_tacs thy ro erls f))) alltacs
1.24 ...
1.25 @@ -578,3 +584,169 @@
1.26 ### atomic_appl_tacs: not impl. for tac = 'Check_elementwise "Assumptions"'
1.27 *)
1.28
1.29 +"----------- fun de_esc_underscore -------------------------------";
1.30 +"----------- fun de_esc_underscore -------------------------------";
1.31 +"----------- fun de_esc_underscore -------------------------------";
1.32 +(*
1.33 +> val str = "Rewrite_Set_Inst";
1.34 +> val esc = esc_underscore str;
1.35 +val it = "Rewrite'_Set'_Inst" : string
1.36 +> val des = de_esc_underscore esc;
1.37 + val des = de_esc_underscore esc;*)
1.38 +
1.39 +"----------- fun go ----------------------------------------------";
1.40 +"----------- fun go ----------------------------------------------";
1.41 +"----------- fun go ----------------------------------------------";
1.42 +(*
1.43 +> val t = (Thm.term_of o the o (parse thy)) "a+b";
1.44 +val it = Const (#,#) $ Free (#,#) $ Free ("b","RealDef.real") : term
1.45 +> val plus_a = go [L] t;
1.46 +> val b = go [R] t;
1.47 +> val plus = go [L,L] t;
1.48 +> val a = go [L,R] t;
1.49 +
1.50 +> val t = (Thm.term_of o the o (parse thy)) "a+b+c";
1.51 +val t = Const (#,#) $ (# $ # $ Free #) $ Free ("c","RealDef.real") : term
1.52 +> val pl_pl_a_b = go [L] t;
1.53 +> val c = go [R] t;
1.54 +> val a = go [L,R,L,R] t;
1.55 +> val b = go [L,R,R] t;
1.56 +*)
1.57 +
1.58 +"----------- fun formal_args -------------------------------------";
1.59 +"----------- fun formal_args -------------------------------------";
1.60 +"----------- fun formal_args -------------------------------------";
1.61 +(*
1.62 +> formal_args scr;
1.63 + [Free ("f_","RealDef.real"),Free ("v_","RealDef.real"),
1.64 + Free ("eqs_","bool List.list")] : term list
1.65 +*)
1.66 +"----------- fun dsc_valT ----------------------------------------";
1.67 +"----------- fun dsc_valT ----------------------------------------";
1.68 +"----------- fun dsc_valT ----------------------------------------";
1.69 +(*> val t = (Thm.term_of o the o (parse thy)) "equality";
1.70 +> val T = type_of t;
1.71 +val T = "bool => Tools.una" : typ
1.72 +> val dsc = dsc_valT t;
1.73 +val dsc = "una" : string
1.74 +
1.75 +> val t = (Thm.term_of o the o (parse thy)) "fixedValues";
1.76 +> val T = type_of t;
1.77 +val T = "bool List.list => Tools.nam" : typ
1.78 +> val dsc = dsc_valT t;
1.79 +val dsc = "nam" : string*)
1.80 +"----------- fun itms2args ---------------------------------------";
1.81 +"----------- fun itms2args ---------------------------------------";
1.82 +"----------- fun itms2args ---------------------------------------";
1.83 +(*
1.84 +> val sc = ... Solve_root_equation ...
1.85 +> val mI = ("Script","sqrt-equ-test");
1.86 +> val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
1.87 +> val ts = itms2args thy mI itms;
1.88 +> map (term_to_string''' thy) ts;
1.89 +["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
1.90 +*)
1.91 +"----------- fun rep_tac_ ----------------------------------------";
1.92 +"----------- fun rep_tac_ ----------------------------------------";
1.93 +"----------- fun rep_tac_ ----------------------------------------";
1.94 +(***************fun rep_tac_ (Rewrite_Inst' (thy', rod, rls, put, subs, (thmID, _), f, (f', _))) =
1.95 +Fehlersuche 25.4.01
1.96 +(a)----- als String zusammensetzen:
1.97 +ML> term2str f;
1.98 +val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
1.99 +ML> term2str f';
1.100 +val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
1.101 +ML> subs;
1.102 +val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
1.103 +> val tt = (Thm.term_of o the o (parse thy))
1.104 + "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
1.105 +> atomty tt;
1.106 +ML> tracing (term2str tt);
1.107 +(Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
1.108 + #0 + d_d x (x ^^^ #2 + #3 * x)
1.109 +
1.110 +(b)----- laut rep_tac_:
1.111 +> val ttt=HOLogic.mk_eq (lhs,f');
1.112 +> atomty ttt;
1.113 +
1.114 +
1.115 +(*Fehlersuche 1-2Monate vor 4.01:*)
1.116 +> val tt = (Thm.term_of o the o (parse thy))
1.117 + "Rewrite_Inst[(bdv,x)]square_equation_left True(x=#1+#2)";
1.118 +> atomty tt;
1.119 +
1.120 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.121 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.122 +> val subs = [((Thm.term_of o the o (parse thy)) "bdv",
1.123 + (Thm.term_of o the o (parse thy)) "x")];
1.124 +> val sT = (type_of o fst o hd) subs;
1.125 +> val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.126 + (map HOLogic.mk_prod subs);
1.127 +> val sT' = type_of subs';
1.128 +> val lhs = Const ("Script.Rewrite'_Inst",[sT',idT,fT,fT] ---> fT)
1.129 + $ subs' $ Free (thmID,idT) $ @{term True} $ f;
1.130 +> lhs = tt;
1.131 +val it = true : bool
1.132 +> rep_tac_ (Rewrite_Inst'
1.133 + ("Script","tless_true","eval_rls",false,subs,
1.134 + ("square_equation_left",""),f,(f',[])));
1.135 +*)
1.136 +(****************************| rep_tac_ (Rewrite' (thy', _, _, put, (thmID, _), f, (f', _)))=
1.137 +> val tt = (Thm.term_of o the o (parse thy)) (*____ ____..test*)
1.138 + "Rewrite square_equation_left True (x=#1+#2) = (x=#3)";
1.139 +
1.140 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.141 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.142 +> val Thm (id,thm) =
1.143 + rep_tac_ (Rewrite'
1.144 + ("Script","tless_true","eval_rls",false,
1.145 + ("square_equation_left",""),f,(f',[])));
1.146 +> val SOME ct = parse thy
1.147 + "Rewrite square_equation_left True (x=#1+#2)";
1.148 +> rewrite_ Script.thy tless_true eval_rls true thm ct;
1.149 +val it = SOME ("x = #3",[]) : (cterm * cterm list) option
1.150 +*)
1.151 +(**************************************** | rep_tac_ (Rewrite_Set_Inst'
1.152 +WN050824: type error ...
1.153 + let val fT = type_of f;
1.154 + val sT = (type_of o fst o hd) subs;
1.155 + val subs' = list2isalist (HOLogic.mk_prodT (sT, sT))
1.156 + (map HOLogic.mk_prod subs);
1.157 + val sT' = type_of subs';
1.158 + val b = if put then @{term True} else @{term False}
1.159 + val lhs = Const ("Script.Rewrite'_Set'_Inst",
1.160 + [sT',idT,fT,fT] ---> fT)
1.161 + $ subs' $ Free (id_rls rls,idT) $ b $ f;
1.162 + in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end*)
1.163 +(* ... vals from Rewrite_Inst' ...
1.164 +> rep_tac_ (Rewrite_Set_Inst'
1.165 + ("Script",false,subs,
1.166 + "isolate_bdv",f,(f',[])));
1.167 +*)
1.168 +(* val (Rewrite_Set' (thy',put,rls,f,(f',asm)))=m;
1.169 +*)
1.170 +(************************************** | rep_tac_ (Rewrite_Set' (thy',put,rls,f,(f',asm)))=
1.171 +13.3.01:
1.172 +val thy = assoc_thy thy';
1.173 +val t = HOLogic.mk_eq (lhs,f');
1.174 +make_rule thy t;
1.175 +--------------------------------------------------
1.176 +val lll = (Thm.term_of o the o (parse thy))
1.177 + "Rewrite_Set SqRoot_simplify False (d_d x (x ^^^ #2 + #3 * x) + d_d x #4)";
1.178 +
1.179 +--------------------------------------------------
1.180 +> val f = (Thm.term_of o the o (parse thy)) "x=#1+#2";
1.181 +> val f' = (Thm.term_of o the o (parse thy)) "x=#3";
1.182 +> val Thm (id,thm) =
1.183 + rep_tac_ (Rewrite_Set'
1.184 + ("Script",false,"SqRoot_simplify",f,(f',[])));
1.185 +val id = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : string
1.186 +val thm = "(Rewrite_Set SqRoot_simplify True x = #1 + #2) = (x = #3)" : thm
1.187 +*)
1.188 +(***************************************** | rep_tac_ (Calculate' (thy',op_,f,(f',thm')))=
1.189 +> val lhs'=(Thm.term_of o the o (parse thy))"Calculate plus (#1+#2)";
1.190 + ... test-root-equ.sml: calculate ...
1.191 +> val Appl m'=applicable_in p pt (Calculate "PLUS");
1.192 +> val (lhs,_)=tac_2etac m';
1.193 +> lhs'=lhs;
1.194 +val it = true : bool*)