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