56 definition increasing :: "['a => 'b::{order}] => 'a program set" where |
56 definition increasing :: "['a => 'b::{order}] => 'a program set" where |
57 --{*Polymorphic in both states and the meaning of @{text "\<le>"}*} |
57 --{*Polymorphic in both states and the meaning of @{text "\<le>"}*} |
58 "increasing f == \<Inter>z. stable {s. z \<le> f s}" |
58 "increasing f == \<Inter>z. stable {s. z \<le> f s}" |
59 |
59 |
60 |
60 |
61 text{*Perhaps HOL shouldn't add this in the first place!*} |
|
62 declare image_Collect [simp del] |
|
63 |
|
64 subsubsection{*The abstract type of programs*} |
61 subsubsection{*The abstract type of programs*} |
65 |
62 |
66 lemmas program_typedef = |
63 lemmas program_typedef = |
67 Rep_Program Rep_Program_inverse Abs_Program_inverse |
64 Rep_Program Rep_Program_inverse Abs_Program_inverse |
68 Program_def Init_def Acts_def AllowedActs_def mk_program_def |
65 Program_def Init_def Acts_def AllowedActs_def mk_program_def |
71 apply (cut_tac x = F in Rep_Program) |
68 apply (cut_tac x = F in Rep_Program) |
72 apply (auto simp add: program_typedef) |
69 apply (auto simp add: program_typedef) |
73 done |
70 done |
74 |
71 |
75 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F" |
72 lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F" |
76 by (simp add: insert_absorb Id_in_Acts) |
73 by (simp add: insert_absorb) |
77 |
74 |
78 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}" |
75 lemma Acts_nonempty [simp]: "Acts F \<noteq> {}" |
79 by auto |
76 by auto |
80 |
77 |
81 lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F" |
78 lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F" |
82 apply (cut_tac x = F in Rep_Program) |
79 apply (cut_tac x = F in Rep_Program) |
83 apply (auto simp add: program_typedef) |
80 apply (auto simp add: program_typedef) |
84 done |
81 done |
85 |
82 |
86 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F" |
83 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F" |
87 by (simp add: insert_absorb Id_in_AllowedActs) |
84 by (simp add: insert_absorb) |
88 |
85 |
89 subsubsection{*Inspectors for type "program"*} |
86 subsubsection{*Inspectors for type "program"*} |
90 |
87 |
91 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init" |
88 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init" |
92 by (simp add: program_typedef) |
89 by (simp add: program_typedef) |