src/HOLCF/IOA/Modelcheck/MuIOA.thy
changeset 32960 69916a850301
parent 32178 0261c3eaae41
child 37140 6ba1b0ef0cc4
     1.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,6 +1,3 @@
     1.4 -
     1.5 -(* $Id$ *)
     1.6 -
     1.7  theory MuIOA
     1.8  imports IOA "../../../HOL/Modelcheck/MuckeSyn"
     1.9  begin
    1.10 @@ -20,8 +17,8 @@
    1.11  ML {*
    1.12  
    1.13  (* MuIOA.ML declares function mk_sim_oracle used by oracle "Sim" (see MuIOAOracle.thy).
    1.14 -	There, implementation relations for I/O automatons are proved using
    1.15 -	the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
    1.16 +        There, implementation relations for I/O automatons are proved using
    1.17 +        the model checker mucke (invoking cal_mucke_tac defined in MCSyn.ML). *)
    1.18  
    1.19  exception SimFailureExn of string;
    1.20  
    1.21 @@ -161,13 +158,13 @@
    1.22  
    1.23  fun double_tupel_of _ _ _ _ [] = "" |
    1.24  double_tupel_of sign s t n [a] = s ^ (Int.toString(n)) ^ "," ^
    1.25 -				 t ^ (Int.toString(n)) |
    1.26 +                                 t ^ (Int.toString(n)) |
    1.27  double_tupel_of sign s t n (a::r) = s ^ (Int.toString(n)) ^ "," ^
    1.28 -		t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
    1.29 +                t ^ (Int.toString(n)) ^ "," ^ (double_tupel_of sign s t (n+1) r);
    1.30  
    1.31  fun eq_string _ _ _ [] = "" |
    1.32  eq_string s t n [a] = s ^ (Int.toString(n)) ^ " = " ^
    1.33 -			 t ^ (Int.toString(n)) |
    1.34 +                         t ^ (Int.toString(n)) |
    1.35  eq_string s t n (a::r) =
    1.36   s ^ (Int.toString(n)) ^ " = " ^
    1.37   t ^ (Int.toString(n)) ^ " & " ^ (eq_string s t (n+1) r);
    1.38 @@ -188,60 +185,60 @@
    1.39      val concl = Logic.strip_imp_concl subgoal;
    1.40      val ic_str = delete_ul_string(Syntax.string_of_term_global sign (IntC sign concl));
    1.41      val ia_str = delete_ul_string(Syntax.string_of_term_global sign (IntA sign concl));
    1.42 -	val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));	
    1.43 -	val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));
    1.44 -	val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl));
    1.45 -	val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl));
    1.46 -	
    1.47 -	val action_type_str =
    1.48 -	Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
    1.49 +        val sc_str = delete_ul_string(Syntax.string_of_term_global sign (StartC sign concl));   
    1.50 +        val sa_str = delete_ul_string(Syntax.string_of_term_global sign (StartA sign concl));
    1.51 +        val tc_str = delete_ul_string(Syntax.string_of_term_global sign (TransC sign concl));
    1.52 +        val ta_str = delete_ul_string(Syntax.string_of_term_global sign (TransA sign concl));
    1.53 +        
    1.54 +        val action_type_str =
    1.55 +        Syntax.string_of_typ_global sign (element_type(#T (rep_cterm(cterm_of sign (IntA sign concl)))));
    1.56  
    1.57 -	val abs_state_type_list =
    1.58 -	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
    1.59 -	val con_state_type_list =
    1.60 -	type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
    1.61 +        val abs_state_type_list =
    1.62 +        type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartA sign concl)))));
    1.63 +        val con_state_type_list =
    1.64 +        type_list_of sign (element_type(#T (rep_cterm(cterm_of sign (StartC sign concl)))));
    1.65  
    1.66 -	val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
    1.67 +        val tupel_eq = eq_string "s" "t" 0 abs_state_type_list;
    1.68  
    1.69 -	val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
    1.70 -	val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
    1.71 -	val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
    1.72 -	val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
    1.73 -	
    1.74 -	val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
    1.75 -	val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
    1.76 -	val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
    1.77 -	val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
    1.78 -	val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
    1.79 -	val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
    1.80 -	val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
    1.81 -	val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
    1.82 +        val abs_pre_tupel_typed = tupel_typed_of sign "s" 0 abs_state_type_list;
    1.83 +        val abs_s_t_tupel_typed = double_tupel_typed_of sign "s" "t" 0 abs_state_type_list;
    1.84 +        val con_pre_tupel_typed = tupel_typed_of sign "cs" 0 con_state_type_list;
    1.85 +        val con_s_t_tupel_typed = double_tupel_typed_of sign "cs" "ct" 0 con_state_type_list;
    1.86 +        
    1.87 +        val abs_pre_tupel = tupel_of sign "s" 0 abs_state_type_list;
    1.88 +        val abs_post_tupel = tupel_of sign "t" 0 abs_state_type_list;
    1.89 +        val abs_s_t_tupel = double_tupel_of sign "s" "t" 0 abs_state_type_list;
    1.90 +        val abs_s_u_tupel = double_tupel_of sign "s" "u" 0 abs_state_type_list;
    1.91 +        val abs_u_t_tupel = double_tupel_of sign "u" "t" 0 abs_state_type_list;
    1.92 +        val abs_u_v_tupel = double_tupel_of sign "u" "v" 0 abs_state_type_list;
    1.93 +        val abs_v_t_tupel = double_tupel_of sign "v" "t" 0 abs_state_type_list;
    1.94 +        val con_pre_tupel = tupel_of sign "cs" 0 con_state_type_list;
    1.95          val con_post_tupel = tupel_of sign "ct" 0 con_state_type_list;
    1.96 -	val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
    1.97 +        val con_s_t_tupel = double_tupel_of sign "cs" "ct" 0 con_state_type_list;
    1.98  
    1.99          val abs_pre_varlist = varlist_of 0 "s" abs_state_type_list;
   1.100          val abs_post_varlist = varlist_of 0 "t" abs_state_type_list;
   1.101          val abs_u_varlist = varlist_of 0 "u" abs_state_type_list;
   1.102          val abs_v_varlist = varlist_of 0 "v" abs_state_type_list;
   1.103 -	val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
   1.104 +        val con_pre_varlist = varlist_of 0 "cs" con_state_type_list;
   1.105          val con_post_varlist = varlist_of 0 "ct" con_state_type_list;
   1.106  
   1.107          val abs_post_str = string_of abs_post_varlist;
   1.108 -	val abs_u_str = string_of abs_u_varlist;
   1.109 -	val con_post_str = string_of con_post_varlist;
   1.110 -	
   1.111 -	val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
   1.112 -	val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
   1.113 +        val abs_u_str = string_of abs_u_varlist;
   1.114 +        val con_post_str = string_of con_post_varlist;
   1.115 +        
   1.116 +        val abs_pre_str_typed = merge_var_and_type abs_pre_varlist abs_state_type_list;
   1.117 +        val abs_u_str_typed = merge_var_and_type abs_u_varlist abs_state_type_list;
   1.118          val abs_v_str_typed = merge_var_and_type abs_v_varlist abs_state_type_list;
   1.119 -	val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
   1.120 +        val con_pre_str_typed = merge_var_and_type con_pre_varlist con_state_type_list;
   1.121  
   1.122 -	val abs_pre_tupel_struct = snd(
   1.123 +        val abs_pre_tupel_struct = snd(
   1.124  structured_tuple abs_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   1.125 -	val abs_post_tupel_struct = snd(
   1.126 +        val abs_post_tupel_struct = snd(
   1.127  structured_tuple abs_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartA sign concl))))));
   1.128 -	val con_pre_tupel_struct = snd(
   1.129 +        val con_pre_tupel_struct = snd(
   1.130  structured_tuple con_pre_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   1.131 -	val con_post_tupel_struct = snd(
   1.132 +        val con_post_tupel_struct = snd(
   1.133  structured_tuple con_post_varlist (element_type(#T(rep_cterm(cterm_of sign (StartC sign concl))))));
   1.134  in
   1.135  (
   1.136 @@ -250,37 +247,37 @@
   1.137  ( "(Internal_of_A = (% a::(" ^ action_type_str ^ "). a:(" ^ ia_str^
   1.138    "))) --> (Internal_of_C = (% a::(" ^ action_type_str ^ "). a:(" ^ ic_str ^ 
   1.139    "))) --> (Start_of_A = (% (" ^ abs_pre_tupel_typed ^
   1.140 -	"). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
   1.141 +        "). (" ^ abs_pre_tupel_struct ^ "):(" ^ sa_str ^
   1.142    "))) --> (Start_of_C = (% (" ^ con_pre_tupel_typed ^
   1.143 -	"). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
   1.144 +        "). (" ^ con_pre_tupel_struct ^ "):(" ^ sc_str ^
   1.145    "))) --> (Trans_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   1.146 -	")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
   1.147 +        ")). ((" ^ abs_pre_tupel_struct ^ "),a,(" ^ abs_post_tupel_struct ^ ")):(" ^ ta_str ^
   1.148    "))) --> (Trans_of_C = (% (" ^ con_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   1.149 -	")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
   1.150 +        ")). ((" ^ con_pre_tupel_struct ^ "),a,(" ^ con_post_tupel_struct ^ ")):(" ^ tc_str ^
   1.151    "))) --> (IntStep_of_A = (% (" ^ abs_s_t_tupel_typed ^ 
   1.152 -	"). ? (a::(" ^ action_type_str ^
   1.153 -	")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
   1.154 +        "). ? (a::(" ^ action_type_str ^
   1.155 +        ")). Internal_of_A a & Trans_of_A (" ^ abs_s_t_tupel ^ ") a" ^
   1.156    ")) --> (IntStepStar_of_A =  mu (% P (" ^ abs_s_t_tupel_typed ^
   1.157 -	 "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
   1.158 -	 ") & P(" ^ abs_u_t_tupel ^ ")))" ^
   1.159 +         "). (" ^ tupel_eq ^ ") | (? " ^ abs_u_str ^ ". IntStep_of_A (" ^ abs_s_u_tupel ^
   1.160 +         ") & P(" ^ abs_u_t_tupel ^ ")))" ^
   1.161    ") --> (Move_of_A = (% (" ^ abs_s_t_tupel_typed ^ ") (a::(" ^ action_type_str ^ 
   1.162 -	")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
   1.163 -	")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
   1.164 -	". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
   1.165 -	"Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
   1.166 +        ")). (Internal_of_C a & IntStepStar_of_A(" ^ abs_s_t_tupel ^ 
   1.167 +        ")) | (? " ^ abs_u_str_typed ^ ". ? " ^ abs_v_str_typed ^
   1.168 +        ". IntStepStar_of_A(" ^ abs_s_u_tupel ^ ") & " ^
   1.169 +        "Trans_of_A (" ^ abs_u_v_tupel ^ ") a  & IntStepStar_of_A(" ^ abs_v_t_tupel ^ "))" ^
   1.170    ")) --> (isSimCA = nu (% P (" ^ con_pre_tupel_typed ^ "," ^ abs_pre_tupel_typed ^ 
   1.171 -	"). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
   1.172 -	". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
   1.173 +        "). (! (a::(" ^ action_type_str ^ ")) " ^ con_post_str ^
   1.174 +        ". Trans_of_C (" ^ con_s_t_tupel ^ ") a  -->" ^ " (? " ^ abs_post_str ^
   1.175    ". Move_of_A (" ^ abs_s_t_tupel ^ ") a  & P(" ^ con_post_tupel ^ "," ^ abs_post_tupel ^ "))))" ^
   1.176   ") --> (! " ^ con_pre_str_typed ^ ". ! " ^ abs_pre_str_typed ^
   1.177 -	". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
   1.178 -	")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
   1.179 +        ". (Start_of_C (" ^ con_pre_tupel ^ ") & Start_of_A (" ^ abs_pre_tupel ^
   1.180 +        ")) --> isSimCA(" ^ con_pre_tupel ^ "," ^ abs_pre_tupel ^ "))");
   1.181  OldGoals.by (REPEAT (rtac impI 1));
   1.182  OldGoals.by (REPEAT (dtac eq_reflection 1));
   1.183  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
   1.184  OldGoals.by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
   1.185                                delsimps [not_iff,split_part])
   1.186 -			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   1.187 +                              addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   1.188                                          rename_simps @ ioa_simps @ asig_simps)) 1);
   1.189  OldGoals.by (full_simp_tac
   1.190    (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);