From 65d8185b45daf087316898425ea498354c53cb05 Mon Sep 17 00:00:00 2001
From: Burkhart Wolff <wolffburkhart@gmail.com>
Date: Wed, 9 Oct 2024 13:00:23 +0200
Subject: [PATCH] Achims patch on recursive function return type
---
.../Clean/examples/SquareRoot_concept.thy | 2 +-
C11-BackEnds/Clean/src/Clean.thy | 4 +-
C11-BackEnds/Clean/src/Symbex_MonadSE.thy | 81 +++++++++++++++++++
3 files changed, 84 insertions(+), 3 deletions(-)
diff --git a/C11-BackEnds/Clean/examples/SquareRoot_concept.thy b/C11-BackEnds/Clean/examples/SquareRoot_concept.thy
index 49098e0ab..075e3874a 100644
--- a/C11-BackEnds/Clean/examples/SquareRoot_concept.thy
+++ b/C11-BackEnds/Clean/examples/SquareRoot_concept.thy
@@ -230,6 +230,6 @@ txt\<open>Instead of testing, we @{emph \<open>prove\<close>} that the test case
*)
oops
-text\<open>TODO: re-establish automatic test-coverage tactics of @{cite "DBLP:conf/tap/Keller18"}.\<close>
+text\<open>TODO: re-establish automatic test-coverage tactics of \cite{"DBLP:conf/tap/Keller18"}.\<close>
end
diff --git a/C11-BackEnds/Clean/src/Clean.thy b/C11-BackEnds/Clean/src/Clean.thy
index 226c1ae9c..2c8203d55 100644
--- a/C11-BackEnds/Clean/src/Clean.thy
+++ b/C11-BackEnds/Clean/src/Clean.thy
@@ -1216,12 +1216,12 @@ structure Function_Specification_Parser =
$ Const(read_constname ctxt (Binding.name_of pop_name),rmty))
val rhs_main_rec = wfrecT
measure
- (Abs(bdg_rec_name, (args_ty --> umty) ,
+ (Abs(bdg_rec_name, (args_ty --> rmty) ,
mk_pat_tupleabs params'
(Const(@{const_name "Clean.block\<^sub>C"}, umty-->umty-->rmty-->rmty)
$ Const(read_constname ctxt (Binding.name_of push_name),umty)
$ (Const(read_constname ctxt bdg_core_name,
- (args_ty --> umty) --> args_ty --> umty)
+ (args_ty --> rmty) --> args_ty --> umty)
$ (Bound (length params))
$ HOLogic.mk_tuple (map Free params'))
$ Const(read_constname ctxt (Binding.name_of pop_name),rmty))))
diff --git a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
index 0c05fa4a5..b163bf17c 100644
--- a/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
+++ b/C11-BackEnds/Clean/src/Symbex_MonadSE.thy
@@ -547,6 +547,87 @@ next
exec_mbindFStop_success list.set_intros(1) list.set_intros(2) valid_bind_cong)
qed
+
+
+lemma assert_suffix_seq :
+ "\<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p xs iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> \<forall>\<sigma>. P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q)))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (xs @ ys) iostep; assert\<^sub>S\<^sub>E (Q))"
+apply(subst mbind'_concat)
+unfolding bind_SE_def assert_SE_def valid_SE_def
+ apply(auto split: option.split option.split_asm, rename_tac "aa" "ba" "ab" "bb" )
+ apply (metis option.distinct(1))
+ by (meson option.distinct(1))
+
+lemma assert_suffix_seq2 :
+ "\<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p xs iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> (\<And> \<sigma>. P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q))))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (xs @ ys) iostep; assert\<^sub>S\<^sub>E (Q))"
+ by (simp add: assert_suffix_seq)
+
+lemma assert_suffix_seq_map :
+ "\<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (map f xs) iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> (\<And> \<sigma>. P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (map f ys) iostep; assert\<^sub>S\<^sub>E (Q))))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (map f (xs @ ys)) iostep; assert\<^sub>S\<^sub>E (Q))"
+ by (simp add: assert_suffix_seq)
+
+
+lemma assert_suffix_seq_tot :
+ "\<forall>x \<sigma>. iostep x \<sigma> \<noteq> None
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e xs iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> \<forall>\<sigma>. P \<sigma> \<longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q)))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (xs @ ys) iostep; assert\<^sub>S\<^sub>E (Q))"
+ apply(subst Symbex_MonadSE.mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e_vs_mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p, simp)
+ apply(subst (asm) Symbex_MonadSE.mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e_vs_mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p, simp)
+ by (simp add: assert_suffix_seq)
+
+lemma assert_suffix_seq_tot2 :
+ "(\<And> x \<sigma>. iostep x \<sigma> \<noteq> None)
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e xs iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> (\<And>\<sigma>. P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p ys iostep; assert\<^sub>S\<^sub>E (Q))))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (xs @ ys) iostep; assert\<^sub>S\<^sub>E (Q))"
+ by (simp add: assert_suffix_seq_tot)
+
+
+lemma assert_suffix_seq_tot3 :
+ "(\<And> x \<sigma>. iostep x \<sigma> \<noteq> None)
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (map f xs) iostep; assert\<^sub>S\<^sub>E (P))
+ \<Longrightarrow> (\<And>\<sigma>. P \<sigma> \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p (map f ys) iostep; assert\<^sub>S\<^sub>E (Q))))
+ \<Longrightarrow> \<sigma> \<Turnstile> ( _ \<leftarrow> mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>a\<^sub>v\<^sub>e (map f (xs @ ys)) iostep; assert\<^sub>S\<^sub>E (Q))"
+ by (simp add: assert_suffix_seq_tot)
+
+
+lemma assert_disch :
+ "(\<sigma> \<Turnstile> (_ \<leftarrow> iostep x; assert\<^sub>S\<^sub>E (Q))) =
+ (case iostep x \<sigma> of None \<Rightarrow> False | Some(_,\<sigma>') \<Rightarrow> Q \<sigma>')"
+ by (smt (verit, best) assert_simp bind_SE_def option.case_eq_if split_def valid_SE_def)
+
+lemma assert_disch_tot :
+ "\<forall>x \<sigma>. iostep x \<sigma> \<noteq> None \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> iostep x; assert\<^sub>S\<^sub>E (Q))) = (Q (snd(the(iostep x \<sigma>))))"
+ apply(subst assert_disch)
+ by (metis option.case_eq_if split_beta')
+
+lemma assert_disch_tot2 :
+ "(\<And>x \<sigma>. iostep x \<sigma> \<noteq> None) \<Longrightarrow> (\<sigma> \<Turnstile> (_ \<leftarrow> iostep x; assert\<^sub>S\<^sub>E (Q))) = (Q (snd(the(iostep x \<sigma>))))"
+ apply(subst assert_disch)
+ by (metis option.case_eq_if split_beta')
+
+lemma mbind_total_if_step_total :
+ "(\<And>x \<sigma>. x \<in> set S \<Longrightarrow> iostep x \<sigma> \<noteq> None) \<Longrightarrow> (\<And>\<sigma>. mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S iostep \<sigma> \<noteq> None)"
+proof(induct S)
+ case Nil
+ then show ?case by (simp add: unit_SE_def)
+next
+ case (Cons a S \<sigma>)
+ have 1 : "\<forall> x \<sigma>. x \<in> set S \<longrightarrow> iostep x \<sigma> \<noteq> None"
+ by (simp add: Cons.prems)
+ have 2 : "\<And>\<sigma>. mbind\<^sub>F\<^sub>a\<^sub>i\<^sub>l\<^sub>S\<^sub>t\<^sub>o\<^sub>p S iostep \<sigma> \<noteq> None"
+ using Cons.hyps Cons.prems by fastforce
+ then show ?case
+ apply(simp add : mbind'.simps(2) 1 2)
+ by (simp add: "2" Cons.prems option.case_eq_if split_beta')
+qed
+
subsection\<open>Miscellaneous\<close>
no_notation unit_SE ("(result _)" 8)
--
GitLab