src/HOLCF/IOA/ex/TrivEx.thy
author wenzelm
Fri Mar 20 15:24:18 2009 +0100 (2009-03-20)
changeset 30607 c3d1590debd8
parent 25135 4f8176c940cf
permissions -rw-r--r--
eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
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 *}
wenzelm@17244
     6
wenzelm@17244
     7
theory TrivEx
wenzelm@17244
     8
imports 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,{},{})"
mueller@6470
    27
wenzelm@25135
    28
definition
wenzelm@25135
    29
  A_asig :: "action signature" where
wenzelm@25135
    30
  "A_asig = ({},{INC},{})"
wenzelm@25135
    31
definition
wenzelm@25135
    32
  A_trans :: "(action, bool)transition set" where
wenzelm@25135
    33
  "A_trans =
wenzelm@25135
    34
   {tr. let s = fst(tr);
wenzelm@25135
    35
            t = snd(snd(tr))
wenzelm@25135
    36
        in case fst(snd(tr))
wenzelm@25135
    37
        of
wenzelm@25135
    38
        INC       => t = True}"
wenzelm@25135
    39
definition
wenzelm@25135
    40
  A_ioa :: "(action, bool)ioa" where
wenzelm@25135
    41
  "A_ioa = (A_asig, {False}, A_trans,{},{})"
mueller@6470
    42
wenzelm@25135
    43
definition
wenzelm@25135
    44
  h_abs :: "nat => bool" where
wenzelm@25135
    45
  "h_abs n = (n~=0)"
mueller@6470
    46
wenzelm@25135
    47
axiomatization where
wenzelm@25135
    48
  MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)"
mueller@6470
    49
wenzelm@19740
    50
lemma h_abs_is_abstraction:
wenzelm@19740
    51
  "is_abstraction h_abs C_ioa A_ioa"
wenzelm@19740
    52
apply (unfold is_abstraction_def)
wenzelm@19740
    53
apply (rule conjI)
wenzelm@19740
    54
txt {* start states *}
wenzelm@19740
    55
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
wenzelm@19740
    56
txt {* step case *}
wenzelm@19740
    57
apply (rule allI)+
wenzelm@19740
    58
apply (rule imp_conj_lemma)
wenzelm@19740
    59
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
wenzelm@19740
    60
apply (induct_tac "a")
wenzelm@19740
    61
apply (simp add: h_abs_def)
wenzelm@19740
    62
done
wenzelm@19740
    63
wenzelm@19740
    64
lemma TrivEx_abstraction: "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"
wenzelm@19740
    65
apply (rule AbsRuleT1)
wenzelm@19740
    66
apply (rule h_abs_is_abstraction)
wenzelm@19740
    67
apply (rule MC_result)
wenzelm@30607
    68
apply abstraction
wenzelm@19740
    69
apply (simp add: h_abs_def)
wenzelm@19740
    70
done
wenzelm@17244
    71
wenzelm@17244
    72
end