1.1 --- a/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 15:00:42 2006 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Atools.ML	Fri Sep 01 17:48:27 2006 +0200
     1.3 @@ -352,6 +352,20 @@
     1.4      else None
     1.5    | eval_argument_in _ _ _ _ = None;
     1.6  
     1.7 +(*.check if the function-identifier of the first argument matches 
     1.8 +   the function-identifier of the lhs of the second argument.*)
     1.9 +(*("same_funid" ,("Atools.same'_funid",
    1.10 +		   eval_same_funid "Atools.same'_funid"))*)
    1.11 +fun eval_same_funid "Atools.same'_funid" 
    1.12 +		     (p as Const ("Atools.same'_funid",_) $ 
    1.13 +			(f1 $ _) $ 
    1.14 +			(Const ("op =", _) $ (f2 $ _) $ _)) =
    1.15 +    if f1 = f2 
    1.16 +    then Some ((term2str p) ^ " = True",
    1.17 +	       Trueprop $ (mk_equality (p, HOLogic.true_const)))
    1.18 +    else Some ((term2str p) ^ " = False",
    1.19 +	       Trueprop $ (mk_equality (p, HOLogic.false_const)))
    1.20 +| eval_same_funid _ _  = None;
    1.21  
    1.22  
    1.23  local

     2.1 --- a/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 15:00:42 2006 +0200
     2.2 +++ b/src/sml/IsacKnowledge/Atools.thy	Fri Sep 01 17:48:27 2006 +0200
     2.3 @@ -38,6 +38,7 @@
     2.4    "ident"     :: ['a, 'a] => bool    ("(_ =!=/ _)" [51, 51] 50)
     2.5  
     2.6    "argument'_in"  :: real => real ("argument'_in _" 10)
     2.7 +  "same'_funid"  :: [real, bool] => bool ("same'_funid _ _" 10)
     2.8  
     2.9  (*-------------------- rules------------------------------------------------*)
    2.10  rules (*for evaluating the assumptions of conditional rules*)

     3.1 --- a/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 15:00:42 2006 +0200
     3.2 +++ b/src/smltest/IsacKnowledge/atools.sml	Fri Sep 01 17:48:27 2006 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4  "-----------------------------------------------------------------";
     3.5  "----------- occurs_in -------------------------------------------";
     3.6  "----------- argument_of -----------------------------------------";
     3.7 +"----------- same_funid ------------------------------------------";
     3.8  "-----------------------------------------------------------------";
     3.9  
    3.10  
    3.11 @@ -37,3 +38,30 @@
    3.12  val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
    3.13  if term2s t' = "(argument_in M_b x) = x" then ()
    3.14  else raise error "atools.sml:(argument_in M_b x) = x  ???";
    3.15 +
    3.16 +"----------- same_funid ------------------------------------------";
    3.17 +"----------- same_funid ------------------------------------------";
    3.18 +"----------- same_funid ------------------------------------------";
    3.19 +val t = str2term "M_b L"; atomty t;
    3.20 +val t as f1 $ _ = str2term "M_b L";
    3.21 +val t as Const ("op =", _) $ (f2 $ _) $ _ = str2term "M_b x = c + L*x";
    3.22 +f1 = f2 (*true*);
    3.23 +val (p as Const ("Atools.same'_funid",_) $ 
    3.24 +			(f1 $ _) $ 
    3.25 +			(Const ("op =", _) $ (f2 $ _) $ _)) = 
    3.26 +    str2term "same_funid (M_b L) (M_b x = c + L*x)";
    3.27 +f1 = f2 (*true*);
    3.28 +eval_same_funid "Atools.same'_funid" 
    3.29 +		 (str2term "same_funid (M_b L) (M_b x = c + L*x)")(*true*);
    3.30 +eval_same_funid "Atools.same'_funid" 
    3.31 +		 (str2term "same_funid (M_b L) ( y' x = c + L*x)")(*false*);
    3.32 +eval_same_funid "Atools.same'_funid" 
    3.33 +		 (str2term "same_funid (M_b L) (  y x = c + L*x)")(*false*);
    3.34 +eval_same_funid "Atools.same'_funid" 
    3.35 +		 (str2term "same_funid (  y L) (M_b x = c + L*x)")(*false*);
    3.36 +eval_same_funid "Atools.same'_funid" 
    3.37 +		 (str2term "same_funid (  y L) (  y x = c + L*x)")(*true*);
    3.38 +
    3.39 +(* use"IsacKnowledge/Atools.ML";
    3.40 +   use"../smltest/IsacKnowledge/atools.sml";
    3.41 +   *)
    3.42 \ No newline at end of file