src/HOLCF/IOA/ex/TrivEx2.thy
author wenzelm
Sat, 27 May 2006 21:18:51 +0200
changeset 19740 6b38551d0798
parent 17244 0b2ff9541727
child 25135 4f8176c940cf
permissions -rw-r--r--
removed legacy ML scripts;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/TrivEx.thy
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 6470
diff changeset
     3
    Author:     Olaf Müller
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     4
*)
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
     5
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     6
header {* Trivial Abstraction Example with fairness *}
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     7
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     8
theory TrivEx2
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
     9
imports IOA Abstraction
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    10
begin
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    11
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    12
datatype action = INC
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    13
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    14
consts
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    15
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    16
C_asig   ::  "action signature"
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    17
C_trans  :: "(action, nat)transition set"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    18
C_ioa    :: "(action, nat)ioa"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    19
C_live_ioa :: "(action, nat)live_ioa"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    20
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    21
A_asig   :: "action signature"
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    22
A_trans  :: "(action, bool)transition set"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    23
A_ioa    :: "(action, bool)ioa"
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    24
A_live_ioa :: "(action, bool)live_ioa"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    25
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    26
h_abs    :: "nat => bool"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    27
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    28
defs
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    29
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    30
C_asig_def:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    31
  "C_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    32
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    33
C_trans_def: "C_trans ==
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    34
 {tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    35
          t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    36
      in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    37
      of
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    38
      INC       => t = Suc(s)}"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    39
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    40
C_ioa_def: "C_ioa ==
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    41
 (C_asig, {0}, C_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    42
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    43
C_live_ioa_def:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    44
  "C_live_ioa == (C_ioa, WF C_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    45
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    46
A_asig_def:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    47
  "A_asig == ({},{INC},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    48
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    49
A_trans_def: "A_trans ==
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    50
 {tr. let s = fst(tr);
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    51
          t = snd(snd(tr))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    52
      in case fst(snd(tr))
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    53
      of
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    54
      INC       => t = True}"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    55
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    56
A_ioa_def: "A_ioa ==
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    57
 (A_asig, {False}, A_trans,{},{})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    58
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    59
A_live_ioa_def:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    60
  "A_live_ioa == (A_ioa, WF A_ioa {INC})"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    61
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    62
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    63
h_abs_def:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    64
  "h_abs n == n~=0"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    65
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    66
axioms
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    67
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    68
MC_result:
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    69
  "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    70
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    71
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    72
lemma h_abs_is_abstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    73
"is_abstraction h_abs C_ioa A_ioa"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    74
apply (unfold is_abstraction_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    75
apply (rule conjI)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    76
txt {* start states *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    77
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
    78
txt {* step case *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    79
apply (rule allI)+
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    80
apply (rule imp_conj_lemma)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    81
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
    82
apply (induct_tac "a")
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    83
apply (simp (no_asm) add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    84
done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    85
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    86
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    87
lemma Enabled_implication:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    88
    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    89
  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
    90
    C_trans_def trans_of_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    91
  apply auto
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    92
  done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    93
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    94
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    95
lemma h_abs_is_liveabstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    96
"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
    97
apply (unfold is_live_abstraction_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    98
apply auto
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    99
txt {* is_abstraction *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   100
apply (rule h_abs_is_abstraction)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   101
txt {* temp_weakening *}
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   102
apply (tactic "abstraction_tac 1")
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   103
apply (erule Enabled_implication)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   104
done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   105
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   106
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   107
lemma TrivEx2_abstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   108
  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   109
apply (unfold C_live_ioa_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   110
apply (rule AbsRuleT2)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   111
apply (rule h_abs_is_liveabstraction)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   112
apply (rule MC_result)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   113
apply (tactic "abstraction_tac 1")
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   114
apply (simp add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
   115
done
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   116
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
   117
end