src/HOLCF/IOA/Modelcheck/MuIOA.thy
author haftmann
Wed May 26 16:44:57 2010 +0200 (2010-05-26)
changeset 37140 6ba1b0ef0cc4
parent 32960 69916a850301
child 37391 476270a6c2dc
permissions -rw-r--r--
dropped legacy theorem bindings
wenzelm@17244
     1
theory MuIOA
wenzelm@28614
     2
imports IOA "../../../HOL/Modelcheck/MuckeSyn"
wenzelm@17244
     3
begin
mueller@6471
     4
mueller@6471
     5
consts
wenzelm@17244
     6
  Internal_of_A :: "'a => bool"
wenzelm@17244
     7
  Internal_of_C :: "'a => bool"
wenzelm@17244
     8
  Start_of_A :: "'a => bool"
wenzelm@17244
     9
  Start_of_C :: "'a => bool"
wenzelm@17244
    10
  Trans_of_A :: "'a => 'b => bool"
wenzelm@17244
    11
  Trans_of_C :: "'a => 'b => bool"
wenzelm@17244
    12
  IntStep_of_A :: "'a => bool"
wenzelm@17244
    13
  IntStepStar_of_A :: "'a => bool"
wenzelm@17244
    14
  Move_of_A :: "'a => 'b => bool"
wenzelm@17244
    15
  isSimCA :: "'a => bool"
mueller@6471
    16
wenzelm@22819
    17
ML {*
wenzelm@22819
    18
wenzelm@22819
    19
(* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
wenzelm@32960
    20
        There, implementation relations for I/O automatons are proved using
wenzelm@32960
    21
        the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
wenzelm@22819
    22
wenzelm@22819
    23
exception SimFailureExn of string;
wenzelm@22819
    24
wenzelm@22819
    25
val ioa_simps = [thm "asig_of_def", thm "starts_of_def", thm "trans_of_def"];
wenzelm@22819
    26
val asig_simps = [thm "asig_inputs_def", thm "asig_outputs_def",
wenzelm@22819
    27
  thm "asig_internals_def", thm "actions_def"];
wenzelm@22819
    28
val comp_simps = [thm "par_def", thm "asig_comp_def"];
wenzelm@22819
    29
val restrict_simps = [thm "restrict_def", thm "restrict_asig_def"];
wenzelm@22819
    30
val hide_simps = [thm "hide_def", thm "hide_asig_def"];
wenzelm@22819
    31
val rename_simps = [thm "rename_def", thm "rename_set_def"];
wenzelm@22819
    32
wenzelm@22819
    33
local
wenzelm@22819
    34
wenzelm@22819
    35
exception malformed;
wenzelm@22819
    36
wenzelm@22819
    37
fun fst_type (Type("*",[a,_])) = a |
wenzelm@22819
    38
fst_type _ = raise malformed; 
wenzelm@22819
    39
fun snd_type (Type("*",[_,a])) = a |
wenzelm@22819
    40
snd_type _ = raise malformed;
wenzelm@22819
    41
wenzelm@22819
    42
fun element_type (Type("set",[a])) = a |
wenzelm@22819
    43
element_type t = raise malformed;
wenzelm@22819
    44
wenzelm@22819
    45
fun IntC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
wenzelm@22819
    46
let
wenzelm@22819
    47
val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
wenzelm@22819
    48
val sig_typ = fst_type aut_typ;
wenzelm@22819
    49
val int_typ = fst_type sig_typ
wenzelm@22819
    50
in 
wenzelm@22819
    51
Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
wenzelm@22819
    52
 (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ concreteIOA)
mueller@6471
    53
end
wenzelm@22819
    54
|
wenzelm@22819
    55
IntC sg t =
wenzelm@26939
    56
error("malformed automaton def for IntC:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
    57
wenzelm@22819
    58
fun StartC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) =
wenzelm@22819
    59
let
wenzelm@22819
    60
val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
wenzelm@22819
    61
val st_typ = fst_type(snd_type aut_typ)
wenzelm@22819
    62
in
wenzelm@22819
    63
Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ concreteIOA
wenzelm@22819
    64
end
wenzelm@22819
    65
|
wenzelm@22819
    66
StartC sg t =
wenzelm@26939
    67
error("malformed automaton def for StartC:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
    68
wenzelm@22819
    69
fun TransC sg (Const("Trueprop",_) $ ((Const("op <=",_) $ (_ $ concreteIOA)) $ _)) = 
wenzelm@22819
    70
let
wenzelm@22819
    71
val aut_typ = #T(rep_cterm(cterm_of sg concreteIOA));
wenzelm@22819
    72
val tr_typ = fst_type(snd_type(snd_type aut_typ))
wenzelm@22819
    73
in
wenzelm@22819
    74
Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ concreteIOA
wenzelm@22819
    75
end
wenzelm@22819
    76
|
wenzelm@22819
    77
TransC sg t =
wenzelm@26939
    78
error("malformed automaton def for TransC:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
    79
wenzelm@22819
    80
fun IntA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
wenzelm@22819
    81
let
wenzelm@22819
    82
val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
wenzelm@22819
    83
val sig_typ = fst_type aut_typ;
wenzelm@22819
    84
val int_typ = fst_type sig_typ
wenzelm@22819
    85
in
wenzelm@22819
    86
Const("Asig.internals",Type("fun",[sig_typ,int_typ])) $
wenzelm@22819
    87
 (Const("Automata.asig_of",Type("fun",[aut_typ,sig_typ])) $ abstractIOA)
wenzelm@22819
    88
end
wenzelm@22819
    89
|
wenzelm@22819
    90
IntA sg t =
wenzelm@26939
    91
error("malformed automaton def for IntA:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
    92
wenzelm@22819
    93
fun StartA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
wenzelm@22819
    94
let
wenzelm@22819
    95
val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
wenzelm@22819
    96
val st_typ = fst_type(snd_type aut_typ)
wenzelm@22819
    97
in
wenzelm@22819
    98
Const("Automata.starts_of",Type("fun",[aut_typ,st_typ])) $ abstractIOA
wenzelm@22819
    99
end
wenzelm@22819
   100
|
wenzelm@22819
   101
StartA sg t =
wenzelm@26939
   102
error("malformed automaton def for StartA:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
   103
wenzelm@22819
   104
fun TransA sg (Const("Trueprop",_) $ ((Const("op <=",_) $ _) $ (_ $ abstractIOA))) =
wenzelm@22819
   105
let
wenzelm@22819
   106
val aut_typ = #T(rep_cterm(cterm_of sg abstractIOA));
wenzelm@22819
   107
val tr_typ = fst_type(snd_type(snd_type aut_typ))
wenzelm@22819
   108
in
wenzelm@22819
   109
Const("Automata.trans_of",Type("fun",[aut_typ,tr_typ])) $ abstractIOA 
wenzelm@22819
   110
end
wenzelm@22819
   111
|
wenzelm@22819
   112
TransA sg t =
wenzelm@26939
   113
error("malformed automaton def for TransA:\n" ^ (Syntax.string_of_term_global sg t));
wenzelm@22819
   114
wenzelm@22819
   115
fun delete_ul [] = []
wenzelm@22819
   116
| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
wenzelm@22819
   117
        then (let val (_::_::_::s) = xs in delete_ul s end)
wenzelm@22819
   118
        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
wenzelm@22819
   119
                then  (let val (_::_::_::s) = xs in delete_ul s end)
wenzelm@22819
   120
                else (x::delete_ul xs));
wenzelm@22819
   121
wenzelm@22819
   122
fun delete_ul_string s = implode(delete_ul (explode s));
wenzelm@22819
   123
wenzelm@22819
   124
fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
wenzelm@26939
   125
type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
wenzelm@22819
   126
wenzelm@22819
   127
fun structured_tuple l (Type("*",s::t::_)) =
wenzelm@22819
   128
let
wenzelm@22819
   129
val (r,str) = structured_tuple l s;
wenzelm@22819
   130
in
wenzelm@22819
   131
(fst(structured_tuple r t),"(" ^ str ^ "),(" ^ (snd(structured_tuple r t)) ^ ")")
wenzelm@22819
   132
end |
wenzelm@22819
   133
structured_tuple (a::r) t = (r,a) |
wenzelm@22819
   134
structured_tuple [] _ = raise malformed;
wenzelm@22819
   135
wenzelm@22819
   136
fun varlist_of _ _ [] = [] |
wenzelm@22819
   137
varlist_of n s (a::r) = (s ^ (Int.toString(n))) :: (varlist_of (n+1) s r);
wenzelm@22819
   138
wenzelm@22819
   139
fun string_of [] = "" |
wenzelm@22819
   140
string_of (a::r) = a ^ " " ^ (string_of r);
wenzelm@22819
   141
wenzelm@22819
   142
fun tupel_typed_of _ _ _ [] = "" |
wenzelm@22819
   143
tupel_typed_of sign s n [a] = s ^ (Int.toString(n)) ^ "::" ^ a |
wenzelm@22819
   144
tupel_typed_of sign s n (a::r) =
wenzelm@22819
   145
 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (tupel_typed_of sign s (n+1) r);
wenzelm@22819
   146
wenzelm@22819
   147
fun double_tupel_typed_of _ _ _ _ [] = "" |
wenzelm@22819
   148
double_tupel_typed_of sign s t n [a] =
wenzelm@22819
   149
 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
wenzelm@22819
   150
 t ^ (Int.toString(n)) ^ "::" ^ a |
wenzelm@22819
   151
double_tupel_typed_of sign s t n (a::r) =
wenzelm@22819
   152
 s ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^
wenzelm@22819
   153
 t ^ (Int.toString(n)) ^ "::" ^ a ^ "," ^ (double_tupel_typed_of sign s t (n+1) r);
wenzelm@22819
   154
wenzelm@22819
   155
fun tupel_of _ _ _ [] = "" |
wenzelm@22819
   156
tupel_of sign s n [a] = s ^ (Int.toString(n)) |
wenzelm@22819
   157
tupel_of sign s n (a::r) = s ^ (Int.toString(n)) ^ "," ^ (tupel_of sign s (n+1) r);
wenzelm@22819
   158
wenzelm@22819
   159
fun double_tupel_of _ _ _ _ [] = "" |
wenzelm@22819
   160
double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
wenzelm@32960
   161
                                 t ^ (Int.toString(n)) |
wenzelm@22819
   162
double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
wenzelm@32960
   163
                t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
wenzelm@22819
   164
wenzelm@22819
   165
fun eq_string _ _ _ [] = "" |
wenzelm@22819
   166
eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
wenzelm@32960
   167
                         t ^ (Int.toString(n)) |
wenzelm@22819
   168
eq_string s t n (a::r) =
wenzelm@22819
   169
 s ^ (Int.toString(n)) ^ " = " ^
wenzelm@22819
   170
 t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
wenzelm@22819
   171
wenzelm@22819
   172
fun merge_var_and_type [] [] = "" |
wenzelm@22819
   173
merge_var_and_type (a::r) (b::s) = "(" ^ a ^ " ::" ^ b ^ ") " ^ (merge_var_and_type r s) |
wenzelm@22819
   174
merge_var_and_type _ _ = raise malformed;
wenzelm@22819
   175
wenzelm@22819
   176
in
wenzelm@22819
   177
wenzelm@28290
   178
fun mk_sim_oracle (csubgoal, thl) =
wenzelm@22819
   179
  let
wenzelm@28290
   180
    val sign = Thm.theory_of_cterm csubgoal;
wenzelm@28290
   181
    val subgoal = Thm.term_of csubgoal;
wenzelm@28290
   182
  in
wenzelm@28290
   183
 (let
haftmann@31787
   184
    val weak_case_congs = (map (#weak_case_cong o snd) o Symtab.dest o Datatype.get_all) sign;
wenzelm@22819
   185
    val concl = Logic.strip_imp_concl subgoal;
wenzelm@26939
   186
    val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
wenzelm@26939
   187
    val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));
wenzelm@32960
   188
        val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));   
wenzelm@32960
   189
        val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));
wenzelm@32960
   190
        val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl));
wenzelm@32960
   191
        val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl));
wenzelm@32960
   192
        
wenzelm@32960
   193
        val action_type_str =
wenzelm@32960
   194
        Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
wenzelm@22819
   195
wenzelm@32960
   196
        val abs_state_type_list =
wenzelm@32960
   197
        type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
wenzelm@32960
   198
        val con_state_type_list =
wenzelm@32960
   199
        type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
wenzelm@22819
   200
wenzelm@32960
   201
        val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
wenzelm@22819
   202
wenzelm@32960
   203
        val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
wenzelm@32960
   204
        val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
wenzelm@32960
   205
        val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
wenzelm@32960
   206
        val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
wenzelm@32960
   207
        
wenzelm@32960
   208
        val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
wenzelm@32960
   209
        val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
wenzelm@32960
   210
        val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
wenzelm@32960
   211
        val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
wenzelm@32960
   212
        val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
wenzelm@32960
   213
        val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
wenzelm@32960
   214
        val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
wenzelm@32960
   215
        val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
wenzelm@22819
   216
        val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
wenzelm@32960
   217
        val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
wenzelm@22819
   218
wenzelm@22819
   219
        val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
wenzelm@22819
   220
        val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
wenzelm@22819
   221
        val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
wenzelm@22819
   222
        val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
wenzelm@32960
   223
        val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
wenzelm@22819
   224
        val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
wenzelm@22819
   225
wenzelm@22819
   226
        val abs_post_str = string_of abs_post_varlist;
wenzelm@32960
   227
        val abs_u_str = string_of abs_u_varlist;
wenzelm@32960
   228
        val con_post_str = string_of con_post_varlist;
wenzelm@32960
   229
        
wenzelm@32960
   230
        val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
wenzelm@32960
   231
        val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
wenzelm@22819
   232
        val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
wenzelm@32960
   233
        val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
wenzelm@22819
   234
wenzelm@32960
   235
        val abs_pre_tupel_struct = snd(
wenzelm@22819
   236
structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
wenzelm@32960
   237
        val abs_post_tupel_struct = snd(
wenzelm@22819
   238
structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
wenzelm@32960
   239
        val con_pre_tupel_struct = snd(
wenzelm@22819
   240
structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
wenzelm@32960
   241
        val con_post_tupel_struct = snd(
wenzelm@22819
   242
structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
wenzelm@22819
   243
in
wenzelm@22819
   244
(
wenzelm@22819
   245
OldGoals.push_proof();
wenzelm@32178
   246
OldGoals.Goal 
wenzelm@22819
   247
( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
wenzelm@22819
   248
  "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
wenzelm@22819
   249
  "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
wenzelm@32960
   250
        "). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
wenzelm@22819
   251
  "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
wenzelm@32960
   252
        "). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
wenzelm@22819
   253
  "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
wenzelm@32960
   254
        ")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
wenzelm@22819
   255
  "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
wenzelm@32960
   256
        ")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
wenzelm@22819
   257
  "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
wenzelm@32960
   258
        "). ? (a::(" ^ action_type_str ^
wenzelm@32960
   259
        ")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
wenzelm@22819
   260
  ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
wenzelm@32960
   261
         "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
wenzelm@32960
   262
         ") & P(" ^ abs_u_t_tupel ^ ")))" ^
wenzelm@22819
   263
  ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
wenzelm@32960
   264
        ")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
wenzelm@32960
   265
        ")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
wenzelm@32960
   266
        ". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
wenzelm@32960
   267
        "Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
wenzelm@22819
   268
  ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
wenzelm@32960
   269
        "). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
wenzelm@32960
   270
        ". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
wenzelm@22819
   271
  ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
wenzelm@22819
   272
 ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
wenzelm@32960
   273
        ". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
wenzelm@32960
   274
        ")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
wenzelm@32178
   275
OldGoals.by (REPEAT (rtac impI 1));
wenzelm@32178
   276
OldGoals.by (REPEAT (dtac eq_reflection 1));
wenzelm@22819
   277
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
wenzelm@32178
   278
OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
haftmann@37140
   279
                              delsimps [not_iff, @{thm split_part}])
wenzelm@32960
   280
                              addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
wenzelm@22819
   281
                                        rename_simps @ ioa_simps @ asig_simps)) 1);
wenzelm@32178
   282
OldGoals.by (full_simp_tac
haftmann@37140
   283
  (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1);
wenzelm@32178
   284
OldGoals.by (REPEAT (if_full_simp_tac
haftmann@37140
   285
  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff, @{thm split_part}]) 1));
wenzelm@32178
   286
OldGoals.by (call_mucke_tac 1);
wenzelm@22819
   287
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
wenzelm@32178
   288
OldGoals.by (atac 1);
wenzelm@32178
   289
OldGoals.result();
wenzelm@22819
   290
OldGoals.pop_proof();
wenzelm@28290
   291
Thm.cterm_of sign (Logic.strip_imp_concl subgoal)
wenzelm@22819
   292
)
wenzelm@22819
   293
end)
wenzelm@22819
   294
handle malformed =>
wenzelm@28290
   295
error("No suitable match to IOA types in " ^ (Syntax.string_of_term_global sign subgoal))
wenzelm@28290
   296
end;
wenzelm@22819
   297
wenzelm@22819
   298
end
wenzelm@22819
   299
wenzelm@22819
   300
*}
wenzelm@22819
   301
wenzelm@22819
   302
end