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