--- a/src/HOLCF/IOA/ex/TrivEx2.thy Sat Nov 27 14:34:54 2010 -0800
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,102 +0,0 @@
-(* Title: HOLCF/IOA/TrivEx.thy
- Author: Olaf Müller
-*)
-
-header {* Trivial Abstraction Example with fairness *}
-
-theory TrivEx2
-imports IOA Abstraction
-begin
-
-datatype action = INC
-
-definition
- C_asig :: "action signature" where
- "C_asig = ({},{INC},{})"
-definition
- C_trans :: "(action, nat)transition set" where
- "C_trans =
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = Suc(s)}"
-definition
- C_ioa :: "(action, nat)ioa" where
- "C_ioa = (C_asig, {0}, C_trans,{},{})"
-definition
- C_live_ioa :: "(action, nat)live_ioa" where
- "C_live_ioa = (C_ioa, WF C_ioa {INC})"
-
-definition
- A_asig :: "action signature" where
- "A_asig = ({},{INC},{})"
-definition
- A_trans :: "(action, bool)transition set" where
- "A_trans =
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = True}"
-definition
- A_ioa :: "(action, bool)ioa" where
- "A_ioa = (A_asig, {False}, A_trans,{},{})"
-definition
- A_live_ioa :: "(action, bool)live_ioa" where
- "A_live_ioa = (A_ioa, WF A_ioa {INC})"
-
-definition
- h_abs :: "nat => bool" where
- "h_abs n = (n~=0)"
-
-axiomatization where
- MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
-
-
-lemma h_abs_is_abstraction:
-"is_abstraction h_abs C_ioa A_ioa"
-apply (unfold is_abstraction_def)
-apply (rule conjI)
-txt {* start states *}
-apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
-apply (rule allI)+
-apply (rule imp_conj_lemma)
-apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
-apply (induct_tac "a")
-apply (simp (no_asm) add: h_abs_def)
-done
-
-
-lemma Enabled_implication:
- "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
- apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
- C_trans_def trans_of_def)
- apply auto
- done
-
-
-lemma h_abs_is_liveabstraction:
-"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
-apply (unfold is_live_abstraction_def)
-apply auto
-txt {* is_abstraction *}
-apply (rule h_abs_is_abstraction)
-txt {* temp_weakening *}
-apply abstraction
-apply (erule Enabled_implication)
-done
-
-
-lemma TrivEx2_abstraction:
- "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
-apply (unfold C_live_ioa_def)
-apply (rule AbsRuleT2)
-apply (rule h_abs_is_liveabstraction)
-apply (rule MC_result)
-apply abstraction
-apply (simp add: h_abs_def)
-done
-
-end