theory SOS imports StrategyPrimitives begin


text {* strategy primitives are correct *}

lemma id_correct_sos: "id e = Some e"
apply (unfold id_def);
apply (auto);
done;

lemma fail_none_sos: "fail e = None";
apply (unfold fail_def);
apply (auto);
done;

lemma sequence_pos_sos: "x e = Some e' & z e' = Some e'' --> sequence x z e = Some e''";
apply (unfold sequence_def);
apply (auto);
done;

lemma sequence_neg_1_sos: "s t = None ==> sequence s s' t = None";
apply (unfold sequence_def);
apply (auto);
done;

lemma sequence_neg_2_sos: "(x e = Some e' & z e' = None) ==> sequence x z e = None";
apply (unfold sequence_def);
apply (auto);
done;

lemma choice_pos_sos: "(f e = Some e' --> choice f f' e =  Some e')";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_partial_fail_sos: "(f e = None & f' e = Some e' --> choice f f' e = Some e')";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_fail_sos: "f e = None & f' e = None --> choice f f' e = None";
apply (unfold choice_def);
apply (auto);
done;

lemma all_pos_sos: "(\<forall> (i::nat). 1 <= i & i <= n --> f (b i) = Some (b' i)) --> (all f (C z (vector n b)) = Some (C z (vector n b')))";
apply (unfold all_def);
apply (insert vector_postMapAll_main_lemma [of n f b b']);
apply (auto);
done;

lemma all_none_sos: "(? (i::nat). 1 <= i & i <= n & f (b i) = None) --> all f (C z (vector n b)) = None";
apply (unfold all_def);
apply (insert one_lemma);
apply (insert vector_postMapAll_main_or_lemma [of n f b]);
apply (auto);
done;

lemma one_not_fail_sos: "(? (i::nat). 1 <= i & i <= n & (\<forall> (i'::nat). 0 < i' & i' > i --> f (b i) = None) & f (b i) = Some (b' i) & (\<forall> (i'::nat). i' ~= i & i' <= n --> b' i = b i) & f (b i) = Some (b' i)) --> one f (C z (vector n b)) = Some (C z (vector n b'))";
apply (unfold one_def);
apply (insert vector_postMapOne_main_one_lemma [of n f b b']);
apply (auto);
done;

lemma one_fail_sos: "(\<forall> (i'::nat). 1 <= i' & i' <= n --> f (b i') = None) --> one f (C z (vector n b)) = None";
apply (unfold one_def);
apply (insert postMapOne_none_or_lemma [of n f b]);
apply (auto);
done;


end