make Test_Isac.thy run in jEdit; intermed.
jEdit behaves differently from emacs in file dependencies.
Test_Isac.thy runs in emacs now.
For jEdit different uses seem appropriate; done in next step.
2 testexamples for RatEq, equations with fractions
4 Compiler.Control.Print.printDepth:=10; (*4 default*)
5 Compiler.Control.Print.printDepth:=5; (*4 default*)
10 "----------- rateq.sml begin--------";
11 "---------(1/x=5) ---------------------";
12 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
14 (*=== inhibit exn ?=============================================================
16 val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
17 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
18 val result = term2str t_;
19 if result <> "HOL.True" then error "rateq.sml: new behaviour 1:" else ();
21 val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
22 val SOME(t_, _) = rewrite_set_ RatEq.thy false RatEq_prls t;
23 val result = term2str t_;
24 if result <> "HOL.False" then error "rateq.sml: new behaviour 2:" else ();
26 val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
27 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
28 val result = term2str t_;
29 if result <> "HOL.False" then error "rateq.sml: new behaviour 3:" else ();
31 val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
32 val SOME(t_,_) = rewrite_set_ RatEq.thy false RatEq_prls t;
33 val result = term2str t_;
34 if result <> "HOL.True" then error "rateq.sml: new behaviour 4:" else ();
36 val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
37 (get_pbt ["rational","univariate","equation"]);
38 case result of NoMatch' _ => () | _ => error "rateq.sml: new behaviour: 5";
40 val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
41 (get_pbt ["rational","univariate","equation"]);
42 case result of Matches' _ => () | _ => error "rateq.sml: new behaviour: 6";
45 (*---------rateq---- 23.8.02 ---------------------*)
46 "---------(1/x=5) ---------------------";
47 val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
48 (* refine fmz ["univariate","equation"];
51 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
52 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
53 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
54 --------------------------------------- Refine_Tacitly*)
55 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
58 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
60 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
61 (* val nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"])*)
62 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
63 (* val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
64 --------------------------------------- Refine_Tacitly*)
65 (*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
66 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
67 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
68 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
70 (*val nxt = Apply_Method ["PolyEq", "normalize_poly"])*)
72 (* get_obj g_fmz pt [2];
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
76 (**** assoc_thm': 'all_left' not in 'RatEq.thy' (and parents)*)
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 (* val nxt = ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
82 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
84 (* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
85 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
93 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
94 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
95 else error "rateq.sml: new behaviour: [x = 1 / 5]";
99 (*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
100 "--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
101 (*EP Schalk_II_p68_n40*)
102 val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
103 (* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
104 "solveFor x","solutions L"];*)
106 (* refine fmz ["univariate","equation"];
109 val (dI',pI',mI') = ("RatEq",["univariate","equation"],["no_met"]);
112 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
113 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
114 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
116 (* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 (* nxt = ("Subproblem",Subproblem ("RatEq",["univariate","equation"]))*)
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 (* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
132 (* ("Subproblem", Subproblem ("PolyEq",["polynomial","univariate","equation"])) *)
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 (* nxt = ("Model_Problem", Model_Problem
135 ["abcFormula","degree_2","polynomial","univariate","equation"])*)
136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
137 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
138 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
139 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
143 (* "x = -2, x = 10" *)
144 if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then()
145 else error "rateq.sml: new behaviour: [x = -2, x = 10]";
147 "----------- rateq.sml end--------";
149 ===== inhibit exn ?===========================================================*)