wneuper/isa: comparison src/Tools/isac/Knowledge/Test.thy

equal deleted inserted replaced

-:637f20154de6
+:74965ce81297
 fun is_div_op (dv, (Const (op_,
 (Type ("fun", [Type (_, []), Type ("fun", [Type _, Type _])])))) ) = (dv = strip_thy op_)
 | is_div_op _ = false;
 fun is_denom bdVar div_op t =
-let fun is bool[v]dv (Const  (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
+let
-	  | is bool[v]dv (Free   (s,Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
+fun is bool [v] _ (Const  (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
-	  | is bool[v]dv (Var((s,_),Type(_,[])))= bool andalso(if v=strip_thy s then true else false)
+	  | is bool [v] _ (Free   (s,Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
-	  | is bool[v]dv((Const ("Bin.integ_of_bin",_)) $ _) = false
+	  | is bool [v] _ (Var((s,_),Type(_,[])))= bool andalso(if v = strip_thy s then true else false)
-	  | is bool[v]dv (h$n$d) =
+	  | is _ [_] _ ((Const ("Bin.integ_of_bin",_)) $ _) = false
-	      if is_div_op(dv,h)
+	  | is bool [v] dv (h$n$d) =
-	      then (is false[v]dv n)orelse(is true[v]dv d)
+	      if is_div_op (dv, h)
-	      else (is bool [v]dv n)orelse(is bool[v]dv d)
+	      then (is false [v] dv n) orelse(is true [v] dv d)
-in is false (varids bdVar) (strip_thy div_op) t end;
+	      else (is bool [v] dv n) orelse(is bool [v] dv d)
+	  | is _ _ _ _ = raise ERROR "is_denom: uncovered case in fun.def."
+in is false (varids bdVar) (strip_thy div_op) t end;
 fun rational t div_op bdVar =
 is_denom bdVar div_op t andalso bin_ops_only t;
 	     "(x \<up> 2 = 0) = (x = 0)" and
 (*isolate root on the LEFT hand side of the equation
 otherwise shuffling from left to right would not terminate*)
-rroot_to_lhs:
+(*Ambiguous input\<^here> produces 2 parse trees -----------------------------\\*)
-"is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
+rroot_to_lhs: "is_root_free a ==> (a = sqrt b) = (a + (-1)*sqrt b = 0)" and
-rroot_to_lhs_mult:
+rroot_to_lhs_mult: "is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
-"is_root_free a ==> (a = c*sqrt b) = (a + (-1)*c*sqrt b = 0)" and
+rroot_to_lhs_add_mult: "is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
-rroot_to_lhs_add_mult:
+(*Ambiguous input\<^here> produces 2 parse trees -----------------------------//*)
-"is_root_free a ==> (a = d+c*sqrt b) = (a + (-1)*c*sqrt b = d)"
-(*17.9.02 aus SqRoot.thy------------------------------ \<up> ---*)
 section \<open>eval functions\<close>
 ML \<open>
 val thy = @{theory};
 (** evaluation of numerals and predicates **)
 (*does a term contain a root ?*)
 fun eval_contains_root (thmid:string) _
-		       (t as (Const("Test.contains'_root",t0) $ arg)) thy =
+		       (t as (Const("Test.contains'_root", _) $ arg)) thy =
 if member op = (ids_of arg) "sqrt"
 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg)"",
 	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
 fun pr_ord EQUAL = "EQUAL"
 | pr_ord LESS  = "LESS"
 | pr_ord GREATER = "GREATER";
 fun dest_hd' (Const (a, T)) =                          (* ~ term.ML *)
 (case a of
 "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0)           (*WN greatest *)
 | _ => (((a, 0), T), 0))
 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
 | dest_hd' (Var v) = (v, 2)
 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
-| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
+| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
-(* RL *)
+| dest_hd' _ = raise ERROR "dest_hd': uncovered case in fun.def.";
-fun get_order_pow (t $ (Free(order,_))) =
+\<^isac_test>\<open>
+fun get_order_pow (t $ (Free(order,_))) =
 	(case TermC.int_opt_of_string order of
 	             SOME d => d
 		   | NONE   => 0)
 | get_order_pow _ = 0;
+\<close>
 fun size_of_term' (Const(str,_) $ t) =
 if "Prog_Expr.pow"=str then 1000 + size_of_term' t else 1 + size_of_term' t(*WN*)
 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
 | size_of_term' (f$t) = size_of_term' f  +  size_of_term' t
 | size_of_term' _ = 1;
 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) =       (* ~ term.ML *)
 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U)
 | ord => ord)
-| term_ord' pr thy (t, u) =
+| term_ord' pr _ (t, u) =
 (if pr then
 	 let val (f, ts) = strip_comb t and (g, us) = strip_comb u;
 	     val _ = tracing ("t= f@ts= \"" ^ UnparseC.term f ^ "\" @ \"[" ^
 	                      commas(map UnparseC.term ts) ^ "]\"")
 	     val _ = tracing ("u= g@us= \"" ^ UnparseC.term g ^"\" @ \"[" ^
 	     | ord => ord)
 	     end
 	 | ord => ord)
 and hd_ord (f, g) =                                        (* ~ term.ML *)
 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
-and terms_ord str pr (ts, us) =
+and terms_ord _ pr (ts, us) =
 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
 in
 fun ord_make_polytest (pr:bool) thy (_: subst) tu =
 (term_ord' pr thy(***) tu = LESS );

changeset 60269	74965ce81297
parent 60262	aa0f0bf98d40
child 60275	98ee674d18d3