--- a/src/HOL/IOA/ABP/Check.ML Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Check.ML Wed May 31 10:45:00 1995 +0200
@@ -1,14 +1,9 @@
-(* Title: HOL/IOA/ABP/Check.ML
- ID: $Id$
- Author: Tobias Nipkow & Olaf Mueller
- Copyright 1995 TU Muenchen
-
-Simple ModelChecker prototype checking Spec against
-the finite version of the ABP-protocol.
-*)
-(* model checker function prototype *)
+
+(* ----------------------------------------------------------------
+ P r o t o t y p e M o d e l C h e c k e r
+ ----------------------------------------------------------------*)
fun check(extacts,intacts,string_of_a,startsI,string_of_s,
nexts,hom,transA,startsS) =
@@ -16,16 +11,16 @@
let fun check_sa(unchecked,a) =
let fun check_sas(unchecked,t) =
(if a mem extacts then
- (if transA(hom s,a,hom t) then ()
+ (if transA(hom s,a,hom t) then ( )
else (writeln("Error: Mapping of Externals!");
string_of_s s; writeln"";
string_of_a a; writeln"";
- string_of_s t;writeln"";writeln""))
- else (if hom(s)=hom(t) then ()
+ string_of_s t;writeln"";writeln"" ))
+ else (if hom(s)=hom(t) then ( )
else (writeln("Error: Mapping of Internals!");
- string_of_s s;writeln"";
- string_of_a a;writeln"";
- string_of_s t;writeln"";writeln""));
+ string_of_s s; writeln"";
+ string_of_a a; writeln"";
+ string_of_s t;writeln"";writeln"" ));
if t mem checked then unchecked else t ins unchecked)
in foldl check_sas (unchecked,nexts s a) end;
val unchecked' = foldl check_sa (unchecked,extacts @ intacts)
@@ -39,41 +34,51 @@
in checks(startsI,[]) end;
-(* datatypes for ABP example *)
+(* ------------------------------------------------------
+ A B P E x a m p l e
+ -------------------------------------------------------*)
-datatype msg = m;
+datatype msg = m | n | l;
datatype act = Next | S_msg of msg | R_msg of msg
| S_pkt of bool * msg | R_pkt of bool * msg
| S_ack of bool | R_ack of bool;
+(* -------------------- Transition relation of Specification -----------*)
+
fun transA((u,s),a,(v,t)) =
(case a of
Next => v andalso t = s |
- S_msg(m) => u andalso not(v) andalso t = s@[m] |
- R_msg(m) => u = v andalso s = (m::t) |
- S_pkt(b,m) => false |
- R_pkt(b,m) => false |
+ S_msg(q) => u andalso not(v) andalso t = s@[q] |
+ R_msg(q) => u = v andalso s = (q::t) |
+ S_pkt(b,q) => false |
+ R_pkt(b,q) => false |
S_ack(b) => false |
R_ack(b) => false);
+
+(* ---------------------- Abstraction function --------------------------*)
+
fun hom((env,p,a,q,b,_,_)) = (env,q@(if (a=b) then tl(p) else p));
+
+(* --------------------- Transition relation of Implementation ----------*)
+
fun nexts (s as (env,p,a,q,b,ch1,ch2)) action =
(case action of
Next => if p=[] then [(true,p,a,q,b,ch1,ch2)] else [] |
- S_msg(m) => if env then [(false,p@[m],a,q,b,ch1,ch2)] else [] |
- R_msg(m) => if (q<>[] andalso m=hd(q))
+ S_msg(mornorl) => if env then [(false,p@[mornorl],a,q,b,ch1,ch2)] else [] |
+ R_msg(mornorl) => if (q<>[] andalso mornorl=hd(q))
then [(env,p,a,tl(q),b,ch1,ch2)]
else [] |
- S_pkt(h,m) => if (p<>[] andalso m=hd(p) andalso h=a)
- then (if (ch1<>[] andalso hd(rev(ch1))=(h,m))
+ S_pkt(h,mornorl) => if (p<>[] andalso mornorl=hd(p) andalso h=a)
+ then (if (ch1<>[] andalso hd(rev(ch1))=(h,mornorl))
then [s]
- else [s,(env,p,a,q,b,ch1@[(h,m)],ch2)])
+ else [s,(env,p,a,q,b,ch1@[(h,mornorl)],ch2)])
else [] |
- R_pkt(h,m) => if (ch1<>[] andalso hd(ch1)=(h,m))
+ R_pkt(h,mornorl) => if (ch1<>[] andalso hd(ch1)=(h,mornorl))
then (if (h<>b andalso q=[])
- then [(env,p,a,q@[m],not(b),ch1,ch2),
- (env,p,a,q@[m],not(b),tl(ch1),ch2)]
+ then [(env,p,a,q@[mornorl],not(b),ch1,ch2),
+ (env,p,a,q@[mornorl],not(b),tl(ch1),ch2)]
else [s,(env,p,a,q,b,tl(ch1),ch2)])
else [] |
S_ack(h) => if (h=b)
@@ -89,36 +94,42 @@
else [])
-val extactions = [Next,S_msg(m),R_msg(m)];
+val extactions = [Next,S_msg(m),R_msg(m),S_msg(n),R_msg(n),S_msg(l),R_msg(l)];
val intactions = [S_pkt(true,m),R_pkt(true,m),S_ack(true),R_ack(true),
- S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false)];
-
+ S_pkt(false,m),R_pkt(false,m),S_ack(false),R_ack(false),
+ S_pkt(true,n),R_pkt(true,n),S_pkt(true,l),R_pkt(true,l),
+ S_pkt(false,n),R_pkt(false,n),S_pkt(false,l),R_pkt(false,l)];
+
-(* Input / Output auxiliary functions *)
+(* ------------------------------------
+ Input / Output utilities
+ ------------------------------------*)
-fun print_list (lpar, rpar, pre: 'a -> unit) (l : 'a list) =
+fun print_list (lpar, rpar, pre: 'a -> unit) (lll : 'a list) =
let fun prec x = (prs ","; pre x)
in
- (case l of
+ (case lll of
[] => (prs lpar; prs rpar)
- | x::l => (prs lpar; pre x; seq prec l; prs rpar))
+ | x::lll => (prs lpar; pre x; seq prec lll; prs rpar))
end;
fun pr_bool true = output(std_out,"true")
| pr_bool false = output(std_out,"false");
-fun pr_msg m = output(std_out,"m");
+fun pr_msg m = output(std_out,"m")
+| pr_msg n = output(std_out,"n")
+| pr_msg l = output(std_out,"l");
fun pr_act a = output(std_out, case a of
Next => "Next"|
- S_msg(m) => "S_msg(m)" |
- R_msg(m) => "R_msg(m)" |
- S_pkt(b,m) => "S_pkt(b,m)" |
- R_pkt(b,m) => "R_pkt(b,m)" |
+ S_msg(ma) => "S_msg(ma)" |
+ R_msg(ma) => "R_msg(ma)" |
+ S_pkt(b,ma) => "S_pkt(b,ma)" |
+ R_pkt(b,ma) => "R_pkt(b,ma)" |
S_ack(b) => "S_ack(b)" |
R_ack(b) => "R_ack(b)");
-fun pr_pkt (b,m) = (prs "<"; pr_bool b;prs ", "; pr_msg m; prs ">");
+fun pr_pkt (b,ma) = (prs "<"; pr_bool b;prs ", "; pr_msg ma; prs ">");
val pr_bool_list = print_list("[","]",pr_bool);
val pr_msg_list = print_list("[","]",pr_msg);
@@ -130,11 +141,30 @@
pr_bool b; prs ", "; pr_pkt_list ch1; prs ", ";
pr_bool_list ch2; prs "}");
-(* ----------------------------*)
-(* main check function call *)
-(* ----------------------------*)
+
+(* ---------------------------------
+ Main function call
+ ---------------------------------*)
+
+(*
check(extactions,intactions,pr_act, [(true,[],true,[],false,[],[])],
pr_tuple, nexts, hom, transA, [(true,[])]);
+*)
+
+
+
+(*
+ Little test example
+
+datatype act = A;
+fun transA(s,a,t) = (not(s)=t);
+fun hom(i) = i mod 2 = 0;
+fun nexts s A = [(s+1) mod 4];
+check([A],[],K"A", [0], string_of_int, nexts, hom, transA, [true]);
+
+fun nexts s A = [(s+1) mod 5];
+
+*)
\ No newline at end of file
--- a/src/HOL/IOA/ABP/Correctness.ML Tue May 30 11:57:27 1995 +0200
+++ b/src/HOL/IOA/ABP/Correctness.ML Wed May 31 10:45:00 1995 +0200
@@ -1,11 +1,12 @@
- (* Title: HOL/IOA/ABP/Correctness.ML
+ (* Title: HOL/IOA/example/Correctness.ML
ID: $Id$
- Author: Tobias Nipkow & Olaf Mueller
- Copyright 1995 TU Muenchen
+ Author: Tobias Nipkow & Konrad Slind
+ Copyright 1994 TU Muenchen
*)
open Correctness; open Abschannel; open Abschannel_finite;
+open Impl; open Impl_finite;
goal Abschannel.thy "(? x.x=P & Q(x)) = Q(P)";
by (fast_tac HOL_cs 1);
@@ -39,6 +40,8 @@
val red_ss_ch = merge_ss(abschannel_fin_ss,red_ss);
+
+
(* auxiliary function *)
fun rotate n i = EVERY(replicate n (etac revcut_rl i));
@@ -168,31 +171,34 @@
by (ALLGOALS (EVERY'[rtac impI,etac conjE,cut_inst_tac [("l","xs")] cons_not_nil,asm_full_simp_tac red_ss]));
by (REPEAT (etac exE 1));
by (REPEAT (etac exE 2));
-by (hyp_subst_tac 2);
+by (REPEAT(hyp_subst_tac 2));
by (ALLGOALS (asm_full_simp_tac red_ss));
val reduce_tl =result();
+(*******************************************************************
+ C h a n n e l A b s t r a c t i o n
+ *******************************************************************)
goal Correctness.thy
"is_weak_pmap reduce ch_ioa ch_fin_ioa";
by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1);
by (rtac conjI 1);
-(* start states *)
+(* -------------- start states ----------------- *)
by (simp_tac red_ss_ch 1);
br ballI 1;
by (asm_full_simp_tac red_ss_ch 1);
-(* main-part *)
+(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
by (act.induct_tac "a" 1);
-(* 2 cases *)
+(* ----------------- 2 cases ---------------------*)
by (ALLGOALS (simp_tac (red_ss_ch addsimps [externals_def])));
-(* fst case *)
+(* fst case --------------------------------------*)
by (rtac impI 1);
by (rtac disjI2 1);
by (rtac reduce_hd 1);
-(* snd case *)
+(* snd case --------------------------------------*)
by (rtac impI 1);
by (REPEAT (etac conjE 1));
by (etac disjE 1);
@@ -240,7 +246,7 @@
"is_weak_pmap (%id.id) receiver_ioa receiver_ioa";
by (simp_tac (red_ss addsimps [Solve.is_weak_pmap_def]) 1);
by (rtac conjI 1);
-(* start states *)
+ (* start states *)
br ballI 1;
by (simp_tac red_ss_ch 1);
(* main-part *)
@@ -355,17 +361,82 @@
by (simp_tac (red_ss_ch addsimps [externals_def]) 1);
val ext_single_ch = result();
-goal Correctness.thy "is_weak_pmap \
-\ (%p.(fst(p),(fst(snd(p)),(fst(snd(snd(p))), \
-\ (reduce(fst(snd(snd(snd(p))))),reduce(snd(snd(snd(snd(p)))))))))) \
-\ (env_ioa || impl_ioa) (env_ioa || impl_fin_ioa)";
-by (simp_tac (impl_ss addsimps [Impl.impl_def,Impl_finite.impl_fin_def]) 1);
-by(REPEAT(EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1,
- simp_tac (red_ss addsimps [env_unchanged,sender_unchanged,
- receiver_unchanged,sender_abstraction,receiver_abstraction]) 1,
- rtac conjI 1]));
-by (ALLGOALS(simp_tac (list_ss addsimps [externals_of_par,ext_single_ch,
- compat_single_ch,compat_single_fin_ch,compat_rec,compat_rec_fin,
- compat_sen,compat_sen_fin,compat_env,compat_env_fin])));
+
+
+
+
+val ext_ss = [externals_of_par,ext_single_ch];
+val compat_ss = [compat_single_ch,compat_single_fin_ch,compat_rec,
+ compat_rec_fin,compat_sen,compat_sen_fin,compat_env,compat_env_fin];
+val abstractions = [env_unchanged,sender_unchanged,
+ receiver_unchanged,sender_abstraction,receiver_abstraction];
+val impl_ss = impl_ss addsimps [impl_def,impl_fin_def,sys_IOA, sys_fin_IOA];
+val sys_ss = impl_ss addsimps [system_def, system_fin_def, abs_def];
+
+
+
+(************************************************************************
+ S o u n d n e s s o f A b s t r a c t i o n
+*************************************************************************)
+
+
+goal Correctness.thy
+ "is_weak_pmap abs system_ioa system_fin_ioa";
+
+by (simp_tac sys_ss 1);
+
+by (REPEAT (EVERY[rtac fxg_is_weak_pmap_of_product_IOA 1,
+ simp_tac (red_ss addsimps abstractions) 1,
+ rtac conjI 1]));
+
+by (ALLGOALS (simp_tac (red_ss addsimps ext_ss @ compat_ss)));
+
qed "system_refinement";
+
+
+(************************************************************************
+ I n t e r a c t i v e A b s t r a c t i o n
+*************************************************************************)
+
+goal Correctness.thy
+ "ioa_implements system_ioa system_fin_ioa";
+
+(* ------------------- Rewriting ----------------------------*)
+by (simp_tac (impl_ss addsimps [ioa_implements_def]) 1);
+by (rtac conjI 1);
+by (simp_tac (sys_ss addsimps ext_ss) 1);
+
+(* ------------------- Lemmata ------------------------------*)
+by (rtac trace_inclusion 1);
+by (rtac system_refinement 4);
+
+(* -------------------- Rewriting ---------------------------*)
+by (ALLGOALS (simp_tac impl_ss));
+by (simp_tac (sys_ss addsimps ext_ss) 1);
+
+qed"interactive_abstraction";
+
+
+
+
+
+(***********************************************************************
+ Illustrative ISABELLE Examples
+************************************************************************)
+
+(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***)
+
+goal Set.thy
+ "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)";
+
+by (best_tac (set_cs addSEs [equalityCE]) 1);
+qed "cantor1";
+
+(***** Theorem 2 *)
+val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
+by (cut_facts_tac prems 1);
+by (rtac equalityI 1);
+by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1);
+qed "inv_image_comp";
\ No newline at end of file