walther@59633: (* Title:  ProgLang/auto_prog.sml
walther@59633:    Author: Walther Neuper 190922
walther@59633:    (c) due to copyright terms
walther@59633: *)
walther@59633: 
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: "table of contents -----------------------------------------------------------------------------";
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59637: "-------- fun op #> ----------------------------------------------------------------------------";
walther@59633: "-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633: "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59802: "-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59633: "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59636: "-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636: "-------- fun subst_typs -----------------------------------------------------------------------";
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: "-----------------------------------------------------------------------------------------------";
walther@59633: 
walther@59633: 
walther@59633: "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633: "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
walther@59633: "-------- check auto-gen.script for Rewrite_Set_Inst -------------------------------------------";
Walther@60543: val rls = get_rls @{context} "integration";
walther@59802: val thy' = @{theory "Integrate"}
Walther@60500: val ctxt = Proof_Context.init_global thy'
walther@59802: val t = @{term "ttt :: real"};
walther@59802: 
walther@59802:  Auto_Prog.gen thy' t rls;
walther@59932: "~~~~~ fun gen , args:"; val (thy, t, rls) = (thy', t, rls);
walther@59802:     val prog = case rls of
walther@59851: 	      Rule_Set.Repeat {rules, ...} => rules2scr_Rls thy rules
walther@59878: 	    | Rule_Set.Sequence {rules, ...} => rules2scr_Seq thy rules
walther@59802:     val auto_script = subst_typs prog (type_of t) (TermC.guess_bdv_typ t) (*return from generate*);
walther@59802: 
walther@59868: if UnparseC.term auto_script =
walther@59802:   "auto_generated_inst t_t v =\n" ^
walther@59802:   "(Try (Rewrite_Set_Inst [(''bdv'', v)] ''integration_rules'') #>\n" ^
walther@59802:   " Try (Rewrite_Set_Inst [(''bdv'', v)] ''add_new_c'') #>\n" ^
walther@59802:   " Try (Rewrite_Set_Inst [(''bdv'', v)] ''simplify_Integral''))\n" ^
walther@59802:   " ??.empty"
walther@59802: then () else error "Auto_Prog.gen integration CHANGED";
walther@59633: 
walther@59633: if contain_bdv (get_rules rls) then ()
walther@59633: else error "scrtools.sml: contain_bdv doesnt work for 'integration'";
walther@59633: 
walther@59997: if UnparseC.terms (formal_args auto_script) = "[\"t_t\", \"v\"]"
walther@59633: then () else error "formal_args of auto-gen.script changed";
walther@59802: 
Walther@60618:     Istate.init_detail ctxt (Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")) (TermC.parse_test @{context} "someTermWithBdv");
walther@59935: "~~~~~ fun init_detail , args:"; val ((Tactic.Rewrite_Set_Inst (subs, rls)), t)
Walther@60565:   = ((Rewrite_Set_Inst (["(''bdv'', x)"], "integration_rules")), TermC.parse_test @{context} "someTermWithBdv");
Walther@60574:       val v = case Tactic.subst_adapt_to_type ctxt subs of
walther@59802:         (_, v) :: _ => v;
Walther@60543:     (*case*) get_rls ctxt rls (*of*);
walther@59802: 
walther@59633: 
walther@59633: "-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Poly -----------------------------------------";
walther@59802: val thy' = @{theory "Poly"}
Walther@60543: val ctxt = Proof_Context.init_global thy'
Walther@60543: val rls = get_rls ctxt "norm_Poly";
walther@59802: val t = @{term "ttt :: real"}
walther@59802: val auto_script = Auto_Prog.gen thy' t rls;
walther@59802: 
walther@59868: if UnparseC.term auto_script =
walther@59802:   "auto_generated t_t =\n" ^
walther@59802:   "(Try (Rewrite_Set ''discard_minus'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''expand_poly_'') #>\n" ^
walther@59802:   " Try (Repeat (Calculate ''TIMES'')) #>\n" ^
walther@59802:   " Try (Rewrite_Set ''order_mult_rls_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''simplify_power_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''calc_add_mult_pow_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''reduce_012_mult_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''order_add_rls_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''collect_numerals_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''reduce_012_'') #>\n" ^
walther@59802:   " Try (Rewrite_Set ''discard_parentheses1''))\n" ^
walther@59802:   " ??.empty"  (*                          ..WORKS, NEVERTHELESS*)
walther@59802: then () else error "Auto_Prog.gen norm_Poly CHANGED";
walther@59633: 
Walther@60549: States.reset (); (*<-- evaluate, if ML-blocks are edited below*)
Walther@60571: CalcTree @{context}
walther@59633: [(["Term (b + a - b)", "normalform N"], 
walther@59997:   ("Poly",["polynomial", "simplification"],
walther@59997:   ["simplification", "for_polynomials"]))];
walther@59633: Iterator 1;
walther@59633: moveActiveRoot 1;
walther@59633: 
walther@59633: autoCalculate 1 CompleteCalc;
Walther@60549: val ((pt,p),_) = States.get_calc 1;
walther@59983: Test_Tool.show_pt pt;
walther@59633: (* isabisac17 = 15 [
walther@59633: (([], Frm), Simplify (b + a - b)),
walther@59633: (([1], Frm), b + a - b),
walther@59633: (([1], Res), a),
walther@59633: (([], Res), a)] *)
walther@59633: 
walther@59633: interSteps 1 ([], Res);
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59983: Test_Tool.show_pt pt;
walther@59633: (* isabisac17 = 15 [
walther@59633: (([], Frm), Simplify (b + a - b)),
walther@59633: (([1], Frm), b + a - b),
walther@59633: (([1], Res), a),
walther@59633: (([], Res), a)] *)
walther@59633: 
walther@59633: interSteps 1 ([1], Res);(*<SYSERROR><CALCID>1</CALCID><ERROR>error in kernel 8</ERROR></SYSERROR>*)
walther@59633: "~~~~~ fun interSteps, args:"; val (cI, ip) = (1, ([1], Res));
Walther@60549:  val ((pt, p), tacis) = States.get_calc cI;
walther@59633: (*if*) (not o is_interpos) ip = false;
walther@59633: val ip' = lev_pred' pt ip;
walther@59633: 
walther@59935: (*Detail_Step.go pt ip      ..ERROR interSteps>..>init_detail: "norm_Poly" has Empty_Prog*)
walther@59833: val ("donesteps", ctree_BEFORE_step_into, pos'_BEFORE_step_into) = Detail_Step.go pt ip;
walther@59833: "~~~~~ fun go, args:"; val (pt, (pos as (p, _))) = (pt, ip);
walther@59633:     val nd = Ctree.get_nd pt p
walther@59633:     val cn = Ctree.children nd;
walther@59633: (*if*) null cn = false;
walther@59633: 
walther@59633: "~~~~~ to detailrls return val:";
walther@59633: (*else*) 
walther@59694: val return_val = ("donesteps", pt, (p @ [length (Ctree.children (Ctree.get_nd pt p))], Pos.Res));
walther@59633: if p @ [length (Ctree.children (Ctree.get_nd pt p))] = [1, 4]
walther@59633: then () else error "detailrls: auto-generated norm_Poly doesnt work";
walther@59633: 
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59983: Test_Tool.show_pt pt; (*[
walther@59633: (([], Frm), Simplify (b + a - b)),
walther@59633: (([1], Frm), b + a - b),
walther@59633: (([1,1], Frm), b + a - b),
walther@59633: (([1,1], Res), b + a + -1 * b),
walther@59633: (([1,2], Res), a + b + -1 * b),
walther@59633: (([1,3], Res), a + 0 * b),
walther@59633: (([1,4], Res), a),
walther@59633: (([1], Res), a),
walther@59633: (([], Res), a)]  *)
walther@59633: if existpt' ([1,4], Res) pt then ()
walther@59633: else error  "auto-generated norm_Poly doesnt work";
walther@59633: 
walther@59802: 
walther@59633: "-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Rational -------------------------------------";
walther@59633: "-------- test the same called by interSteps norm_Rational -------------------------------------";
Walther@60543: val thy = @{theory (** )"Poly" ( **) Rational(**) (*required for rls "norm_Rational"*)}
Walther@60543: val ctxt = Proof_Context.init_global thy
Walther@60543: val auto_script = 
Walther@60543:   Auto_Prog.gen thy @{term "ttt :: real"} (get_rls ctxt "norm_Rational");
walther@59868: writeln(UnparseC.term auto_script);
Walther@60650: TermC.atom_trace_detail @{context} auto_script;
walther@59633: (*** 
walther@59633: *** Const (Program.Stepwise, 'z => 'z => 'z)
walther@59633: *** . Free (t_t, 'z)
walther@59633: *** . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633: *** . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
walther@59633: *** . . . . Free (discard_minus, ID)
walther@59633: *** . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633: *** . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633: *** . . . . . Free (rat_mult_poly, ID)
walther@59633: *** . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633: *** . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633: *** . . . . . . Free (make_rat_poly_with_parentheses, ID)
walther@59633: *** . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633: *** . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633: *** . . . . . . . Free (cancel_p_rls, ID)
walther@59633: *** . . . . . Const (Program.Seq, ('a => 'a) => ('a => 'a) => 'a => 'a)
walther@59633: *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . . . . . Const (Program.Rewrite_Set, ID  => 'a => 'a)
walther@59633: *** . . . . . . . . Free (norm_Rational_rls, ID)
walther@59633: *** . . . . . . Const (Program.Try, ('a => 'a) => 'a => 'a)
walther@60278: *** . . . . . . . Const (Program.Rewrite_Set, ID => 'a => 'a)
walther@59633: *** . . . . . . . . Free (discard_parentheses1, ID)
walther@59633: *** . . Const (empty, 'a)
walther@59633: ***)
Walther@60549: States.reset ();
Walther@60571: CalcTree @{context}
walther@59633: [(["Term (b + a - b)", "normalform N"], 
Walther@60543:   ((** )"Poly"( **)"Rational"(**),["polynomial", "simplification"],
walther@59997:   ["simplification", "of_rationals"]))];
walther@59633: Iterator 1;
walther@59633: moveActiveRoot 1;
walther@59633: autoCalculate 1 CompleteCalc;
walther@59633: 
walther@59633: interSteps 1 ([], Res);
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59633: 
walther@59633: interSteps 1 ([1], Res);
Walther@60549: val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
walther@59633: 
walther@59633: (*with "Program SimplifyScript (t_::real) =                \
walther@59635:        \  ((Rewrite_Set norm_Rational) t_)"
walther@59983: val (Form form, SOME tac, asm) = ME_Misc.pt_extract (pt, ([1], Res));
walther@59633: *)
Walther@60577: val (Form form, SOME tac, asm) = ME_Misc.pt_extract ctxt (pt, ([2], Res));
walther@59868: case (UnparseC.term form, tac, UnparseC.terms_to_strings asm) of
walther@59633:     ("a", Check_Postcond ["polynomial", "simplification"], []) => ()
walther@59633:   | _ => error "scrtools.sml: auto-generated norm_Rational doesnt work";
walther@59633: 
walther@59802: 
walther@59637: "-------- fun op #> ----------------------------------------------------------------------------";
walther@59637: "-------- fun op #> ----------------------------------------------------------------------------";
walther@59637: "-------- fun op #> ----------------------------------------------------------------------------";
walther@59852:  val rules = (#rules o Rule_Set.rep) isolate_root;
walther@59633:  val rs = map (rule2stac @{theory}) rules;
walther@59637:  val t = #> rs;
walther@59868: if UnparseC.term t = "Try (Repeat (Rewrite ''rroot_to_lhs'')) #>\n" ^ 
walther@59637:   "Try (Repeat (Rewrite ''rroot_to_lhs_mult'')) #>\n" ^ 
walther@59637:   "Try (Repeat (Rewrite ''rroot_to_lhs_add_mult'')) #>\n" ^ 
walther@59637:   "Try (Repeat (Rewrite ''risolate_root_add'')) #>\n" ^ 
walther@59637:   "Try (Repeat (Rewrite ''risolate_root_mult'')) #>\n" ^ 
walther@59635:   "Try (Repeat (Rewrite ''risolate_root_div''))"
walther@59637: then () else error "fun #> changed"
walther@59633: 
walther@59802: 
walther@59633: "-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633: "-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633: "-------- fun rules2scr_Rls --------------------------------------------------------------------";
walther@59633: (*compare Prog_Expr.*)
walther@60333: val prog = Auto_Prog.rules2scr_Rls @{theory} [\<^rule_thm>\<open>thm111\<close>, \<^rule_thm>\<open>refl\<close>]
walther@59633: ;
walther@59870: writeln (UnparseC.term_in_thy @{theory} prog);
walther@59633: (*auto_generated t_t =
walther@59633: Repeat
walther@59637:  ((Try (Repeat (Rewrite ''thm111'')) #>
walther@59635:    Try (Repeat (Rewrite ''refl'')))
walther@59633:    ??.empty)*)
walther@59633: ;
walther@59870: if UnparseC.term_in_thy @{theory} prog =
walther@59635:   "auto_generated t_t =\n" ^
walther@59635:   "Repeat\n" ^
walther@59637:   " ((Try (Repeat (Rewrite ''thm111'')) #> Try (Repeat (Rewrite ''refl'')))\n" ^
walther@59635:   "   ??.empty)"
walther@59635: then () else error "rules2scr_Rls auto_generated changed";
walther@59633: 
walther@59802: 
walther@59633: "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59633: "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@59633: "-------- fun rule2stac, fun rule2stac_inst ----------------------------------------------------";
walther@60337: val t = rule2stac @{theory} (Thm ("real_diff_minus", @{thm real_diff_minus}));
walther@59868: if UnparseC.term t = "Try (Repeat (Rewrite ''real_diff_minus''))" then ()
walther@59633: else error "rule2stac Thm.. changed";
walther@59633: 
Walther@60516: val t = rule2stac @{theory} (Eval (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"));
walther@59868: if UnparseC.term t = "Try (Repeat (Calculate ''PLUS''))" then ()
walther@59878: else error "rule2stac Eval.. changed";
walther@59633: 
walther@59633: val t = rule2stac @{theory} (Rls_ rearrange_assoc);
walther@59868: if UnparseC.term t = "Try (Rewrite_Set ''rearrange_assoc'')" then ()
walther@59633: else error "rule2stac Rls_.. changed";
walther@59633: 
walther@60337: val t = rule2stac_inst @{theory} (Thm ("risolate_bdv_add", @{thm risolate_bdv_add}));
walther@59868: if UnparseC.term t = "Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add''))" then ()
walther@59633: else error "rule2stac_inst Thm.. changed";
walther@59633: case t of
walther@60336:   (Const (\<^const_name>\<open>Try\<close>, _) $
walther@60336:     (Const (\<^const_name>\<open>Repeat\<close>, _) $
walther@60336:       (Const (\<^const_name>\<open>Rewrite_Inst\<close>, _) $
wenzelm@60309:         (Const (\<^const_name>\<open>Cons\<close>, _) $
wenzelm@60309:           (Const (\<^const_name>\<open>Pair\<close>, _) $
walther@59633:             bdv $
walther@59633:             Free ("v", _)) $
wenzelm@60309:           Const (\<^const_name>\<open>Nil\<close>, _)) $
walther@59635:         risolate_bdv_add))) => 
walther@59633:       (if HOLogic.dest_string bdv = "bdv" andalso 
walther@59633:         HOLogic.dest_string risolate_bdv_add = "risolate_bdv_add" then ()
walther@59633:       else error "rule2stac_inst changed 1")
walther@59633: | _ => error "rule2stac_inst changed 2";
walther@59633: 
walther@59802: 
walther@59802: "-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59802: "-------- fun stacpbls, fun eval_leaf -----------------------------------";
walther@59802: "-------- fun stacpbls, fun eval_leaf -----------------------------------";
Walther@60586: val {program, ...} = MethodC.from_store ctxt ["Test", "sqrt-equ-test"]; val Prog sc = program; val ts = stacpbls sc;
walther@59633: case stacpbls sc of
walther@60336:   [Const (\<^const_name>\<open>Rewrite\<close>, _) $ square_equation_left,
walther@60336:    Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ Test_simplify,
walther@60336:    Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ rearrange_assoc,
walther@60336:    Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ isolate_root,
walther@60336:    Const (\<^const_name>\<open>Rewrite_Set\<close>, _) $ norm_equation,
walther@60336:    Const (\<^const_name>\<open>Rewrite_Set_Inst\<close>, _) $
wenzelm@60309:      (Const (\<^const_name>\<open>Cons\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ bdv $ Free ("v_v", _)) $
wenzelm@60309:        Const (\<^const_name>\<open>Nil\<close>, _)) $ isolate_bdv] => 
walther@59633:      if HOLogic.dest_string square_equation_left = "square_equation_left" andalso
walther@59633:        HOLogic.dest_string Test_simplify = "Test_simplify" andalso
walther@59633:        HOLogic.dest_string rearrange_assoc = "rearrange_assoc" andalso
walther@59633:        HOLogic.dest_string isolate_root = "isolate_root" andalso
walther@59633:        HOLogic.dest_string norm_equation = "norm_equation" andalso
walther@59633:        HOLogic.dest_string bdv = "bdv" andalso
walther@59633:        HOLogic.dest_string isolate_bdv = "isolate_bdv"
walther@59633:      then () else error "stacpbls (Test.Solve_root_equation) changed 2"
walther@59633: | _  => error "stacpbls (Test.Solve_root_equation) changed 1";
walther@59633: 
walther@59633: (* inappropriate input is skipped *)
walther@59633: val t = @{term "(a::real) = (rhs (NTH 1 sol_a))"};
walther@59633: case stacpbls t of [] => () | _ => error "stacpbls rhs (NTH 1 sol_a) changed";
walther@59633: 
walther@59633: @{term "(SubProblem (BiegelinieX,[vonBelastungZu,Biegelinien], [Biegelinien,ausBelastung]) [REAL q__q, REAL v_v])"};
walther@59633: case stacpbls t of [] => () | _ => error "stacpbls (SubProblem ...) changed";
walther@59633: 
walther@59802: 
walther@59633: "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633: "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633: "-------- fun is_calc, fun op_of_calc ----------------------------------------------------------";
walther@59633: val rls = prep_rls @{theory} Test_simplify; (* adds the Program *)
walther@59802: val sc = Auto_Prog.gen thy' t rls;
walther@59633: val stacs = stacpbls sc;
walther@59633: 
walther@59633: val calcs = filter is_calc stacs;
walther@59633: val ids = map op_of_calc calcs;
walther@59633: case ids of
walther@59633:   ["PLUS", "TIMES", "DIVIDE", "POWER"] => ()
walther@59633: | _ => error "op_of_calc";
walther@59633: 
Walther@60550: val calcs = ((get_calc (@{theory} |> Proof_Context.init_global) |> map) o (map Auto_Prog.op_of_calc) o
walther@59633:   (filter Auto_Prog.is_calc) o Auto_Prog.stacpbls) sc;
walther@59633: case calcs of
wenzelm@60309:   [("PLUS", (\<^const_name>\<open>plus\<close>, _)), ("TIMES", (\<^const_name>\<open>times\<close>, _)), 
wenzelm@60405:   ("DIVIDE", (\<^const_name>\<open>divide\<close>, _)), ("POWER", (\<^const_name>\<open>realpow\<close>, _))] => ()
walther@59633: | _ => error "get_calcs changed"
walther@59636: 
walther@59802: 
walther@59636: "-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636: "-------- fun subst_typ ------------------------------------------------------------------------";
walther@59636: "-------- fun subst_typ ------------------------------------------------------------------------";
Walther@60543: val thy = @{theory "Isac_Knowledge"}
Walther@60543: val ctxt = Proof_Context.init_global thy
Walther@60543: val prog = Auto_Prog.gen thy t (get_rls ctxt "isolate_bdv");
walther@59868: (* UnparseC.term prog |> writeln
walther@59636: auto_generated_inst t_t v =
walther@59636: Repeat
walther@59637:  ((Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_add'')) #>
walther@59637:    Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult_add'')) #>
walther@59637:    Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''risolate_bdv_mult'')) #>
walther@59637:    Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''mult_square'')) #>
walther@59637:    Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_square'')) #>
walther@59636:    Try (Repeat (Rewrite_Inst [(''bdv'', v)] ''constant_mult_square'')))
walther@59636:    ??.empty) 
walther@59636: *)
walther@59636: 
walther@59802: val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59802: if length frees = 2 then () else error "test setup Auto_Prog.subst_typ changed 1";
walther@59802: 
walther@59636: val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59636: if length args = 2 then () else error "test setup Auto_Prog.subst_typ changed 2";
walther@59636: 
walther@59636: val typ_t = HOLogic.realT
walther@59636: val typ_bdv = HOLogic.realT
walther@59636: 
walther@59636: val vars_v = (* = [Free ("v", "real"), Free ("v", "'a")]*)
walther@59636:   filter (fn t => curry op = (t |> dest_Free |> fst) "v") frees
walther@59636: val typs_v = (* = ["real", "'a"]*)
walther@59636:   map (fn t => (t |> dest_Free |> snd)) vars_v;
walther@59636: 
walther@59802: val subst_ty = subst_typ "v" HOLogic.realT frees; (* = [("real", "real")]*)
walther@59802: if length subst_ty = 1 then () else error "Auto_Prog.subst_typ changed";
walther@59802: 
walther@59636: 
walther@59636: "-------- fun subst_typs -----------------------------------------------------------------------";
walther@59636: "-------- fun subst_typs -----------------------------------------------------------------------";
walther@59636: "-------- fun subst_typs -----------------------------------------------------------------------";
Walther@60543: val prog = Auto_Prog.gen thy' t (get_rls ctxt "isolate_bdv");
walther@59636: val frees = vars prog; (* = [Free ("t_t", "'z"), Free ("v", "real"), Free ("v", "'a")]*)
walther@59802: if length frees = 2 then () else error "test setup Auto_Prog.subst_typs changed 1";
walther@59802: 
walther@59636: val args = formal_args prog; (* = [Free ("t_t", "'z"), Free ("v", "real")]*)
walther@59636: if length args = 2 then () else error "test setup Auto_Prog.subst_typs changed 2";
walther@59636: 
walther@59636: val prog' = subst_typs prog HOLogic.realT HOLogic.realT
walther@59636: val frees' = vars prog'; (* = [Free ("t_t", "'z"), Free ("v", "real")]*);
walther@59636: if length frees' = 2 then () else error "Auto_Prog.subst_typs changed 2"