# HG changeset patch
# User wneuper
# Date 1157125707 -7200
# Node ID 9dd39e3f81f6fb6175ef62fa8a9fbdae4f40b58c
# Parent  1bcaf23cb178364d8a9e8a1633375aad1d5d1bac
Biegelinie2, intermediate state (fun eval_same_funid)

diff -r 1bcaf23cb178 -r 9dd39e3f81f6 src/sml/IsacKnowledge/Atools.ML
--- a/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 15:00:42 2006 +0200
+++ b/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 17:48:27 2006 +0200
@@ -352,6 +352,20 @@
     else None
   | eval_argument_in _ _ _ _ = None;
 
+(*.check if the function-identifier of the first argument matches 
+   the function-identifier of the lhs of the second argument.*)
+(*("same_funid" ,("Atools.same'_funid",
+		   eval_same_funid "Atools.same'_funid"))*)
+fun eval_same_funid "Atools.same'_funid" 
+		     (p as Const ("Atools.same'_funid",_) $ 
+			(f1 $ _) $ 
+			(Const ("op =", _) $ (f2 $ _) $ _)) =
+    if f1 = f2 
+    then Some ((term2str p) ^ " = True",
+	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
+    else Some ((term2str p) ^ " = False",
+	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
+| eval_same_funid _ _  = None;
 
 
 local
diff -r 1bcaf23cb178 -r 9dd39e3f81f6 src/sml/IsacKnowledge/Atools.thy
--- a/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 15:00:42 2006 +0200
+++ b/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 17:48:27 2006 +0200
@@ -38,6 +38,7 @@
   "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)
 
   "argument'_in"  :: real => real ("argument'_in _" 10)
+  "same'_funid"  :: [real, bool] => bool ("same'_funid _ _" 10)
 
 (*-------------------- rules------------------------------------------------*)
 rules (*for evaluating the assumptions of conditional rules*)
diff -r 1bcaf23cb178 -r 9dd39e3f81f6 src/smltest/IsacKnowledge/atools.sml
--- a/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 15:00:42 2006 +0200
+++ b/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 17:48:27 2006 +0200
@@ -12,6 +12,7 @@
 "-----------------------------------------------------------------";
 "----------- occurs_in -------------------------------------------";
 "----------- argument_of -----------------------------------------";
+"----------- same_funid ------------------------------------------";
 "-----------------------------------------------------------------";
 
 
@@ -37,3 +38,30 @@
 val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
 if term2s t' = "(argument_in M_b x) = x" then ()
 else raise error "atools.sml:(argument_in M_b x) = x  ???";
+
+"----------- same_funid ------------------------------------------";
+"----------- same_funid ------------------------------------------";
+"----------- same_funid ------------------------------------------";
+val t = str2term "M_b L"; atomty t;
+val t as f1 $ _ = str2term "M_b L";
+val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
+f1 = f2 (*true*);
+val (p as Const ("Atools.same'_funid",_) $ 
+			(f1 $ _) $ 
+			(Const ("op =", _) $ (f2 $ _) $ _)) = 
+    str2term "same_funid (M_b L) (M_b x = c + L*x)";
+f1 = f2 (*true*);
+eval_same_funid "Atools.same'_funid" 
+		 (str2term "same_funid (M_b L) (M_b x = c + L*x)")(*true*);
+eval_same_funid "Atools.same'_funid" 
+		 (str2term "same_funid (M_b L) ( y' x = c + L*x)")(*false*);
+eval_same_funid "Atools.same'_funid" 
+		 (str2term "same_funid (M_b L) (  y x = c + L*x)")(*false*);
+eval_same_funid "Atools.same'_funid" 
+		 (str2term "same_funid (  y L) (M_b x = c + L*x)")(*false*);
+eval_same_funid "Atools.same'_funid" 
+		 (str2term "same_funid (  y L) (  y x = c + L*x)")(*true*);
+
+(* use"IsacKnowledge/Atools.ML";
+   use"../smltest/IsacKnowledge/atools.sml";
+   *)
\ No newline at end of file