1.1 --- a/src/sml/IsacKnowledge/AlgEin.thy	Tue Oct 28 15:16:31 2008 +0100
     1.2 +++ b/src/sml/IsacKnowledge/AlgEin.thy	Tue Nov 18 16:34:39 2008 +0100
     1.3 @@ -28,4 +28,10 @@
     1.4  				bool] => bool"
     1.5  	      ("((Script RechnenSymbolScript (_ _ _ _ _ _ =))// (_))" 9)
     1.6  
     1.7 +(*
     1.8 +rules
     1.9 +  (*this axiom creates a contradictory formal system,
    1.10 +    see problem TOOODO *)
    1.11 +*)
    1.12 +
    1.13  end

     2.1 --- a/src/sml/ME/appl.sml	Tue Oct 28 15:16:31 2008 +0100
     2.2 +++ b/src/sml/ME/appl.sml	Tue Nov 18 16:34:39 2008 +0100
     2.3 @@ -544,6 +544,34 @@
     2.4       else Notappl msg
     2.5    end
     2.6  
     2.7 +(*Substitute combines two different kind of "substitution":
     2.8 +  (1) subst_atomic: for ?a..?z
     2.9 +  (2) Pattern.match: for solving equational systems 
    2.10 +      (which raises exn for ?a..?z)*)
    2.11 +  | applicable_in (p,p_) pt (m as Substitute sube) = 
    2.12 +  if p_ mem [Pbl,Met] 
    2.13 +  then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    2.14 +  else let val pp = par_pblobj pt p
    2.15 +	   val thy = assoc_thy (get_obj g_domID pt pp)
    2.16 +	   val f = case p_ of
    2.17 +		       Frm => get_obj g_form pt p
    2.18 +		     | Res => (fst o (get_obj g_result pt)) p
    2.19 +	   val {rew_ord',erls,...} = get_met (get_obj g_metID pt pp)
    2.20 +	   val subte = sube2subte sube
    2.21 +	   val subst = sube2subst thy sube
    2.22 +       in if foldl and_ (true, map contains_Var subte)
    2.23 +	  (*1*)
    2.24 +	  then let val f' = subst_atomic subst f
    2.25 +	       in if f = f' then Notappl (sube2str sube^" not applicable")
    2.26 +		  else Appl (Substitute' (subte, f, f'))
    2.27 +	       end
    2.28 +	  (*2*)
    2.29 +	  else case rewrite_terms_ thy (assoc_rew_ord rew_ord') 
    2.30 +				   erls subte f of
    2.31 +		   Some (f', _) =>  Appl (Substitute' (subte, f, f'))
    2.32 +		 | None => Notappl (sube2str sube^" not applicable")
    2.33 +       end
    2.34 +(*-------WN08114 interrupted with error in polyminus.sml "11 = 11"
    2.35    | applicable_in (p,p_) pt (m as Substitute sube) = 
    2.36    if p_ mem [Pbl,Met] 
    2.37    then Notappl ((tac2str m)^" not for pos "^(pos'2str (p,p_)))
    2.38 @@ -558,17 +586,6 @@
    2.39  	      Some (f', _) =>  Appl (Substitute' (subte, f, f'))
    2.40  	    | None => Notappl (sube2str sube^" not applicable")
    2.41         end
    2.42 -
    2.43 -(*---------
    2.44 -      let val subst = subs2subst (assoc_thy thy') subs;
    2.45 -	  val subs' = subst2subs' subst;
    2.46 -	  val f' = subst_atomic subst f;
    2.47 -      in if f = f' 
    2.48 -	   then Notappl ((subs2str subs)^" not applicable")
    2.49 -	 else Appl (Substitute' (subst, f, f')) end
    2.50 -####################################################################
    2.51 -       handle _ => Notappl ("syntax error in "^(subs2str subs)) end
    2.52 -####################################################################
    2.53  ------------------*)
    2.54  
    2.55    | applicable_in p pt (Apply_Assumption cts') = 

     3.1 --- a/src/sml/ME/ctree.sml	Tue Oct 28 15:16:31 2008 +0100
     3.2 +++ b/src/sml/ME/ctree.sml	Tue Nov 18 16:34:39 2008 +0100
     3.3 @@ -243,6 +243,11 @@
     3.4    [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real")),
     3.5     (Free ("err","RealDef.real"),Free ("#0","RealDef.real"))] 
     3.6     : (term * term) list*)
     3.7 +(*["bdv=x","err=0"] ---> [(bdv,x), (err,0)]*)
     3.8 +fun sube2subst thy s = map (dest_equals' o term_of o the o (parse thy)) s;
     3.9 +(* val ts = sube2subst thy ["bdv=x","err=0"];
    3.10 +   subst2str' ts;
    3.11 +   *)
    3.12  fun sube2subte ss = map str2term ss;
    3.13  
    3.14  

     4.1 --- a/src/sml/Scripts/rewrite.sml	Tue Oct 28 15:16:31 2008 +0100
     4.2 +++ b/src/sml/Scripts/rewrite.sml	Tue Nov 18 16:34:39 2008 +0100
     4.3 @@ -32,6 +32,8 @@
     4.4  (* val (thy, i, bdv, tless, rls, put_asm, r,             t) = 
     4.5         (thy, i, bdv, tless, rls, put_asm, 
     4.6  	(((inst_bdv bdv) o norm o #prop o rep_thm) thm), ct);
     4.7 +   val (thy, i, bdv, tless, rls, put_asm, lrd, r, t) = 
     4.8 +       (thy, 1, [],  ord,   erls,false,   [],  r, t);
     4.9     *)
    4.10  and rew_sub thy i bdv tless rls put_asm lrd r t = 
    4.11    ((*TODO.new_c:( *)(*writeln ("@@@ rew_sub begin: t = "^(term2str t));*)
    4.12 @@ -298,7 +300,8 @@
    4.13    in*) rewrite__set_ thy 1 put_asm subst (*sub*)rls ct
    4.14    (*end*);
    4.15  
    4.16 -
    4.17 +(* val (thy, ord, erls, subte, t) = (thy, dummy_ord, Erls, subte, t);
    4.18 +   *)
    4.19  (*.rewrite using a list of terms.*)
    4.20  fun rewrite_terms_ thy ord erls subte t =
    4.21      let (*val _=writeln("### rewrite_terms_ subte= '"^terms2str subte^"' ..."^
    4.22 @@ -306,12 +309,19 @@
    4.23  		      "### rewrite_terms_ t= '"^term2str t^"' ..."^
    4.24  		      term_detail2str t);*)
    4.25  	fun rew_ (t', asm') [] _ = (t', asm')
    4.26 +	  (* 1st val (t', asm', rules as r::rs, t) = (e_term, [], subte, t);
    4.27 +	     2nd val (t', asm', rules as r::rs, t) = (t'', [], rules, t'');
    4.28 +	     rew_ (t', asm') (r::rs) t;
    4.29 +	     *)
    4.30  	  | rew_ (t', asm') (rules as r::rs) t =
    4.31 -	    let val (t'', asm'', lrd, rew) = 
    4.32 +	    let val _ = writeln("rew_ "^term2str t);
    4.33 +		val (t'', asm'', lrd, rew) = 
    4.34  		    rew_sub thy 1 [] ord erls false [] r t
    4.35  	    in if rew 
    4.36 -	       then rew_ (t'', asm' @ asm'') rules t''
    4.37 -	       else rew_ (t', asm') rs t'
    4.38 +	       then (writeln("true  rew_ "^term2str t'');
    4.39 +		   rew_ (t'', asm' @ asm'') rules t'')
    4.40 +	       else (writeln("false rew_ "^term2str t'');
    4.41 +		   rew_ (t', asm') rs t')
    4.42  	    end
    4.43  	val (t'', asm'') = rew_ (e_term, []) subte t
    4.44      in if t'' = e_term 
    4.45 @@ -725,4 +735,4 @@
    4.46  		       else (INDET, t)
    4.47  		     | None => (INDET, t) end
    4.48  	in (determine o (map eval)) cs end;
    4.49 -WN.16.5.0-------------------------------------------------------------*)
    4.50 \ No newline at end of file
    4.51 +WN.16.5.0-------------------------------------------------------------*)

     5.1 --- a/src/sml/Scripts/term_G.sml	Tue Oct 28 15:16:31 2008 +0100
     5.2 +++ b/src/sml/Scripts/term_G.sml	Tue Nov 18 16:34:39 2008 +0100
     5.3 @@ -108,8 +108,17 @@
     5.4  
     5.5  (*.contains the fst argument the second argument (a leave! of term).*)
     5.6  fun contains_term (Abs(_,_,body)) t = contains_term body t 
     5.7 -  | contains_term (f $ f') t = contains_term f t orelse contains_term f' t
     5.8 +  | contains_term (f $ f') t = 
     5.9 +    contains_term f t orelse contains_term f' t
    5.10    | contains_term s t = t = s;
    5.11 +(*.contains the term a VAR(("*",_),_) ?.*)
    5.12 +fun contains_Var (Abs(_,_,body)) = contains_Var body
    5.13 +  | contains_Var (f $ f') = contains_Var f orelse contains_Var f'
    5.14 +  | contains_Var (Var _) = true
    5.15 +  | contains_Var _ = false;
    5.16 +(* contains_Var (str2term "?z = 3") (*true*);
    5.17 +   contains_Var (str2term "z = 3")  (*false*);
    5.18 +   *)
    5.19  
    5.20  (*..*)
    5.21  fun int_of_str str =
    5.22 @@ -235,7 +244,9 @@
    5.23  > cterm_of (sign_of thy) ss;
    5.24  val it = "[R = R, R = R, R = R]" : cterm  *)
    5.25  
    5.26 -fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);
    5.27 +fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
    5.28 +  | isapair2pair t = 
    5.29 +    raise error ("isapair2pair called with "^term2str t);
    5.30  
    5.31  val listType = Type ("List.list",[Type ("bool",[])]);
    5.32  fun isalist2list ls =

     6.1 --- a/src/smltest/IsacKnowledge/algein.sml	Tue Oct 28 15:16:31 2008 +0100
     6.2 +++ b/src/smltest/IsacKnowledge/algein.sml	Tue Nov 18 16:34:39 2008 +0100
     6.3 @@ -13,6 +13,7 @@
     6.4  "----------- build method 'Berechnung' 'erstSymbolisch' ----------";
     6.5  "----------- me 'Berechnung' 'erstNumerisch' ---------------------";
     6.6  "----------- auto 'Berechnung' 'erstSymbolisch' ------------------";
     6.7 +"----------- Widerspruch 3 = 777 ---------------------------------";
     6.8  "-----------------------------------------------------------------";
     6.9  "-----------------------------------------------------------------";
    6.10  "-----------------------------------------------------------------";
    6.11 @@ -124,5 +125,34 @@
    6.12  trace_script:=false;
    6.13  *)
    6.14  
    6.15 +"----------- Widerspruch 3 = 777 ---------------------------------";
    6.16 +"----------- Widerspruch 3 = 777 ---------------------------------";
    6.17 +"----------- Widerspruch 3 = 777 ---------------------------------";
    6.18 +val thy = Isac.thy; 
    6.19 +val rew_ord = dummy_ord;
    6.20 +val erls = Erls;
    6.21 +
    6.22 +val thm = assoc_thm' thy ("sym_real_mult_0_right","");
    6.23 +val t = str2term "0 = 0";
    6.24 +val Some (t',_) = rewrite_ thy rew_ord erls false thm t;
    6.25 +term2str t';
    6.26 +(*"0 = ?z1 * 0"*)
    6.27 +
    6.28 +(*testing code in ME/appl.sml*)
    6.29 +val sube = ["?z1 = 3"];
    6.30 +val subte = sube2subte sube;
    6.31 +val subst = sube2subst thy sube;
    6.32 +foldl and_ (true, map contains_Var subte);
    6.33 +
    6.34 +val t'' = subst_atomic subst t';
    6.35 +term2str t'';
    6.36 +(*"0 = 3 * 0"*)
    6.37 +
    6.38 +val thm = assoc_thm' thy ("sym","");
    6.39 +(*----- GOON Widerspruch 3 = 777
    6.40 +val Some (t''',_) = rewrite_ thy rew_ord erls false thm t'';
    6.41 +*)
    6.42 +
    6.43  (* use"../smltest/IsacKnowledge/algein.sml";
    6.44 -   *)
    6.45 \ No newline at end of file
    6.46 +   *)
    6.47 +

     7.1 --- a/src/smltest/IsacKnowledge/polyminus.sml	Tue Oct 28 15:16:31 2008 +0100
     7.2 +++ b/src/smltest/IsacKnowledge/polyminus.sml	Tue Nov 18 16:34:39 2008 +0100
     7.3 @@ -341,6 +341,12 @@
     7.4  	    ["probe","fuer_polynom"]))];
     7.5  moveActiveRoot 1;
     7.6  autoCalculate 1 CompleteCalc;
     7.7 +(* autoCalculate 1 CompleteCalcHead;
     7.8 +   autoCalculate 1 (Step 1);
     7.9 +   autoCalculate 1 (Step 1);
    7.10 +   val ((pt,p),_) = get_calc 1; term2str (get_obj g_res pt (fst p));
    7.11 +@@@@@WN081114 gives "??.empty", all "Pruefe" are the same,
    7.12 +although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)
    7.13  val ((pt,p),_) = get_calc 1;
    7.14  if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"
    7.15  then () else raise error "polyminus.sml: Probe 11 = 11";