theory Dch imports Chorus Dmng begin (* Revitsky interpretation: result of command is set of sets from which angel chooses, and demon chooses one of those *) consts wp_ch :: "('a => 'b uca) => ('b => bool) => ('a => bool)" (* monotonic predicate transformer *) mono_pt :: "(('b => bool) => ('a => bool)) => bool" (* extended substitution of a predicate transformer *) sub_of_pt :: "(('b => bool) => ('a => bool)) => ('a => 'b uca)" seq_ch :: "('a => 'b uca) => ('b => 'c uca) => ('a => 'c uca)" trm_ch :: "('a => 'b uca) => 'a => bool" fis_ch :: "('a => 'b uca) => 'a => bool" ref_ch :: "('a => 'b uca) => ('a => 'b uca) => bool" abort_ch :: "('a => 'b uca)" magic_ch :: "('a => 'b uca)" conjugate :: "('a => 'b uca) => ('a => 'b uca)" dem_ch :: "('a => 'b uca) set => ('a => 'b uca)" ang_ch :: "('a => 'b uca) set => ('a => 'b uca)" prd_ch :: "'b => ('a => 'b uca) => 'a => bool" crd_ch :: "'b => ('a => 'b uca) => 'a => bool" pod_ch :: "'b set => ('a => 'b uca) => 'a => bool" cod_ch :: "'b set => ('a => 'b uca) => 'a => bool" guard_ch :: "('a => bool) => ('a => 'b uca) => ('a => 'b uca)" precon_ch :: "('a => bool) => ('a => 'b uca) => ('a => 'b uca)" defs wp_ch_def : "wp_ch A P s == EX ang : Rep_uca (A s). ang <= Collect P" seq_ch_def : "seq_ch A B s == extU B (A s)" fis_ch_def : "fis_ch A s == {} ~: Rep_uca (A s)" trm_ch_def : "trm_ch A s == Rep_uca (A s) ~= {}" ref_ch_def : "ref_ch A B == ALL Q. wp_ch A Q ---> wp_ch B Q" magic_ch_def : "magic_ch s == uc_Abs UNIV" abort_ch_def : "abort_ch s == uc_Abs {}" conjugate_def : "conjugate A s == uc_Abs (uc_swap (Rep_uca (A s)))" ang_ch_def : "ang_ch As s == uc_Abs (UNION As (%A. Rep_uca (A s)))" dem_ch_def : "dem_ch As s == uc_Abs (uc_pext (%A. Rep_uca (A s)) As)" prd_ch_def : "prd_ch s' A s == s' : Inter (Rep_uca (A s))" crd_ch_def : "crd_ch s' A s == {s'} : Rep_uca (A s)" pod_ch_def : "pod_ch u A s == u : uc_swap (Rep_uca (A s))" cod_ch_def : "cod_ch u A s == u : Rep_uca (A s)" precon_ch_def : "precon_ch P A s == if P s then A s else uc_Abs {}" guard_ch_def : "guard_ch P A s == if P s then A s else uc_Abs UNIV" sub_of_pt_def : "sub_of_pt F s == uc_Abs {A. F (%b. b : A) s}" mono_pt_def : "mono_pt F == (ALL P Q. (P ---> Q) --> (F P ---> F Q))" end