src/HOL/HOLCF/IOA/ex/TrivEx.thy
author wenzelm
Thu, 31 Dec 2015 12:55:39 +0100
changeset 62009 ecb5212d5885
parent 62004 8c6226d88ced
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
clarified imports;
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/TrivEx.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
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 61999
diff changeset
     5
section \<open>Trivial Abstraction Example\<close>
17244
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 TrivEx
62009
ecb5212d5885 clarified imports;
wenzelm
parents: 62004
diff changeset
     8
imports "../Abstraction"
17244
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,{},{})"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    27
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    28
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    29
  A_asig :: "action signature" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    30
  "A_asig = ({},{INC},{})"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    31
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    32
  A_trans :: "(action, bool)transition set" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    33
  "A_trans =
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    34
   {tr. let s = fst(tr);
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    35
            t = snd(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    36
        in case fst(snd(tr))
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    37
        of
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    38
        INC       => t = True}"
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    39
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    40
  A_ioa :: "(action, bool)ioa" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    41
  "A_ioa = (A_asig, {False}, A_trans,{},{})"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    42
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    43
definition
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    44
  h_abs :: "nat => bool" where
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    45
  "h_abs n = (n~=0)"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    46
25135
4f8176c940cf modernized specifications ('definition', 'axiomatization');
wenzelm
parents: 19740
diff changeset
    47
axiomatization where
62004
8c6226d88ced more symbols;
wenzelm
parents: 62002
diff changeset
    48
  MC_result: "validIOA A_ioa (\<diamond>\<box>\<langle>%(b,a,c). b\<rangle>)"
6470
f3015fd68d66 moved this trivial example to new ex dir;
mueller
parents:
diff changeset
    49
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    50
lemma h_abs_is_abstraction:
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    51
  "is_abstraction h_abs C_ioa A_ioa"
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    52
apply (unfold is_abstraction_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    53
apply (rule conjI)
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 61999
diff changeset
    54
txt \<open>start states\<close>
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    55
apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 61999
diff changeset
    56
txt \<open>step case\<close>
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    57
apply (rule allI)+
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    58
apply (rule imp_conj_lemma)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    59
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
    60
apply (induct_tac "a")
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    61
apply (simp add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    62
done
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    63
62004
8c6226d88ced more symbols;
wenzelm
parents: 62002
diff changeset
    64
lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box>\<langle>%(n,a,m). n~=0\<rangle>)"
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    65
apply (rule AbsRuleT1)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    66
apply (rule h_abs_is_abstraction)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    67
apply (rule MC_result)
30607
c3d1590debd8 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
wenzelm
parents: 25135
diff changeset
    68
apply abstraction
19740
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    69
apply (simp add: h_abs_def)
6b38551d0798 removed legacy ML scripts;
wenzelm
parents: 17244
diff changeset
    70
done
17244
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    71
0b2ff9541727 converted to Isar theory format;
wenzelm
parents: 14981
diff changeset
    72
end