theory Laws imports SOS begin

consts
bind :: "'a option => ('a => 'z option) => 'z option"
map' :: "('a => 'a option) => 'a list => 'a list option"
con_map :: "con => cterm list => cterm option"
x_term :: "(cterm list => cterm list option) => cterm  => cterm option"

primrec
"bind None f = None"
"bind (Some e) f = f e"

defs
map'_def: "map' f b == postMapAll (map f b)"
con_map_def: "con_map z b == (Some (C z b))"
x_term_def: "x_term f e == bind (f (children e)) (con_map (con_of e))"

axioms
map'_rule: "map' (sequence f f') b = bind (map' f b) (map' f')";



text {* algebra *}

lemma id_not_fail: "infallible id";
apply (unfold infallible_def);
apply (unfold fallible_def);
apply (unfold id_def);
apply (auto);
done;

lemma fail_none: "fallible fail";
apply (unfold fallible_def);
apply (unfold fail_def);
apply (auto);
done;


text {* sequence, id, fail *}

lemma id_row_lemma: "\<forall> (e::cterm). sequence id f e = f e";
apply (unfold sequence_def);
apply (insert id_lemma);
apply (auto);
done;

lemma id_row_or_reform: "sequence f id e = f e";
apply (unfold sequence_def);
apply (insert id_lemma);
apply (case_tac "f e = None");
apply (force);
apply (frule result_form_lemma [of "f e"]);
apply (auto);
done;

lemma sequence_left_unit_law: "sequence id s = s";
apply (insert id_row_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma id_row_or_lemma: "\<forall> (e::cterm). sequence f id e = f e";
apply (insert id_row_or_reform [of f]);
apply (auto);
done;

lemma sequence_right_unit_law: "sequence s id = s";
apply (insert id_row_or_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma id_sequence_law: "sequence s id = sequence id s";
apply (insert sequence_left_unit_law [of s]);
apply (insert sequence_right_unit_law [of s]);
apply (auto);
done;

lemma fail_row_reform: "sequence f fail e = fail e";
apply (unfold sequence_def);
apply (insert fail_lemma);
apply (frule_tac x=e in spec);
apply (case_tac "f e = None");
apply (auto);
done;

lemma fail_row_lemma: "\<forall> (e::cterm). sequence f fail e = fail e";
apply (insert fail_row_reform);
apply (auto);
done;

lemma sequence_right_zero_law: "sequence s fail = fail";
apply (insert fail_row_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma fail_row_or_lemma: "\<forall> (e::cterm). sequence fail f e = fail e";
apply (unfold sequence_def);
apply (insert fail_lemma);
apply (auto);
done;

lemma sequence_left_zero_law: "sequence fail s = fail";
apply (insert fail_row_or_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma fail_row_form_law: "sequence fail f = sequence f fail";
apply (insert sequence_right_zero_law [of f]);
apply (insert sequence_left_zero_law [of f])
apply (auto);
done;

lemma sequence_fail_left_lemma: "? (e::cterm). f e = None ==> ? (e::cterm). sequence f f' e = None";
apply (insert sequence_neg_1_sos);
apply (auto);
done;


text {* sequence does not fail, if f, f' not fail *}

lemma expr_row_lemma: "\<forall> (e::cterm). f e ~= None ==> sequence f f e ~= None";
apply (frule option_lemma [of f f e]);
apply (force);
apply (frule_tac someI_ex);
apply (frule_tac someI_ex);
back;
apply (frule sequence_main_lemma [of f e _ f]);
apply (insert result_form_lemma);
apply (auto);
done;

lemma expr_row_reform: "\<forall> (e::cterm). f e ~= None ==> (\<forall> (e::cterm). sequence f f e ~= None)";
apply (insert expr_row_lemma [of f]);
apply (auto);
done;

lemma sequence_not_fail_law: "infallible f ==> infallible (sequence f f)";
apply (insert expr_row_reform [of f]);
apply (insert infallible_law);
apply (auto);
done;

lemma rex_row_lemma: "[|\<forall> (e::cterm). f e ~= None; \<forall> (e::cterm). f' e ~= None |] ==> sequence f f' e ~= None";
apply (frule option_lemma [of f f' e]);
apply (force);
apply (frule_tac someI_ex);
apply (frule_tac someI_ex);
back;
apply (frule sequence_main_lemma [of f e _ f']);
apply (insert result_form_lemma);
apply (auto);
done;

lemma rex_row_reform: "[|\<forall> (e::cterm). f e ~= None; \<forall> (e::cterm). f' e ~= None |] ==> \<forall> (e::cterm). sequence f f' e ~= None";
apply (insert rex_row_lemma [of f f']);
apply (auto);
done;

lemma sequence_not_fail: "(infallible s \<and> infallible s') ==> infallible (sequence s s')";
apply (insert infallible_law);
apply (insert rex_row_reform);
apply (auto);
done;


text {* sequence may fail *}

lemma sequence_fail_left_law: "fallible f ==> fallible (sequence f f')";
apply (unfold fallible_def);
apply (insert sequence_fail_left_lemma);
apply (auto);
done;

lemma sequence_fail_right_lemma: "f e = Some e' & f' e' = None ==> sequence f f' e = None";
apply (unfold sequence_def);
apply (case_tac "f e = None");
apply (frule sequence_neg_1_sos [of f e f']);
apply (insert sequence_application_lemma [of f e e' f']);
apply (auto);
done;

lemma sequence_fail_right_reform: "f e = Some e' & f' e' = None ==> ? (e::cterm). sequence f f' e = None";
apply (insert sequence_fail_right_lemma [of f e e' f']);
apply (auto);
done;

lemma sequence_fail_right_law: "f e = Some e' & f' e' = None ==> fallible (sequence f f')";
apply (unfold fallible_def);
apply (insert sequence_fail_right_reform [of f e e' f']);
apply (auto);
done;

lemma sequence_fail_law: "(fallible f \<or>  (f e = Some e' & f' e' = None)) ==> fallible (sequence f f')";
apply (insert sequence_fail_left_law [of f f']);
apply (insert sequence_fail_right_law [of f e e' f']);
apply (auto);
done;


text {* sequence *}

lemma sequence_or_reform: "sequence (sequence f f') f'' e = sequence f (sequence f' f'') e";
apply (unfold sequence_def);
apply (case_tac "f e = None");
apply (auto);
done;

lemma sequence_or_lemma: "\<forall> (e::cterm). sequence (sequence f f') f'' e = sequence f (sequence f' f'') e";
apply (insert sequence_or_reform [of f f' f'']);
apply (auto);
done;

lemma sequence_or_law: "sequence (sequence f f') f'' = sequence f (sequence f' f'')";
apply (insert sequence_or_lemma [of f f' f'']);
apply (insert ext);
apply (auto);
done;

lemma sequence_assoc_law: "sequence s (sequence s' s'') = sequence (sequence s s') s''";
apply (insert sequence_or_law);
apply (auto);
done;

text {* choice does not fail, if f or f' not fail *}

lemma main_choice_not_fail_reform: "\<forall> (e::cterm). f e ~= None ==> choice f f e ~= None";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_not_fail_reform: "\<forall> (e::cterm). f e ~= None ==> (\<forall> (e::cterm). choice f f e ~= None)";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_not_fail_law: "infallible f ==> infallible (choice f f)";
apply (insert infallible_law);
apply (insert choice_def);
apply (auto);
done;

lemma main_choice_not_fail_right_reform: "(\<forall> (e::cterm). f e ~= None) ==> choice f f' e ~= None";
apply (unfold choice_def);
apply (auto);
done;

lemma main_choice_not_fail_left_reform: "(\<forall> (e::cterm). f' e ~= None) ==> choice f f' e ~= None";
apply (unfold choice_def);
apply (auto);
done;

lemma main_choice_not_fail_or_reform: "(\<forall> (e::cterm). f e ~= None) | (\<forall> (e::cterm). f' e ~= None) ==> choice f f' e ~= None";
apply (case_tac "\<forall> (e::cterm). f e ~= None");
apply (frule main_choice_not_fail_right_reform [of f f' e]);
apply (force);
apply (case_tac "\<forall> (e::cterm). f' e ~= None");
apply (frule main_choice_not_fail_left_reform [of f' f e]);
apply (simp);
apply (fast);
done;

lemma choice_not_fail_or_reform: "((\<forall> (e::cterm). f e ~= None) \<or> (\<forall> (e::cterm). f' e ~= None)) ==> \<forall> (e::cterm). choice f f' e ~= None";
apply (insert main_choice_not_fail_or_reform);
apply (auto);
done;

lemma choice_not_fail: "(infallible s \<or> infallible s') ==> infallible (choice s s')";
apply (insert infallible_law);
apply (insert choice_not_fail_or_reform);
apply (auto);
done;


text {* choice, id, fail *}

lemma choice_id_lemma: "\<forall> (e::cterm). choice id f e = id e";
apply (unfold choice_def);
apply (insert id_not_fail_lemma);
apply (auto);
done;

lemma choice_left_zero_law: "choice id s = id";
apply (insert choice_id_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma choice_id_not_fail_law: "infallible (choice id f)";
apply (insert choice_left_zero_law [of f]);
apply (insert id_not_fail);
apply (auto);
done;

lemma choice_fail_main_lemma: "\<forall> (e::cterm). choice fail f e = f e";
apply (unfold choice_def);
apply (insert fail_lemma);
apply (auto);
done;

lemma choice_left_unit_law: "choice fail s = s";
apply (insert choice_fail_main_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma choice_fail_or_lemma: "\<forall> (e::cterm). choice f fail e = f e";
apply (unfold choice_def);
apply (insert fail_lemma);
apply (auto);
done;

lemma choice_right_unit_law: "choice s fail = s";
apply (insert choice_fail_or_lemma [of s]);
apply (insert ext);
apply (auto);
done;

lemma choice_fail_form_law: "choice f fail = choice fail f";
apply (insert choice_right_unit_law [of f]);
apply (insert choice_left_unit_law [of f]);
apply (auto);
done;


text {* choice *}

lemma choice_or_reform: "choice (choice f f') f'' e = choice f (choice f' f'') e";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_or_lemma: "\<forall> (e::cterm). choice (choice f f') f'' e = choice f (choice f' f'') e";
apply (insert choice_or_reform [of f f' f'']);
apply (auto);
done;

lemma choice_or_law: "choice (choice f f') f''= choice f (choice f' f'')";
apply (insert choice_or_lemma [of f f' f'']);
apply (insert ext);
apply (auto);
done;

lemma  choice_assoc_law: "choice s (choice s' s'') = choice (choice s s') s''";apply (insert choice_or_law);
apply (auto);
done;

text {* sequence, choice *}

lemma sequence_choice_lemma: "f e = None ==> sequence f (choice f' f'') e = choice (sequence f f') (sequence f f'') e";
apply (frule sequence_neg_1_sos [of f e "choice f' f''"]);
apply (frule sequence_neg_1_sos [of f e f']);
apply (frule sequence_neg_1_sos [of f e f'']);
apply (insert choice_fail_sos [of "sequence f f'" e "sequence f f''"]);
apply (auto);
done;

lemma sequence_choice_reform: "[|f e = Some e'; f' e' = None|] ==> sequence f (choice f' f'') e = choice (sequence f f') (sequence f f'') e";
apply (frule sequence_application_lemma [of f _ _ f']);
apply (frule sequence_application_lemma [of f _ _ f'']);
apply (frule sequence_application_lemma [of f _ _ "choice f' f''"]);
apply (frule choice_partial_fail_reform [of f' _ f'']);
apply (case_tac "sequence f f' e = None");
apply (frule choice_partial_fail_reform [of "sequence f f'" _ "sequence f f''"]);
apply (auto);
done;

lemma sequence_choice_not_fail_lemma: "[|f e = Some e'; f' e' ~= None|] ==> sequence f (choice f' f'') e = choice (sequence f f') (sequence f f'') e";
apply (frule sequence_application_lemma [of f _ _ f']);
apply (frule sequence_application_lemma [of f _ _ f'']);
apply (frule sequence_application_lemma [of f _ _ "choice f' f''"]);
apply (frule choice_application_lemma [of f' _ f'']);
apply (case_tac "sequence f f' e ~= None");
apply (frule choice_application_lemma [of "sequence f f'" _ "sequence f f''"]);
apply (auto);
done;

lemma distr_left_lemma: "sequence f (choice f' f'') e = choice (sequence f f') (sequence f f'') e";
apply (case_tac "f e = None");
apply (insert sequence_choice_lemma [of f e f' f'']);
apply (force);
apply (frule result_form_lemma);
apply (frule_tac someI_ex);
apply (case_tac "f' (SOME x. f e = Some x) = None");
apply (frule sequence_choice_reform [of f e _ f' f'']);
apply (force);
apply (force);
apply (frule sequence_choice_not_fail_lemma [of f e _ f' f'']);
apply (auto);
done;

lemma distr_left_law: "sequence f (choice f' f'') = choice (sequence f f') (sequence f f'')";
apply (insert distr_left_lemma [of f f' f'']);
apply (insert ext);
apply (auto);
done;


text {* if f not fails for all terms, all with f applied to a term not fails *}

lemma all_expr_nil_lemma: "\<forall> (e::cterm). f e ~= None ==> all f (C z []) ~= None";
apply (unfold all_def);
apply (auto);
done;

lemma all_expr_cnr_lemma: "\<forall> (e::cterm). f e ~= None ==> all f (C z b) ~= None";
apply (insert all_expr_lemma [of f b _ z]);
apply (insert postMapAll_none_map_lemma [of f b]);
apply (auto);
done;

lemma all_expr_fail_lemma: "\<forall> (e::cterm). f e ~= None ==> all f e ~= None";
apply (insert con_of_children_lemma [of e]);
apply (insert all_expr_cnr_lemma [of f "con_of e" "children e"]);
apply (auto);
done;

lemma all_not_fail_law: "\<forall> (e::cterm). f e ~= None ==> \<forall> (e::cterm). all f e ~= None";
apply (insert all_expr_fail_lemma [of f]);
apply (auto);
done;

lemma all_not_fail: "infallible s ==> infallible (all s)";
apply (insert infallible_law);
apply (insert all_not_fail_law [of s]);
apply (auto);
done;


text {* all, id *}

lemma postMapAll_map_id_lemma: "postMapAll (map id b) ~= None";
apply (insert id_not_fail_lemma);
apply (insert postMapAll_none_map_lemma [of id b]);
apply (auto);
done;

lemma map_id_empty_case: "postMapAll (map id []) = Some []";
apply (auto);
done;

lemma map_id_not_empty_case: "postMapAll (map id b) = Some b ==> postMapAll (map id (e#b)) = Some (e#b)";
apply (insert map_form_lemma);
apply (insert id_lemma);
apply (auto);
done;

lemma map_id_lemma: "postMapAll (map id b) =  Some b";
apply (induct_tac b);
apply (insert map_id_not_empty_case);
apply (auto);
done;

lemma all_id_lemma: "all id e = id e";
apply (unfold all_def)
apply (insert postMapAll_map_id_lemma [of "children e"]);
apply (insert con_of_children_lemma [of e]);
apply (insert map_id_lemma [of "children e"]);
apply (insert id_lemma);
apply (auto);
done;

lemma all_id_law: "all id = id";
apply (insert all_id_lemma);
apply (insert ext);
apply (auto);
done;


text {* all *}

lemma all_fail_reform: "f x = None ==> all f (C z [x]) = None";
apply (unfold all_def);
apply (auto);
done;

lemma all_fail_main_reform: "? (x::cterm). f x = None ==> ? (x::cterm). all f x  = None";
apply (insert all_fail_reform);
apply (auto);
done;

lemma all_fail: "fallible f ==> fallible (all f)";
apply (unfold fallible_def);
apply (insert all_fail_reform [of f]);
apply (auto);
done;

lemma all_constant_law: "constant t ==> all s t = id t";
apply (unfold constant_def);
apply (unfold all_def);
apply (unfold id_def);
apply (insert con_of_children_lemma [of t]);
apply (auto);
done; 

lemma postMapAll_fail_reform: "postMapAll (map fail (e#b)) = None";
apply (insert fail_def);
apply (insert map_form_lemma [of fail e b]);
apply (auto);
done;

lemma postMapAll_fail_lemma: "b ~= [] ==> postMapAll (map fail b) = None";
apply (case_tac b);
apply (insert postMapAll_fail_reform);
apply (auto);
done;

lemma all_not_constant_law: "~(constant t) ==> all fail t = fail t";
apply (unfold constant_def);
apply (unfold all_def);
apply (unfold fail_def);
apply (frule postMapAll_fail_lemma [of "children t"]);
apply (insert con_of_children_lemma [of t]);
apply (auto);
done;

lemma all_con_lemma: "all s t = Some t' ==> con_of t = con_of t'";
apply (case_tac "postMapAll (map s (children t)) = None");
apply (unfold all_def);
apply (auto);
done;


text {* one *}

lemma one_empty_case: "b = [] ==> one f (C z b) = None";
apply (unfold one_def);
apply (auto);
done;

lemma one_unit_list_fail_case_lemma: "(unit_list None (map f b)) ==> one f (C z b) = None";
apply (insert map_one_unit_list_lemma [of f b]);
apply (drule mp);
apply (force);
apply (unfold one_def);
apply (auto);
done;

lemma one_unit_list_not_fail_case_lemma: "(postMapOne b (map f b) = Some b') ==> one f (C z b) = Some (C z b')";
apply (frule result_lemma);
apply (frule map_one_unit_list_or_main_lemma [of b f]);
apply (unfold one_def);
apply (auto);
done;

lemma unit_list_not_fail_lemma: "b ~= [] --> unit_list None (map fail b)";
apply (induct_tac b);
apply (insert fail_def);
apply (auto);
done;

lemma map_one_fail_empty_lemma: "postMapOne [] (map fail []) = None";
apply (auto);
done;

lemma map_one_fail_not_empty_lemma: "postMapOne b (map fail b) = None ==> postMapOne (e#b) (map fail (e#b)) = None";
apply (insert fail_def);
apply (auto);
done;

lemma map_one_fail_lemma: "postMapOne b (map fail b) = None";
apply (induct_tac b);
apply (insert map_one_fail_not_empty_lemma);
apply (auto);
done;

lemma one_not_fail_reform: "postMapOne b (map f b) = Some b' ==> one f (C z b) = Some (C z b')";
apply (unfold one_def);
apply (auto);
done;

lemma one_fail_lemma: "one fail e = fail e";
apply (unfold one_def);
apply (unfold fail_def);
apply (insert map_one_fail_lemma);
apply (auto);
done;

lemma one_fail_law: "one fail = fail";
apply (insert one_fail_lemma);
apply (insert ext);
apply (auto);
done;

lemma one_fail_main_lemma: "one f (C z []) = None";
apply (unfold one_def);
apply (auto);
done;

lemma one_fail_main_reform: "? (x::cterm). one f x = None";
apply (insert one_fail_main_lemma);
apply (auto);
done;

lemma one_fail: "fallible (one f)";
apply (unfold fallible_def);
apply (insert one_empty_case);
apply (auto);
done;

lemma one_constant_law: "constant t ==> one s t = fail t";
apply (unfold constant_def);
apply (unfold fail_def);
apply (insert one_fail_main_lemma [of s "con_of t"]);
apply (insert con_of_children_lemma [of t]);
apply (auto);
done;

lemma unit_list_id_map_not_empty_lemma: "b ~= [] --> ~unit_list None (map id b) --> (b ~= [] --> ~unit_list None (map id (e#b)))";
apply (insert id_not_fail_lemma);
apply (auto);
done;

lemma id_not_fail_none_reform: "None ~= id e";
apply (unfold id_def);
apply (auto);
done;

lemma unit_list_id_map_lemma: "b ~= [] --> ~unit_list None (map id b)";
apply (induct_tac b);
apply (clarify);
apply (insert unit_list_id_map_not_empty_lemma);
apply (insert id_not_fail_none_reform)
apply (auto);
done;

lemma map_one_id_empty_case: "postMapOne [] (map  id []) = None";
apply (auto);
done;

lemma map_one_id_not_empty_case: "(b ~= [] --> postMapOne b (map id b) = Some b) ==> postMapOne (e#b) (map id (e#b)) = Some (e#b)";
apply (insert id_lemma);
apply (auto);
done;

lemma map_one_id_lemma: "b ~= [] --> postMapOne b (map id b) = Some b";
apply (induct_tac b);
apply (insert map_one_id_empty_case);
apply (force);
apply (insert map_one_id_not_empty_case);
apply (auto);
done;

lemma one_not_constant_law: "~(constant t) ==> one id t = id t";
apply (unfold constant_def);
apply (unfold one_def);
apply (unfold id_def);
apply (insert unit_list_id_map_lemma [of "children t"]);
apply (insert map_one_id_lemma [of "children t"]);
apply (insert con_of_children_lemma [of t]);
apply (auto);
done;

lemma one_con_lemma: "one s t = Some t' ==> con_of t = con_of t'";
apply (case_tac "children t = []");
apply (insert one_fail_main_lemma [of s "con_of t"]);
apply (insert con_of_children_lemma [of t]);
apply (force);
apply (case_tac "postMapOne (children t) (map s (children t)) = None");
apply (unfold one_def);
apply (auto);
done;


text {* not *}

lemma not_id_fail_lemma: "\<forall> (e::cterm). not id e = fail e";
apply (insert id_def);
apply (insert fail_def);
apply (insert not_def);
apply (auto);
done;

lemma not_id_fail_reform: "not id = fail";
apply (insert not_id_fail_lemma);
apply (insert ext);
apply (auto);
done;

lemma not_fail_id_lemma: "\<forall> (e::cterm). not fail e = id e";
apply (insert fail_def);
apply (insert id_def);
apply (insert not_def);
apply (auto);
done;

lemma not_fail_id_reform: "not fail = id";
apply (insert not_fail_id_lemma);
apply (insert ext);
apply (auto);
done;

lemma one_id_fail_lemma: "one id (C 1 []) = None";
apply (unfold one_def);
apply (auto);
done;

lemma one_id_fail_reform: "? (e::cterm). one id e = None";
apply (insert one_id_fail_lemma);
apply (auto);
done;

lemma not_one_id_fail_lemma: "? (e::cterm). not (one id) e ~= None";
apply (unfold not_def);
apply (insert one_id_fail_reform);
apply (auto);
done;

lemma one_id_not_fail_lemma: "one id (C 1 [C 1 []]) ~= None";
apply (unfold one_def);
apply (insert id_lemma);
apply (auto);
done;

lemma one_id_not_fail_reform: "? (e::cterm). one id e ~= None";
apply (insert one_id_not_fail_lemma);
apply (auto);
done;

lemma not_one_id_fail_reform: "? (e::cterm). not (one id) e = None";
apply (unfold not_def);
apply (insert one_id_not_fail_reform);
apply (auto);
done;

lemma not_fail_reform: "fallible (not (one id))";
apply (unfold fallible_def);
apply (insert not_one_id_fail_lemma);
apply (insert not_one_id_fail_reform);
apply (auto);
done;


text {* a corrolary *}

lemma sequence_reform: "? (e'::cterm). ? (e''::cterm). x e = Some e' & z e' = Some e'' --> sequence x z e ~= None";
apply (insert sequence_pos_sos [of x e _ z]);
apply (auto);
done;


text {* sequence fails, if f or f' return None *}

lemma row_fail_or_lemma: "f e = None \<or> (? (e'::cterm). f e = Some e' & f' e' = None) ==> sequence f f' e = None";
apply (case_tac "f e = None");
apply (frule sequence_neg_1_sos [of f e f']);
apply (clarify);
apply (insert sequence_neg_2_sos [of f e _ f']);
apply (auto);
done;

lemma sequence_fail: "fallible f  ==> fallible (sequence f f')";
apply (unfold fallible_def);
apply (insert sequence_neg_1_sos [of f _ f']);
apply (auto);
done;


text {* all *}

lemma map_sequence_lemma: "x e = Some e' ==> y e' = sequence x y e";
apply (unfold sequence_def);
apply (auto);
done;

lemma map_lemma: "[|x e = Some e'; postMapAll (map x b) = Some b'|] ==> postMapAll (map x (e#b)) = Some (e'#b')";
apply (auto);
done;

lemma map_or_lemma: "[|x e = Some e'; postMapAll (map x (e#b)) = Some (e'#b')|] ==> postMapAll (map x b) = Some b'";
apply (case_tac "postMapAll (map x b) = None");
apply (auto);
done;

lemma postMapAll_id_lemma: "[|postMapAlll (map x (e#b)) = Some (e'#b'); postMapAlll (map x (e#b)) = Some (e''#b')|] ==> e' = e''";
apply (auto);
done;

lemma map_reform: "[|x e = Some e''; postMapAll (map x b) = Some b''; postMapAll (map x (e#b)) = Some (e'#b')|] ==> e' = e''";
apply (frule map_lemma [of x e e'' b b'']);
apply (auto);
done;

lemma postMapAll_main_lemma: "(postMapAll (map x (e#b)) = Some (e'#b')) ==> postMapAll (map x b) = Some b'";
apply (case_tac "x e = None");
apply (frule postMapAll_none_lemma [of x e b]);
apply (force);
apply (frule result_form_lemma);
apply (frule someI_ex);
apply (case_tac "postMapAll (map x b) = None");
apply (frule postMapAll_none_map_form_lemma [of x e b]);
apply (frule map_or_lemma [of x e _ b b']);
apply (frule map_reform [of x e _ b b']);
apply (auto);
done;

lemma postMapAll_or_lemma: "(postMapAll (map x (e#b)) = Some (e'#b')) ==> x e = Some e'";
apply (frule postMapAll_main_lemma [of x e b e' b']);
apply (case_tac "x e = None");
apply (frule postMapAll_none_lemma [of x e b]);
apply (auto);
done;

lemma postMapAll_form_lemma: "postMapAll (map x (e#b)) = postMapAll (x e#(map x b))";
apply (insert map_form_lemma [of x e b]);
apply (auto);
done;

lemma postMapAll_sequence_lemma: "[|x e = Some e'; postMapAll (map x b) = Some b'; postMapAll (map y b') = postMapAll (map (sequence x y) b)|] ==> postMapAll (y e'#(map y b')) = postMapAll (sequence x y e#(map (sequence x y) b))";
apply (frule map_lemma [of x e e' b b']);
apply (force);
apply (frule map_sequence_lemma [of x e _ y]);
apply (case_tac "y e' = None");
apply (auto);
done;

lemma postMapAll_sequence_reform: "(postMapAll (map x b) = Some b' --> postMapAll (map y b') = postMapAll (map (sequence x y) b)) ==> postMapAll (map x (e#b)) = Some (e'#b') --> postMapAll (map y (e'#b')) = postMapAll (map (sequence x y) (e#b))";
apply (insert postMapAll_form_lemma [of x e b]);
apply (insert postMapAll_form_lemma [of y e' b']);
apply (insert postMapAll_form_lemma [of "sequence x y" e b]);
apply (case_tac "postMapAll (map x (e#b)) = Some (e'#b')");
apply (frule postMapAll_main_lemma [of x e b e' b']);
apply (frule postMapAll_or_lemma [of x e b e' b']);
apply (frule postMapAll_sequence_lemma [of x e e' b b' y]);
apply (auto);
done;

lemma postMapAll_main_none_lemma: "(? (e::cterm). in_list e b & x e = None) ==> postMapAll (map x b) = None";
apply (frule in_list_main_lemma [of b x None]);
apply (insert postMapAll_lemma);
apply (auto);
done;

lemma postMapAll_in_list_main_lemma: "(? (e::cterm). in_list e b & x e = None) ==> (? (e::cterm). in_list e b & (sequence x y) e = None)";
apply (frule postMapAll_main_none_lemma);
apply (insert sequence_neg_1_sos [of x _ y]);
apply (auto);
done;

lemma postMapAll_main_none_or_lemma: "(? (e::cterm). in_list e b & x e = None) ==> postMapAll (map (sequence x y) b) = None";
apply (frule postMapAll_in_list_main_lemma [of b x y]);
apply (frule postMapAll_main_none_lemma [of b "sequence x y"]);
apply (auto);
done;

lemma all_none_lemma: "postMapAll (map f (children e)) = None --> all f e = None";
apply (unfold all_def);
apply (auto);
done;

lemma postMapAll_main_children_lemma: "(? (e::cterm). in_list e (children e') & x e = None) ==> sequence (all x) (all y) e' = None";
apply (insert con_of_children_lemma [of e']);
apply (frule postMapAll_main_none_lemma [of "children e'" x]);
apply (insert all_none_lemma [of x e']);
apply (frule mp);
apply (force);
apply (frule sequence_neg_1_sos [of "all x" e' "all y"]);
apply (auto);
done;

lemma postMapAll_main_children_or_lemma: "(? (e::cterm). in_list e (children e') & x e = None) ==> all (sequence x y) e' = None";
apply (insert con_of_children_lemma [of e']);
apply (frule postMapAll_main_none_or_lemma [of "children e'" x y]);
apply (insert all_none_lemma [of "sequence x y" e']);
apply (frule mp);
apply (auto);
done;

lemma sequence_all_none_lemma: "(? (e::cterm). in_list e (children e') & x e = None) ==> sequence (all x) (all y) e' = all (sequence x y) e'";
apply (frule postMapAll_main_children_lemma [of e' x y]);
apply (frule postMapAll_main_children_or_lemma [of e' x y]);
apply (auto);
done;

lemma postMapAll_children_lemma: "(\<forall> (e::cterm). in_list e (children e') --> x e ~= None) ==> (? (b::cterm list). postMapAll (map x (children e')) = Some b)";
apply (insert in_list_postMapAll_lemma [of "children e'" x]);
apply (auto);
done;

lemma postMapAll_children_or_lemma: "(postMapAll (map x (children e')) = Some b) ==> (all x e' = Some (C (con_of e') b))";
apply (unfold all_def);
apply (auto);
done;

lemma all_children_lemma: "(\<forall> (e::cterm). in_list e (children e') --> x e ~= None) ==> (? (b::cterm list). all x e' = Some (C (con_of e') b))";
apply (frule postMapAll_children_lemma [of e' x]);
apply (insert postMapAll_children_or_lemma [of x e']);
apply (auto);
done;

lemma all_children_or_lemma: "(\<forall> (e::cterm). in_list e (children e') --> x e ~= None) ==> (? (b::cterm list). sequence (all x) (all y) e' = all y (C (con_of e') b))";
apply (frule all_children_lemma [of e' x]);
apply (insert sequence_application_lemma [of "all x"]);
apply (auto);
done;

lemma postMapAll_none_lemma: "(postMapAll (map y b') = None) ==> all y (C (con_of e') b') = None";
apply (unfold all_def);
apply (auto);
done;

lemma postMapAll_not_fail_lemma: "(postMapAll (map y b') = Some b'') --> all y (C (con_of e') b') = Some (C (con_of e') b'')";
apply (unfold all_def);
apply (auto);
done;

lemma postMapAll_not_fail_or_lemma: "(postMapAll (map (sequence x y) (children e')) = Some b'') --> all (sequence x y) e' = Some (C (con_of e') b'')";
apply (unfold all_def);
apply (auto);
done;

lemma postMapAll_main_or_lemma: "(postMapAll (map y b') = postMapAll (map (sequence x y) (children e'))) ==> (postMapAll (map y b') = Some b'' --> all (sequence x y) e' = Some (C (con_of e') b''))";
apply (insert postMapAll_not_fail_or_lemma [of x y e' b'']);
apply (auto);
done;

lemma main_all_children_lemma: "[|all x e' = Some (C (con_of e') b'); postMapAll (map y b') = None|] ==> sequence (all x) (all y) e' = None";
apply (frule postMapAll_none_lemma [of y b' e']);
apply (insert sequence_application_lemma [of "all x" e' "C (con_of e') b'"]);
apply (auto);
done;

lemma main_all_children_or_lemma: "[|all x e' = Some (C (con_of e') b'); postMapAll (map y b') = Some b''|] ==> sequence (all x) (all y) e' = Some (C (con_of e') b'')";
apply (insert all_def [of y]);
apply (insert sequence_application_lemma [of "all x" e' "C (con_of e') b'" "all y"]);
apply (auto);
done;

lemma postMapAll_sequence_not_fail_lemma: "[|postMapAll (map x b) = Some b'; postMapAll (map y b') = postMapAll (map (sequence x y) b); postMapAll (map x (e#b)) = Some (e'#b')|] ==> postMapAll (map y (e'#b')) = postMapAll (map (sequence x y) (e#b))";
apply (insert postMapAll_sequence_reform [of x b b' y e e']);
apply (auto);
done;

lemma sequence_bind_lemma: "sequence x y e = bind (x e) y";
apply (unfold sequence_def);
apply (case_tac "x e = None");
apply (auto);
done;

lemma all_map'_bind_lemma: "all f (C z b) = bind (map' f b) (con_map z)";
apply (unfold all_def);
apply (unfold map'_def);
apply (insert con_map_def [of z]);
apply (case_tac " postMapAll (map f b) = None");
apply (auto);
done;

lemma all_map'_bind_reform: "all f e = x_term (map' f) e";
apply (unfold x_term_def);
apply (insert con_of_children_lemma [of  e]);
apply (insert all_map'_bind_lemma [of f "con_of e" "children e"]);
apply (auto);
done;

lemma all_map'_lemma: "all f = x_term (map' f)";
apply (insert all_map'_bind_reform [of f]);
apply (insert ext);
apply (auto);
done;

lemma bind_map'_none_lemma: "bind (bind None (con_map z)) (x_term (map' f)) = bind (bind None (map' f)) (con_map z)";
apply (auto);
done;

lemma bind_left_lemma: "bind (con_map z b) (x_term (map' f)) = bind (map' f b) (con_map z)";
apply (insert con_map_def [of z b]);
apply (insert x_term_def [of "map' f"]);
apply (auto);
done;

lemma bind_map'_not_fail_lemma: "bind (bind (Some b) (con_map z)) (x_term (map' f)) = bind (bind (Some b) (map' f)) (con_map z)";
apply (insert con_of_children_lemma [of  e]);
apply (insert x_term_def [of "map' f" "C z b"]);
apply (insert bind_left_lemma [of z b f]);
apply (auto);
done;

lemma bind_map'_lemma: "bind (bind b (con_map z)) (x_term (map' f)) = bind (bind b (map' f)) (con_map z)";
apply (case_tac "b = None");
apply (insert bind_map'_none_lemma [of z f]);
apply (insert bind_map'_not_fail_lemma [of _ z f]);
apply (auto);
done;

lemma all_map'_or_lemma: "(sequence (all x) (all y) e) = bind (x_term (map' x) e) (x_term (map' y)) ";
apply (insert sequence_bind_lemma [of "all x" "all y" e]);
apply (insert all_map'_lemma [of x]);
apply (insert all_map'_lemma [of y]);
apply (auto);
done;

lemma map'_or_lemma: "bind (x_term (map' x) e) (x_term (map' y)) = bind (bind (map' x (children e)) (con_map (con_of e))) (x_term (map' y))";
apply (insert x_term_def [of "map' x" e]);
apply (auto);
done;

lemma map'_lemma: "(sequence (all x) (all y) e) = bind (bind (map' x (children e)) (map' y)) (con_map (con_of e))";
apply (insert all_map'_or_lemma [of x y e]);
apply (insert map'_or_lemma [of x e y]);
apply (insert bind_map'_lemma [of "map' x (children e)" "con_of e"]);
apply (auto);
done;

lemma map'_or_lemma: "all (sequence x y) e = bind (bind (map' x (children e)) (map' y)) (con_map (con_of e))";
apply (insert all_map'_lemma [of "sequence x y"]);
apply (insert x_term_def [of "map' (sequence x y)" e]);
apply (insert map'_rule [of x y "children e"]);
apply (auto);
done;

lemma map'_id_lemma: "all (sequence x y) e = sequence (all x) (all y) e";
apply (insert map'_lemma [of x y e]);
apply (insert map'_or_lemma [of x y e]);
apply (auto);
done;

lemma all_fusion_law: "all (sequence x y) = sequence (all x) (all y)";
apply (insert map'_id_lemma [of x y]);
apply (insert ext);
apply (auto);
done;


text {* choice *}

lemma id_map_none_lemma: "b = [] ==> postMapOne b (map id b) = None";
apply (auto);
done;

lemma id_map_not_empty_lemma: "(b ~= [] --> postMapOne b (map id b) = Some b) ==> ((e#b) ~= [] --> postMapOne (e#b) (map id (e#b)) = Some (e#b))";
apply (insert id_lemma);
apply (auto);
done;

lemma id_map_lemma: "b ~= [] --> postMapOne b (map id b) = Some b";
apply (induct_tac b);
apply (insert id_map_not_empty_lemma);
apply (auto);
done;

lemma one_fail_reform: "(postMapOne (children e) (map f (children e)) = None) --> one f e = None";
apply (unfold one_def);
apply (auto);
done;

lemma one_id_lemma: "one id e ~= None ==> one id e = id e";
apply (insert con_of_children_lemma [of e]);
apply (case_tac "children e = []");
apply (frule id_map_none_lemma [of "children e"]);
apply (insert one_fail_reform [of e id]);
apply (frule mp);
apply (force);
apply (force);
apply (insert id_map_lemma [of "children e"]);
apply (frule mp);
back;
apply (force);
apply (frule one_unit_list_not_fail_case_lemma [of "children e" id _ "con_of e"]);
apply (unfold id_def);
apply (auto);
done;

lemma choice_lemma: "choice (one id) (not (one id)) e = id e";
apply (unfold id_def);
apply (case_tac "(one id) e = None");
apply (frule choice_partial_fail_reform [of "one id" e "not (one id)"]);
apply (insert not_id_lemma [of "one id" e]);
apply (force);
apply (frule choice_application_lemma [of "one id" e "not (one id)"]);
apply (frule one_id_lemma);
apply (insert id_lemma);
apply (auto);
done;

lemma choice_reform: "choice (one id) (not (one id)) = id";
apply (insert choice_lemma);
apply (insert ext);
apply (auto);
done;

lemma choice_not_fail_lemma: "infallible (choice (one id) (not (one id)))";
apply (insert id_not_fail);
apply (insert choice_reform);
apply (auto);
done;

lemma choice_fail: "(? (f::strategy). ? (f'::strategy). fallible f & fallible f' --> infallible (choice f f'))";
apply (insert one_fail);
apply (insert not_fail_reform);
apply (insert choice_not_fail_lemma);
apply (auto);
done;


end