src/HOL/HOLCF/IOA/ex/TrivEx2.thy
author blanchet
Thu, 11 Sep 2014 19:32:36 +0200
changeset 58310 91ea607a34d8
parent 58249 180f1b3508ed
child 58880 0baae4311a9f
permissions -rw-r--r--
updated news
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 40945
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/ex/TrivEx2.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     3
*)
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     4
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     5
header {* Trivial Abstraction Example with fairness *}
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
theory TrivEx2
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
imports IOA Abstraction
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
begin
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    10
58310
91ea607a34d8 updated news
blanchet
parents: 58249
diff changeset
    11
datatype action = INC
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    12
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    13
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    14
  C_asig :: "action signature" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    15
  "C_asig = ({},{INC},{})"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    16
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    17
  C_trans :: "(action, nat)transition set" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    18
  "C_trans =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    19
   {tr. let s = fst(tr);
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    20
            t = snd(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    21
        in case fst(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    22
        of
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    23
        INC       => t = Suc(s)}"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    24
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    25
  C_ioa :: "(action, nat)ioa" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    26
  "C_ioa = (C_asig, {0}, C_trans,{},{})"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    27
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    28
  C_live_ioa :: "(action, nat)live_ioa" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    29
  "C_live_ioa = (C_ioa, WF C_ioa {INC})"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    30
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    31
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    32
  A_asig :: "action signature" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    33
  "A_asig = ({},{INC},{})"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    34
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    35
  A_trans :: "(action, bool)transition set" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    36
  "A_trans =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    37
   {tr. let s = fst(tr);
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    38
            t = snd(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    39
        in case fst(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    40
        of
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    41
        INC       => t = True}"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    42
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    43
  A_ioa :: "(action, bool)ioa" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    44
  "A_ioa = (A_asig, {False}, A_trans,{},{})"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    45
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    46
  A_live_ioa :: "(action, bool)live_ioa" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    47
  "A_live_ioa = (A_ioa, WF A_ioa {INC})"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    48
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    49
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    50
  h_abs :: "nat => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    51
  "h_abs n = (n~=0)"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    52
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    53
axiomatization where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    54
  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    55
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    56
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    57
lemma h_abs_is_abstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    58
"is_abstraction h_abs C_ioa A_ioa"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    59
apply (unfold is_abstraction_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    60
apply (rule conjI)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    61
txt {* start states *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    62
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    63
txt {* step case *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    64
apply (rule allI)+
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    65
apply (rule imp_conj_lemma)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    66
apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    67
apply (induct_tac "a")
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    68
apply (simp (no_asm) add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    69
done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    70
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    71
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    72
lemma Enabled_implication:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    73
    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    74
  apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    75
    C_trans_def trans_of_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    76
  apply auto
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    77
  done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    78
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    79
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    80
lemma h_abs_is_liveabstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    81
"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    82
apply (unfold is_live_abstraction_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    83
apply auto
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    84
txt {* is_abstraction *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    85
apply (rule h_abs_is_abstraction)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    86
txt {* temp_weakening *}
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 25135
diff changeset
    87
apply abstraction
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    88
apply (erule Enabled_implication)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    89
done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    90
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    91
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    92
lemma TrivEx2_abstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    93
  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    94
apply (unfold C_live_ioa_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    95
apply (rule AbsRuleT2)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    96
apply (rule h_abs_is_liveabstraction)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    97
apply (rule MC_result)
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 25135
diff changeset
    98
apply abstraction
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    99
apply (simp add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   100
done
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   101
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   102
end