moved this trivial example to new ex dir;
authormueller
Thu Apr 22 11:06:35 1999 +0200 (1999-04-22)
changeset 6470f3015fd68d66
parent 6469 bafd705ee38e
child 6471 08d12ef5fc19
moved this trivial example to new ex dir;
src/HOLCF/IOA/ex/ROOT.ML
src/HOLCF/IOA/ex/TrivEx.ML
src/HOLCF/IOA/ex/TrivEx.thy
src/HOLCF/IOA/ex/TrivEx2.ML
src/HOLCF/IOA/ex/TrivEx2.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOLCF/IOA/ex/ROOT.ML	Thu Apr 22 11:06:35 1999 +0200
     1.3 @@ -0,0 +1,14 @@
     1.4 +(*  Title:      HOL/IOA/ex/ROOT.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Olaf Mueller
     1.7 +    Copyright   1997  TU Muenchen
     1.8 +
     1.9 +This is the ROOT file for the formalization of a semantic model of
    1.10 +I/O-Automata.  See the README.html file for details.
    1.11 +*)
    1.12 +
    1.13 +goals_limit := 1;
    1.14 +
    1.15 +
    1.16 +use_thy "TrivEx";
    1.17 +use_thy "TrivEx2";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOLCF/IOA/ex/TrivEx.ML	Thu Apr 22 11:06:35 1999 +0200
     2.3 @@ -0,0 +1,39 @@
     2.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Olaf Mueller
     2.7 +    Copyright   1995  TU Muenchen
     2.8 +
     2.9 +Trivial Abstraction Example
    2.10 +*)
    2.11 +
    2.12 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    2.13 +  by (fast_tac (claset() addDs prems) 1);
    2.14 +qed "imp_conj_lemma";
    2.15 +
    2.16 +
    2.17 +Goalw [is_abstraction_def] 
    2.18 +"is_abstraction h_abs C_ioa A_ioa";
    2.19 +by (rtac conjI 1);
    2.20 +(* ------------- start states ------------ *)
    2.21 +by (simp_tac (simpset() addsimps 
    2.22 +    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
    2.23 +(* -------------- step case ---------------- *)
    2.24 +by (REPEAT (rtac allI 1));
    2.25 +by (rtac imp_conj_lemma 1);
    2.26 +by (simp_tac (simpset() addsimps [trans_of_def,
    2.27 +        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    2.28 +by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    2.29 +by (induct_tac "a" 1);
    2.30 +by Auto_tac;
    2.31 +qed"h_abs_is_abstraction";
    2.32 +
    2.33 +
    2.34 +Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
    2.35 +by (rtac AbsRuleT1 1);
    2.36 +by (rtac h_abs_is_abstraction 1);
    2.37 +by (rtac MC_result 1);
    2.38 +by (abstraction_tac 1);
    2.39 +by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
    2.40 +qed"TrivEx_abstraction";
    2.41 +
    2.42 +
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOLCF/IOA/ex/TrivEx.thy	Thu Apr 22 11:06:35 1999 +0200
     3.3 @@ -0,0 +1,61 @@
     3.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
     3.5 +    ID:         $Id$
     3.6 +    Author:     Olaf Mueller
     3.7 +    Copyright   1995  TU Muenchen
     3.8 +
     3.9 +Trivial Abstraction Example
    3.10 +*)
    3.11 +
    3.12 +TrivEx = Abstraction + 
    3.13 +
    3.14 +datatype action = INC
    3.15 +
    3.16 +consts
    3.17 +
    3.18 +C_asig   ::  "action signature"
    3.19 +C_trans  :: (action, nat)transition set
    3.20 +C_ioa    :: (action, nat)ioa
    3.21 +
    3.22 +A_asig   :: "action signature"
    3.23 +A_trans  :: (action, bool)transition set
    3.24 +A_ioa    :: (action, bool)ioa
    3.25 +
    3.26 +h_abs    :: "nat => bool"
    3.27 +
    3.28 +defs
    3.29 +
    3.30 +C_asig_def
    3.31 +  "C_asig == ({},{INC},{})"
    3.32 +
    3.33 +C_trans_def "C_trans ==                                           
    3.34 + {tr. let s = fst(tr);                                               
    3.35 +          t = snd(snd(tr))                                           
    3.36 +      in case fst(snd(tr))                                           
    3.37 +      of                                                             
    3.38 +      INC       => t = Suc(s)}"
    3.39 +
    3.40 +C_ioa_def "C_ioa == 
    3.41 + (C_asig, {0}, C_trans,{},{})"
    3.42 +
    3.43 +A_asig_def
    3.44 +  "A_asig == ({},{INC},{})"
    3.45 +
    3.46 +A_trans_def "A_trans ==                                           
    3.47 + {tr. let s = fst(tr);                                               
    3.48 +          t = snd(snd(tr))                                           
    3.49 +      in case fst(snd(tr))                                           
    3.50 +      of                                                             
    3.51 +      INC       => t = True}"
    3.52 +
    3.53 +A_ioa_def "A_ioa == 
    3.54 + (A_asig, {False}, A_trans,{},{})"
    3.55 +
    3.56 +h_abs_def
    3.57 +  "h_abs n == n~=0"
    3.58 +
    3.59 +rules
    3.60 +
    3.61 +MC_result
    3.62 +  "validIOA A_ioa (<>[] <%(b,a,c). b>)"
    3.63 +
    3.64 +end
    3.65 \ No newline at end of file
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.ML	Thu Apr 22 11:06:35 1999 +0200
     4.3 @@ -0,0 +1,72 @@
     4.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Olaf Mueller
     4.7 +    Copyright   1995  TU Muenchen
     4.8 +
     4.9 +Trivial Abstraction Example
    4.10 +*)
    4.11 +
    4.12 +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    4.13 +  by (fast_tac (claset() addDs prems) 1);
    4.14 +qed "imp_conj_lemma";
    4.15 +
    4.16 +
    4.17 +Goalw [is_abstraction_def] 
    4.18 +"is_abstraction h_abs C_ioa A_ioa";
    4.19 +by (rtac conjI 1);
    4.20 +(* ------------- start states ------------ *)
    4.21 +by (simp_tac (simpset() addsimps 
    4.22 +    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
    4.23 +(* -------------- step case ---------------- *)
    4.24 +by (REPEAT (rtac allI 1));
    4.25 +by (rtac imp_conj_lemma 1);
    4.26 +by (simp_tac (simpset() addsimps [trans_of_def,
    4.27 +        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
    4.28 +by (simp_tac (simpset() addsimps [h_abs_def]) 1);
    4.29 +by (induct_tac "a" 1);
    4.30 +by Auto_tac;
    4.31 +qed"h_abs_is_abstraction";
    4.32 +
    4.33 +
    4.34 +(*
    4.35 +Goalw [xt2_def,plift,option_lift]
    4.36 +  "(xt2 (plift afun)) (s,a,t) = (afun a)";
    4.37 +(* !!!!!!!!!!!!! Occurs check !!!! *)
    4.38 +by (induct_tac "a" 1);
    4.39 +
    4.40 +*)
    4.41 +
    4.42 +Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
    4.43 +           C_trans_def,trans_of_def] 
    4.44 +"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
    4.45 +by Auto_tac;
    4.46 +qed"Enabled_implication";
    4.47 +
    4.48 +
    4.49 +Goalw [is_live_abstraction_def]
    4.50 +"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
    4.51 +by Auto_tac;
    4.52 +(* is_abstraction *)
    4.53 +by (rtac h_abs_is_abstraction 1);
    4.54 +(* temp_weakening *)
    4.55 +by (abstraction_tac 1);
    4.56 +by (etac Enabled_implication 1);
    4.57 +qed"h_abs_is_liveabstraction";
    4.58 +
    4.59 +
    4.60 +Goalw [C_live_ioa_def]
    4.61 +"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
    4.62 +by (rtac AbsRuleT2 1);
    4.63 +by (rtac h_abs_is_liveabstraction 1);
    4.64 +by (rtac MC_result 1);
    4.65 +by (abstraction_tac 1);
    4.66 +by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
    4.67 +qed"TrivEx2_abstraction";
    4.68 +
    4.69 +
    4.70 +(*
    4.71 +Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) 
    4.72 +IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
    4.73 +
    4.74 +*)
    4.75 +
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOLCF/IOA/ex/TrivEx2.thy	Thu Apr 22 11:06:35 1999 +0200
     5.3 @@ -0,0 +1,71 @@
     5.4 +(*  Title:      HOLCF/IOA/TrivEx.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Olaf Mueller
     5.7 +    Copyright   1995  TU Muenchen
     5.8 +
     5.9 +Trivial Abstraction Example with fairness
    5.10 +*)
    5.11 +
    5.12 +TrivEx2 = Abstraction + IOA +
    5.13 +
    5.14 +datatype action = INC
    5.15 +
    5.16 +consts
    5.17 +
    5.18 +C_asig   ::  "action signature"
    5.19 +C_trans  :: (action, nat)transition set
    5.20 +C_ioa    :: (action, nat)ioa
    5.21 +C_live_ioa :: (action, nat)live_ioa
    5.22 +
    5.23 +A_asig   :: "action signature"
    5.24 +A_trans  :: (action, bool)transition set
    5.25 +A_ioa    :: (action, bool)ioa
    5.26 +A_live_ioa :: (action, bool)live_ioa
    5.27 +
    5.28 +h_abs    :: "nat => bool"
    5.29 +
    5.30 +defs
    5.31 +
    5.32 +C_asig_def
    5.33 +  "C_asig == ({},{INC},{})"
    5.34 +
    5.35 +C_trans_def "C_trans ==                                           
    5.36 + {tr. let s = fst(tr);                                               
    5.37 +          t = snd(snd(tr))                                           
    5.38 +      in case fst(snd(tr))                                           
    5.39 +      of                                                             
    5.40 +      INC       => t = Suc(s)}"
    5.41 +
    5.42 +C_ioa_def "C_ioa == 
    5.43 + (C_asig, {0}, C_trans,{},{})"
    5.44 +
    5.45 +C_live_ioa_def 
    5.46 +  "C_live_ioa == (C_ioa, WF C_ioa {INC})"
    5.47 +
    5.48 +A_asig_def
    5.49 +  "A_asig == ({},{INC},{})"
    5.50 +
    5.51 +A_trans_def "A_trans ==                                           
    5.52 + {tr. let s = fst(tr);                                               
    5.53 +          t = snd(snd(tr))                                           
    5.54 +      in case fst(snd(tr))                                           
    5.55 +      of                                                             
    5.56 +      INC       => t = True}"
    5.57 +
    5.58 +A_ioa_def "A_ioa == 
    5.59 + (A_asig, {False}, A_trans,{},{})"
    5.60 +
    5.61 +A_live_ioa_def 
    5.62 +  "A_live_ioa == (A_ioa, WF A_ioa {INC})"
    5.63 +
    5.64 +
    5.65 +
    5.66 +h_abs_def
    5.67 +  "h_abs n == n~=0"
    5.68 +
    5.69 +rules
    5.70 +
    5.71 +MC_result
    5.72 +  "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
    5.73 +
    5.74 +end
    5.75 \ No newline at end of file