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