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