src/HOL/Modelcheck/mucke_oracle.ML
author wenzelm
Sun Jun 05 11:31:21 2005 +0200 (2005-06-05)
changeset 16258 f3d913abf7e5
parent 16152 7294283b0c45
child 16429 e871f4b1a4f0
permissions -rw-r--r--
File.shell_path;
     1 
     2 (* $Id$ *)
     3 
     4 exception MuckeOracleExn of term;
     5 
     6 val trace_mc = ref false; 
     7 
     8 
     9 (* transform_case post-processes output strings of the syntax "Mucke" *)
    10 (* with respect to the syntax of the case construct                   *)
    11 local
    12   fun extract_argument [] = []
    13   | extract_argument ("*"::_) = []
    14   | extract_argument (x::xs) = x::(extract_argument xs);
    15 
    16   fun cut_argument [] = []
    17   | cut_argument ("*"::r) = r
    18   | cut_argument (_::xs) = cut_argument xs;
    19 
    20   fun insert_case_argument [] s = []
    21   | insert_case_argument ("*"::"="::xl) (x::xs) =
    22          (explode(x)@(" "::"="::(insert_case_argument xl (x::xs))))
    23   | insert_case_argument ("c"::"a"::"s"::"e"::"*"::xl) s =
    24         (let
    25         val arg=implode(extract_argument xl);
    26         val xr=cut_argument xl
    27         in
    28          "c"::"a"::"s"::"e"::" "::(insert_case_argument xr (arg::s))
    29         end)
    30   | insert_case_argument ("e"::"s"::"a"::"c"::"*"::xl) (x::xs) =
    31         "e"::"s"::"a"::"c"::(insert_case_argument xl xs)
    32   | insert_case_argument (x::xl) s = x::(insert_case_argument xl s);
    33 in
    34 
    35 fun transform_case s = implode(insert_case_argument (explode s) []);
    36 
    37 end;
    38 
    39 
    40 (* if_full_simp_tac is a tactic for rewriting non-boolean ifs *)
    41 local
    42   (* searching an if-term as below as possible *)
    43   fun contains_if (Abs(a,T,t)) = [] |
    44   contains_if (Const("If",T) $ b $ a1 $ a2) =
    45   let
    46   fun tn (Type(s,_)) = s |
    47   tn _ = error "cannot master type variables in if term";
    48   val s = tn(body_type T);
    49   in
    50   if (s="bool") then [] else [b,a1,a2]
    51   end |
    52   contains_if (a $ b) = if ((contains_if b)=[]) then (contains_if a)
    53 		        else (contains_if b) |
    54   contains_if _ = [];
    55 
    56   fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(variant_abs(a,T,t))) |
    57   find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then
    58   (if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b))
    59   else (a $ b,contains_if(a $ b))|
    60   find_replace_term t = (t,[]);
    61 
    62   fun if_substi (Abs(a,T,t)) trm = Abs(a,T,t) |
    63   if_substi (Const("If",T) $ b $ a1 $ a2) t = t |
    64   if_substi (a $ b) t = if ((contains_if b)=[]) then ((if_substi a t)$b)
    65 		        else (a$(if_substi b t)) |
    66   if_substi t v = t;
    67 
    68   fun deliver_term (t,[]) = [] |
    69   deliver_term (t,[b,a1,a2]) =
    70   [
    71   Const("Trueprop",Type("fun",[Type("bool",[]),Type("prop",[])])) $
    72   (
    73 Const("op =",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
    74   $ t $
    75   (
    76 Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
    77   $
    78   (
    79 Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
    80   $ b $ (if_substi t a1))
    81   $
    82   (
    83 Const("op -->",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
    84   $ (Const("Not",Type("fun",[Type("bool",[]),Type("bool",[])])) $ b) $ (if_substi t a2))
    85   ))] |
    86   deliver_term _ =
    87   error "tactic failed due to occurence of malformed if-term" (* shouldnt occur *);
    88 
    89   fun search_if (*((Const("==",_)) $ _ $*) (a) = deliver_term(find_replace_term a);
    90 
    91   fun search_ifs [] = [] |
    92   search_ifs (a::r) =
    93   let
    94   val i = search_if a
    95   in
    96   if (i=[]) then (search_ifs r) else i
    97   end;
    98 in
    99 
   100 fun if_full_simp_tac sset i state =
   101 let val sign = #sign (rep_thm state);
   102         val (subgoal::_) = Library.drop(i-1,prems_of state);
   103         val prems = Logic.strip_imp_prems subgoal;
   104 	val concl = Logic.strip_imp_concl subgoal;
   105 	val prems = prems @ [concl];
   106         val itrm = search_ifs prems;
   107 in
   108 if (itrm = []) then no_tac state else
   109 (
   110 let
   111 val trm = hd(itrm)
   112 in
   113 (
   114 push_proof();
   115 goalw_cterm [] (cterm_of sign trm);
   116 by (simp_tac (simpset()) 1);
   117         let
   118         val if_tmp_result = result()
   119         in
   120         (
   121         pop_proof();
   122         CHANGED(full_simp_tac (sset addsimps [if_tmp_result]) i) state)
   123         end
   124 )
   125 end)
   126 end;
   127 
   128 end;
   129 
   130 (********************************************************)
   131 (* All following stuff serves for defining mk_mc_oracle *)
   132 (********************************************************)
   133 
   134 (***************************************)
   135 (* SECTION 0: some auxiliary functions *)
   136 
   137 fun list_contains_key [] _ = false |
   138 list_contains_key ((a,l)::r) t = if (a=t) then true else (list_contains_key r t);
   139 
   140 fun search_in_keylist [] _ = [] |
   141 search_in_keylist ((a,l)::r) t = if (a=t) then l else (search_in_keylist r t);
   142 
   143 (* delivers the part of a qualified type/const-name after the last dot *)
   144 fun post_last_dot str =
   145 let
   146 fun fl [] = [] |
   147 fl (a::r) = if (a=".") then [] else (a::(fl r));
   148 in
   149 implode(rev(fl(rev(explode str))))
   150 end;
   151 
   152 (* OUTPUT - relevant *)
   153 (* converts type to string by a mucke-suitable convention *)
   154 fun type_to_string_OUTPUT (Type(a,[])) = post_last_dot a |
   155 type_to_string_OUTPUT (Type("*",[a,b])) =
   156          "P_" ^ (type_to_string_OUTPUT a) ^ "_AI_" ^ (type_to_string_OUTPUT b) ^ "_R" |
   157 type_to_string_OUTPUT (Type(a,l)) =
   158 let
   159 fun ts_to_string [] = "" |
   160 ts_to_string (a::[]) = type_to_string_OUTPUT a |
   161 ts_to_string (a::l) = (type_to_string_OUTPUT a) ^ "_I_" ^ (ts_to_string l);
   162 in
   163 (post_last_dot a) ^ "_A_" ^ (ts_to_string l) ^ "_C"
   164 end |
   165 type_to_string_OUTPUT _ =
   166 error "unexpected type variable in type_to_string";
   167 
   168 (* delivers type of a term *)
   169 fun type_of_term (Const(_,t)) = t |
   170 type_of_term (Free(_,t)) = t |
   171 type_of_term (Var(_,t)) = t |
   172 type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(variant_abs(x,t,trm)))]) |
   173 type_of_term (a $ b) =
   174 let
   175  fun accept_fun_type (Type("fun",[x,y])) = (x,y) |
   176  accept_fun_type _ =
   177  error "no function type returned, where it was expected (in type_of_term)";
   178  val (x,y) = accept_fun_type(type_of_term a)
   179 in
   180 y
   181 end |
   182 type_of_term _ = 
   183 error "unexpected bound variable when calculating type of a term (in type_of_term)";
   184 
   185 (* makes list [a1..an] and ty to type an -> .. -> a1 -> ty *)
   186 fun fun_type_of [] ty = ty |
   187 fun_type_of (a::r) ty = fun_type_of r (Type("fun",[a,ty]));
   188 
   189 (* creates a constructor term from constructor and its argument terms *)
   190 fun con_term_of t [] = t |
   191 con_term_of t (a::r) = con_term_of (t $ a) r;
   192 
   193 (* creates list of constructor terms *)
   194 fun con_term_list_of trm [] = [] |
   195 con_term_list_of trm (a::r) = (con_term_of trm a)::(con_term_list_of trm r);
   196 
   197 (* list multiplication *)
   198 fun multiply_element a [] = [] |
   199 multiply_element a (l::r) = (a::l)::(multiply_element a r);
   200 fun multiply_list [] l = [] |
   201 multiply_list (a::r) l = (multiply_element a l)@(multiply_list r l);
   202 
   203 (* To a list of types, delivers all lists of proper argument terms; tl has to *)
   204 (* be a preprocessed type list with element type: (type,[(string,[type])])    *)
   205 fun arglist_of sg tl [] = [[]] |
   206 arglist_of sg tl (a::r) =
   207 let
   208 fun ispair (Type("*",x::y::[])) = (true,(x,y)) |
   209 ispair x = (false,(x,x));
   210 val erg =
   211 (if (fst(ispair a))
   212  then (let
   213         val (x,y) = snd(ispair a)
   214        in
   215         con_term_list_of (Const("pair",Type("fun",[x,Type("fun",[y,a])])))
   216 			 (arglist_of sg tl [x,y])
   217        end)
   218  else
   219  (let
   220   fun deliver_erg sg tl _ [] = [] |
   221   deliver_erg sg tl typ ((c,tyl)::r) = let
   222                         val ft = fun_type_of (rev tyl) typ;
   223                         val trm = #t(rep_cterm(read_cterm sg (c,ft)));
   224                         in
   225                         (con_term_list_of trm (arglist_of sg tl tyl))
   226 			@(deliver_erg sg tl typ r)
   227                         end;
   228   val cl = search_in_keylist tl a;
   229   in
   230   deliver_erg sg tl a cl
   231   end))
   232 in
   233 multiply_list erg (arglist_of sg tl r)
   234 end;
   235 
   236 (*******************************************************************)
   237 (* SECTION 1: Robert Sandner's source was improved and extended by *)
   238 (* generation of function declarations                             *)
   239 
   240 fun dest_Abs (Abs s_T_t) = s_T_t
   241   | dest_Abs t = raise TERM("dest_Abs", [t]);
   242 
   243 (*
   244 fun force_Abs (Abs s_T_t) = Abs s_T_t
   245   | force_Abs t = Abs("x", hd(fst(strip_type (type_of t))),
   246 		      (incr_boundvars 1 t) $ (Bound 0));
   247 
   248 fun etaexp_dest_Abs t = dest_Abs (force_Abs t);
   249 *)
   250 
   251 (* replace Vars bei Frees, freeze_thaw shares code of tactic/freeze_thaw
   252    and thm.instantiate *)
   253 fun freeze_thaw t =
   254   let val used = add_term_names (t, [])
   255           and vars = term_vars t;
   256       fun newName (Var(ix,_), (pairs,used)) = 
   257           let val v = variant used (string_of_indexname ix)
   258           in  ((ix,v)::pairs, v::used)  end;
   259       val (alist, _) = foldr newName ([], used) vars;
   260       fun mk_inst (Var(v,T)) = 
   261           (Var(v,T),
   262            Free(valOf (assoc(alist,v)), T));
   263       val insts = map mk_inst vars;
   264   in subst_atomic insts t end;
   265 
   266 fun make_fun_type (a::b::l) = Type("fun",a::(make_fun_type (b::l))::[]) 
   267   | make_fun_type (a::l) = a;
   268 
   269 fun make_decl muckeType id isaType =
   270   let val constMuckeType = Const(muckeType,isaType);
   271       val constId = Const(id,isaType);
   272       val constDecl = Const("_decl", make_fun_type [isaType,isaType,isaType]); 
   273   in (constDecl $ constMuckeType) $ constId end;
   274 
   275 fun make_MuTerm muDeclTerm ParamDeclTerm muTerm isaType =
   276   let val constMu = Const("_mu",
   277 			  make_fun_type [isaType,isaType,isaType,isaType]);
   278       val t1 = constMu $ muDeclTerm;
   279       val t2 = t1 $ ParamDeclTerm;
   280       val t3 = t2 $  muTerm
   281   in t3 end;
   282 
   283 fun make_MuDecl muDeclTerm ParamDeclTerm isaType =
   284   let val constMu = Const("_mudec",
   285                           make_fun_type [isaType,isaType,isaType]);
   286       val t1 = constMu $ muDeclTerm;
   287       val t2 = t1 $ ParamDeclTerm
   288   in t2 end;
   289 
   290 fun make_NuTerm muDeclTerm ParamDeclTerm muTerm isaType =
   291   let val constMu = Const("_nu",
   292                           make_fun_type [isaType,isaType,isaType,isaType]);
   293       val t1 = constMu $ muDeclTerm;
   294       val t2 = t1 $ ParamDeclTerm;
   295       val t3 = t2 $  muTerm
   296   in t3 end;
   297 
   298 fun make_NuDecl muDeclTerm ParamDeclTerm isaType =
   299   let val constMu = Const("_nudec",
   300                           make_fun_type [isaType,isaType,isaType]);
   301       val t1 = constMu $ muDeclTerm;
   302       val t2 = t1 $ ParamDeclTerm
   303   in t2 end;
   304 
   305 fun is_mudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.mu",_)) $ t2)) = true
   306   | is_mudef _ = false;
   307 
   308 fun is_nudef (( Const("==",_) $ t1) $ ((Const("MuCalculus.nu",_)) $ t2)) = true
   309   | is_nudef _ = false;
   310 
   311 fun make_decls sign Dtype (Const(str,tp)::n::Clist) = 
   312     let val const_decls = Const("_decls",make_fun_type [Dtype,Dtype,Dtype]);
   313         val decl = make_decl (type_to_string_OUTPUT tp) str Dtype;
   314     in
   315     ((const_decls $ decl) $ (make_decls sign Dtype (n::Clist)))
   316     end
   317   | make_decls sign Dtype [Const(str,tp)] = 
   318       make_decl (type_to_string_OUTPUT tp) str Dtype;
   319 
   320 
   321 (* make_mu_def transforms an Isabelle Mu-Definition into Mucke format
   322    Takes equation of the form f = Mu Q. % x. t *)
   323 
   324 fun dest_atom (Const t) = dest_Const (Const t)
   325   | dest_atom (Free t)  = dest_Free (Free t);
   326 
   327 fun get_decls sign Clist (Abs(s,tp,trm)) = 
   328     let val VarAbs = variant_abs(s,tp,trm);
   329     in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
   330     end
   331   | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
   332   | get_decls sign Clist trm = (Clist,trm);
   333 
   334 fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
   335   let 	val LHSStr = fst (dest_atom LHS);
   336 	val MuType = Type("bool",[]); (* always ResType of mu, also serves
   337 					 as dummy type *)
   338 	val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
   339   	val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
   340 	val PConsts = rev PCon_LHS;
   341 	val muDeclTerm = make_decl "bool" LHSStr MuType;
   342 	val PDeclsTerm = make_decls sign MuType PConsts;
   343 	val MuDefTerm = make_MuTerm muDeclTerm PDeclsTerm MMuTerm MuType;		
   344   in MuDefTerm end;
   345 
   346 fun make_mu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
   347   let   val LHSStr = fst (dest_atom LHS);
   348         val MuType = Type("bool",[]); (* always ResType of mu, also serves
   349                                          as dummy type *)
   350         val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
   351         val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
   352         val PConsts = rev PCon_LHS;
   353         val muDeclTerm = make_decl "bool" LHSStr MuType;
   354         val PDeclsTerm = make_decls sign MuType PConsts;
   355         val MuDeclTerm = make_MuDecl muDeclTerm PDeclsTerm MuType;
   356   in MuDeclTerm end;
   357 
   358 fun make_nu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
   359   let   val LHSStr = fst (dest_atom LHS);
   360         val MuType = Type("bool",[]); (* always ResType of mu, also serves
   361                                          as dummy type *)
   362         val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
   363         val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
   364         val PConsts = rev PCon_LHS;
   365         val muDeclTerm = make_decl "bool" LHSStr MuType;
   366         val PDeclsTerm = make_decls sign MuType PConsts;
   367         val NuDefTerm = make_NuTerm muDeclTerm PDeclsTerm MMuTerm MuType;
   368   in NuDefTerm end;
   369 
   370 fun make_nu_decl sign ((tt $ LHS) $ (ttt $ RHS)) =
   371   let   val LHSStr = fst (dest_atom LHS);
   372         val MuType = Type("bool",[]); (* always ResType of mu, also serves
   373                                          as dummy type *)
   374         val (_,_,PAbs) = dest_Abs (RHS); (* RHS is %Q. ... *)
   375         val (PCon_LHS,MMuTerm) = get_decls sign [] (subst_bound (LHS,PAbs));
   376         val PConsts = rev PCon_LHS; 
   377         val muDeclTerm = make_decl "bool" LHSStr MuType;
   378         val PDeclsTerm = make_decls sign MuType PConsts; 
   379         val NuDeclTerm = make_NuDecl muDeclTerm PDeclsTerm MuType;
   380   in NuDeclTerm end;
   381 
   382 fun make_FunMuckeTerm FunDeclTerm ParamDeclTerm Term isaType =
   383   let 	val constFun = Const("_fun",
   384 			    make_fun_type [isaType,isaType,isaType,isaType]);
   385       	val t1 = constFun $ FunDeclTerm;
   386       	val t2 = t1 $ ParamDeclTerm;
   387       	val t3 = t2 $  Term
   388   in t3 end;
   389 
   390 fun make_FunMuckeDecl FunDeclTerm ParamDeclTerm isaType =
   391   let   val constFun = Const("_dec",
   392                             make_fun_type [isaType,isaType,isaType]);
   393       val t1 = constFun $ FunDeclTerm;
   394       val t2 = t1 $ ParamDeclTerm
   395   in t2 end;
   396 
   397 fun is_fundef (( Const("==",_) $ _) $ ((Const("split",_)) $ _)) = true |
   398 is_fundef (( Const("==",_) $ _) $ Abs(x_T_t)) = true 
   399 | is_fundef _ = false; 
   400 
   401 fun make_mucke_fun_def sign ((_ $ LHS) $ RHS) =
   402   let 	(* fun dest_atom (Const t) = dest_Const (Const t)
   403           | dest_atom (Free t)  = dest_Free (Free t); *)
   404 	val LHSStr = fst (dest_atom LHS);
   405 	val LHSResType = body_type(snd(dest_atom LHS));
   406 	val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
   407 (*	val (_,AbsType,RawTerm) = dest_Abs(RHS);
   408 *)	val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
   409 	val Consts_LHS = rev Consts_LHS_rev;
   410 	val PDeclsTerm = make_decls sign LHSResType Consts_LHS; 
   411 		(* Boolean functions only, list necessary in general *)
   412 	val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
   413 	val MuckeDefTerm = make_FunMuckeTerm DeclTerm PDeclsTerm Free_RHS
   414 					 LHSResType;	
   415   in MuckeDefTerm end;
   416 
   417 fun make_mucke_fun_decl sign ((_ $ LHS) $ RHS) =
   418   let   (* fun dest_atom (Const t) = dest_Const (Const t)
   419           | dest_atom (Free t)  = dest_Free (Free t); *)
   420         val LHSStr = fst (dest_atom LHS);
   421 	val LHSResType = body_type(snd(dest_atom LHS));
   422         val LHSResTypeStr = type_to_string_OUTPUT LHSResType;
   423 (*      val (_,AbsType,RawTerm) = dest_Abs(RHS);
   424 *)      val (Consts_LHS_rev,Free_RHS) = get_decls sign [] RHS;
   425         val Consts_LHS = rev Consts_LHS_rev;
   426         val PDeclsTerm = make_decls sign LHSResType Consts_LHS;
   427                 (* Boolean functions only, list necessary in general *)
   428         val DeclTerm = make_decl LHSResTypeStr LHSStr LHSResType;
   429 	val MuckeDeclTerm = make_FunMuckeDecl DeclTerm PDeclsTerm LHSResType;
   430 in MuckeDeclTerm end;
   431 
   432 fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) =
   433     (let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]);
   434      	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
   435 	 val VarAbs = variant_abs(str,tp,t);
   436 	 val BoundConst = Const(fst VarAbs,tp);
   437 	 val t1 = ExConst $ TypeConst;
   438 	 val t2 = t1 $ BoundConst;
   439  	 val t3 = elim_quantifications sign (snd VarAbs)
   440      in t2 $ t3 end)
   441   |  elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) =
   442     (let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]);
   443     	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
   444 	 val VarAbs = variant_abs(str,tp,t);
   445 	 val BoundConst = Const(fst VarAbs,tp);
   446 	 val t1 = AllConst $ TypeConst;
   447 	 val t2 = t1 $ BoundConst;
   448 	 val t3 = elim_quantifications sign (snd VarAbs)
   449      in t2 $ t3 end)
   450   | elim_quantifications sign (t1 $ t2) = 
   451    	(elim_quantifications sign t1) $ (elim_quantifications sign t2)
   452   | elim_quantifications sign (Abs(_,_,t)) = elim_quantifications sign t
   453   | elim_quantifications sign t = t;
   454 fun elim_quant_in_list sign [] = []
   455   | elim_quant_in_list sign (trm::list) = 
   456 			(elim_quantifications sign trm)::(elim_quant_in_list sign list);
   457 
   458 fun dummy true = writeln "True\n" |
   459     dummy false = writeln "Fals\n";
   460 
   461 fun transform_definitions sign [] = []
   462   | transform_definitions sign (trm::list) = 
   463       if is_mudef trm 
   464       then (make_mu_def sign trm)::(transform_definitions sign list)
   465       else 
   466 	if is_nudef trm
   467 	 then (make_nu_def sign trm)::(transform_definitions sign list)
   468      	 else 
   469 	   if is_fundef trm
   470  	   then (make_mucke_fun_def sign trm)::(transform_definitions sign list)
   471 		     else trm::(transform_definitions sign list);
   472 
   473 fun terms_to_decls sign [] = []
   474  | terms_to_decls sign (trm::list) =
   475       if is_mudef trm
   476       then (make_mu_decl sign trm)::(terms_to_decls sign list)
   477       else
   478         if is_nudef trm
   479          then (make_nu_decl sign trm)::(terms_to_decls sign list)
   480          else
   481            if is_fundef trm
   482            then (make_mucke_fun_decl sign trm)::(terms_to_decls sign list)
   483                      else (transform_definitions sign list);
   484 
   485 fun transform_terms sign list = 
   486 let val DefsOk = transform_definitions sign list;
   487 in elim_quant_in_list sign DefsOk
   488 end;
   489 
   490 fun string_of_terms sign terms =
   491 let fun make_string sign [] = "" |
   492  	make_string sign (trm::list) =
   493            Sign.string_of_term sign trm ^ "\n" ^ make_string sign list
   494 in
   495 (setmp print_mode ["Mucke"] (make_string sign) terms)
   496 end;
   497 
   498 fun callmc s =
   499   let
   500     val mucke_home = getenv "MUCKE_HOME";
   501     val mucke =
   502       if mucke_home = "" then error "Environment variable MUCKE_HOME not set"
   503       else mucke_home ^ "/mucke";
   504     val mucke_input_file = File.tmp_path (Path.basic "tmp.mu");
   505     val _ = File.write mucke_input_file s;
   506     val result = execute (mucke ^ " -nb -res " ^ File.shell_path mucke_input_file);
   507   in
   508     if not (!trace_mc) then (File.rm mucke_input_file) else (); 
   509     result
   510   end;
   511 
   512 (* extract_result looks for true value before *) 
   513 (* finishing line "===..." of mucke output    *)
   514 (* ------------------------------------------ *)
   515 (* Be Careful:                                *)
   516 (* If the mucke version changes, some changes *)
   517 (* have also to be made here:                 *)
   518 (* In extract_result, the value               *)
   519 (* answer_with_info_lines checks the output   *)
   520 (* of the muche version, where the output     *)
   521 (* finishes with information about memory and *)
   522 (* time (segregated from the "true" value by  *)
   523 (* a line of equality signs).                 *)
   524 (* For older versions, where this line does   *)
   525 (* exist, value general_answer checks whether *)
   526 (* "true" stand at the end of the output.     *)
   527 local
   528 
   529 infix is_prefix_of contains at_post string_contains string_at_post;
   530 
   531   val is_blank : string -> bool =
   532       fn " " => true | "\t" => true | "\n" => true | "\^L" => true 
   533        | "\160" => true | _ => false;
   534 
   535   fun delete_blanks [] = []
   536     | delete_blanks (":"::xs) = delete_blanks xs
   537     | delete_blanks (x::xs) = 
   538         if (is_blank x) then (delete_blanks xs)
   539 	       	        else x::(delete_blanks xs);
   540   
   541   fun delete_blanks_string s = implode(delete_blanks (explode s));
   542 
   543   fun [] is_prefix_of s = true
   544     | (p::ps) is_prefix_of  [] = false
   545     | (p::ps) is_prefix_of (x::xs) = (p = x) andalso (ps is_prefix_of xs);
   546 
   547   fun [] contains [] = true
   548     | [] contains s = false
   549     | (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);
   550 
   551   fun [] at_post [] = true
   552     | [] at_post s = false
   553     | (x::xs) at_post s = (s = (x::xs)) orelse (xs at_post s);
   554  
   555   fun s string_contains s1 = 
   556       (explode s) contains (explode s1);
   557   fun s string_at_post s1 =
   558       (explode s) at_post (explode s1);
   559 
   560 in 
   561 
   562 fun extract_result goal answer =
   563   let 
   564     val search_text_true = "istrue===";
   565     val short_answer = delete_blanks_string answer;
   566     val answer_with_info_lines = short_answer string_contains search_text_true;
   567     (* val general_answer = short_answer string_at_post "true" *) 
   568   in
   569     (answer_with_info_lines) (* orelse (general_answer) *)
   570   end;
   571 
   572 end; 
   573 
   574 (**************************************************************)
   575 (* SECTION 2: rewrites case-constructs over complex datatypes *)
   576 local
   577 
   578 (* check_case checks, whether a term is of the form a $ "(case x of ...)", *)
   579 (* where x is of complex datatype; the second argument of the result is    *)
   580 (* the number of constructors of the type of x                             *) 
   581 fun check_case sg tl (a $ b) =
   582 let
   583  (* tl_contains_complex returns true in the 1st argument when argument type is *)
   584  (* complex; the 2nd argument is the number of constructors                    *)
   585  fun tl_contains_complex [] _ = (false,0) |
   586  tl_contains_complex ((a,l)::r) t =
   587  let
   588   fun check_complex [] p = p |
   589   check_complex ((a,[])::r) (t,i) = check_complex r (t,i+1) |
   590   check_complex ((a,_)::r) (t,i) = check_complex r (true,i+1);
   591  in
   592 	if (a=t) then (check_complex l (false,0)) else (tl_contains_complex r t)
   593  end;
   594  fun check_head_for_case sg (Const(s,_)) st 0 = 
   595 	if (post_last_dot(s) = (st ^ "_case")) then true else false |
   596  check_head_for_case sg (a $ (Const(s,_))) st 0 = 
   597 	if (post_last_dot(s) = (st ^ "_case")) then true else false |
   598  check_head_for_case _ _ _ 0 = false |
   599  check_head_for_case sg (a $ b) st n = check_head_for_case sg a st (n-1) |
   600  check_head_for_case _ _ _ _ = false;
   601  fun qtn (Type(a,_)) = a | 
   602  qtn _ = error "unexpected type variable in check_case";
   603  val t = type_of_term b;
   604  val (bv,n) = tl_contains_complex tl t
   605  val st = post_last_dot(qtn t); 
   606 in
   607  if (bv) then ((check_head_for_case sg a st n),n) else (false,n) 
   608 end |
   609 check_case sg tl trm = (false,0);
   610 
   611 (* enrich_case_with_terms enriches a case term with additional *)
   612 (* conditions according to the context of the case replacement *)
   613 fun enrich_case_with_terms sg [] t = t |
   614 enrich_case_with_terms sg [trm] (Abs(x,T,t)) =
   615 let
   616  val v = variant_abs(x,T,t);
   617  val f = fst v;
   618  val s = snd v
   619 in
   620 (Const("Ex",Type("fun",[Type("fun",[T,Type("bool",[])]),Type("bool",[])])) $
   621 (Abs(x,T,
   622 abstract_over(Free(f,T),
   623 Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
   624 $
   625 (Const("op =",Type("fun",[T,Type("fun",[T,Type("bool",[])])])) $ (Free(f,T)) $ trm)
   626 $ s))))
   627 end |
   628 enrich_case_with_terms sg (a::r) (Abs(x,T,t)) =
   629         enrich_case_with_terms sg [a] (Abs(x,T,(enrich_case_with_terms sg r t))) |
   630 enrich_case_with_terms sg (t::r) trm =
   631 let val ty = type_of_term t
   632 in
   633 (Const("Ex",Type("fun",[Type("fun",[ ty ,Type("bool",[])]),Type("bool",[])])) $
   634 Abs("a", ty,
   635 Const("op &",Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])]))
   636 $
   637 (Const("op =",Type("fun",[ ty ,Type("fun",[ ty ,Type("bool",[])])])) $ Bound(0) $ t)
   638 $
   639 enrich_case_with_terms sg r (trm $ (Bound(length(r))))))
   640 end;
   641 
   642 fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t = 
   643 let
   644  fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(variant_abs(x,T,t))) |
   645  heart_of_trm t = t;
   646  fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) |
   647  replace_termlist_with_args sg _ trm _ [a] _ ([],[]) =
   648 	if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else 
   649 	(enrich_case_with_terms sg a trm) |
   650  replace_termlist_with_args sg tl trm con [] t (l1,l2) =
   651 	(replace_termlist_with_constrs sg tl l1 l2 t) | 
   652  replace_termlist_with_args sg tl trm con (a::r) t (l1,l2) =
   653  let
   654   val tty = type_of_term t;
   655   val con_term = con_term_of con a;
   656  in
   657 	(Const("If",Type("fun",[Type("bool",[]),
   658         Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])])) $
   659 	(Const("op =",Type("fun",[tty,Type("fun",[tty,Type("bool",[])])])) $
   660         t $ con_term) $
   661 	(if ((heart_of_trm trm)= Const("False",Type("bool",[]))) then trm else 
   662 	(enrich_case_with_terms sg a trm)) $
   663 	(replace_termlist_with_args sg tl trm con r t (l1,l2)))
   664  end;
   665  val arglist = arglist_of sg tl (snd c);
   666  val tty = type_of_term t;
   667  val con_typ = fun_type_of (rev (snd c)) tty;
   668  val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
   669 in
   670  replace_termlist_with_args sg tl a con arglist t (l1,l2)
   671 end |
   672 replace_termlist_with_constrs _ _ _ _ _ = 
   673 error "malformed arguments in replace_termlist_with_constrs" (* shouldnt occur *);
   674 
   675 (* rc_in_termlist constructs a cascading if with the case terms in trm_list, *)
   676 (* which were found in rc_in_term (see replace_case)                         *)
   677 fun rc_in_termlist sg tl trm_list trm =  
   678 let
   679  val ty = type_of_term trm;
   680  val constr_list = search_in_keylist tl ty;
   681 in
   682 	replace_termlist_with_constrs sg tl trm_list constr_list trm
   683 end;  
   684 
   685 in
   686 
   687 (* replace_case replaces each case statement over a complex datatype by a cascading if; *)
   688 (* it is normally called with a 0 in the 4th argument, it is positive, if in the course *)
   689 (* of calculation, a "case" is discovered and then indicates the distance to that case  *)
   690 fun replace_case sg tl (a $ b) 0 =
   691 let
   692  (* rc_in_term changes the case statement over term x to a cascading if; the last *)
   693  (* indicates the distance to the "case"-constant                                 *)
   694  fun rc_in_term sg tl (a $ b) l x 0 =
   695 	 (replace_case sg tl a 0) $ (rc_in_termlist sg tl l x) |  
   696  rc_in_term sg tl  _ l x 0 = rc_in_termlist sg tl l x |
   697  rc_in_term sg tl (a $ b) l x n = rc_in_term sg tl a (b::l) x (n-1) |
   698  rc_in_term sg _ trm _ _ n =
   699  error("malformed term for case-replacement: " ^ (Sign.string_of_term sg trm));
   700  val (bv,n) = check_case sg tl (a $ b);
   701 in
   702  if (bv) then 
   703 	(let
   704 	val t = (replace_case sg tl a n) 
   705 	in 
   706 	rc_in_term sg tl t [] b n	
   707 	end)
   708  else ((replace_case sg tl a 0) $ (replace_case sg tl b 0))
   709 end |
   710 replace_case sg tl (a $ b) 1 = a $ (replace_case sg tl b 0) |
   711 replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) |
   712 replace_case sg tl (Abs(x,T,t)) _ = 
   713 let 
   714  val v = variant_abs(x,T,t);
   715  val f = fst v;
   716  val s = snd v
   717 in
   718  Abs(x,T,abstract_over(Free(f,T),replace_case sg tl s 0))
   719 end |
   720 replace_case _ _ t _ = t;
   721 
   722 end;
   723 
   724 (*******************************************************************)
   725 (* SECTION 3: replacing variables being part of a constructor term *)
   726 
   727 (* transforming terms so that nowhere a variable is subterm of *)
   728 (* a constructor term; the transformation uses cascading ifs   *)
   729 fun remove_vars sg tl (Abs(x,ty,trm)) =
   730 let
   731 (* checks freeness of variable x in term *)
   732 fun xFree x (a $ b) = if (xFree x a) then true else (xFree x b) |
   733 xFree x (Abs(a,T,trm)) = xFree x trm |
   734 xFree x (Free(y,_)) = if (x=y) then true else false |
   735 xFree _ _ = false;
   736 (* really substitues variable x by term c *)
   737 fun real_subst sg tl x c (a$b) = (real_subst sg tl x c a) $ (real_subst sg tl x c b) |
   738 real_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,real_subst sg tl x c trm) |
   739 real_subst sg tl x c (Free(y,t)) = if (x=y) then c else Free(y,t) |
   740 real_subst sg tl x c t = t;
   741 (* substituting variable x by term c *)
   742 fun x_subst sg tl x c (a $ b) =
   743 let
   744  val t = (type_of_term (a $ b))
   745 in
   746  if ((list_contains_key tl t) andalso (xFree x (a$b)))
   747  then (real_subst sg tl x c (a$b)) else ((x_subst sg tl x c a) $ (x_subst sg tl x c b))
   748 end |
   749 x_subst sg tl x c (Abs(y,T,trm)) = Abs(y,T,x_subst sg tl x c trm) |
   750 x_subst sg tl x c t = t;
   751 (* genearting a cascading if *)
   752 fun casc_if sg tl x ty (c::l) trm =
   753 let
   754  val arglist = arglist_of sg tl (snd c);
   755  val con_typ = fun_type_of (rev (snd c)) ty;
   756  val con = #t(rep_cterm(read_cterm sg (fst c,con_typ)));
   757  fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
   758  casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
   759  casc_if2 sg tl x con (a::r) ty trm cl =
   760         Const("If",Type("fun",[Type("bool",[]),
   761         Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])
   762         ])) $
   763      (Const("op =",Type("fun",[ty,Type("fun",[ty,Type("bool",[])])])) $
   764         Free(x,ty) $ (real_subst sg tl x (con_term_of con a) (Free(x,ty)))) $
   765    (x_subst sg tl x (con_term_of con a) trm) $
   766    (casc_if2 sg tl x con r ty trm cl) |
   767  casc_if2 sg tl x con [] ty trm cl = casc_if sg tl x ty cl trm;
   768 in
   769  casc_if2 sg tl x con arglist ty trm l
   770 end |
   771 casc_if _ _ _ _ [] trm = trm (* should never occur *); 
   772 fun if_term sg tl x ty trm =
   773 let
   774  val tyC_list = search_in_keylist tl ty;
   775 in
   776  casc_if sg tl x ty tyC_list trm
   777 end;
   778 (* checking whether a variable occurs in a constructor term *)
   779 fun constr_term_contains_var sg tl (a $ b) x =
   780 let
   781  val t = type_of_term (a $ b)
   782 in
   783  if ((list_contains_key tl t) andalso (xFree x (a$b))) then true
   784  else
   785  (if (constr_term_contains_var sg tl a x) then true 
   786   else (constr_term_contains_var sg tl b x))
   787 end |
   788 constr_term_contains_var sg tl (Abs(y,ty,trm)) x =
   789          constr_term_contains_var sg tl (snd(variant_abs(y,ty,trm))) x |
   790 constr_term_contains_var _ _ _ _ = false;
   791 val vt = variant_abs(x,ty,trm);
   792 val tt = remove_vars sg tl (snd(vt))
   793 in
   794 if (constr_term_contains_var sg tl tt (fst vt))
   795 (* fst vt muss frei vorkommen, als ECHTER TeilKonstruktorterm *)
   796 then (Abs(x,ty,
   797         abstract_over(Free(fst vt,ty),
   798 	if_term sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) (fst vt) ty tt)))
   799 else Abs(x,ty,abstract_over(Free(fst vt,ty),tt))
   800 end |
   801 remove_vars sg tl (a $ b) = (remove_vars sg tl a) $ (remove_vars sg tl b) |
   802 remove_vars sg tl t = t;
   803 
   804 (* dissolves equalities "=" of boolean terms, where one of them is a complex term *)
   805 fun remove_equal sg tl (Abs(x,ty,trm)) = Abs(x,ty,remove_equal sg tl trm) |
   806 remove_equal sg tl (Const("op =",Type("fun",[Type("bool",[]),
   807 	Type("fun",[Type("bool",[]),Type("bool",[])])])) $ lhs $ rhs) =
   808 let
   809 fun complex_trm (Abs(_,_,_)) = true |
   810 complex_trm (_ $ _) = true |
   811 complex_trm _ = false;
   812 in
   813 (if ((complex_trm lhs) orelse (complex_trm rhs)) then
   814 (let
   815 val lhs = remove_equal sg tl lhs;
   816 val rhs = remove_equal sg tl rhs
   817 in
   818 (
   819 Const("op &",
   820 Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
   821 (Const("op -->",
   822  Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
   823 	lhs $ rhs) $
   824 (Const("op -->",
   825  Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
   826 	rhs $ lhs)
   827 )
   828 end)
   829 else
   830 (Const("op =",
   831  Type("fun",[Type("bool",[]),Type("fun",[Type("bool",[]),Type("bool",[])])])) $
   832 	lhs $ rhs))
   833 end |
   834 remove_equal sg tl (a $ b) = (remove_equal sg tl a) $ (remove_equal sg tl b) |
   835 remove_equal sg tl trm = trm;
   836 
   837 (* rewrites constructor terms (without vars) for mucke *)
   838 fun rewrite_dt_term sg tl (Abs(x,ty,t)) = Abs(x,ty,(rewrite_dt_term sg tl t)) |
   839 rewrite_dt_term sg tl (a $ b) =
   840 let
   841 
   842 (* OUTPUT - relevant *)
   843 (* transforms constructor term to a mucke-suitable output *)
   844 fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
   845 		(term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
   846 term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
   847 term_OUTPUT sg (Const(s,t)) = post_last_dot s |
   848 term_OUTPUT _ _ = 
   849 error "term contains an unprintable constructor term (in term_OUTPUT)";
   850 
   851 fun contains_bound i (Bound(j)) = if (j>=i) then true else false |
   852 contains_bound i (a $ b) = if (contains_bound i a) then true else (contains_bound i b) |
   853 contains_bound i (Abs(_,_,t)) = contains_bound (i+1) t |
   854 contains_bound _ _ = false;
   855 
   856 in
   857         if (contains_bound 0 (a $ b)) 
   858 	then ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
   859         else
   860         (
   861         let
   862         val t = type_of_term (a $ b);
   863         in
   864         if (list_contains_key tl t) then (Const((term_OUTPUT sg (a $ b)),t)) else
   865         ((rewrite_dt_term sg tl a) $ (rewrite_dt_term sg tl b))
   866         end)
   867 end |
   868 rewrite_dt_term sg tl t = t;
   869 
   870 fun rewrite_dt_terms sg tl [] = [] |
   871 rewrite_dt_terms sg tl (a::r) =
   872 let
   873  val c = (replace_case sg ((Type("bool",[]),[("True",[]),("False",[])])::tl) a 0);
   874  val rv = (remove_vars sg tl c);  
   875  val rv = (remove_equal sg tl rv);
   876 in
   877  ((rewrite_dt_term sg tl rv) 
   878  :: (rewrite_dt_terms sg tl r))
   879 end;
   880 
   881 (**********************************************************************)
   882 (* SECTION 4: generating type declaration and preprocessing type list *)
   883 
   884 fun make_type_decls [] tl = "" |
   885 make_type_decls ((a,l)::r) tl = 
   886 let
   887 fun comma_list_of [] = "" |
   888 comma_list_of (a::[]) = a |
   889 comma_list_of (a::r) = a ^ "," ^ (comma_list_of r);
   890 
   891 (* OUTPUT - relevant *)
   892 (* produces for each type of the 2nd argument its constant names (see *)
   893 (* concat_constr) and appends them to prestring (see concat_types)    *)
   894 fun generate_constnames_OUTPUT prestring [] _ = [prestring] |
   895 generate_constnames_OUTPUT prestring ((Type("*",[a,b]))::r) tl =
   896  generate_constnames_OUTPUT prestring (a::b::r) tl |
   897 generate_constnames_OUTPUT prestring (a::r) tl =
   898 let
   899  fun concat_constrs [] _ = [] |
   900  concat_constrs ((c,[])::r) tl = c::(concat_constrs r tl)  |
   901  concat_constrs ((c,l)::r) tl =
   902          (generate_constnames_OUTPUT (c ^ "_I_") l tl) @ (concat_constrs r tl);
   903  fun concat_types _ [] _ _ = [] |
   904  concat_types prestring (a::q) [] tl = [prestring ^ a] 
   905 				       @ (concat_types prestring q [] tl) |
   906  concat_types prestring (a::q) r tl = 
   907 		(generate_constnames_OUTPUT (prestring ^ a ^ "_I_") r tl) 
   908 		@ (concat_types prestring q r tl);
   909  val g = concat_constrs (search_in_keylist tl a) tl;
   910 in
   911  concat_types prestring g r tl
   912 end;
   913 
   914 fun make_type_decl a tl =
   915 let
   916         val astr = type_to_string_OUTPUT a;
   917         val dl = generate_constnames_OUTPUT "" [a] tl;
   918         val cl = comma_list_of dl;
   919 in
   920         ("enum " ^ astr ^ " {" ^ cl ^ "};\n")
   921 end;
   922 in
   923  (make_type_decl a tl) ^ (make_type_decls r tl)
   924 end;
   925 
   926 fun check_finity gl [] [] true = true |
   927 check_finity gl bl [] true = (check_finity gl [] bl false) |
   928 check_finity _ _ [] false =
   929 error "used datatypes are not finite" |
   930 check_finity gl bl ((t,cl)::r) b =
   931 let
   932 fun listmem [] _ = true |
   933 listmem (a::r) l = if (a mem l) then (listmem r l) else false;
   934 fun snd_listmem [] _ = true |
   935 snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false;
   936 in
   937 (if (snd_listmem cl gl) then (check_finity (t::gl) bl r true)
   938 else (check_finity gl ((t,cl)::bl) r b))
   939 end;
   940 
   941 fun preprocess_td sg [] done = [] |
   942 preprocess_td sg (a::b) done =
   943 let
   944 fun extract_hd sg (_ $ Abs(_,_,r)) = extract_hd sg r |
   945 extract_hd sg (Const("Trueprop",_) $ r) = extract_hd sg r |
   946 extract_hd sg (Var(_,_) $ r) = extract_hd sg r |
   947 extract_hd sg (a $ b) = extract_hd sg a |
   948 extract_hd sg (Const(s,t)) = post_last_dot s |
   949 extract_hd _ _ =
   950 error "malformed constructor term in a induct-theorem";
   951 fun list_of_param_types sg tl pl (_ $ Abs(_,t,r)) =
   952 let
   953  fun select_type [] [] t = t |
   954  select_type (a::r) (b::s) t =
   955  if (t=b) then a else (select_type r s t) |
   956  select_type _ _ _ =
   957  error "wrong number of argument of a constructor in a induct-theorem";
   958 in
   959  (select_type tl pl t) :: (list_of_param_types sg tl pl r)
   960 end |
   961 list_of_param_types sg tl pl (Const("Trueprop",_) $ r) = list_of_param_types sg tl pl r |
   962 list_of_param_types _ _ _ _ = [];
   963 fun split_constr sg tl pl a = (extract_hd sg a,list_of_param_types sg tl pl a);
   964 fun split_constrs _ _ _ [] = [] |
   965 split_constrs sg tl pl (a::r) = (split_constr sg tl pl a) :: (split_constrs sg tl pl r);
   966 fun new_types [] = [] |
   967 new_types ((t,l)::r) =
   968 let
   969  fun ex_bool [] = [] |
   970  ex_bool ((Type("bool",[]))::r) = ex_bool r |
   971  ex_bool ((Type("*",[a,b]))::r) = ex_bool (a::b::r) |
   972  ex_bool (s::r) = s:: (ex_bool r);
   973  val ll = ex_bool l
   974 in
   975  (ll @ (new_types r))
   976 end;
   977 in
   978         if (a mem done)
   979         then (preprocess_td sg b done)
   980         else
   981         (let
   982 	 fun qtn (Type(a,tl)) = (a,tl) |
   983 	 qtn _ = error "unexpected type variable in preprocess_td";
   984 	 val s =  post_last_dot(fst(qtn a));
   985 	 fun param_types ((Const("Trueprop",_)) $ (_ $ (Var(_,Type(_,t)))))  = t |
   986 	 param_types _ = error "malformed induct-theorem in preprocess_td";	
   987 	 val pl = param_types (concl_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));		
   988          val l = split_constrs sg (snd(qtn a)) pl (prems_of (get_thm (theory_of_sign sg) (s ^ ".induct", NONE)));
   989 	 val ntl = new_types l;
   990         in 
   991         ((a,l) :: (preprocess_td sg (ntl @ b) (a :: done)))
   992         end)
   993 end;
   994 
   995 fun extract_type_names_prems sg [] = [] |
   996 extract_type_names_prems sg (a::b) =
   997 let
   998 fun analyze_types sg [] = [] |
   999 analyze_types sg [Type(a,[])] =
  1000 (let
  1001  val s = (Sign.string_of_typ sg (Type(a,[])))
  1002 in
  1003  (if (s="bool") then ([]) else ([Type(a,[])]))
  1004 end) |
  1005 analyze_types sg [Type("*",l)] = analyze_types sg l |
  1006 analyze_types sg [Type("fun",l)] = analyze_types sg l |
  1007 analyze_types sg [Type(t,l)] = ((Type(t,l))::(analyze_types sg l)) |
  1008 analyze_types sg (a::l) = (analyze_types sg [a]) @ (analyze_types sg l);
  1009 fun extract_type_names sg (Const("==",_)) = [] |
  1010 extract_type_names sg (Const("Trueprop",_)) = [] |
  1011 extract_type_names sg (Const(_,typ)) = analyze_types sg [typ] |
  1012 extract_type_names sg (a $ b) = (extract_type_names sg a) @ (extract_type_names sg b) |
  1013 extract_type_names sg (Abs(x,T,t)) = (analyze_types sg [T]) @ (extract_type_names sg t) |
  1014 extract_type_names _ _ = [];
  1015 in
  1016  (extract_type_names sg a) @ extract_type_names_prems sg b
  1017 end;
  1018 
  1019 (**********************************************************)
  1020 (* mk_mc_oracle:  new argument of MuckeOracleExn: source_thy *)
  1021 
  1022 fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) = 
  1023   let 	val Freesubgoal = freeze_thaw subgoal;
  1024 
  1025 	val prems = Logic.strip_imp_prems Freesubgoal; 
  1026 	val concl = Logic.strip_imp_concl Freesubgoal; 
  1027 	
  1028 	val Muckedecls = terms_to_decls sign prems;
  1029 	val decls_str = string_of_terms sign Muckedecls;
  1030 	
  1031 	val type_list = (extract_type_names_prems sign (prems@[concl]));
  1032 	val ctl =  preprocess_td sign type_list [];
  1033 	val b = if (ctl=[]) then true else (check_finity [Type("bool",[])] [] ctl false);
  1034 	val type_str = make_type_decls ctl 
  1035 				((Type("bool",[]),("True",[])::("False",[])::[])::ctl);
  1036 	
  1037 	val mprems = rewrite_dt_terms sign ctl prems;
  1038 	val mconcl = rewrite_dt_terms sign ctl [concl];
  1039 
  1040 	val Muckeprems = transform_terms sign mprems;
  1041         val prems_str = transform_case(string_of_terms sign Muckeprems);
  1042 
  1043         val Muckeconcl = elim_quant_in_list sign mconcl;
  1044 	val concl_str = transform_case(string_of_terms sign Muckeconcl);
  1045 
  1046 	val MCstr = (
  1047 		"/**** type declarations: ****/\n" ^ type_str ^
  1048 		"/**** declarations: ****/\n" ^ decls_str ^
  1049 		"/**** definitions: ****/\n" ^ prems_str ^ 
  1050 		"/**** formula: ****/\n" ^ concl_str ^";");
  1051 	val result = callmc MCstr;
  1052   in
  1053 (if !trace_mc then 
  1054 	(writeln ("\nmodelchecker input:\n" ^ MCstr ^ "\n/**** end ****/"))
  1055           else ();
  1056 (case (extract_result concl_str result) of 
  1057 	true  =>  (Logic.strip_imp_concl subgoal) | 
  1058 	false => (error ("Mucke couldn't solve subgoal: \n" ^result)))) 
  1059   end;