1.1 --- a/src/Tools/isac/Build_Isac.thy Mon Sep 06 17:07:28 2010 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Wed Sep 08 10:15:51 2010 +0200
1.3 @@ -70,10 +70,15 @@
1.4 use_thy "Knowledge/LinEq"
1.5 use_thy "Knowledge/Root"
1.6
1.7 +
1.8 +ML {*
1.9 +incr_boundvars;
1.10 +*}
1.11 +
1.12 use_thy "Knowledge/RootEq"
1.13
1.14 +
1.15 ML {*
1.16 -111;
1.17 *}
1.18
1.19
2.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Mon Sep 06 17:07:28 2010 +0200
2.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Wed Sep 08 10:15:51 2010 +0200
2.3 @@ -7,11 +7,11 @@
2.4 date: 02.11.14
2.5 *)
2.6
2.7 -theory RootEq imports Root end
2.8 +theory RootEq imports Root begin
2.9
2.10 consts
2.11 - (*-------------------------root-----------------------*)
2.12 - is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
2.13 +
2.14 + is'_rootTerm'_in :: "[real, real] => bool" ("_ is'_rootTerm'_in _")
2.15 is'_sqrtTerm'_in :: "[real, real] => bool" ("_ is'_sqrtTerm'_in _")
2.16 is'_normSqrtTerm'_in :: "[real, real] => bool" ("_ is'_normSqrtTerm'_in _")
2.17
2.18 @@ -522,6 +522,7 @@
2.19 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
2.20 crls=RootEq_crls, nrls=norm_Poly(*,
2.21 asm_rls=[],asm_thm=[]*)}, "empty_script"));
2.22 +
2.23 (*-- normalize 20.10.02 --*)
2.24 store_met
2.25 (prep_met thy "met_rooteq_norm" [] e_metID
2.26 @@ -533,56 +534,72 @@
2.27 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
2.28 ("#Find" ,["solutions v_i"])
2.29 ],
2.30 - {rew_ord'="termlessI",
2.31 - rls'=RootEq_erls,
2.32 - srls=e_rls,
2.33 - prls=RootEq_prls,
2.34 - calc=[],
2.35 - crls=RootEq_crls, nrls=norm_Poly(*,
2.36 - asm_rls=[],
2.37 - asm_thm=[("sqrt_square_1","")]*)},
2.38 + {rew_ord'="termlessI", rls'=RootEq_erls, srls=e_rls, prls=RootEq_prls,
2.39 + calc=[], crls=RootEq_crls, nrls=norm_Poly},
2.40 "Script Norm_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.41 "(let e_e = ((Repeat(Try (Rewrite makex1_x False))) @@ " ^
2.42 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.43 " (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
2.44 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.45 " (Try (Rewrite_Set rooteq_simplify True))) e_e " ^
2.46 - " in ((SubProblem (RootEq_,[univariate,equation], " ^
2.47 - " [no_met]) [BOOL e_e, REAL v_])))"
2.48 + " in ((SubProblem (RootEq_',[univariate,equation], " ^
2.49 + " [no_met]) [BOOL e_e, REAL v_v])))"
2.50 ));
2.51
2.52 +*}
2.53 +
2.54 +ML {* (*-----del------------------------------------------------del-----*)
2.55 +Toplevel.debug := true;
2.56 +val scr =
2.57 +"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.58 +"(let e_e = " ^
2.59 +" ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
2.60 +" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
2.61 +" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.62 +" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.63 +" (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
2.64 +" (L_L::bool list) = " ^
2.65 +" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
2.66 +" then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^
2.67 +" [no_met]) [BOOL e_e, REAL v_v]) " ^
2.68 +" else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^
2.69 +" [BOOL e_e, REAL v_v])) " ^
2.70 +"in Check_elementwise L_L {(v_v::real). Assumptions})";
2.71 +val sss = ( term_of o the o (parse thy)) scr;
2.72 +*}
2.73 +
2.74 +ML {*
2.75 +val -------------------------------------------------- = "00000";
2.76 store_met
2.77 (prep_met thy "met_rooteq_sq" [] e_metID
2.78 (["RootEq","solve_sq_root_equation"],
2.79 - [("#Given" ,["equality e_e","solveFor v_v"]),
2.80 - ("#Where" ,["( ((lhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
2.81 - " ((lhs e_e) is_normSqrtTerm_in (v_v::real)) ) |" ^
2.82 - "( ((rhs e_e) is_sqrtTerm_in (v_v::real)) &" ^
2.83 - " ((rhs e_e) is_normSqrtTerm_in (v_v::real)) )"]),
2.84 + [("#Given" ,["equality e_e", "solveFor v_v"]),
2.85 + ("#Where" ,["(((lhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
2.86 + " ((lhs e_e) is_normSqrtTerm_in (v_v::real))) |" ^
2.87 + "(((rhs e_e) is_sqrtTerm_in (v_v::real)) & " ^
2.88 + " ((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
2.89 ("#Find" ,["solutions v_i"])
2.90 ],
2.91 - {rew_ord'="termlessI",
2.92 - rls'=RootEq_erls,
2.93 - srls = rooteq_srls,
2.94 - prls = RootEq_prls,
2.95 - calc = [],
2.96 - crls=RootEq_crls, nrls=norm_Poly},
2.97 -"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.98 -"(let e_e = " ^
2.99 -" ((Try (Rewrite_Set_Inst [(bdv,v_::real)] sqrt_isolate True)) @@ " ^
2.100 -" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
2.101 -" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.102 -" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.103 -" (Try (Rewrite_Set rooteq_simplify True))) e_;" ^
2.104 -" (L_::bool list) = " ^
2.105 -" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
2.106 -" then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
2.107 -" [no_met]) [BOOL e_e, REAL v_]) " ^
2.108 -" else (SubProblem (RootEq_,[univariate,equation], " ^
2.109 -" [no_met]) [BOOL e_e, REAL v_])) " ^
2.110 -" in Check_elementwise L_ {(v_v::real). Assumptions})"
2.111 + {rew_ord'="termlessI", rls'=RootEq_erls, srls = rooteq_srls,
2.112 + prls = RootEq_prls, calc = [], crls=RootEq_crls, nrls=norm_Poly},
2.113 +"Script Solve_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.114 +"(let e_e = " ^
2.115 +" ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] sqrt_isolate True)) @@ " ^
2.116 +" (Try (Rewrite_Set rooteq_simplify True)) @@ " ^
2.117 +" (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.118 +" (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.119 +" (Try (Rewrite_Set rooteq_simplify True)) ) e_e; " ^
2.120 +" (L_L::bool list) = " ^
2.121 +" (if (((lhs e_e) is_sqrtTerm_in v_v) | ((rhs e_e) is_sqrtTerm_in v_v))" ^
2.122 +" then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^
2.123 +" [no_met]) [BOOL e_e, REAL v_v]) " ^
2.124 +" else (SubProblem (RootEq_',[univariate,equation], [no_met]) " ^
2.125 +" [BOOL e_e, REAL v_v])) " ^
2.126 +"in Check_elementwise L_L {(v_v::real). Assumptions})"
2.127 ));
2.128 +*}
2.129
2.130 +ML {*
2.131 (*-- right 28.08.02 --*)
2.132 store_met
2.133 (prep_met thy "met_rooteq_sq_right" [] e_metID
2.134 @@ -591,25 +608,22 @@
2.135 ("#Where" ,["(rhs e_e) is_sqrtTerm_in v_v"]),
2.136 ("#Find" ,["solutions v_i"])
2.137 ],
2.138 - {rew_ord'="termlessI",
2.139 - rls'=RootEq_erls,
2.140 - srls=e_rls,
2.141 - prls=RootEq_prls,
2.142 - calc=[],
2.143 - crls=RootEq_crls, nrls=norm_Poly},
2.144 - "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.145 - "(let e_e = " ^
2.146 - " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] r_sqrt_isolate False)) @@ " ^
2.147 - " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
2.148 - " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.149 - " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.150 + {rew_ord' = "termlessI", rls' = RootEq_erls, srls = e_rls,
2.151 + prls = RootEq_prls, calc = [], crls = RootEq_crls, nrls = norm_Poly},
2.152 + "Script Solve_right_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.153 + "(let e_e = " ^
2.154 + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] r_sqrt_isolate False)) @@ " ^
2.155 + " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
2.156 + " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.157 + " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.158 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
2.159 - " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
2.160 - " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
2.161 - " [no_met]) [BOOL e_e, REAL v_]) " ^
2.162 - " else ((SubProblem (RootEq_,[univariate,equation], " ^
2.163 - " [no_met]) [BOOL e_e, REAL v_])))"
2.164 + " in if ((rhs e_e) is_sqrtTerm_in v_v) " ^
2.165 + " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^
2.166 + " [no_met]) [BOOL e_e, REAL v_v]) " ^
2.167 + " else ((SubProblem (RootEq_',[univariate,equation], " ^
2.168 + " [no_met]) [BOOL e_e, REAL v_v])))"
2.169 ));
2.170 +val --------------------------------------------------+++ = "33333";
2.171
2.172 (*-- left 28.08.02 --*)
2.173 store_met
2.174 @@ -627,17 +641,18 @@
2.175 crls=RootEq_crls, nrls=norm_Poly},
2.176 "Script Solve_left_sq_root_equation (e_e::bool) (v_v::real) = " ^
2.177 "(let e_e = " ^
2.178 - " ((Try (Rewrite_Set_Inst [(bdv,v_::real)] l_sqrt_isolate False)) @@ " ^
2.179 + " ((Try (Rewrite_Set_Inst [(bdv,v_v::real)] l_sqrt_isolate False)) @@ " ^
2.180 " (Try (Rewrite_Set rooteq_simplify False)) @@ " ^
2.181 " (Try (Repeat (Rewrite_Set expand_rootbinoms False))) @@ " ^
2.182 " (Try (Repeat (Rewrite_Set make_rooteq False))) @@ " ^
2.183 " (Try (Rewrite_Set rooteq_simplify False))) e_e " ^
2.184 " in if ((lhs e_e) is_sqrtTerm_in v_v) " ^
2.185 - " then (SubProblem (RootEq_,[normalize,root,univariate,equation], " ^
2.186 - " [no_met]) [BOOL e_e, REAL v_]) " ^
2.187 - " else ((SubProblem (RootEq_,[univariate,equation], " ^
2.188 - " [no_met]) [BOOL e_e, REAL v_])))"
2.189 + " then (SubProblem (RootEq_',[normalize,root',univariate,equation], " ^
2.190 + " [no_met]) [BOOL e_e, REAL v_v]) " ^
2.191 + " else ((SubProblem (RootEq_',[univariate,equation], " ^
2.192 + " [no_met]) [BOOL e_e, REAL v_v])))"
2.193 ));
2.194 +val --------------------------------------------------++++ = "44444";
2.195
2.196 calclist':= overwritel (!calclist',
2.197 [("is_rootTerm_in", ("RootEq.is'_rootTerm'_in",
3.1 --- a/src/Tools/isac/ProgLang/Script.thy Mon Sep 06 17:07:28 2010 +0200
3.2 +++ b/src/Tools/isac/ProgLang/Script.thy Wed Sep 08 10:15:51 2010 +0200
3.3 @@ -18,12 +18,12 @@
3.4 consts
3.5
3.6 (*types of subproblems' arguments*)
3.7 - real_' :: "real => arg"
3.8 - REAL_LIST' :: "(real list) => arg"
3.9 - REAL_SET' :: "(real set) => arg"
3.10 - BOOL' :: "bool => arg"
3.11 - BOOL_LIST' :: "(bool list) => arg"
3.12 - REAL_REAL' :: "(real => real) => arg"
3.13 + REAL :: "real => arg"
3.14 + REAL_LIST :: "(real list) => arg"
3.15 + REAL_SET :: "(real set) => arg"
3.16 + BOOL :: "bool => arg"
3.17 + BOOL_LIST :: "(bool list) => arg"
3.18 + REAL_REAL :: "(real => real) => arg"
3.19
3.20 (*tactics*)
3.21 Rewrite :: "[ID, bool, 'a] => 'a"
4.1 --- a/src/Tools/isac/ProgLang/term.sml Mon Sep 06 17:07:28 2010 +0200
4.2 +++ b/src/Tools/isac/ProgLang/term.sml Wed Sep 08 10:15:51 2010 +0200
4.3 @@ -20,7 +20,7 @@
4.4 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
4.5 handle _ => false
4.6
4.7 -fun atomtyp t = (*see raw_pp_typ*)
4.8 +fun atomtyp t = (*WN10 see raw_pp_typ*)
4.9 let
4.10 fun ato n (Type (s,[])) =
4.11 ("\n*** "^indent n^"Type ("^s^",[])")
4.12 @@ -37,9 +37,20 @@
4.13 ("\n*** "^indent n^"]")
4.14 | atol n (T::Ts) = (ato n T ^ atol n Ts)
4.15 (*in print (ato 0 t ^ "\n") end; TODO TUM10*)
4.16 -in writeln(ato 0 t) end;
4.17 +in writeln (ato 0 t) end;
4.18 +(*
4.19 +> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
4.20 +> atomtyp T;
4.21 +*** Type (fun,[
4.22 +*** Type (RealDef.real,[])
4.23 +*** Type (fun,[
4.24 +*** Type (IntDef.int,[])
4.25 +*** Type (nat,[])
4.26 +*** ]
4.27 +*** ]
4.28 +*)
4.29
4.30 -(*Prog.Tutorial.p.34*)
4.31 +(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*)
4.32 local
4.33 fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
4.34 fun pp_list xs = Pretty.list "[" "]" xs
4.35 @@ -64,49 +75,37 @@
4.36 (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
4.37 *)
4.38
4.39 -(*
4.40 -> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
4.41 -> atomtyp T;
4.42 -*** Type (fun,[
4.43 -*** Type (RealDef.real,[])
4.44 -*** Type (fun,[
4.45 -*** Type (IntDef.int,[])
4.46 -*** Type (nat,[])
4.47 -*** ]
4.48 -*** ]
4.49 -*)
4.50 -
4.51 fun atomt t =
4.52 - let fun ato (Const(a,T)) n =
4.53 - ("\n*** "^indent n^"Const ("^a^")")
4.54 - | ato (Free (a,T)) n =
4.55 - ("\n*** "^indent n^"Free ("^a^", "^")")
4.56 - | ato (Var ((a,ix),T)) n =
4.57 - ("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")")
4.58 - | ato (Bound ix) n =
4.59 - ("\n*** "^indent n^"Bound "^(string_of_int ix))
4.60 - | ato (Abs(a,T,body)) n =
4.61 - ("\n*** "^indent n^"Abs("^a^",..")^ato body (n+1)
4.62 - | ato (f$t') n = (ato f n; ato t' (n+1))
4.63 - in writeln("\n*** -------------"^ ato t 0 ^"\n***") end;
4.64 + let fun ato (Const (a, _)) n =
4.65 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
4.66 + | ato (Free (a, _)) n =
4.67 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
4.68 + | ato (Var ((a, i), _)) n =
4.69 + "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^
4.70 + string_of_int i ^ "), _)"
4.71 + | ato (Bound i) n =
4.72 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
4.73 + | ato (Abs (a, _, body)) n =
4.74 + "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
4.75 + | ato (f $ t) n = (ato f n ^ ato t (n + 1))
4.76 + in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
4.77
4.78 fun term_detail2str t =
4.79 - let fun ato (Const (a, T)) n =
4.80 - "\n*** "^indent n^"Const ("^a^", "^string_of_typ T^")"
4.81 - | ato (Free (a, T)) n =
4.82 - "\n*** "^indent n^"Free ("^a^", "^string_of_typ T^")"
4.83 - | ato (Var ((a, ix), T)) n =
4.84 - "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^
4.85 - string_of_typ T^")"
4.86 - | ato (Bound ix) n =
4.87 - "\n*** "^indent n^"Bound "^string_of_int ix
4.88 + let fun ato (Const (a, T)) n =
4.89 + "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
4.90 + | ato (Free (a, T)) n =
4.91 + "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")"
4.92 + | ato (Var ((a, i), T)) n =
4.93 + "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
4.94 + string_of_typ T ^ ")"
4.95 + | ato (Bound i) n =
4.96 + "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
4.97 | ato (Abs(a, T, body)) n =
4.98 - "\n*** "^indent n^"Abs ("^a^", "^
4.99 - (string_of_typ T)^",.."
4.100 - ^ato body (n + 1)
4.101 - | ato (f $ t') n = ato f n^ato t' (n+1)
4.102 - in "\n*** "^ato t 0^"\n***" end;
4.103 -fun atomty t = (writeln o term_detail2str) t;
4.104 + "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
4.105 + ^ ato body (n + 1)
4.106 + | ato (f $ t) n = ato f n ^ ato t (n + 1)
4.107 + in "\n*** " ^ ato t 0 ^ "\n***" end;
4.108 +fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
4.109
4.110 fun term_str thy (Const(s,_)) = s
4.111 | term_str thy (Free(s,_)) = s
4.112 @@ -802,98 +801,28 @@
4.113 fun mk_Free (s,T) = Free(s,T);
4.114 fun mk_free T s = Free(s,T);
4.115
4.116 +(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*)
4.117 +fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*)
4.118 + let fun subst (t as Bound i, lev) =
4.119 + if i<lev then t (*var is locally bound*)
4.120 + else if i=lev then incr_boundvars lev arg
4.121 + else Bound(i-1) (*loose: change it*)
4.122 + | subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))
4.123 + | subst (f$t, lev) = subst(f,lev) $ subst(t,lev)
4.124 + | subst (t,lev) = t
4.125 + in subst (t,0) end;
4.126 +
4.127 (*instantiate let; necessary for ass_up*)
4.128 -fun inst_abs thy (Const sT) = Const sT
4.129 +fun inst_abs thy (Const sT) = Const sT (*TODO.WN100907 drop thy*)
4.130 | inst_abs thy (Free sT) = Free sT
4.131 | inst_abs thy (Bound n) = Bound n
4.132 | inst_abs thy (Var iT) = Var iT
4.133 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
4.134 - let val (v',b') = variant_abs (v,T2,b); (*fun variant_abs: term.ML*)
4.135 - in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
4.136 + | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) =
4.137 + let val b' = subst_bound (Free (v, T2), b);
4.138 + (*fun variant_abs: term.ML*)
4.139 + in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
4.140 | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
4.141 - | inst_abs thy t =
4.142 - (writeln("inst_abs: unchanged t= "^ term2str t);
4.143 - t);
4.144 -(*val scr as (Script sc) = Script ((term_of o the o (parse thy))
4.145 - "Script Testeq (e_::bool) = \
4.146 - \While (contains_root e_) Do \
4.147 - \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
4.148 - \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
4.149 - \ in Try (Repeat (Rewrite radd_0 False e_))) ");
4.150 -ML> atomt sc;
4.151 -*** Const ( Script.Testeq)
4.152 -*** . Free ( e_, )
4.153 -*** . Const ( Script.While)
4.154 -*** . . Const ( RatArith.contains'_root)
4.155 -*** . . . Free ( e_, )
4.156 -*** . . Const ( Let)
4.157 -*** . . . Const ( Script.Try)
4.158 -*** . . . . Const ( Script.Repeat)
4.159 -*** . . . . . Const ( Script.Rewrite)
4.160 -*** . . . . . . Free ( rroot_square_inv, )
4.161 -*** . . . . . . Const ( False)
4.162 -*** . . . . . . Free ( e_, )
4.163 -*** . . . Abs( e_,..
4.164 -*** . . . . Const ( Let)
4.165 -*** . . . . . Const ( Script.Try)
4.166 -*** . . . . . . Const ( Script.Repeat)
4.167 -*** . . . . . . . Const ( Script.Rewrite)
4.168 -*** . . . . . . . . Free ( square_equation_left, )
4.169 -*** . . . . . . . . Const ( True)
4.170 -*** . . . . . . . . Bound 0 <-- !!!
4.171 -*** . . . . . Abs( e_,..
4.172 -*** . . . . . . Const ( Script.Try)
4.173 -*** . . . . . . . Const ( Script.Repeat)
4.174 -*** . . . . . . . . Const ( Script.Rewrite)
4.175 -*** . . . . . . . . . Free ( radd_0, )
4.176 -*** . . . . . . . . . Const ( False)
4.177 -*** . . . . . . . . . Bound 0 <-- !!!
4.178 -val it = () : unit
4.179 -ML> atomt (inst_abs thy sc);
4.180 -*** Const ( Script.Testeq)
4.181 -*** . Free ( e_, )
4.182 -*** . Const ( Script.While)
4.183 -*** . . Const ( RatArith.contains'_root)
4.184 -*** . . . Free ( e_, )
4.185 -*** . . Const ( Let)
4.186 -*** . . . Const ( Script.Try)
4.187 -*** . . . . Const ( Script.Repeat)
4.188 -*** . . . . . Const ( Script.Rewrite)
4.189 -*** . . . . . . Free ( rroot_square_inv, )
4.190 -*** . . . . . . Const ( False)
4.191 -*** . . . . . . Free ( e_, )
4.192 -*** . . . Abs( e_,..
4.193 -*** . . . . Const ( Let)
4.194 -*** . . . . . Const ( Script.Try)
4.195 -*** . . . . . . Const ( Script.Repeat)
4.196 -*** . . . . . . . Const ( Script.Rewrite)
4.197 -*** . . . . . . . . Free ( square_equation_left, )
4.198 -*** . . . . . . . . Const ( True)
4.199 -*** . . . . . . . . Free ( e_, ) <-- !!!
4.200 -*** . . . . . Abs( e_,..
4.201 -*** . . . . . . Const ( Script.Try)
4.202 -*** . . . . . . . Const ( Script.Repeat)
4.203 -*** . . . . . . . . Const ( Script.Rewrite)
4.204 -*** . . . . . . . . . Free ( radd_0, )
4.205 -*** . . . . . . . . . Const ( False)
4.206 -*** . . . . . . . . . Free ( e_, ) <-- ZUFALL vor 5.03!!!
4.207 -val it = () : unit*)
4.208 -
4.209 -
4.210 -
4.211 -
4.212 -fun inst_abs thy (Const sT) = Const sT
4.213 - | inst_abs thy (Free sT) = Free sT
4.214 - | inst_abs thy (Bound n) = Bound n
4.215 - | inst_abs thy (Var iT) = Var iT
4.216 - | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) =
4.217 - let val b' = subst_bound (Free(v,T2),b);
4.218 - (*fun variant_abs: term.ML*)
4.219 - in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end
4.220 - | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
4.221 - | inst_abs thy t =
4.222 - (writeln("inst_abs: unchanged t= "^ term2str t);
4.223 - t);
4.224 + | inst_abs thy t = t;
4.225 (*val scr =
4.226 "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
4.227 \ (let h_ = (hd o (filterVar f_)) eqs_; \
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/test/Tools/isac/Run_Tests.thy Wed Sep 08 10:15:51 2010 +0200
5.3 @@ -0,0 +1,11 @@
5.4 +(*
5.5 +$ cd /usr/local/isabisac/test/Tools/isac
5.6 +$ /usr/local/isabisac/bin/isabelle emacs Run_Tests.thy &
5.7 +
5.8 +*)
5.9 +
5.10 +theory Run_Tests imports Main begin
5.11 +
5.12 +use "ProgLang/term.sml"
5.13 +
5.14 +end