updating everything!
This commit is contained in:
y.nemouchi
parent
d297000259
commit
a01eb9721f
|
|
@ -342,9 +342,9 @@ method upreds_blast_slow = utp_tac_control upreds_defs slow_uexpr_transfer upred
|
|||
|
||||
subsubsection \<open> UTP relations tactics\<close>
|
||||
|
||||
method urels_defs = (unfold upred_defs urel_defs)[1]
|
||||
method urels_rewrites = (simp add: fun_eq_iff relcomp_unfold OO_def
|
||||
lens_defs upred_defs alpha_splits Product_Type.split_beta)
|
||||
method urels_defs = (unfold upred_defs urel_defs)[1]
|
||||
method urels_rewrites = (simp add: fun_eq_iff relcomp_unfold OO_def lens_defs upred_defs
|
||||
alpha_splits Product_Type.split_beta)
|
||||
method urels_simp = utp_tac_control urels_defs fast_uexpr_transfer urels_rewrites uexpr_interp_tac utp_simp_tac
|
||||
method urels_simp_slow = utp_tac_control urels_defs slow_uexpr_transfer urels_rewrites uexpr_interp_tac utp_simp_tac
|
||||
method urels_auto = utp_tac_control urels_defs fast_uexpr_transfer urels_rewrites uexpr_interp_tac utp_auto_tac
|
||||
|
|
|
|||
|
|
@ -1102,5 +1102,99 @@ term "DO body WHILE b OD"
|
|||
|
||||
term "MODIFY VARS DO body OD"
|
||||
|
||||
term "(X:[P] = P)"
|
||||
|
||||
term "frame X (assign_r (x ) v)"
|
||||
term "(antiframe X (assign_r (x;\<^sub>L X) v) = (assign_r (x;\<^sub>L X) v))"
|
||||
|
||||
lemma \<open>mwb_lens X \<Longrightarrow> mwb_lens x \<Longrightarrow> x \<subseteq>\<^sub>L X \<Longrightarrow>
|
||||
antiframe X (assign_r (x) v) = (assign_r (x) v)\<close>
|
||||
by rel_auto
|
||||
|
||||
lemma antiframe_prog_hoare_basic_weak:
|
||||
assumes vwb_lens_g :\<open>vwb_lens g\<close>
|
||||
assumes vwb_lens_g':\<open>vwb_lens g'\<close>
|
||||
assumes vwb_lens_l :\<open>vwb_lens l\<close>
|
||||
assumes indep_g_l :\<open>g \<bowtie> l\<close>
|
||||
assumes region :\<open>g' \<subseteq>\<^sub>L g\<close>
|
||||
assumes modifies :\<open>{&g', &l}:[PROG] = PROG\<close> (*TODO: From algebraic laws of program of antiframe this assumption can be derived from {&g'}:[PROG] = PROG*)
|
||||
assumes hoare :\<open>\<lbrace>P\<rbrace>PROG\<lbrace>Q\<rbrace>\<^sub>P\<close>
|
||||
shows \<open>\<lbrace>P \<and> R\<rbrace>MODIFY g' DO PROG OD\<lbrace>(\<exists> {&l, &g'} \<bullet> Q \<oplus>\<^sub>p g') \<and> (\<exists> {&l, &g'} \<bullet> R \<oplus>\<^sub>p l)\<rbrace>\<^sub>P\<close>
|
||||
using vwb_lens_g vwb_lens_g' vwb_lens_l indep_g_l modifies hoare
|
||||
unfolding lens_indep_def
|
||||
apply (simp add:prog_rep_eq)
|
||||
apply rel_simp
|
||||
using indep_g_l
|
||||
apply rel_simp
|
||||
apply auto
|
||||
apply(insert region)
|
||||
subgoal for _ more _ x
|
||||
apply (rule exI[where x = \<open>get\<^bsub>l\<^esub>x\<close>])
|
||||
using region unfolding lens_indep_def
|
||||
apply auto
|
||||
apply (drule sublens_pres_indep[OF _ indep_g_l])
|
||||
unfolding lens_indep_def
|
||||
apply simp apply blast
|
||||
done
|
||||
done
|
||||
|
||||
term "Rep_uexpr(\<exists>g' \<bullet> R)"
|
||||
lemma \<open>\<lbrakk>\<exists> g' \<bullet> R\<rbrakk>\<^sub>e s = (\<exists>v. \<lbrakk>R\<rbrakk>\<^sub>e (put\<^bsub>g\<^esub> s v))\<close>
|
||||
apply rel_auto
|
||||
oops
|
||||
|
||||
lemma
|
||||
assumes vwb_lens_g :\<open>vwb_lens g\<close>
|
||||
assumes vwb_lens_g':\<open>vwb_lens g'\<close>
|
||||
assumes vwb_lens_l :\<open>vwb_lens l\<close>
|
||||
assumes indep_g_l :\<open>g \<bowtie> l\<close>
|
||||
assumes region :\<open>g' \<subseteq>\<^sub>L g\<close>
|
||||
assumes strict :\<open>(g +\<^sub>L l) = 1\<^sub>L\<close>
|
||||
assumes modifies :\<open>{&g', &l}:[PROG] = PROG\<close> (*TODO: From algebraic laws of program of antiframe this assumption can be derived from {&g'}:[PROG] = PROG*)
|
||||
assumes hoare :\<open>\<lbrace>P\<rbrace>PROG\<lbrace>Q\<rbrace>\<^sub>P\<close>
|
||||
shows \<open>\<lbrace>P \<and> R\<rbrace>MODIFY g' DO PROG OD\<lbrace>(\<exists>l \<bullet> Q ) \<and> (\<exists>g' \<bullet> R)\<rbrace>\<^sub>P\<close>
|
||||
using vwb_lens_g vwb_lens_g' vwb_lens_l indep_g_l modifies hoare strict
|
||||
unfolding lens_indep_def
|
||||
apply (simp add:prog_rep_eq)
|
||||
apply rel_simp
|
||||
using indep_g_l
|
||||
apply rel_simp
|
||||
apply auto
|
||||
apply(insert region)
|
||||
subgoal for _ more more' _ _ _ ab bb
|
||||
apply (rule exI[where x = \<open>get\<^bsub>l\<^esub>(ab , bb )\<close>])
|
||||
using region unfolding lens_indep_def
|
||||
apply auto
|
||||
apply (drule sublens_pres_indep[OF _ indep_g_l])
|
||||
unfolding lens_indep_def
|
||||
apply simp
|
||||
apply (metis mwb_lens_def vwb_lens_mwb weak_lens.put_get)
|
||||
done
|
||||
subgoal for _ a b _ _ _ ab bb
|
||||
apply (rule exI[where x = \<open>get\<^bsub>g'\<^esub>(a , b)\<close>])
|
||||
unfolding lens_indep_def
|
||||
apply (metis sublens_put_put vwb_lens_mwb vwb_lens_wb wb_lens.get_put)
|
||||
done
|
||||
done
|
||||
|
||||
|
||||
lemma \<open>&x = utp_expr.var (x )\<close>
|
||||
apply rel_simp
|
||||
done
|
||||
|
||||
lemma \<open>\<forall> s s'. Rep_uexpr ($x) (s, s') = Rep_uexpr (utp_expr.var (x ;\<^sub>L fst_lens)) (s, s')\<close>
|
||||
apply rel_simp
|
||||
done
|
||||
|
||||
lemma \<open>bop f x y = sda\<close>
|
||||
apply rel_simp
|
||||
oops
|
||||
lemma \<open>(\<lambda> x \<bullet> e) = sda\<close>
|
||||
apply rel_simp
|
||||
oops
|
||||
|
||||
term "subst_upd_uvar \<sigma> X e"
|
||||
thm swap_usubst_inj
|
||||
term \<open>subst (subst_upd_uvar id X v) e\<close>
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -264,7 +264,7 @@ program_spec Talk_gcd_example:
|
|||
ELSE x :== (&x - &r)
|
||||
FI
|
||||
OD"
|
||||
vcg_wp
|
||||
vcg_wp
|
||||
apply (simp add: gcd_diff1)
|
||||
apply (metis gcd.commute gcd_diff1)+
|
||||
done
|
||||
|
|
|
|||
|
|
@ -34,6 +34,20 @@ subsection \<open>SKIP Laws\<close>
|
|||
text \<open>In this section we introduce the algebraic laws of programming related to the SKIP
|
||||
statement.\<close>
|
||||
|
||||
lemma antiframe_test:
|
||||
"vwb_lens a \<Longrightarrow> vwb_lens b \<Longrightarrow>a\<bowtie>b \<Longrightarrow>
|
||||
a:[a :== \<guillemotleft>x\<guillemotright>;; b :== \<guillemotleft>y\<guillemotright>] = a :== \<guillemotleft>x\<guillemotright>"
|
||||
unfolding lens_indep_def
|
||||
apply rel_simp
|
||||
done
|
||||
|
||||
lemma
|
||||
"mwb_lens a \<Longrightarrow>
|
||||
a:[a :== \<guillemotleft>x\<guillemotright>;; a:\<lbrakk>a :== \<guillemotleft>y\<guillemotright>\<rbrakk>] = a :== \<guillemotleft>x\<guillemotright>"
|
||||
apply rel_simp
|
||||
done
|
||||
|
||||
|
||||
lemma pre_skip_post: "(\<lceil>b\<rceil>\<^sub>< \<and> II) = (II \<and> \<lceil>b\<rceil>\<^sub>>)"
|
||||
by rel_auto
|
||||
|
||||
|
|
|
|||
|
|
@ -538,7 +538,7 @@ lemma if_d_H4_true:
|
|||
lemma if_d_mono:
|
||||
"mono (\<lambda>X. bif\<^sub>D b then P ;; X else Q eif)"
|
||||
by (auto intro: monoI seqr_mono cond_mono)
|
||||
|
||||
|
||||
subsection \<open>Recursion laws for designs\<close>
|
||||
|
||||
lemma H1_H3_mu_refine_intro:
|
||||
|
|
|
|||
|
|
@ -351,6 +351,11 @@ lemma comp_prog_if_prog_left_distr:
|
|||
"((IF b THEN P ELSE Q FI); R) = (IF b THEN (P ; R) ELSE (Q ; R) FI)"
|
||||
by pauto
|
||||
|
||||
lemma comp_prog_if_prog_skip_prog_distr_right:
|
||||
"(IF b THEN SKIP ELSE Q1 FI ; IF b THEN SKIP ELSE Q2 FI) =
|
||||
IF b THEN SKIP ELSE Q1; IF b THEN SKIP ELSE Q2 FI FI"
|
||||
by pauto
|
||||
|
||||
lemma if_prog_monoI:
|
||||
"P\<^sub>1 \<sqsubseteq> P\<^sub>2 \<Longrightarrow> Q\<^sub>1 \<sqsubseteq> Q\<^sub>2 \<Longrightarrow> (IF b THEN P\<^sub>1 ELSE Q\<^sub>1 FI) \<sqsubseteq> (IF b THEN P\<^sub>2 ELSE Q\<^sub>2 FI)"
|
||||
by (simp add: prog_rep_eq cond_mono)
|
||||
|
|
@ -359,6 +364,35 @@ lemma If_refines_intro:
|
|||
" \<not>b \<longrightarrow> z \<sqsubseteq> Q\<Longrightarrow> b\<longrightarrow> z \<sqsubseteq> P \<Longrightarrow> z \<sqsubseteq> (if b then P else Q)"
|
||||
by simp
|
||||
|
||||
lemma \<open>vwb_lens x \<Longrightarrow>
|
||||
(x :== \<guillemotleft>c1\<guillemotright> ; IF \<not>(&x =\<^sub>u \<guillemotleft>c1\<guillemotright>) THEN SKIP ELSE x :== \<guillemotleft>c2\<guillemotright> ; Q FI) =
|
||||
(x :== \<guillemotleft>c1\<guillemotright> ; IF false THEN SKIP ELSE x :== \<guillemotleft>c2\<guillemotright> ; Q FI)\<close>
|
||||
apply (simp only: if_prog_false)
|
||||
apply (smt assigns_prog_left_cond_cond if_prog_symm if_prog_true subst_eq_upred subst_lit ulit_eq usubst_cancel vwb_lens_weak)
|
||||
done
|
||||
lemma \<open>vwb_lens x \<Longrightarrow>
|
||||
(x :== \<guillemotleft>c1\<guillemotright> ; IF \<not>(&x =\<^sub>u \<guillemotleft>c1\<guillemotright>) THEN SKIP ELSE x :== \<guillemotleft>c2\<guillemotright> ; Q FI) =
|
||||
(x :== \<guillemotleft>c2\<guillemotright> ; Q )\<close>
|
||||
apply (subst assigns_prog_left_cond_cond)
|
||||
apply (subst assigns_prog_left_subst)
|
||||
apply (subst assigns_prog_left_subst)
|
||||
apply (subst assigns_prog_left_subst)
|
||||
apply (subst assigns_prog_left_subst)
|
||||
apply ptransfer
|
||||
using [[simp_trace]]
|
||||
apply pred_simp
|
||||
done
|
||||
lemma blahblahblah: \<open>vwb_lens x \<Longrightarrow>
|
||||
(x :== \<guillemotleft>c1\<guillemotright> ; IF \<not>(&x =\<^sub>u \<guillemotleft>c1\<guillemotright>) THEN SKIP ELSE x :== \<guillemotleft>c2\<guillemotright> ; Q FI) =
|
||||
( x :== \<guillemotleft>c2\<guillemotright> ; Q )\<close>
|
||||
by (smt assigns_prog_left_cond_cond assigns_prog_left_subst assigns_prog_test if_prog_symm if_prog_true psubst_seq subst_eq_upred subst_lit ulit_eq usubst_cancel vwb_lens_mwb vwb_lens_weak)
|
||||
lemma blahblahblah1: \<open>vwb_lens x \<Longrightarrow>
|
||||
(x :== \<guillemotleft>Some e\<guillemotright> ; IF (&x =\<^sub>u \<guillemotleft>None\<guillemotright>) THEN SKIP ELSE x :== \<guillemotleft>None\<guillemotright> ; Q FI) =
|
||||
(x :== \<guillemotleft>None\<guillemotright> ; Q )\<close>
|
||||
|
||||
by (smt assigns_prog_left_cond_cond assigns_prog_left_subst assigns_prog_test if_prog_false option.distinct(1) psubst_seq subst_eq_upred subst_lit ulit_neq usubst_cancel vwb_lens_mwb vwb_lens_weak)
|
||||
|
||||
|
||||
section \<open>Laws for Sequential Composition \<close>
|
||||
|
||||
lemma seq_prog_monoI:
|
||||
|
|
@ -1079,6 +1113,15 @@ lemma antiframe_test:
|
|||
apply (metis vwb_lens.put_eq)
|
||||
done
|
||||
|
||||
lemma
|
||||
"vwb_lens a \<Longrightarrow> vwb_lens b \<Longrightarrow>
|
||||
a:[a :== \<guillemotleft>x\<guillemotright>; a:\<lbrakk>a :== \<guillemotleft>y\<guillemotright>\<rbrakk>] = a :== \<guillemotleft>x\<guillemotright>"
|
||||
unfolding lens_indep_def
|
||||
apply (simp add: prog_rep_eq)
|
||||
apply rel_simp
|
||||
apply (metis vwb_lens.put_eq)
|
||||
done
|
||||
|
||||
lemma antiframe_prog_idemp:
|
||||
"vwb_lens g \<Longrightarrow>g:[g:[P]] = g:[P]"
|
||||
apply (simp add: prog_rep_eq)
|
||||
|
|
@ -1224,7 +1267,6 @@ lemma If_prog_anti_frame_prog_modifies:
|
|||
shows "g:[IF b THEN P1 ELSE P2 FI] = IF b THEN P1 ELSE P2 FI"
|
||||
by (metis If_prog_anti_frame_prog_distr modifies1 modifies2)
|
||||
|
||||
term "subst_upd \<sigma> g (\<langle>\<sigma>\<rangle>\<^sub>s g)"
|
||||
definition
|
||||
"get_put' g \<sigma> = \<sigma>(g \<mapsto>\<^sub>s \<langle>\<sigma>\<rangle>\<^sub>s g)"
|
||||
|
||||
|
|
@ -1952,28 +1994,6 @@ lemma antiframe_prog_refinedBy_while_lfp_scp_prog:
|
|||
order_refl order_trans seq_prog_monoI)
|
||||
done
|
||||
|
||||
lemma " (x = y) = (x\<sqsubseteq>y \<and> y\<sqsubseteq>x)"
|
||||
using antisym by blast
|
||||
|
||||
find_theorems "\<Sqinter>\<^sub>p_ \<in> _"
|
||||
|
||||
lemma "vwb_lens G \<Longrightarrow> G:[\<Sqinter>\<^sub>pA] \<in> pantiframe_prog G ` A \<Longrightarrow>
|
||||
pantiframe_prog G (\<Sqinter>\<^sub>p A) = \<Sqinter>\<^sub>p (image (pantiframe_prog G) A)"
|
||||
proof (rule antisym, goal_cases)
|
||||
case 1
|
||||
then show ?case
|
||||
apply (subst inf_prog_lower)
|
||||
apply simp_all
|
||||
done
|
||||
next
|
||||
case 2
|
||||
then show ?case
|
||||
apply (subst inf_prog_greatest)
|
||||
apply (metis antiframe_prog_monoI imageE inf_prog_lower)
|
||||
apply simp
|
||||
done
|
||||
qed
|
||||
|
||||
lemma antiframe_prog_modifies_while_lfp_scp_prog:
|
||||
assumes vwb_lens: "vwb_lens G"
|
||||
assumes modifies: "G:[body] = body"
|
||||
|
|
@ -1981,6 +2001,106 @@ lemma antiframe_prog_modifies_while_lfp_scp_prog:
|
|||
by (simp add: antiframe_prog_refinedBy_while_lfp_scp_prog
|
||||
antiframe_prog_refines_while_lfp_scp_prog antisym modifies vwb_lens)
|
||||
|
||||
find_theorems "\<Sqinter>\<^sub>p_ \<in> _"
|
||||
thm antiframe_prog_mono
|
||||
antiframe_prog_monoI
|
||||
|
||||
lemma
|
||||
assumes \<open>\<Sqinter>\<^sub>pA \<in> A\<close>
|
||||
shows \<open>G:[\<Sqinter>\<^sub>pA] \<in> pantiframe_prog G ` A\<close>
|
||||
unfolding image_def Bex_def
|
||||
apply simp
|
||||
apply (rule exI[where x = \<open>\<Sqinter>\<^sub>pA\<close>])
|
||||
using assms
|
||||
apply simp
|
||||
done
|
||||
|
||||
lemma least_in_same_set_mono:
|
||||
\<open>mono F \<Longrightarrow> \<Sqinter>\<^sub>p{x. F x \<sqsubseteq> x} \<in> {x. F x \<sqsubseteq> x}\<close>
|
||||
apply auto
|
||||
apply (rule inf_prog_greatest)
|
||||
apply (metis (full_types) inf_prog_lower lfp_prog_alt_def lfp_prog_unfold mono_Monotone_prog)
|
||||
done
|
||||
|
||||
lemma anti_frame_is_continues:
|
||||
assumes least_in: \<open> \<Sqinter>\<^sub>pA \<in> A\<close>
|
||||
shows \<open>pantiframe_prog G (\<Sqinter>\<^sub>p A) = \<Sqinter>\<^sub>p (image (pantiframe_prog G) A)\<close>
|
||||
proof (rule antisym, goal_cases)
|
||||
case 1
|
||||
then show ?case
|
||||
apply (rule inf_prog_lower)
|
||||
apply (rule imageI)
|
||||
using least_in
|
||||
apply simp
|
||||
done
|
||||
next
|
||||
case 2
|
||||
then show ?case
|
||||
apply (rule inf_prog_greatest)
|
||||
apply (erule imageE)
|
||||
apply simp
|
||||
apply (rule antiframe_prog_monoI)
|
||||
apply (rule inf_prog_lower)
|
||||
apply auto
|
||||
done
|
||||
qed
|
||||
|
||||
lemma \<open>mono F \<Longrightarrow> pantiframe_prog G (\<Sqinter>\<^sub>p{x. F x \<sqsubseteq> x}) = P\<close>
|
||||
apply (subst anti_frame_is_continues)
|
||||
using least_in_same_set_mono apply blast
|
||||
oops
|
||||
lemma \<open>mono F \<Longrightarrow>
|
||||
G:[\<mu>\<^sub>p ((pantiframe_prog G) o F)] = (\<mu>\<^sub>p ((pantiframe_prog G) o F))\<close>
|
||||
unfolding lfp_prog_alt_def
|
||||
apply simp
|
||||
apply (subst anti_frame_is_continues)
|
||||
apply simp
|
||||
apply (rule inf_prog_greatest)
|
||||
apply simp
|
||||
apply (rule order_trans)
|
||||
apply simp
|
||||
apply (rule antiframe_prog_monoI)
|
||||
apply (simp only: mono_def)
|
||||
apply (simp add: inf_prog_lower)
|
||||
unfolding image_def Bex_def
|
||||
apply simp
|
||||
apply (smt antiframe_prog_mono inf_prog_lower mem_Collect_eq mono_def order_subst1)
|
||||
thm antiframe_prog_monoI[THEN order_trans]
|
||||
thm order_trans[OF antiframe_prog_monoI]
|
||||
apply (rule order_trans)
|
||||
oops
|
||||
|
||||
lemma
|
||||
assumes vwb_lens: \<open>vwb_lens G\<close>
|
||||
assumes modifies: \<open>G:[body] = body\<close>
|
||||
shows \<open>G:[WHILE b DO body OD] = WHILE b DO body OD\<close>
|
||||
unfolding while_lfp_prog_mu_prog lfp_prog_alt_def
|
||||
apply (rule antisym)
|
||||
apply (rule inf_prog_lower)
|
||||
apply auto
|
||||
apply (subst lfp_prog_alt_def[THEN sym])
|
||||
apply (subst lfp_prog_unfold)
|
||||
apply (fold lfp_prog_alt_def)
|
||||
apply (simp add: Mono_progI if_prog_monoI seq_prog_monoI)
|
||||
apply (subst If_prog_anti_frame_prog_distr[THEN sym])
|
||||
apply (subst seq_prog_anti_frame_prog_distr[THEN sym])
|
||||
defer
|
||||
defer
|
||||
apply (unfold modifies)
|
||||
apply (subst algebraic_laws_prog.SKIP_prog_anti_frame_prog_modifies)
|
||||
defer
|
||||
apply simp
|
||||
unfolding lfp_prog_alt_def
|
||||
apply (subst anti_frame_is_continues)
|
||||
defer
|
||||
|
||||
apply (rule lfp_prog_greatest)
|
||||
thm lfp_prog_greatest
|
||||
apply auto
|
||||
apply (subst anti_frame_is_continues[THEN sym])
|
||||
thm monoI
|
||||
oops
|
||||
|
||||
end
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ begin
|
|||
|
||||
section \<open>Program Type\<close>
|
||||
|
||||
typedef '\<alpha> aprog = "{P :: '\<alpha> abr_prog. abrh P = P}"
|
||||
typedef ('s, 'e) aprog = "{P :: ('s, 'e) abr_prog. abrh P = P}"
|
||||
by (rule exI[where x= "abrh MAGIC"], simp)
|
||||
|
||||
named_theorems aprog_rep_eq
|
||||
|
|
@ -38,11 +38,11 @@ setup_lifting type_definition_aprog
|
|||
|
||||
section \<open>The Order\<close>
|
||||
|
||||
instantiation aprog :: (type) refine
|
||||
instantiation aprog :: (type,type) refine
|
||||
begin
|
||||
lift_definition less_eq_aprog :: "'a aprog \<Rightarrow> 'a aprog \<Rightarrow> bool" is
|
||||
lift_definition less_eq_aprog :: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> bool" is
|
||||
"op \<le>" .
|
||||
lift_definition less_aprog :: "'a aprog \<Rightarrow> 'a aprog \<Rightarrow> bool" is
|
||||
lift_definition less_aprog :: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> bool" is
|
||||
"op <" .
|
||||
instance
|
||||
apply (intro_classes)
|
||||
|
|
@ -76,29 +76,30 @@ subsection \<open>Abort\<close>
|
|||
|
||||
no_notation abort ("ABORT")
|
||||
|
||||
lift_definition abort_a :: "'\<alpha> aprog" ("ABORT") is "abrh utp_prog.abort" by simp
|
||||
lift_definition abort_a :: "('s, 'e) aprog" ("ABORT") is "abrh utp_prog.abort" by simp
|
||||
|
||||
subsection \<open>Magic\<close>
|
||||
|
||||
no_notation magic ("MAGIC")
|
||||
|
||||
lift_definition magic_a :: "'\<alpha> aprog" ("MAGIC") is "abrh utp_prog.magic" by simp
|
||||
lift_definition magic_a :: "('s, 'e) aprog" ("MAGIC") is "abrh utp_prog.magic" by simp
|
||||
|
||||
subsection \<open>Skip\<close>
|
||||
|
||||
no_notation skip ("SKIP")
|
||||
|
||||
lift_definition skip_a :: "'\<alpha> aprog" ("SKIP")is "utp_prog.skip" by simp
|
||||
lift_definition skip_a :: "('s, 'e) aprog" ("SKIP")is "utp_prog.skip" by simp
|
||||
|
||||
subsection \<open>Throw\<close>
|
||||
no_notation throw_abr ("THROW")
|
||||
lift_definition throw_a :: "'\<alpha> aprog" ("THROW")is "throw_abr" unfolding throw_abr_def by simp
|
||||
no_notation throw_abr ("THROW '(_')")
|
||||
lift_definition throw_a :: "'e \<Rightarrow> ('s, 'e) aprog" ("THROW '(_')")is "throw_abr" unfolding throw_abr_def by simp
|
||||
|
||||
subsection \<open>Sequence\<close>
|
||||
|
||||
purge_notation pseq (infixr ";" 71)
|
||||
|
||||
lift_definition seq_a :: "'\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" (infixr ";" 71) is "pseq" by (simp add: closure)
|
||||
lift_definition seq_a :: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" (infixr ";" 71) is
|
||||
"pseq" by (simp add: closure)
|
||||
|
||||
subsection \<open>Assignment\<close>
|
||||
|
||||
|
|
@ -107,7 +108,7 @@ no_notation passigns ("\<langle>_\<rangle>\<^sub>a")
|
|||
no_notation assigns_r ("\<langle>_\<rangle>\<^sub>a")
|
||||
no_notation uassigns("\<langle>_\<rangle>\<^sub>a")
|
||||
|
||||
lift_definition assigns_a :: "'\<alpha> usubst \<Rightarrow> '\<alpha> aprog" ("\<langle>_\<rangle>\<^sub>a") is "assigns_abr" unfolding assigns_abr_def by simp
|
||||
lift_definition assigns_a :: "'s usubst \<Rightarrow> ('s, 'e) aprog" ("\<langle>_\<rangle>\<^sub>a") is "assigns_abr" unfolding assigns_abr_def by simp
|
||||
subsubsection \<open>Syntax Translations\<close>
|
||||
|
||||
adhoc_overloading
|
||||
|
|
@ -119,7 +120,7 @@ translations
|
|||
|
||||
subsection \<open>Substitution\<close>
|
||||
|
||||
lift_definition subst_a :: "'\<alpha> usubst \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" is
|
||||
lift_definition subst_a :: "'s usubst \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" is
|
||||
"\<lambda> \<sigma> P. abrh (psubst (\<sigma> \<oplus>\<^sub>s \<Sigma>\<^sub>A\<^sub>B\<^sub>R) ( P))"
|
||||
by simp
|
||||
|
||||
|
|
@ -129,7 +130,7 @@ subsection \<open>Conditional\<close>
|
|||
|
||||
no_notation pcond_prog ("IF (_)/ THEN (_) ELSE (_) FI")
|
||||
|
||||
lift_definition cond_a :: "'\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" ("IF (_)/ THEN (_) ELSE (_) FI")
|
||||
lift_definition cond_a :: "'s cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" ("IF (_)/ THEN (_) ELSE (_) FI")
|
||||
is "if_abr"
|
||||
unfolding if_abr_def
|
||||
by (simp add: prog_rep_eq abrh_def utp_pred_laws.cond_distr)
|
||||
|
|
@ -138,56 +139,56 @@ subsection \<open>assert and assume\<close>
|
|||
|
||||
no_notation passume_prog ("_\<^sup>\<top>\<^sup>P")
|
||||
|
||||
abbreviation assume_a :: "'\<alpha> upred \<Rightarrow> '\<alpha> aprog" ("_\<^sup>\<top>\<^sup>P")
|
||||
abbreviation assume_a :: "'s upred \<Rightarrow> ('s, 'e) aprog" ("_\<^sup>\<top>\<^sup>P")
|
||||
where "assume_a c \<equiv> (IF c THEN SKIP ELSE MAGIC FI)"
|
||||
|
||||
no_notation passert_prog ("_\<^sub>\<bottom>\<^sub>P")
|
||||
|
||||
abbreviation assert_a :: "'\<alpha> upred \<Rightarrow> '\<alpha> aprog" ("_\<^sub>\<bottom>\<^sub>P")
|
||||
abbreviation assert_a :: "'s upred \<Rightarrow> ('s, 'e) aprog" ("_\<^sub>\<bottom>\<^sub>P")
|
||||
where "assert_a c \<equiv> (IF c THEN SKIP ELSE ABORT FI)"
|
||||
|
||||
subsection \<open>try catch\<close>
|
||||
|
||||
lift_definition try_catch_a :: "'\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" ("TRY (_)/ CATCH (_) END")
|
||||
lift_definition try_catch_a :: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" ("TRY (_)/ CATCH (_) END")
|
||||
is "try_catch_abr"
|
||||
unfolding try_catch_abr_def by simp
|
||||
|
||||
|
||||
subsection \<open>Lattices\<close>
|
||||
|
||||
lift_definition Lower_a:: "'\<alpha> aprog set \<Rightarrow> '\<alpha> aprog set"
|
||||
lift_definition Lower_a:: "('s, 'e) aprog set \<Rightarrow> ('s, 'e) aprog set"
|
||||
is "Lower_abr"
|
||||
by (simp add: Lower_abr_def)
|
||||
|
||||
lift_definition Upper_a:: "'\<alpha> aprog set \<Rightarrow> '\<alpha> aprog set"
|
||||
lift_definition Upper_a:: "('s, 'e) aprog set \<Rightarrow> ('s, 'e) aprog set"
|
||||
is "Upper_abr"
|
||||
by (simp add: Upper_abr_def)
|
||||
|
||||
lift_definition least_a:: " '\<alpha> aprog \<Rightarrow> ('\<alpha> aprog) set \<Rightarrow> bool"
|
||||
lift_definition least_a:: "('s, 'e) aprog \<Rightarrow> (('s, 'e) aprog) set \<Rightarrow> bool"
|
||||
is "least_abr".
|
||||
|
||||
lift_definition greatest_a:: " '\<alpha> aprog \<Rightarrow> ('\<alpha> aprog) set \<Rightarrow> bool"
|
||||
lift_definition greatest_a:: " ('s, 'e) aprog \<Rightarrow> (('s, 'e) aprog) set \<Rightarrow> bool"
|
||||
is "greatest_abr".
|
||||
|
||||
lift_definition inf_a :: "('\<alpha> aprog) set \<Rightarrow> '\<alpha> aprog" ("\<Sqinter>\<^sub>a_" [900] 900)
|
||||
lift_definition inf_a :: "(('s, 'e) aprog) set \<Rightarrow> ('s, 'e) aprog" ("\<Sqinter>\<^sub>a_" [900] 900)
|
||||
is "inf_abr"
|
||||
by (simp add: inf_abr_prog_is_abrh subsetI)
|
||||
|
||||
lift_definition sup_a :: "('\<alpha> aprog) set \<Rightarrow> '\<alpha> aprog" ("\<Squnion>\<^sub>a_" [900] 900)
|
||||
lift_definition sup_a :: "(('s, 'e) aprog) set \<Rightarrow> ('s, 'e) aprog" ("\<Squnion>\<^sub>a_" [900] 900)
|
||||
is "sup_abr"
|
||||
by (simp add: subsetI sup_abr_prog_is_abrh)
|
||||
|
||||
lift_definition meet_a:: "'\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" (infixl "\<sqinter>\<^sub>p" 70)
|
||||
lift_definition meet_a:: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" (infixl "\<sqinter>\<^sub>p" 70)
|
||||
is "meet_abr_prog"
|
||||
by (simp add: closure)
|
||||
|
||||
lift_definition join_a:: "'\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" (infixl "\<squnion>\<^sub>p" 65)
|
||||
lift_definition join_a:: "('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" (infixl "\<squnion>\<^sub>p" 65)
|
||||
is "join_abr_prog"
|
||||
by (simp add: closure)
|
||||
|
||||
subsection \<open>fixed points\<close>
|
||||
|
||||
lift_definition lfp_a :: "('\<alpha> aprog \<Rightarrow> '\<alpha> aprog) \<Rightarrow> '\<alpha> aprog"
|
||||
lift_definition lfp_a :: "(('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog) \<Rightarrow> ('s, 'e) aprog"
|
||||
is "LFP_abr"
|
||||
apply (subst (3) lfp_abr_healthy_comp)
|
||||
apply (subst (4) lfp_abr_healthy_comp)
|
||||
|
|
@ -195,7 +196,7 @@ lift_definition lfp_a :: "('\<alpha> aprog \<Rightarrow> '\<alpha> aprog) \<Righ
|
|||
apply (simp_all add: comp_def lfp_abr_prog_is_abrh)
|
||||
done
|
||||
|
||||
lift_definition gfp_a :: "('\<alpha> aprog \<Rightarrow> '\<alpha> aprog) \<Rightarrow> '\<alpha> aprog"
|
||||
lift_definition gfp_a :: "(('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog) \<Rightarrow> ('s, 'e) aprog"
|
||||
is "GFP_abr"
|
||||
apply (subst (3) gfp_abr_healthy_comp)
|
||||
apply (subst (4) gfp_abr_healthy_comp)
|
||||
|
|
@ -221,75 +222,75 @@ subsection \<open>Iterations\<close>
|
|||
|
||||
no_notation from_until_lfp_prog ("FROM (_)/ UNTIL (_)/ DO (_) OD")
|
||||
definition from_until_lfp_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FROM (_)/ UNTIL (_)/ DO (_) OD")
|
||||
where "FROM init UNTIL exit DO body OD = init ; (\<mu>\<^sub>a X \<bullet> IF \<not> exit THEN (body ; X) ELSE SKIP FI)"
|
||||
|
||||
no_notation from_until_lfp_invr_prog("FROM (_)/ INVAR (_)/ UNTIL (_)/ DO (_) OD")
|
||||
definition from_until_lfp_invr_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FROM (_)/ INVAR (_)/ UNTIL (_)/ DO (_) OD")
|
||||
where "FROM init INVAR invar UNTIL exit DO body OD = FROM init UNTIL exit DO body OD"
|
||||
|
||||
no_notation from_until_lfp_invr_vrt_prog("FROM (_)/ INVAR (_)/ VRT (_)/ UNTIL (_)/ DO (_) OD")
|
||||
definition from_until_lfp_invr_vrt_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> ('t,'\<alpha>) uexpr \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('t,'s) uexpr \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FROM (_)/ INVAR (_)/ VRT (_)/ UNTIL (_)/ DO (_) OD")
|
||||
where "FROM init INVAR invar VRT vari UNTIL exit DO body OD = FROM init UNTIL exit DO body OD"
|
||||
|
||||
no_notation while_lfp_prog("WHILE (_)/ DO (_) OD")
|
||||
definition while_lfp_a ::
|
||||
"'\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"'s cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("WHILE (_)/ DO (_) OD")
|
||||
where "WHILE b DO body OD = FROM SKIP UNTIL \<not>b DO body OD"
|
||||
|
||||
no_notation while_lfp_invr_prog ("INVAR (_)/ WHILE (_)/ DO (_) OD")
|
||||
definition while_lfp_invr_a ::
|
||||
"'\<alpha> cond \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"'s cond \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("INVAR (_)/ WHILE (_)/ DO (_) OD")
|
||||
where "INVAR invar WHILE b DO body OD = WHILE b DO body OD"
|
||||
|
||||
no_notation while_lfp_invr_vrt_prog ("INVAR (_)/ VRT (_)/ WHILE (_)/ DO (_) OD")
|
||||
definition while_lfp_invr_vrt_a ::
|
||||
"'\<alpha> cond \<Rightarrow> ('t,'\<alpha>) uexpr \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"'s cond \<Rightarrow> ('t,'s) uexpr \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("INVAR (_)/ VRT (_)/ WHILE (_)/ DO (_) OD")
|
||||
where "INVAR invar VRT vari WHILE b DO body OD = WHILE b DO body OD"
|
||||
|
||||
no_notation do_while_lfp_prog ("DO (_)/ WHILE (_) OD")
|
||||
definition do_while_lfp_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog"
|
||||
("DO (_)/ WHILE (_) OD")
|
||||
where "DO body WHILE b OD = FROM body UNTIL \<not> b DO body OD"
|
||||
|
||||
no_notation do_while_lfp_invr_prog ("DO (_)/ INVAR (_)/ WHILE (_) OD")
|
||||
definition do_while_lfp_invr_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog"
|
||||
("DO (_)/ INVAR (_)/ WHILE (_) OD")
|
||||
where "DO body INVAR invar WHILE b OD = DO body WHILE b OD"
|
||||
|
||||
no_notation do_while_lfp_invr_vrt_prog ("DO (_)/ INVAR (_)/ VRT (_)/ WHILE (_) OD")
|
||||
definition do_while_lfp_invr_vrt_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> ('t,'\<alpha>) uexpr \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('t,'s) uexpr \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog"
|
||||
("DO (_)/ INVAR (_)/ VRT (_)/ WHILE (_) OD")
|
||||
where "DO body INVAR invar VRT vari WHILE b OD = DO body WHILE b OD"
|
||||
|
||||
no_notation for_lfp_prog ("FOR ('(_,_,_'))/ DO (_) OD")
|
||||
definition for_lfp_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FOR ('(_,_,_'))/ DO (_) OD")
|
||||
where "FOR (init, b, incr) DO body OD = FROM init UNTIL \<not> b DO body ; incr OD"
|
||||
|
||||
no_notation for_lfp_invr_prog ("FOR ('(_,_,_'))/ INVAR (_)/ DO (_) OD")
|
||||
|
||||
definition for_lfp_invr_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FOR ('(_,_,_'))/ INVAR (_)/ DO (_) OD")
|
||||
where "FOR (init, b, incr) INVAR invar DO body OD = FOR (init, b, incr) DO body OD"
|
||||
|
||||
no_notation for_lfp_invr_vrt_prog ("FOR ('(_,_,_'))/ INVAR (_)/ VRT (_)/ DO (_) OD")
|
||||
|
||||
definition for_lfp_invr_vrt_a ::
|
||||
"'\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> ('t,'\<alpha>) uexpr \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog"
|
||||
"('s, 'e) aprog \<Rightarrow> 's cond \<Rightarrow> ('s, 'e) aprog \<Rightarrow> '\<alpha> cond \<Rightarrow> ('t,'s) uexpr \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog"
|
||||
("FOR ('(_,_,_'))/ INVAR (_)/ VRT (_)/ DO (_) OD")
|
||||
where "FOR (init, b, incr) INVAR invar VRT vari DO body OD = FOR (init, b, incr) DO body OD"
|
||||
|
||||
|
|
@ -301,11 +302,11 @@ abbreviation
|
|||
"anti_frame_abr x P \<equiv> abrh (pantiframe_prog (lens_comp x \<Sigma>\<^sub>A\<^sub>B\<^sub>R) P)"
|
||||
no_notation pframe_prog ("RESTOR (_)/ DO (_) OD")
|
||||
|
||||
lift_definition frame_a :: "('a \<Longrightarrow> '\<alpha>) \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" ("RESTOR (_)/ DO (_) OD") is
|
||||
lift_definition frame_a :: "('a \<Longrightarrow> 's) \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" ("RESTOR (_)/ DO (_) OD") is
|
||||
"frame_abr " by simp
|
||||
no_notation pantiframe_prog ("MODIFY (_)/ DO (_) OD")
|
||||
|
||||
lift_definition antiframe_a :: "('a \<Longrightarrow> '\<alpha>) \<Rightarrow> '\<alpha> aprog \<Rightarrow> '\<alpha> aprog" ("MODIFY (_)/ DO (_) OD") is
|
||||
lift_definition antiframe_a :: "('a \<Longrightarrow> 's) \<Rightarrow> ('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog" ("MODIFY (_)/ DO (_) OD") is
|
||||
"anti_frame_abr" by simp
|
||||
|
||||
translations
|
||||
|
|
@ -315,7 +316,7 @@ translations
|
|||
"_antiframe (_salphaset (_salphamk x)) P" <= "CONST antiframe_a x P"
|
||||
|
||||
subsection \<open>monotonicity for PROG\<close>
|
||||
lift_definition mono_a::"('a aprog \<Rightarrow> 'a aprog) \<Rightarrow> bool" is
|
||||
lift_definition mono_a::"(('s, 'e) aprog \<Rightarrow> ('s, 'e) aprog) \<Rightarrow> bool" is
|
||||
"mono_abr_prog"
|
||||
unfolding prog_order_def abrh_hcond_def
|
||||
by (simp add: isotone_def)
|
||||
|
|
@ -346,7 +347,7 @@ declare antiframe_a.rep_eq [aprog_rep_eq]
|
|||
declare psubst.rep_eq [aprog_rep_eq]
|
||||
|
||||
section \<open>Substitution Laws\<close>
|
||||
sledgehammer_params[stop_on_first,parallel_subgoals, join_subgoals, timeout = 60]
|
||||
(*sledgehammer_params[stop_on_first,parallel_subgoals, join_subgoals, timeout = 60]*)
|
||||
|
||||
lemma psubst_seq [usubst]:
|
||||
"\<sigma> \<dagger> (P ; Q) = (\<sigma> \<dagger> P) ; Q"
|
||||
|
|
@ -379,8 +380,9 @@ theorem magic_a_left_zero [simp]:
|
|||
apply (metis Rep_prog_abrh_closed abrh_def comp_prog_if_prog_left_distr if_prog_L6 if_prog_assoc magic_left_zero pseq.rep_eq skip_prog_left_unit)
|
||||
done
|
||||
|
||||
|
||||
lemma seq_a_throw_a_try_catch1:
|
||||
"TRY THROW CATCH Q END = Q"
|
||||
"TRY THROW(e) CATCH Q END = Q"
|
||||
apply transfer
|
||||
unfolding throw_abr_def abrh_def assigns_abr_def try_catch_abr_def
|
||||
apply ptransfer
|
||||
|
|
@ -388,9 +390,34 @@ lemma seq_a_throw_a_try_catch1:
|
|||
apply transfer
|
||||
apply auto
|
||||
unfolding Healthy_def H1_def H3_def
|
||||
apply (rel_simp, metis)+
|
||||
done
|
||||
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
apply metis
|
||||
apply rel_simp
|
||||
a
|
||||
|
||||
oops
|
||||
|
||||
lemma
|
||||
"TRY THROW(e) CATCH Q END = Q"
|
||||
apply transfer
|
||||
unfolding try_catch_abr_def throw_abr_def abrh_def
|
||||
apply (subst comp_prog_if_prog_skip_prog_distr_right)
|
||||
apply (subst if_prog_L6)
|
||||
thm blahblahblah1[of "abrupt" _]
|
||||
apply (rule blahblahblah1[of "abrupt" _ ])
|
||||
|
||||
oops
|
||||
lemma throw_left_zero:
|
||||
"THROW; P = THROW"
|
||||
apply transfer
|
||||
|
|
|
|||
|
|
@ -32,8 +32,8 @@ text
|
|||
\<^item> abrupt: a boolean variable used to specify if the program is in an abrupt state or not.
|
||||
\end{itemize}\<close>
|
||||
|
||||
alphabet abr_vars =
|
||||
abrupt :: bool
|
||||
alphabet 'e abr_vars =
|
||||
abrupt :: \<open>'e option\<close>
|
||||
|
||||
declare abr_vars.splits [alpha_splits]
|
||||
|
||||
|
|
@ -63,14 +63,14 @@ done
|
|||
|
||||
subsection \<open>Type lifting\<close>
|
||||
|
||||
type_synonym '\<alpha> abr_prog = "'\<alpha> abr_vars_scheme prog"
|
||||
type_synonym '\<alpha> abr = "'\<alpha> abr_vars_scheme"
|
||||
type_synonym ('s, 'e) abr_prog = "('e, 's) abr_vars_scheme prog"
|
||||
type_synonym ('s, 'e) abr = "('e , 's) abr_vars_scheme"
|
||||
|
||||
translations
|
||||
(type) "'\<alpha> abr" <= (type) "'\<alpha> abr_vars_scheme"
|
||||
(type) "'\<alpha> abr" <= (type) "'\<alpha> abr_vars_ext"
|
||||
(type) "'\<alpha> abr_prog" <= (type) "'\<alpha> abr_vars_scheme prog"
|
||||
(type) "'\<alpha> abr_prog" <= (type) "'\<alpha> abr_vars_ext prog"
|
||||
(type) "('s, 'e) abr" <= (type) "('e, 's) abr_vars_scheme"
|
||||
(type) "('s, 'e) abr" <= (type) "('e, 's) abr_vars_ext"
|
||||
(type) "('s, 'e) abr_prog" <= (type) "('e, 's) abr_vars_scheme prog"
|
||||
(type) "('s, 'e) abr_prog" <= (type) "('e, 's) abr_vars_ext prog"
|
||||
|
||||
|
||||
subsection \<open>Syntactic type setup\<close>
|
||||
|
|
@ -120,7 +120,7 @@ where "\<lfloor>P\<rfloor>\<^sub>>\<^sub>A\<^sub>B\<^sub>R \<equiv> \<lfloor>\<l
|
|||
section \<open>Healthiness conditions\<close>
|
||||
|
||||
definition abrh_def [upred_defs]:
|
||||
"abrh(P) = (IF &abrupt THEN SKIP ELSE P FI)"
|
||||
"abrh(P) = (IF &abrupt =\<^sub>u \<guillemotleft>None\<guillemotright> THEN SKIP ELSE P FI)"
|
||||
|
||||
lemma abrh_idem[simp]:"(abrh (abrh X)) = (abrh X)"
|
||||
unfolding abrh_def
|
||||
|
|
@ -193,8 +193,8 @@ subsubsection \<open>Algebraic laws\<close>
|
|||
|
||||
subsection \<open>Throw\<close>
|
||||
|
||||
definition throw_abr:: "'a abr_prog" ("THROW")
|
||||
where "throw_abr = abrh (passigns (subst_upd id abrupt (\<not>(&abrupt))))"
|
||||
definition throw_abr:: "'e \<Rightarrow> ('s, 'e) abr_prog" ("THROW '(_')")
|
||||
where "THROW(e) = abrh(passigns (subst_upd id abrupt (\<guillemotleft>Some e\<guillemotright>)))"
|
||||
|
||||
subsubsection \<open>Algebraic laws\<close>
|
||||
|
||||
|
|
@ -215,16 +215,21 @@ lemma pseq_abrh_closed [closure]: (*TODO @Yakoub: make this proof nicer with cl
|
|||
subsection \<open>Conditional\<close>
|
||||
|
||||
|
||||
definition if_abr :: "'a upred \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog"
|
||||
definition if_abr :: "'s upred \<Rightarrow> ('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog"
|
||||
where "if_abr b P Q = pcond_prog (b \<oplus>\<^sub>p \<Sigma>\<^sub>A\<^sub>B\<^sub>R) P Q"
|
||||
|
||||
subsubsection \<open>Algebraic laws\<close>
|
||||
|
||||
subsection \<open>Try catch\<close>
|
||||
|
||||
definition try_catch_abr:: "'a abr_prog \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog"
|
||||
definition try_catch_abr:: "('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog"
|
||||
where "try_catch_abr P Q =
|
||||
abrh (P ; pcond_prog (&abrupt) (passigns (subst_upd id abrupt (\<not> &abrupt)) ; Q) SKIP)"
|
||||
abrh (P ; pcond_prog (&abrupt =\<^sub>u \<guillemotleft>None\<guillemotright>) SKIP ((passigns (subst_upd id abrupt \<guillemotleft>None\<guillemotright>)) ; Q))"
|
||||
|
||||
term \<open>(passigns (subst_upd id abrupt \<guillemotleft>None\<guillemotright>)) ; Q\<close>
|
||||
(*definition try_catch_abr:: "'a abr_prog \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog"
|
||||
where "try_catch_abr P Q =
|
||||
abrh (P ; pcond_prog (&abrupt) (passigns (subst_upd id abrupt (\<not> &abrupt)) ; Q) SKIP)"*)
|
||||
|
||||
subsubsection \<open>Algebraic laws\<close>
|
||||
|
||||
|
|
@ -287,7 +292,7 @@ lemma upper_abr_prog_subset_upper_prog:
|
|||
|
||||
subsection \<open>Inf for exceptions\<close>
|
||||
|
||||
definition inf_abr :: "'a abr_prog set \<Rightarrow> 'a abr_prog" ("\<^bold>\<Sqinter>\<^sub>a_" [900] 900)
|
||||
definition inf_abr :: "('s, 'e) abr_prog set \<Rightarrow> ('s, 'e) abr_prog" ("\<^bold>\<Sqinter>\<^sub>a_" [900] 900)
|
||||
where "inf_abr A = (SOME x. greatest_abr x (Lower_abr A))"
|
||||
|
||||
subsubsection \<open>Algebraic laws\<close>
|
||||
|
|
@ -464,7 +469,7 @@ lemma inf_abr_prog_univ:
|
|||
|
||||
subsection \<open>Sup for exceptions\<close>
|
||||
|
||||
definition sup_abr :: "'a abr_prog set \<Rightarrow> 'a abr_prog" ("\<^bold>\<Squnion>\<^sub>a_" [900] 900)
|
||||
definition sup_abr :: "('s, 'e) abr_prog set \<Rightarrow> ('s, 'e) abr_prog" ("\<^bold>\<Squnion>\<^sub>a_" [900] 900)
|
||||
where "sup_abr A = (SOME x. least_abr x (Upper_abr A))"
|
||||
|
||||
subsubsection \<open>Algebraic laws\<close>
|
||||
|
|
@ -610,7 +615,7 @@ lemma sup_abr_prog_is_least_abr_prog_upper_abr:
|
|||
|
||||
subsection\<open>meet for exceptions theory\<close>
|
||||
|
||||
definition meet_abr_prog :: "'a abr_prog \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog" (infixl "\<^bold>\<sqinter>\<^sub>a" 70)
|
||||
definition meet_abr_prog :: "('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog" (infixl "\<^bold>\<sqinter>\<^sub>a" 70)
|
||||
where "meet_abr_prog a b = \<^bold>\<Sqinter>\<^sub>a{a, b}"
|
||||
|
||||
subsubsection\<open>algebraic laws\<close>
|
||||
|
|
@ -649,7 +654,7 @@ lemma le_meet_prog_abr_is_abrh[closure]:
|
|||
|
||||
subsection\<open>join for exception theory\<close>
|
||||
|
||||
definition join_abr_prog :: "'a abr_prog \<Rightarrow> 'a abr_prog \<Rightarrow> 'a abr_prog" (infixl "\<^bold>\<squnion>\<^sub>a" 70)
|
||||
definition join_abr_prog :: "('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog" (infixl "\<^bold>\<squnion>\<^sub>a" 70)
|
||||
where "join_abr_prog a b = \<^bold>\<Squnion>\<^sub>a{a, b}"
|
||||
|
||||
subsubsection\<open>algebraic laws\<close>
|
||||
|
|
@ -698,12 +703,12 @@ subsection \<open>setup for generalisation purpose\<close>
|
|||
|
||||
typedecl ABRH
|
||||
|
||||
abbreviation "ABRH \<equiv> UTHY(ABRH, '\<alpha> abr)"
|
||||
abbreviation "ABRH \<equiv> UTHY(ABRH, ('s, 'e) abr)"
|
||||
|
||||
definition abrh_hcond :: "(ABRH, '\<alpha> abr) uthy \<Rightarrow> ('\<alpha> abr) prog_health" where
|
||||
definition abrh_hcond :: "(ABRH, ('s, 'e) abr) uthy \<Rightarrow> (('s, 'e) abr) prog_health" where
|
||||
"abrh_hcond t = abrh"
|
||||
|
||||
definition abrh_unit :: "(ABRH, '\<alpha> abr) uthy \<Rightarrow> '\<alpha> abr_prog" where
|
||||
definition abrh_unit :: "(ABRH, ('s, 'e) abr) uthy \<Rightarrow> ('s, 'e) abr_prog" where
|
||||
[upred_defs]: "abrh_unit t = abrh SKIP"
|
||||
|
||||
subsubsection \<open>algebraic laws\<close>
|
||||
|
|
@ -807,7 +812,7 @@ section \<open>Fixed points for exceptions\<close>
|
|||
|
||||
subsection \<open>Least fixed point\<close>
|
||||
|
||||
definition LFP_abr :: " ('a abr_prog \<Rightarrow> 'a abr_prog) \<Rightarrow> 'a abr_prog"
|
||||
definition LFP_abr :: " (('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog) \<Rightarrow> ('s, 'e) abr_prog"
|
||||
where "LFP_abr F = \<^bold>\<Sqinter>\<^sub>a {x \<in> {P. abrh P = P} . F x \<sqsubseteq> x}"
|
||||
syntax
|
||||
"_amu" :: "pttrn \<Rightarrow> logic \<Rightarrow> logic" ("\<^bold>\<mu>\<^sub>a _ \<bullet> _" [0, 10] 10)
|
||||
|
|
@ -855,7 +860,7 @@ proof (rule antisym)
|
|||
proof -
|
||||
have 1: "\<And> P. F (abrh(P)) = abrh(F (abrh(P)))"
|
||||
proof -
|
||||
fix P :: "'a abr_prog"
|
||||
fix P :: "('b, 'a) abr_prog"
|
||||
have "abrh P \<in> {p. abrh p = p}"
|
||||
by (metis abr_abrh_closed)
|
||||
then have "F (abrh P) \<in> {p. abrh p = p}"
|
||||
|
|
@ -877,7 +882,7 @@ proof (rule antisym)
|
|||
qed
|
||||
have 1: "\<And> P. F (abrh(P)) = abrh(F (abrh(P)))"
|
||||
proof -
|
||||
fix P :: "'a abr_prog"
|
||||
fix P :: "('b, 'a) abr_prog"
|
||||
have "abrh P \<in> {p. abrh p = p}"
|
||||
by (metis abr_abrh_closed)
|
||||
then have "F (abrh P) \<in> {p. abrh p = p}"
|
||||
|
|
@ -1022,7 +1027,7 @@ qed
|
|||
|
||||
subsection \<open>greatest fixed point\<close>
|
||||
|
||||
definition GFP_abr :: " ('a abr_prog \<Rightarrow> 'a abr_prog) \<Rightarrow> 'a abr_prog"
|
||||
definition GFP_abr :: " (('s, 'e) abr_prog \<Rightarrow> ('s, 'e) abr_prog) \<Rightarrow> ('s, 'e) abr_prog"
|
||||
where "GFP_abr F = \<^bold>\<Squnion>\<^sub>a {x \<in> {P. abrh P = P} . x \<sqsubseteq> F x}"
|
||||
|
||||
syntax
|
||||
|
|
@ -1069,7 +1074,7 @@ proof (rule antisym)
|
|||
proof -
|
||||
have 1: "\<And> P. F (abrh(P)) = abrh(F (abrh(P)))"
|
||||
proof -
|
||||
fix P :: "'a abr_prog"
|
||||
fix P :: "('b,'a) abr_prog"
|
||||
have "abrh P \<in> {p. abrh p = p}"
|
||||
by (metis abr_abrh_closed)
|
||||
then have "F (abrh P) \<in> {p. abrh p = p}"
|
||||
|
|
@ -1089,7 +1094,7 @@ proof (rule antisym)
|
|||
qed
|
||||
have 1: "\<And> P. F (abrh(P)) = abrh(F (abrh(P)))"
|
||||
proof -
|
||||
fix P :: "'a abr_prog"
|
||||
fix P :: "('b,'a) abr_prog"
|
||||
have "abrh P \<in> {p. abrh p = p}"
|
||||
by (metis abr_abrh_closed)
|
||||
then have "F (abrh P) \<in> {p. abrh p = p}"
|
||||
|
|
@ -1343,5 +1348,5 @@ lemma "abrh(P) ; abrh (throw_abr ; if_abr (&abrupt) (passigns (subst_upd id ab
|
|||
apply (smt abr_vars.select_convs(2))
|
||||
done *)
|
||||
|
||||
|
||||
term \<open> Q \<and>(A \<oplus>\<^sub>p abrupt)\<close>
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue