src/HOL/HOLCF/IOA/ex/TrivEx2.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 30607 src/HOLCF/IOA/ex/TrivEx2.thy@c3d1590debd8
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
mueller@6470
     1
(*  Title:      HOLCF/IOA/TrivEx.thy
wenzelm@12218
     2
    Author:     Olaf Müller
mueller@6470
     3
*)
mueller@6470
     4
wenzelm@17244
     5
header {* Trivial Abstraction Example with fairness *}
wenzelm@17244
     6
wenzelm@17244
     7
theory TrivEx2
wenzelm@17244
     8
imports IOA Abstraction
wenzelm@17244
     9
begin
mueller@6470
    10
mueller@6470
    11
datatype action = INC
mueller@6470
    12
wenzelm@25135
    13
definition
wenzelm@25135
    14
  C_asig :: "action signature" where
wenzelm@25135
    15
  "C_asig = ({},{INC},{})"
wenzelm@25135
    16
definition
wenzelm@25135
    17
  C_trans :: "(action, nat)transition set" where
wenzelm@25135
    18
  "C_trans =
wenzelm@25135
    19
   {tr. let s = fst(tr);
wenzelm@25135
    20
            t = snd(snd(tr))
wenzelm@25135
    21
        in case fst(snd(tr))
wenzelm@25135
    22
        of
wenzelm@25135
    23
        INC       => t = Suc(s)}"
wenzelm@25135
    24
definition
wenzelm@25135
    25
  C_ioa :: "(action, nat)ioa" where
wenzelm@25135
    26
  "C_ioa = (C_asig, {0}, C_trans,{},{})"
wenzelm@25135
    27
definition
wenzelm@25135
    28
  C_live_ioa :: "(action, nat)live_ioa" where
wenzelm@25135
    29
  "C_live_ioa = (C_ioa, WF C_ioa {INC})"
mueller@6470
    30
wenzelm@25135
    31
definition
wenzelm@25135
    32
  A_asig :: "action signature" where
wenzelm@25135
    33
  "A_asig = ({},{INC},{})"
wenzelm@25135
    34
definition
wenzelm@25135
    35
  A_trans :: "(action, bool)transition set" where
wenzelm@25135
    36
  "A_trans =
wenzelm@25135
    37
   {tr. let s = fst(tr);
wenzelm@25135
    38
            t = snd(snd(tr))
wenzelm@25135
    39
        in case fst(snd(tr))
wenzelm@25135
    40
        of
wenzelm@25135
    41
        INC       => t = True}"
wenzelm@25135
    42
definition
wenzelm@25135
    43
  A_ioa :: "(action, bool)ioa" where
wenzelm@25135
    44
  "A_ioa = (A_asig, {False}, A_trans,{},{})"
wenzelm@25135
    45
definition
wenzelm@25135
    46
  A_live_ioa :: "(action, bool)live_ioa" where
wenzelm@25135
    47
  "A_live_ioa = (A_ioa, WF A_ioa {INC})"
mueller@6470
    48
wenzelm@25135
    49
definition
wenzelm@25135
    50
  h_abs :: "nat => bool" where
wenzelm@25135
    51
  "h_abs n = (n~=0)"
mueller@6470
    52
wenzelm@25135
    53
axiomatization where
wenzelm@25135
    54
  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
mueller@6470
    55
wenzelm@19740
    56
wenzelm@19740
    57
lemma h_abs_is_abstraction:
wenzelm@19740
    58
"is_abstraction h_abs C_ioa A_ioa"
wenzelm@19740
    59
apply (unfold is_abstraction_def)
wenzelm@19740
    60
apply (rule conjI)
wenzelm@19740
    61
txt {* start states *}
wenzelm@19740
    62
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
wenzelm@19740
    63
txt {* step case *}
wenzelm@19740
    64
apply (rule allI)+
wenzelm@19740
    65
apply (rule imp_conj_lemma)
wenzelm@19740
    66
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
wenzelm@19740
    67
apply (induct_tac "a")
wenzelm@19740
    68
apply (simp (no_asm) add: h_abs_def)
wenzelm@19740
    69
done
wenzelm@19740
    70
wenzelm@19740
    71
wenzelm@19740
    72
lemma Enabled_implication:
wenzelm@19740
    73
    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
wenzelm@19740
    74
  apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
wenzelm@19740
    75
    C_trans_def trans_of_def)
wenzelm@19740
    76
  apply auto
wenzelm@19740
    77
  done
wenzelm@19740
    78
wenzelm@19740
    79
wenzelm@19740
    80
lemma h_abs_is_liveabstraction:
wenzelm@19740
    81
"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
wenzelm@19740
    82
apply (unfold is_live_abstraction_def)
wenzelm@19740
    83
apply auto
wenzelm@19740
    84
txt {* is_abstraction *}
wenzelm@19740
    85
apply (rule h_abs_is_abstraction)
wenzelm@19740
    86
txt {* temp_weakening *}
wenzelm@30607
    87
apply abstraction
wenzelm@19740
    88
apply (erule Enabled_implication)
wenzelm@19740
    89
done
wenzelm@19740
    90
wenzelm@19740
    91
wenzelm@19740
    92
lemma TrivEx2_abstraction:
wenzelm@19740
    93
  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
wenzelm@19740
    94
apply (unfold C_live_ioa_def)
wenzelm@19740
    95
apply (rule AbsRuleT2)
wenzelm@19740
    96
apply (rule h_abs_is_liveabstraction)
wenzelm@19740
    97
apply (rule MC_result)
wenzelm@30607
    98
apply abstraction
wenzelm@19740
    99
apply (simp add: h_abs_def)
wenzelm@19740
   100
done
wenzelm@17244
   101
wenzelm@17244
   102
end