diff -r 6c12f5e24e34 -r 0437dbc127b3 src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Sat Nov 27 16:08:10 2010 -0800
@@ -0,0 +1,102 @@
+(*  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