1.1 --- a/src/Tools/isac/BridgeJEdit/SPARK_FDL.thy Thu Apr 29 12:43:50 2021 +0200
1.2 +++ b/src/Tools/isac/BridgeJEdit/SPARK_FDL.thy Thu Apr 29 14:13:11 2021 +0200
1.3 @@ -2,7 +2,7 @@
1.4 imports Complex_Main
1.5 begin
1.6
1.7 -ML_file fdl_lexer.ML
1.8 -ML_file fdl_parser.ML
1.9 +ML_file fdl_lexer.ML (*replace with native Isabelle*)
1.10 +ML_file fdl_parser.ML (*replace with native Isabelle*)
1.11
1.12 end
1.13 \ No newline at end of file
2.1 --- a/src/Tools/isac/BridgeJEdit/parseC.sml Thu Apr 29 12:43:50 2021 +0200
2.2 +++ b/src/Tools/isac/BridgeJEdit/parseC.sml Thu Apr 29 14:13:11 2021 +0200
2.3 @@ -231,15 +231,19 @@
2.4
2.5 (** Step of term + tactic**)
2.6
2.7 +\<^isac_test>\<open>
2.8 val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", ""))))
2.9 +\<close>
2.10
2.11 fun exec_step_term (tm, (tac1, tac2)) =
2.12 "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")";
2.13 +\<^isac_test>\<open>
2.14 val steps_subpbl =
2.15 Scan.repeat (
2.16 ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) ||
2.17 (problem >> exec_subproblem) ( **)
2.18 )
2.19 +\<close>
2.20
2.21 (** Body **)
2.22
3.1 --- a/src/Tools/isac/BridgeJEdit/preliminary.sml Thu Apr 29 12:43:50 2021 +0200
3.2 +++ b/src/Tools/isac/BridgeJEdit/preliminary.sml Thu Apr 29 14:13:11 2021 +0200
3.3 @@ -56,13 +56,13 @@
3.4
3.5 fun store_and_show HACKthy formalise thy =
3.6 let
3.7 -(**)val file_read_correct = case formalise of xxx as
3.8 +(**)val _(*file_read_correct*) = case formalise of xxx as
3.9 [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"],
3.10 ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx
3.11 | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed"
3.12 (**)
3.13 val formalise = hd formalise (*we expect only one Formalise.T in the list*)
3.14 - val (hdlPIDE, _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDEHACK HACKthy formalise
3.15 + val (_(*hdlPIDE*), _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDEHACK HACKthy formalise
3.16 (* ^^ TODO remove with cleanup in nxt_specify_init_calc *)
3.17 (*
3.18 TODO: present "Problem hdlPIDE" via PIDE
4.1 --- a/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 29 12:43:50 2021 +0200
4.2 +++ b/src/Tools/isac/BridgeLibisabelle/thy-hierarchy.sml Thu Apr 29 14:13:11 2021 +0200
4.3 @@ -97,7 +97,8 @@
4.4 |> map (thms_of_rls o #2 o #2)
4.5 |> flat
4.6 |> map (ThmC.revert_sym_rule thy)
4.7 - |> map (fn Rule.Thm (thmID, thm) => (thmID, thm))
4.8 + |> map (fn Rule.Thm (thmID, thm) => (thmID, thm)
4.9 + | _ => raise ERROR "thms_of_rlss: uncovered case")
4.10 |> distinct (fn ((thmID1, _), (thmID2, _)) => thmID1 = thmID2)
4.11 : ThmC.T list
4.12
5.1 --- a/src/Tools/isac/Interpret/derive.sml Thu Apr 29 12:43:50 2021 +0200
5.2 +++ b/src/Tools/isac/Interpret/derive.sml Thu Apr 29 14:13:11 2021 +0200
5.3 @@ -94,7 +94,7 @@
5.4 val _ = msg_5 t'
5.5 val r' = Rule.Thm (thmid, tm)
5.6 in rew_once (lim - 1) (rts @ [(t, r', (t', a'))]) t' Appl rrs' end)
5.7 - handle NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
5.8 + handle Rewrite.NO_REWRITE => raise ERROR "derive_norm, Eval: no rewrite")
5.9 | Rule.Rls_ rls =>
5.10 (case Rewrite.rewrite_set_ thy true rls t of
5.11 NONE => rew_once lim rts t apno rs'
6.1 --- a/src/Tools/isac/Knowledge/Diff.thy Thu Apr 29 12:43:50 2021 +0200
6.2 +++ b/src/Tools/isac/Knowledge/Diff.thy Thu Apr 29 14:13:11 2021 +0200
6.3 @@ -76,7 +76,9 @@
6.4
6.5 sqrt_conv_bdv: "sqrt bdv = bdv \<up> (1 / 2)" and
6.6 sqrt_conv_bdv_n: "sqrt (bdv \<up> n) = bdv \<up> (n / 2)" and
6.7 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
6.8 sqrt_conv: "bdv occurs_in u ==> sqrt u = u \<up> (1 / 2)" and
6.9 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
6.10 sqrt_sym_conv: "u \<up> (a / 2) = sqrt (u \<up> a)" and
6.11
6.12 root_conv: "bdv occurs_in u ==> nroot n u = u \<up> (1 / n)" and
7.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy Thu Apr 29 12:43:50 2021 +0200
7.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy Thu Apr 29 14:13:11 2021 +0200
7.3 @@ -108,7 +108,8 @@
7.4 | _ => (((ccc, 0), T), 1))
7.5 | dest_hd' (Var v) = (v, 2)
7.6 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
7.7 - | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
7.8 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
7.9 + | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
7.10
7.11 fun size_of_term' (Free (ccc, _)) =
7.12 (case Symbol.explode ccc of (*WN0510 hack for the bound variables*)
7.13 @@ -147,7 +148,7 @@
7.14 | ord => ord)
7.15 and hd_ord (f, g) = (* ~ term.ML *)
7.16 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
7.17 -and terms_ord str pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
7.18 +and terms_ord _ pr (ts, us) = list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
7.19 (**)
7.20 in
7.21 (**)
7.22 @@ -156,7 +157,7 @@
7.23 (term_ord' pr thy (Library.swap tu) = LESS);*)
7.24
7.25 (*for the rls's*)
7.26 -fun ord_simplify_System (pr:bool) thy subst tu =
7.27 +fun ord_simplify_System (pr:bool) thy _(*subst*) tu =
7.28 (term_ord' pr thy tu = LESS);
7.29 (**)
7.30 end;
8.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Thu Apr 29 12:43:50 2021 +0200
8.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Thu Apr 29 14:13:11 2021 +0200
8.3 @@ -477,6 +477,7 @@
8.4 if c1 = 0
8.5 then add ((c2, es2) :: ms) new
8.6 else add ((c2, es2) :: ms) (new @ [(c1, es1)])
8.7 + | add _ _ = raise ERROR "add_monoms: uncovered case in fun.def."
8.8 in add p [] : poly end
8.9
8.10 (* brings the polynom in correct order and adds monomials *)
8.11 @@ -494,16 +495,17 @@
8.12 fun eval (p: poly) var value = order (map (eval_monom var value) p)
8.13
8.14 (* transform a multivariate to a univariate polynomial TODO map?*)
8.15 - fun multi_to_uni (p as (_, es)::_ : poly) =
8.16 - if length es = 1
8.17 - then
8.18 - let fun transfer ([]: poly) (up: unipoly) = up
8.19 - | transfer (mp as (c, es)::ps) up =
8.20 - if length up = hd es
8.21 - then transfer ps (up @ [c])
8.22 - else transfer mp (up @ [0])
8.23 - in transfer (order p) [] end
8.24 - else raise ERROR "Polynom has more than one variable!";
8.25 + fun multi_to_uni (p as (_, es) :: _ : poly) =
8.26 + if length es = 1
8.27 + then
8.28 + let fun transfer ([]: poly) (up: unipoly) = up
8.29 + | transfer (mp as (c, es)::ps) up =
8.30 + if length up = hd es
8.31 + then transfer ps (up @ [c])
8.32 + else transfer mp (up @ [0])
8.33 + in transfer (order p) [] end
8.34 + else raise ERROR "Polynom has more than one variable!"
8.35 + | multi_to_uni _ = raise ERROR "multi_to_uni: uncovered case in fun.def";
8.36
8.37 (* transform a univariate to a multivariate polynomial TODO map *)
8.38 fun uni_to_multi (up: unipoly) =
8.39 @@ -522,11 +524,12 @@
8.40 let
8.41 (* the inner loop *)
8.42 fun mult' (_: poly) ([]: unipoly) (_) (new': poly) (_: int) = order new'
8.43 - | mult' (mp' as (c, es)::ps) up' var new' c2' =
8.44 + | mult' (mp' as (c, es) :: _) up' var new' c2' =
8.45 let val (first, last) = chop var es
8.46 in mult' mp' (tl up') var
8.47 (new' @ [(c * hd up', first @ [c2'] @ last)]) (c2' + 1)
8.48 end
8.49 + | mult' _ _ _ _ _ = raise ERROR "mult_with_new_var: uncovered case in fun.def."
8.50 in mult (tl mp) up var (new @ (mult' mp up var [] 0)) (0) end
8.51 in mult mp up var [] 0 : poly end
8.52
8.53 @@ -539,14 +542,21 @@
8.54
8.55 (* Winkler p.95 *)
8.56 fun find_new_r (p1 as (_, es1)::_ : poly) (p2 as (_, es2)::_ : poly) old =
8.57 - let val p1' as (_, es1')::_ = eval p1 (length es1 - 2) (old + 1)
8.58 - val p2' as (_, es2')::_ = eval p2 (length es2 - 2) (old + 1);
8.59 + let val (p1', es1') =
8.60 + case eval p1 (length es1 - 2) (old + 1) of
8.61 + (p1' as (_, es1') :: _) => (p1', es1')
8.62 + | _ => raise ERROR "find_new_r: uncovered case 1"
8.63 + val (p2', es2') =
8.64 + case eval p2 (length es2 - 2) (old + 1) of
8.65 + (p2' as (_, es2') :: _) => (p2', es2')
8.66 + | _ => raise ERROR "find_new_r: uncovered case 1"
8.67 in
8.68 if max_deg_var p1' (length es1' - 1) = max_deg_var p1 (length es1 - 1) orelse
8.69 max_deg_var p2' (length es2' - 1) = max_deg_var p2 (length es1 - 1)
8.70 then old + 1
8.71 else find_new_r p1 p2 (old + 1)
8.72 end
8.73 + | find_new_r _ _ _ = raise ERROR "find_new_r: uncovered case in fun.def."
8.74 \<close>
8.75
8.76 subsection \<open>addition, multiplication, division\<close>
8.77 @@ -608,9 +618,15 @@
8.78 let
8.79 fun div_up p1 p2 quot_old =
8.80 let
8.81 - val p1 as (c, es)::_ = drop_lc0 (order p1);
8.82 + val (p1, es) =
8.83 + case drop_lc0 (order p1) of
8.84 + (p1 as (_, es) :: _) => (p1, es)
8.85 + | _ => raise ERROR "op %%/%% : uncovered case 1"
8.86 val p2 = drop_lc0 (order p2);
8.87 - val [c] = zero_poly (length es);
8.88 + val c =
8.89 + case zero_poly (length es) of
8.90 + [c] => c
8.91 + | _ => raise ERROR "op %%/%% : uncovered case 2"
8.92 val d = (replicate (List.length p1 - List.length p2) c) @ p2 ;
8.93 val quot = [(lcoeff p1 div2 lcoeff d, lexp p1 %-% lexp p2)];
8.94 val remd = drop_lc0 (p1 %%-%% (d %%*%% quot));
8.95 @@ -663,8 +679,8 @@
8.96 (* naming of n, M, m, r, ... follows Winkler p. 95
8.97 assumes: n = length es1 = length es2
8.98 r: *)
8.99 - fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
8.100 - | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
8.101 + fun gcd_poly' a [monom] _ _ = [fold gcd_monom a monom]
8.102 + | gcd_poly' [monom] b _ _ = [fold gcd_monom b monom]
8.103 | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
8.104 if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
8.105 if n > 1
8.106 @@ -678,6 +694,7 @@
8.107 uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %*
8.108 (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
8.109 end
8.110 + | gcd_poly' _ _ _ _ = raise ERROR "gcd_poly': uncovered case in fun.def."
8.111
8.112 (* try_new_r :: poly -> poly -> int -> int -> int -> int list -> poly list -> poly
8.113 try_new_r a b n M r r_list steps =
8.114 @@ -742,6 +759,7 @@
8.115 then ((a' %%* ~1, b' %%* ~1), c %%* ~1) (*makes results look nicer*)
8.116 else ((a', b'), c)
8.117 end
8.118 + | gcd_poly _ _ = raise ERROR "gcd_poly: uncovered case in fun.def."
8.119 \<close>
8.120
8.121 section \<open>example from the last mail to Tobias Nipkow\<close>
9.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Thu Apr 29 12:43:50 2021 +0200
9.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Apr 29 14:13:11 2021 +0200
9.3 @@ -25,6 +25,7 @@
9.4 'bdv' is a constant handled on the meta-level
9.5 specifically as a 'bound variable' *)
9.6
9.7 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
9.8 integral_const: "Not (bdv occurs_in u) ==> Integral u D bdv = u * bdv" and
9.9 integral_var: "Integral bdv D bdv = bdv \<up> 2 / 2" and
9.10
9.11 @@ -37,6 +38,7 @@
9.12 a = a + new_c a"
9.13 *)
9.14 integral_pow: "Integral bdv \<up> n D bdv = bdv \<up> (n+1) / (n + 1)"
9.15 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
9.16
9.17 ML \<open>
9.18 val thy = @{theory};
9.19 @@ -63,7 +65,7 @@
9.20 in
9.21 case cs of
9.22 [] => c
9.23 - | [c] => Free ("c_2", HOLogic.realT)
9.24 + | [_] => Free ("c_2", HOLogic.realT)
9.25 | cs =>
9.26 let val max_coeff = maxl (map get_coeff cs)
9.27 in Free ("c_"^string_of_int (max_coeff + 1), HOLogic.realT) end
10.1 --- a/src/Tools/isac/Knowledge/Isac_Knowledge.thy Thu Apr 29 12:43:50 2021 +0200
10.2 +++ b/src/Tools/isac/Knowledge/Isac_Knowledge.thy Thu Apr 29 14:13:11 2021 +0200
10.3 @@ -25,10 +25,8 @@
10.4
10.5 ML \<open>val version_isac = "isac version 120504 15:33";\<close>
10.6 ML \<open>
10.7 -"~~~~~ fun xxx , args:"; val () = ();
10.8 \<close> ML \<open>
10.9 \<close> ML \<open>
10.10 -"~~~~~ fun xxx , args:"; val () = ();
10.11 \<close>
10.12
10.13 end
11.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy Thu Apr 29 12:43:50 2021 +0200
11.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy Thu Apr 29 14:13:11 2021 +0200
11.3 @@ -34,10 +34,12 @@
11.4 (- b + a) = (a - b)" and
11.5 tausche_vor_minus: "[| b ist_monom; a kleiner b |] ==>
11.6 (- b - a) = (-a - b)" and
11.7 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
11.8 tausche_plus_plus: "b kleiner c ==> (a + c + b) = (a + b + c)" and
11.9 tausche_plus_minus: "b kleiner c ==> (a + c - b) = (a - b + c)" and
11.10 tausche_minus_plus: "b kleiner c ==> (a - c + b) = (a + b - c)" and
11.11 tausche_minus_minus: "b kleiner c ==> (a - c - b) = (a - b - c)" and
11.12 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
11.13
11.14 (*commute with invariant (a.b).c -association*)
11.15 tausche_mal: "[| b is_atom; a kleiner b |] ==>
11.16 @@ -87,10 +89,12 @@
11.17 subtrahiere_eins_vor_minus:"[| m is_const |] ==>
11.18 - v - m * v = (-1 - m) * v" and
11.19
11.20 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
11.21 vorzeichen_minus_weg1: "l kleiner 0 ==> a + l * b = a - -1*l * b" and
11.22 vorzeichen_minus_weg2: "l kleiner 0 ==> a - l * b = a + -1*l * b" and
11.23 vorzeichen_minus_weg3: "l kleiner 0 ==> k + a - l * b = k + a + -1*l * b" and
11.24 vorzeichen_minus_weg4: "l kleiner 0 ==> k - a - l * b = k - a + -1*l * b" and
11.25 +(*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
11.26
11.27 (*klammer_plus_plus = (add.assoc RS sym)*)
11.28 klammer_plus_minus: "a + (b - c) = (a + b) - c" and
11.29 @@ -108,22 +112,26 @@
11.30 (*. get the identifier from specific monomials; see fun ist_monom .*)
11.31 (*HACK.WN080107*)
11.32 fun increase str =
11.33 - let val s::ss = Symbol.explode str
11.34 - in implode ((chr (ord s + 1))::ss) end;
11.35 -fun identifier (Free (id,_)) = id (* 2, a *)
11.36 - | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
11.37 - id (* 2*a, a*b *)
11.38 + let
11.39 + val (s, ss) =
11.40 + case Symbol.explode str of
11.41 + s :: ss => (s, ss)
11.42 + | _ => raise ERROR "PolyMinus.increase: uncovered case"
11.43 + in implode ((chr (ord s + 1))::ss) end;
11.44 +fun identifier (Free (id,_)) = id (* 2 , a *)
11.45 + | identifier (Const ("Groups.times_class.times", _) $ Free (_(*num*), _) $ Free (id, _)) =
11.46 + id (* 2*a , a*b *)
11.47 | identifier (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
11.48 (Const ("Groups.times_class.times", _) $
11.49 Free (num, _) $ Free _) $ Free (id, _)) =
11.50 if TermC.is_num' num then id
11.51 else "|||||||||||||"
11.52 - | identifier (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (exp, _)) =
11.53 - if TermC.is_num' base then "|||||||||||||" (* a^2 *)
11.54 + | identifier (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (_(*exp*), _)) =
11.55 + if TermC.is_num' base then "|||||||||||||" (* a^2 *)
11.56 else (*increase*) base
11.57 | identifier (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
11.58 (Const ("Prog_Expr.pow", _) $
11.59 - Free (base, _) $ Free (exp, _))) =
11.60 + Free (base, _) $ Free (_(*exp*), _))) =
11.61 if TermC.is_num' num andalso not (TermC.is_num' base) then (*increase*) base
11.62 else "|||||||||||||"
11.63 | identifier _ = "|||||||||||||"(*the "largest" string*);
11.64 @@ -149,23 +157,23 @@
11.65 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
11.66 | eval_kleiner _ _ _ _ = NONE;
11.67
11.68 -fun ist_monom (Free (id,_)) = true
11.69 - | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free (id, _)) =
11.70 +fun ist_monom (Free _) = true
11.71 + | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ Free _) =
11.72 if TermC.is_num' num then true else false
11.73 | ist_monom _ = false;
11.74 -(*. this function only accepts the most simple monoms vvvvvvvvvv .*)
11.75 -fun ist_monom (Free (id,_)) = true (* 2, a *)
11.76 +(*. this function only accepts the most simple monoms vvvvvvvvvv .*)
11.77 +fun ist_monom (Free _) = true (* 2, a *)
11.78 | ist_monom (Const ("Groups.times_class.times", _) $ Free _ $ Free (id, _)) = (* 2*a, a*b *)
11.79 if TermC.is_num' id then false else true
11.80 | ist_monom (Const ("Groups.times_class.times", _) $ (* 3*a*b *)
11.81 (Const ("Groups.times_class.times", _) $
11.82 Free (num, _) $ Free _) $ Free (id, _)) =
11.83 if TermC.is_num' num andalso not (TermC.is_num' id) then true else false
11.84 - | ist_monom (Const ("Prog_Expr.pow", _) $ Free (base, _) $ Free (exp, _)) =
11.85 + | ist_monom (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) =
11.86 true (* a^2 *)
11.87 | ist_monom (Const ("Groups.times_class.times", _) $ Free (num, _) $ (* 3*a^2 *)
11.88 (Const ("Prog_Expr.pow", _) $
11.89 - Free (base, _) $ Free (exp, _))) =
11.90 + Free _ $ Free _)) =
11.91 if TermC.is_num' num then true else false
11.92 | ist_monom _ = false;
11.93
12.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Apr 29 12:43:50 2021 +0200
12.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Apr 29 14:13:11 2021 +0200
12.3 @@ -213,9 +213,10 @@
12.4 subsubsection \<open>Factor out gcd for cancellation\<close>
12.5 ML \<open>
12.6 fun check_fraction t =
12.7 - let val Const ("Rings.divide_class.divide", _) $ numerator $ denominator = t
12.8 - in SOME (numerator, denominator) end
12.9 - handle Bind => NONE
12.10 + case t of
12.11 + Const ("Rings.divide_class.divide", _) $ numerator $ denominator
12.12 + => SOME (numerator, denominator)
12.13 + | _ => NONE
12.14
12.15 (* prepare a term for cancellation by factoring out the gcd
12.16 assumes: is a fraction with outmost "/"*)
13.1 --- a/src/Tools/isac/Knowledge/Root.thy Thu Apr 29 12:43:50 2021 +0200
13.2 +++ b/src/Tools/isac/Knowledge/Root.thy Thu Apr 29 14:13:11 2021 +0200
13.3 @@ -46,8 +46,8 @@
13.4
13.5 (*-------------------------functions---------------------*)
13.6 (*evaluation square-root over the integers*)
13.7 -fun eval_sqrt (thmid:string) (op_:string) (t as
13.8 - (Const(op0,t0) $ arg)) thy =
13.9 +fun eval_sqrt (_ : string) (_ : string) (t as
13.10 + (Const(op0, _) $ arg)) _(*thy*) =
13.11 (case arg of
13.12 Free (n1,t1) =>
13.13 (case TermC.int_opt_of_string n1 of
13.14 @@ -99,7 +99,8 @@
13.15 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
13.16 | dest_hd' (Var v) = (v, 2)
13.17 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
13.18 - | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
13.19 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
13.20 + | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
13.21 fun size_of_term' (Const(str,_) $ t) =
13.22 (case str of "NthRoot.sqrt" => (1000 + size_of_term' t)
13.23 | _ => 1 + size_of_term' t)
13.24 @@ -109,7 +110,7 @@
13.25 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
13.26 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
13.27 | ord => ord)
13.28 - | term_ord' pr thy (t, u) =
13.29 + | term_ord' pr _(*thy*) (t, u) =
13.30 (if pr then
13.31 let
13.32 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
13.33 @@ -136,7 +137,7 @@
13.34 and hd_ord (f, g) = (* ~ term.ML *)
13.35 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord
13.36 (dest_hd' f, dest_hd' g)
13.37 -and terms_ord str pr (ts, us) =
13.38 +and terms_ord _(*str*) pr (ts, us) =
13.39 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
13.40
13.41 in
14.1 --- a/src/Tools/isac/Knowledge/RootEq.thy Thu Apr 29 12:43:50 2021 +0200
14.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy Thu Apr 29 14:13:11 2021 +0200
14.3 @@ -442,6 +442,7 @@
14.4 ("rooteq_simplify", (Context.theory_name @{theory}, rooteq_simplify))]\<close>
14.5
14.6 subsection \<open>problems\<close>
14.7 +(*Ambiguous input produces 5 parse trees -----------------------------------------------------\\*)
14.8 setup \<open>KEStore_Elems.add_pbts
14.9 (* ---------root----------- *)
14.10 [(Problem.prep_input thy "pbl_equ_univ_root" [] Problem.id_empty
14.11 @@ -471,6 +472,7 @@
14.12 " Not((rhs e_e) is_normSqrtTerm_in (v_v::real)))"]),
14.13 ("#Find" ,["solutions v_v'i'"])],
14.14 RootEq_prls, SOME "solve (e_e::bool, v_v)", [["RootEq", "norm_sq_root_equation"]]))]\<close>
14.15 +(*Ambiguous input produces 5 parse trees -----------------------------------------------------//*)
14.16
14.17 subsection \<open>methods\<close>
14.18 setup \<open>KEStore_Elems.add_mets
15.1 --- a/src/Tools/isac/Knowledge/Simplify.thy Thu Apr 29 12:43:50 2021 +0200
15.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy Thu Apr 29 14:13:11 2021 +0200
15.3 @@ -70,4 +70,8 @@
15.4 ((Thm.term_of o the o (TermC.parse thy)) "Vereinfache",
15.5 (("Isac_Knowledge", ["vereinfachen"], ["no_met"]), argl2dtss))]\<close>
15.6
15.7 +ML \<open>
15.8 +\<close> ML \<open>
15.9 +\<close> ML \<open>
15.10 +\<close>
15.11 end
15.12 \ No newline at end of file
16.1 --- a/src/Tools/isac/Knowledge/Test.thy Thu Apr 29 12:43:50 2021 +0200
16.2 +++ b/src/Tools/isac/Knowledge/Test.thy Thu Apr 29 14:13:11 2021 +0200
16.3 @@ -122,15 +122,17 @@
16.4 | is_div_op _ = false;
16.5
16.6 fun is_denom bdVar div_op t =
16.7 - let fun is bool[v]dv (Const (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
16.8 - | is bool[v]dv (Free (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
16.9 - | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
16.10 - | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
16.11 - | is bool[v]dv (h$n$d) =
16.12 - if is_div_op(dv,h)
16.13 - then (is false[v]dv n)orelse(is true[v]dv d)
16.14 - else (is bool [v]dv n)orelse(is bool[v]dv d)
16.15 -in is false (varids bdVar) (strip_thy div_op) t end;
16.16 + let
16.17 + fun is bool [v] _ (Const (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
16.18 + | is bool [v] _ (Free (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
16.19 + | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
16.20 + | is _ [_] _ ((Const ("Bin.integ_of_bin",_)) $ _) = false
16.21 + | is bool [v] dv (h$n$d) =
16.22 + if is_div_op (dv, h)
16.23 + then (is false [v] dv n) orelse(is true [v] dv d)
16.24 + else (is bool [v] dv n) orelse(is bool [v] dv d)
16.25 + | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."
16.26 + in is false (varids bdVar) (strip_thy div_op) t end;
16.27
16.28
16.29 fun rational t div_op bdVar =
16.30 @@ -238,13 +240,11 @@
16.31 (*isolate root on the LEFT hand side of the equation
16.32 otherwise shuffling from left to right would not terminate*)
16.33
16.34 - rroot_to_lhs:
16.35 - "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
16.36 - rroot_to_lhs_mult:
16.37 - "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
16.38 - rroot_to_lhs_add_mult:
16.39 - "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
16.40 -(*17.9.02 aus SqRoot.thy------------------------------ \<up> ---*)
16.41 +(*Ambiguous input\<^here> produces 2 parse trees -----------------------------\\*)
16.42 + rroot_to_lhs: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
16.43 + rroot_to_lhs_mult: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
16.44 + rroot_to_lhs_add_mult: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
16.45 +(*Ambiguous input\<^here> produces 2 parse trees -----------------------------//*)
16.46
16.47 section \<open>eval functions\<close>
16.48 ML \<open>
16.49 @@ -254,7 +254,7 @@
16.50
16.51 (*does a term contain a root ?*)
16.52 fun eval_contains_root (thmid:string) _
16.53 - (t as (Const("Test.contains'_root",t0) $ arg)) thy =
16.54 + (t as (Const("Test.contains'_root", _) $ arg)) thy =
16.55 if member op = (ids_of arg) "sqrt"
16.56 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
16.57 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
16.58 @@ -294,19 +294,22 @@
16.59 | pr_ord GREATER = "GREATER";
16.60
16.61 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
16.62 - (case a of
16.63 - "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
16.64 - | _ => (((a, 0), T), 0))
16.65 + (case a of
16.66 + "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest *)
16.67 + | _ => (((a, 0), T), 0))
16.68 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
16.69 | dest_hd' (Var v) = (v, 2)
16.70 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
16.71 - | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
16.72 -(* RL *)
16.73 -fun get_order_pow (t $ (Free(order,_))) =
16.74 + | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
16.75 + | dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
16.76 +
16.77 +\<^isac_test>\<open>
16.78 +fun get_order_pow (t $ (Free(order,_))) =
16.79 (case TermC.int_opt_of_string order of
16.80 SOME d => d
16.81 | NONE => 0)
16.82 | get_order_pow _ = 0;
16.83 +\<close>
16.84
16.85 fun size_of_term' (Const(str,_) $ t) =
16.86 if "Prog_Expr.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
16.87 @@ -316,7 +319,7 @@
16.88 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
16.89 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
16.90 | ord => ord)
16.91 - | term_ord' pr thy (t, u) =
16.92 + | term_ord' pr _ (t, u) =
16.93 (if pr then
16.94 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
16.95 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
16.96 @@ -341,7 +344,7 @@
16.97 | ord => ord)
16.98 and hd_ord (f, g) = (* ~ term.ML *)
16.99 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
16.100 -and terms_ord str pr (ts, us) =
16.101 +and terms_ord _ pr (ts, us) =
16.102 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
16.103 in
16.104
17.1 --- a/src/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 29 12:43:50 2021 +0200
17.2 +++ b/src/Tools/isac/MathEngBasic/rewrite.sml Thu Apr 29 14:13:11 2021 +0200
17.3 @@ -4,6 +4,7 @@
17.4
17.5 signature REWRITE =
17.6 sig
17.7 + exception NO_REWRITE
17.8 val calculate_: theory -> string * Eval_Def.eval_fn -> term -> (term * (string * thm)) option
17.9 val eval__true: theory -> int -> term list -> (term * term) list -> Rule_Set.T -> term list * bool
17.10 val eval_prog_expr: theory -> Rule_Set.T -> term -> term
17.11 @@ -25,7 +26,6 @@
17.12 val lim_deriv: int Unsynchronized.ref
17.13
17.14 \<^isac_test>\<open>
17.15 - exception NO_REWRITE
17.16 val rewrite__: theory -> int -> (term * term) list -> Rule_Def.rew_ord_ ->
17.17 Rule_Set.T -> bool -> thm -> term -> (term * term list) option
17.18 val rewrite__set_: theory -> int -> bool -> (term * term) list -> Rule_Set.T -> term -> (term * term list) option
18.1 --- a/src/Tools/isac/MathEngine/states.sml Thu Apr 29 12:43:50 2021 +0200
18.2 +++ b/src/Tools/isac/MathEngine/states.sml Thu Apr 29 14:13:11 2021 +0200
18.3 @@ -71,8 +71,8 @@
18.4 NONE => raise ERROR ("get_calc " ^ string_of_int cI ^ " not existent")
18.5 | SOME (c, _) =>
18.6 let
18.7 - val (_, tacis) = c
18.8 - (*val _ = if length tacis > 1 then raise ERROR "length tacis > 1" else ()
18.9 + (*val (_, tacis) = c
18.10 + val _ = if length tacis > 1 then raise ERROR "length tacis > 1" else ()
18.11 in Test_Isac.thy raise ERROR in Interpret/inform.sml*)
18.12 in c end;
18.13 fun get_pos (cI: calcID) (uI: iterID) =
18.14 @@ -88,7 +88,7 @@
18.15
18.16 fun del_assoc ([],_) = []
18.17 | del_assoc a =
18.18 - let fun del ([], key) ps = ps
18.19 + let fun del ([], _) ps = ps
18.20 | del ((keyi, xi) :: pairs, key) ps =
18.21 if key = keyi then ps @ pairs
18.22 else del (pairs, key) (ps @ [(keyi, xi)])
18.23 @@ -171,7 +171,7 @@
18.24 (fn s => case assoc (s, cI) of
18.25 NONE =>
18.26 raise ERROR ("upd_ipos: calctree " ^ (string_of_int cI) ^ " not existent")
18.27 - | SOME (cs, us) => overwrite2 (s, ((cI, uI), ip)));
18.28 + | SOME _ => overwrite2 (s, ((cI, uI), ip)));
18.29
18.30
18.31 (** add and delete calcs **)
18.32 @@ -204,7 +204,7 @@
18.33 (fn s => case assoc (s, cI) of
18.34 NONE =>
18.35 raise ERROR ("add_user: calctree " ^ (string_of_int cI) ^ " not existent")
18.36 - | SOME (cs, us) =>
18.37 + | SOME (_, us) =>
18.38 let
18.39 val new_uI = new_key us 1
18.40 in (new_uI: iterID, overwrite2 (s, ((cI, new_uI), Pos.e_pos'))) end);
19.1 --- a/src/Tools/isac/MathEngine/step.sml Thu Apr 29 12:43:50 2021 +0200
19.2 +++ b/src/Tools/isac/MathEngine/step.sml Thu Apr 29 14:13:11 2021 +0200
19.3 @@ -76,6 +76,7 @@
19.4 (*unclean alternatives*)
19.5 scs as ("ok", _) => scs
19.6 | (_, cs as ([], _, _)) => ("helpless", cs)
19.7 + | _ => raise ERROR "switch_specify_solve: uncovered case in fun.def."
19.8 end
19.9
19.10 (* does a step forward; returns tactic used, ctree updated (i.e. with NEW term/calchead) *)