theory Library imports Laws OncebuModel TopdownModel RepeatModel begin

consts
generalized_set :: "(strategy => cterm => result list => result) => strategy => (cterm \<times> result) set"
oncebottomup_step :: "strategy => cterm  => result list => result"
oncebottomup_set :: "strategy => (cterm \<times> result) set"
oncebottomup_fun :: "strategy => cterm  => result"

inductive "generalized_set f s"
intros
rule[intro!]:
"(\<forall> (t::cterm). in_list t (children p) --> (? (r::result). in_list (t,r) (zip (children p) rs) \<and> length (children p) = length rs \<and> (t,r):(generalized_set f s))) ==> (p,f s p rs):(generalized_set f s)"

defs
oncebottomup_step_def: "oncebottomup_step f e r == (case (postMapOne (children e) r) of None => f e | Some b => Some (C (con_of e) b))"
oncebottomup_set_def: "oncebottomup_set == generalized_set oncebottomup_step"


text {* a control strategy and combinators *}

consts
try :: "strategy => strategy"
all' ::  "strategy => cterm => cterm list"
one'::  "strategy => cterm => result"
one_of :: "strategy => cterm list => result"

defs
try_def: "try x e == choice x id e"
all'_def: "all' s t == (case (postMapAll (map s (children t))) of None => [] | (Some b) => b)"
one'_def: "one' s t == (case (children t) of [] => None | (e#b) => one_of s (e#b))"

primrec
"one_of x [] = None"
"one_of x (e#b) = (if x e = None then one_of x b else x e)"


text {* traversal schemes *}

consts
bottomup :: "strategy => strategy"
oncebu :: "strategy => strategy"
oncetd :: "strategy => strategy"
lookup :: "strategy => strategy"

axioms
bottomup_rule: " bottomup f = sequence (all (bottomup f)) f"
oncebu_rule: "oncebu f = choice (one (oncebu f)) f"
oncetd_rule: "oncetd f = choice f (one (oncetd f))"
lookup_rule: "lookup f = choice f (one' (lookup f))"


text {* id/fail *}

consts
fallible :: "(cterm \<times> result) set => bool"
infallible :: "(cterm \<times> result) set => bool"
succeedable :: "(cterm \<times> result) set => bool"
unsucceedable :: "(cterm \<times> result) set => bool"

defs
fallible_def: "fallible s == \<exists> (t::cterm). (t, None):s"
infallible_def: "infallible s == ~fallible s"
succeedable_def: "succeedable s == \<exists> (t::cterm). ~(t, None):s"
unsucceedable_def: "unsucceedable s == ~succeedable s"

lemma in_list_lemma[simp]: "(\<forall> (e'::cterm). in_list e' (children e) --> size e' < size e)" ;
apply (insert con_of_children_lemma [of e]);
apply (insert in_list_congr_main_lemma [of "children e" "con_of e"]);
apply (auto);
done;


text {* aspects *}

consts
relational :: "strategy => (cterm \<times> result) set"
in_term :: "cterm => cterm set"

axioms
relational_rule: "f e = e' == (e,e'):(relational f)";

recdef in_term "measure (\<lambda> e. size e)"
in_term_def:  "in_term e = (\<Union> (e'::cterm). (if in_list e' (children e) then in_term e' else {})) \<union> {e}";



text {* oncebottomup 

lemma oncebottomup_set_lemma: "generalized_set.rule = ((\<forall> (t::cterm). in_list t (children p) --> (? (r::result). in_list (t,r) (zip ts rs) \<and> length ts = length rs \<and> (t,r):(oncebottomup_set s))) ==> (p,oncebottomup_step s p rs):(oncebottomup_set s))"
apply (unfold oncebottomup_set_def);
apply (unfold generalized_set.rule);

*}


lemma oncebottomup_or_lemma: "[|(\<forall> (x::cterm). in_list x (children (C z b)) --> (? (e'::result). in_list (x,e') (zip (children (C z b)) b') & length (children (C z b))  = length b' & (x,e'):(oncebottomup_set f))); postMapOne (children (C z b)) b' = None|] ==> (C z b,f (C z b)):(oncebottomup_set f)";
apply (unfold oncebottomup_set_def);
apply (frule generalized_set.rule [of "C z b" b' oncebottomup_step f]);
apply (unfold oncebottomup_step_def);
apply (auto);
done;

lemma oncebottomup_none_lemma: "((\<forall> (x::cterm). in_list x b --> (? (e'::result). in_list (x,e') (zip b b') & length b = length b' & (x,e'):(oncebottomup_set f))) & postMapOne b b' = None) ==> (C z b,f (C z b)):(oncebottomup_set f)";
apply (insert oncebottomup_or_lemma [of z b b' f]);
apply (auto);
done;

lemma oncebottomup_main_lemma: "[|(\<forall> (x::cterm). in_list x (children (C z b)) --> (? (e'::result). in_list (x,e') (zip (children (C z b)) b') & length (children (C z b))  = length b' & (x,e'):(oncebottomup_set f))); postMapOne (children (C z b)) b' = Some r|] ==> (C z b,Some (C z r)):(oncebottomup_set f)";
apply (unfold oncebottomup_set_def);
apply (frule generalized_set.rule [of "C z b" b' oncebottomup_step f]);
apply (unfold oncebottomup_step_def);
apply (auto);
done;

lemma oncebottomup_some_lemma: "((\<forall> (x::cterm). in_list x b --> (? (e'::result). in_list (x,e') (zip b b') & length b = length b' & (x,e'):(oncebottomup_set f))) & postMapOne b b' = Some r) ==> (C z b,Some (C z r)):(oncebottomup_set f)";
apply (insert oncebottomup_main_lemma [of z b b' f]);
apply (auto);
done;

text {* basic laws *}

lemma infallible_law: "infallible f == \<forall> (e::cterm). ~(e, None):f";
apply (unfold infallible_def);
apply (unfold fallible_def);
apply (auto);
done;

lemma unsucceedable_law: "unsucceedable s == \<forall> (t::cterm). (t, None):s";
apply (unfold unsucceedable_def);
apply (unfold succeedable_def);
apply (auto);
done;

lemma unsucceedable_fail_lemma: "unsucceedable f ==> (e,fail e):f";
apply (insert unsucceedable_law [of f]);
apply (insert fail_def);
apply (auto);
done;


text {* sequence *}

lemma sequence_partial_fail_lemma: "[|x e = Some e'; z e' = None|] ==> sequence x z e = None";
apply (unfold sequence_def);
apply (auto);
done;

text {* choice *}

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

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

lemma choice_main_lemma: "f' e ~= None ==> choice f f' e ~= None";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_main_or_lemma: "f e ~= None ==> choice f f' e ~= None";
apply (unfold choice_def);
apply (auto);
done;

lemma choice_none_or_lemma: "[|choice f f' e ~= None; f' e = None|] ==> choice f f' e = f e";
apply (unfold choice_def);
apply (auto);
done;


text {* oncebu_fun *}

lemma oncebu_form_or_lemma: "one (oncebu_fun f) e = Some e' ==> oncebu_fun f e = one (oncebu_fun f) e";
apply (insert once_choice_theorem [of f]);
apply (unfold choice_def);
apply (auto);
done;

lemma oncebu_or_lemma: "oncebu_fun f e ~= None ==> (one (oncebu_fun f) e ~= None | f e ~= None)";
apply (insert once_choice_theorem [of f e]);
apply (unfold choice_def);
apply (auto);
done;

lemma oncebu_or_main_lemma: "oncebu_fun f e = one (oncebu_fun f) e  | oncebu_fun f e = f e";
apply (insert once_choice_theorem [of f e]);
apply (unfold choice_def);
apply (auto);
done;

lemma oncebu_not_fail_or_lemma: "oncebu_fun f e = Some e' ==> (one (oncebu_fun f) e = Some e' | f e = Some e')";
apply (insert oncebu_or_main_lemma [of f e]);
apply (auto);
done;

lemma oncebu_fail_or_lemma: "oncebu_fun f e = None ==> (one (oncebu_fun f) e = None & f e = None)";
apply (insert once_choice_theorem [of f e]);
apply (unfold choice_def);
apply (case_tac "one (oncebu_fun f) e = None");
apply (auto);
done;

lemma oncebu_partial_fail_lemma: "one (oncebu_fun f) e = None ==> oncebu_fun f e = f e";
apply (insert once_choice_theorem [of f e]);
apply (unfold choice_def);
apply (auto);
done;


text {* conCount *}

lemma map_gr_form_main_or_reform: "[|\<forall> (e::cterm). \<forall> (e'::cterm). f e = Some e' --> conCount z' e' < conCount z' e; \<forall> (e::cterm). size e < size x --> (\<forall> (e'::cterm). oncebu_fun f e = Some e' --> conCount z' e' < conCount z' e); one (oncebu_fun f) x = None; f x = Some x'|] ==> conCount z' x' < conCount z' x";
apply (frule oncebu_partial_fail_lemma [of f x]);
apply (auto);
done;

lemma map_gr_main_reform: "[|\<forall> (e::cterm). \<forall> (e'::cterm). f e = Some e' --> conCount z' e' < conCount z' e; \<forall> (e::cterm). size e < size x --> (\<forall> (e'::cterm). oncebu_fun f e = Some e' --> conCount z' e' <  conCount z' e); oncebu_fun f x = Some x'|] ==> conCount z' x' < conCount z' x";
apply (frule oncebu_not_fail_or_lemma [of f x]);
apply (insert map_gr_or_main_lemma [of x oncebu_fun f]);
apply (insert map_gr_form_main_or_reform [of f z' x]);
apply (auto);
done;

lemma map_gr_main_or_lemma: "[|\<forall> (e::cterm). \<forall> (e'::cterm). f e = Some e' --> conCount z' e' < conCount z' e; \<forall> (e::cterm). size e < size x --> (\<forall> (e'::cterm). oncebu_fun f e = Some e' --> conCount z' e' < conCount z' e)|] ==> (\<forall> (x'::cterm). oncebu_fun f x = Some x' --> conCount z' x' < conCount z' x)";
apply (insert map_gr_main_reform [of f z' x]);
apply (auto);
done;

lemma map_gr_form_main_lemma: "(\<forall> (e::cterm). \<forall> (e'::cterm). f e = Some e' --> conCount z' e' < conCount z' e) ==> (\<forall> (e'::cterm). oncebu_fun f e = Some e' --> conCount z' e' < conCount z' e)";
apply (induct_tac e rule: measure_induct [of size]);
apply (insert map_gr_main_or_lemma [of f z']);
apply (insert oncebu_form_or_lemma [of f]);
apply (auto);
done;

lemma oncebu_gr_main_lemma: "(\<forall> (e::cterm). \<forall> (e'::cterm). f e = Some e' --> conCount z' e' < conCount z' e) ==> (\<forall> (e::cterm). \<forall> (e'::cterm). oncebu_fun f e = Some e' --> conCount z' e' < conCount z' e)";
apply (insert map_gr_form_main_lemma [of f z']);
apply (auto);
done;


text {* repeat *}

lemma repeat_id_lemma: "x e = None ==> repeat_fun x e = id e";
apply (frule application_none_lemma [of x]);
apply (unfold id_def);
apply (frule repeat_set_one [of x 0 e e]);
apply (insert repeat_fun_rule [of e "id e" x]);
apply (auto);
done;

lemma repeat_id_main_lemma: "x e = None ==> (e, repeat_fun x e):(repeat_set x)";
apply (frule application_none_lemma [of x]);
apply (unfold id_def);
apply (frule repeat_set_one [of x 0 e e]);
apply (insert repeat_fun_rule [of e "id e" x]);
apply (auto);
done;

lemma repeat_fun_fail_lemma: "f e = None ==> repeat_fun f e = try (sequence f (repeat_fun f)) e";
apply (unfold try_def);
apply (insert repeat_id_lemma [of f e]);
apply (frule sequence_neg_1_sos [of f e "repeat_fun f"]);
apply (frule choice_none_id_lemma [of "sequence f (repeat_fun f)" e id]);
apply (auto);
done;

theorem repeat_halt: "(\<forall> (e::cterm). (\<forall> (e'::cterm). f e = Some e' -->  conCount z' e' < conCount z' e)) ==> (repeat_fun f x = x' == (x,x'):(repeat_set f))";
apply (insert repeat_halt_main_theorem [of f "conCount z'" x x']);
apply (auto);
done;

lemma repeat_not_fail_reform: "\<forall> (e::cterm). ~(e,None):(repeat_set f)";
apply (insert repeat_none_lemma [of _ f]);
apply (auto);
done;

lemma repeat_not_fail_main_lemma: "infallible (repeat_set f)";
apply (insert infallible_law [of "repeat_set f"]);
apply (insert repeat_not_fail_reform [of f]);
apply (auto);
done;

lemma repeat_equality_lemma: "[|chain x r e' = Some e''; x e = Some e'; x e'' = None|] ==> (e,id e''):(repeat_set x)";
apply (frule application_main_lemma [of x e e' r e'']);
apply (force);
apply (frule repeat_set_one [of x "r+1"]);
apply (auto);
done;

lemma repeat_equality_or_lemma: "[|chain x r e' = Some e''; x e = Some e'; x e'' = None|] ==> repeat_fun x e = repeat_fun x e'";
apply (frule repeat_equality_lemma [of x _ e' e'' e]);
apply (force);
apply (fast);
apply (frule repeat_fun_rule [of e "id e''" x]);
apply (frule repeat_set_one [of x r e']);
apply (force);
apply (frule repeat_fun_rule [of e' "id e''" x]);
apply (auto);
done;

lemma repeat_equality_zero_lemma: "[|chain x 0 e = Some e'; x e' = None|] ==> repeat_fun x e = try (sequence x (repeat_fun x)) e";
apply (drule chain_id_lemma [of x e e']);
apply (insert repeat_fun_fail_lemma [of x e]);
apply (auto);
done;

lemma repeat_equality_choice_lemma: "[|chain x r e' = Some e''; x e = Some e'; x e'' = None|] ==> repeat_fun x e = try (sequence x (repeat_fun x)) e";
apply (unfold try_def);
apply (frule sequence_application_lemma [of x e e' "repeat_fun x"]);
apply (frule repeat_set_one [of x r e']);
apply (force);
apply (frule repeat_fun_rule [of e' "id e''" x]);
apply (frule repeat_equality_or_lemma [of x r e']);
apply (unfold id_def);
apply (insert choice_main_id_lemma [of "sequence x (repeat_fun x)" e e'' id]);
apply (auto);
done;

lemma repeat_equality_main_lemma: "[|chain x (r+1) e = Some e''; x e'' = None|] ==> repeat_fun x e = try (sequence x (repeat_fun x)) e";
apply (case_tac "x e = None");
apply (frule repeat_fun_fail_lemma [of x e]);
apply (force);
apply (frule result_form_lemma [of "x e"]);
apply (frule_tac someI_ex);
apply (frule application_main_id_lemma [of x e _ r e'']);
apply (force);
apply (frule repeat_equality_choice_lemma [of x r _ e'' e]);
apply (auto);
done;

lemma repeat_equality_naive_lemma: "[|chain x r e = Some e''; x e'' = None|] ==> repeat_fun x e = try (sequence x (repeat_fun x)) e";
apply (case_tac r);
apply (insert repeat_equality_zero_lemma [of x e e'']);
apply (force);
apply (insert repeat_equality_main_lemma [of x _ e e'']);
apply (auto);
done;

lemma repeat_naive_lemma: "repeat_condition x e ==> repeat_fun x e = try (sequence x (repeat_fun x)) e";
apply (unfold repeat_condition_def);
apply (insert repeat_equality_naive_lemma [of x]);
apply (auto);
done;


text {* try *}

lemma try_lemma: "try id (C 1 []) = Some (C 1 [])";
apply (unfold try_def);
apply (unfold choice_def);
apply (unfold id_def);
apply (auto);
done;

lemma try_not_fail_lemma: "try f e ~= None";
apply (unfold try_def);
apply (unfold choice_def);
apply (unfold id_def);
apply (auto);
done;

lemma try_not_fail_reform: "\<forall> (e::cterm). try f e ~= None";
apply (unfold try_def);
apply (unfold choice_def);
apply (unfold id_def);
apply (auto);
done;

lemma one_in_term_lemma: "one x (C z b) ~= None ==> one x (C z (e#b)) ~= None";
apply (unfold one_def);
apply (case_tac "postMapOne b (map x b) = None");
apply (force);
apply (frule postMapOne_or_lemma [of b x e]);
apply (auto);
done;

lemma one_main_or_lemma: "(f x' ~= None) ==> one (choice f (one f')) (C z (x'#b')) ~= None";
apply (unfold one_def);
apply (insert choice_def);
apply (auto);
done;

lemma one_not_fail_reform: "(postMapOne b (map f b) ~= None) ==> one f (C z b) ~= None";
apply (frule result_form_lemma [of "postMapOne b (map f b)"]);
apply (frule_tac someI_ex);
apply (frule one_unit_list_not_fail_case_lemma [of b f _ z]);
apply (auto);
done;

lemma postMapOne_in_list_lemma: "[|in_list e b; f e ~= None|] ==> postMapOne b (map f b) ~= None";
apply (insert unit_list_aim_lemma [of e b f None]);
apply (frule mp);
apply (force);
apply (insert map_one_unit_list_main_lemma [of f b]);
apply (auto);
done;

lemma one_in_list_lemma: "[|in_list e (children x); f e ~= None|] ==> one f x ~= None";
apply (unfold one_def);
apply (frule postMapOne_in_list_lemma [of e "children x" f]);
apply (auto);
done;


text {* topdown_fun *}

lemma topdown_set_none_lemma: "s t = None ==> (t,None):(topdown_set s)";
apply (insert con_of_children_lemma [of t]);
apply (insert topdown_halt_lemma [of s t None]);
apply (insert halt_fail [of s "con_of t" "children t"]);
apply (auto);
done;

lemma topdown_halt_none_lemma: "[|s t = None; nonincreasing s|] ==> topdown_fun s t = None";
apply (insert con_of_children_lemma [of t]);
apply (insert topdown_halt_lemma [of s t None]);
apply (insert halt_fail [of s "con_of t" "children t"]);
apply (frule sequence_neg_1_sos [of s t  "all (topdown_fun s)"]);
apply (auto);
done;

lemma topdown_set_main_lemma: "s t = Some (C c []) ==> (t,Some (C c [])):(topdown_set s)";
apply (insert con_of_children_lemma [of t]);
apply (insert con_of_children_lemma [of "C c []"]);
apply (insert halt_map [of "C c []" "[]" s "con_of t" "children t" "[]"]);
apply (auto);
done;

lemma topdown_halt_main_lemma: "[|s t = Some (C c []); nonincreasing s|] ==> topdown_fun s t = Some (C c [])";
apply (insert topdown_halt_lemma [of s t ]);
apply (insert topdown_set_main_lemma [of s t c]);
apply (auto);
done;

lemma topdown_halt_map_none_lemma: "[|s t = Some t'; nonincreasing s; postMapAll (map (topdown_fun s) (children t')) = None|] ==> topdown_fun s t = None";
apply (insert con_of_children_lemma [of t']);
apply (frule all_fail_lemma [of "topdown_fun s" "children t'" "con_of t'"]);
apply (insert topdown_halt [of s t]);
apply (frule sequence_partial_fail_lemma [of s t t' "all (topdown_fun s)"]);
apply (auto);
done;

lemma topdown_halt_map_aim_lemma: "[|s t = Some t'; nonincreasing s; postMapAll (map (topdown_fun s) (children t')) = Some ts|] ==> topdown_fun s t = Some (C (con_of t') ts)";
apply (insert con_of_children_lemma [of t']);
apply (frule all_expr_lemma [of "topdown_fun s" "children t'" ts "con_of t'"]);
apply (insert topdown_halt [of s t]);
apply (frule sequence_application_lemma [of s t t' "all (topdown_fun s)"]);
apply (auto);
done;


text {* oncebu *}

lemma oncebu_lemma: "oncebu f e = choice (one (oncebu f)) f e";
apply (insert oncebu_rule [of f]);
apply (auto);
done;

lemma oncebu_not_fail_lemma: "f e ~= None ==> oncebu f e ~= None";
apply (insert oncebu_lemma [of f e]);
apply (unfold choice_def);
apply (unfold one_def);
apply (auto);
done;

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

lemma oncebu_not_empty_lemma: "[|e = (C z (x#b)); f e ~= None|] ==> oncebu f (C z (x#b)) ~= None";
apply (insert oncebu_not_fail_lemma [of f "C z (x#b)"]);
apply (auto);
done;

lemma oncebu_not_empty_none_lemma: "[|e = x; one (oncebu f) x = None; f e ~= None|] ==> oncebu f (C z (x#b)) ~= None";
apply (insert oncebu_lemma [of f "C z (x#b)"]);
apply (frule choice_partial_fail_reform [of "one (oncebu f)" x f]);
apply (insert oncebu_lemma [of f x]);
apply (case_tac "oncebu f x = None");
apply (force);
apply (frule postMapOne_main_lemma [of "oncebu f" x b]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu f" z]);
apply (frule choice_main_or_lemma [of "one (oncebu f)" "C z (x#b)" f]);
apply (auto);
done;

lemma one_postMapOne_lemma: "[|one f e ~= None|] ==> postMapOne (children e) (map f (children e)) ~= None";
apply (unfold one_def);
apply (case_tac "postMapOne (children e) (map f (children e)) = None");
apply (auto);
done;

lemma one_postMapOne_reform: "[|one f (C z b) ~= None|] ==> postMapOne b (map f b) ~= None";
apply (insert one_postMapOne_lemma [of f "C z b"]);
apply (auto);
done;

lemma oncebu_not_empty_none_or_lemma: "[|e = x; one (oncebu f) x ~= None; f e ~= None|] ==> oncebu f (C z (x#b)) ~= None";
apply (insert oncebu_lemma [of f "C z (x#b)"]);
apply (frule choice_main_or_lemma [of "one (oncebu f)" x f]);
apply (insert oncebu_lemma [of f x]);
apply (case_tac "oncebu f x = None");
apply (force);
apply (frule postMapOne_main_lemma [of "oncebu f" x b]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu f" z]);
apply (frule choice_main_or_lemma [of "one (oncebu f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncebu_main_lemma: "f (C z b) ~= None ==> oncebu f (C z b) ~= None";
apply (insert oncebu_lemma [of f "C z b"]);
apply (case_tac "one (oncebu f) (C z b) = None");
apply (frule choice_partial_fail_reform [of "one (oncebu f)" "C z b"  f]);
apply (force);
apply (frule choice_main_or_lemma [of "one (oncebu f)" "C z b" f]);
apply (auto);
done;

lemma oncebu_main_or_lemma: "[|oncebu f (C z b) ~= None; f (C z b) = None|] ==> oncebu f (C z (x#b)) ~= None";
apply (insert oncebu_lemma [of f "C z b"]);
apply (case_tac "choice (one (oncebu f)) f (C z b) = None");
apply (force);
apply (frule choice_none_or_lemma [of "one (oncebu f)" f "C z b"]);
apply (force);
apply (case_tac "one (oncebu f) (C z b) = None");
apply (force);
apply (frule one_postMapOne_reform [of "oncebu f" z b]);
apply (frule postMapOne_or_lemma [of b "oncebu f" x]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu f" z]);
apply (insert oncebu_lemma [of f "C z (x#b)"]);
apply (frule choice_main_or_lemma [of "one (oncebu f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncebu_in_term_lemma: "[|e:(in_term (C z b)); f e ~= None; f (C z b) = None; (e:(in_term (C z b))) & f e ~= None  & f (C z b) = None --> oncebu f (C z b) ~= None|] ==> oncebu f (C z (x#b)) ~= None";
apply (insert oncebu_lemma [of f "C z (x#b)"]);
apply (insert oncebu_main_or_lemma [of f z b x]);
apply (auto);
done;


text {* oncetd *}

lemma oncetd_lemma: "oncetd f e = choice f (one (oncetd f)) e";
apply (insert oncetd_rule [of f]);
apply (auto);
done;

lemma oncetd_not_fail_lemma: "f e ~= None ==> oncetd f e ~= None";
apply (insert oncetd_lemma [of f e]);
apply (unfold choice_def);
apply (unfold one_def);
apply (auto);
done;

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

lemma oncetd_not_fail_or_lemma: "f e = Some e' ==> oncetd f e = Some e'";
apply (insert oncetd_lemma [of f e]);
apply (unfold choice_def);
apply (unfold one_def);
apply (auto);
done;

lemma oncetd_not_fail_main_or_lemma: "f (C z b) ~= None ==> oncetd f (C z b) ~= None";
apply (frule result_form_lemma [of "f (C z b)"]);
apply (frule_tac someI_ex);
apply (frule oncetd_not_fail_or_lemma [of f "C z b"]);
apply (auto);
done;

lemma oncetd_none_or_lemma: "[|e = C z (e'#b'); f e' = Some e''; f e = None|] ==> oncetd f e = Some (C z (e''#b'))";
apply (insert oncetd_lemma [of f e]);
apply (unfold choice_def);
apply (unfold one_def);
apply (frule postMapOne_lemma [of f e' e'' b']);
apply (frule oncetd_not_fail_or_lemma [of f e' e'']);
apply (auto);
done;

lemma oncetd_none_reform: "[|e = C z (e'#b'); f e' ~= None; f e = None|] ==> oncetd f e ~= None";
apply (frule result_form_lemma [of "f e'"]);
apply (frule_tac someI_ex);
apply (frule oncetd_none_or_lemma [of e z e' b' f]);
apply (auto);
done;

lemma oncetd_in_term_lemma: "[|x (C z b') = None; oncetd x (C z b') ~= None|] ==> oncetd x (C z (e'#b')) ~= None";
apply (insert oncetd_lemma [of x "C z b'"]);
apply (insert oncetd_lemma [of x "C z (e'#b')"]);
apply (unfold choice_def);
apply (insert choice_def [of x "one (oncetd x)" "C z (e'#b')"]);
apply (case_tac "x (C z b') = None");
apply (case_tac "one (oncetd x) (C z b') = None");
apply (force);
apply (case_tac "x (C z (e'#b')) = None");
apply (frule one_in_term_lemma [of "oncetd x" z b' e']);
apply (auto);
done;

lemma oncetd_one_main_or_lemma: "(f e = None) ==> choice f (one f') e = one f' e";
apply (insert oncetd_lemma [of f e]);
apply (insert choice_def);
apply (auto);
done;

lemma oncetd_reform: "oncetd f e = (choice f (one (choice f (one (oncetd f))))) e";
apply (insert oncetd_rule [of f]);
apply (auto);
done;

lemma oncetd_in_term_main_or_lemma: "(f x' ~= None) ==> oncetd f (C z (x'#b')) ~= None";
apply (insert oncetd_lemma [of f "C z (x'#b')"]);
apply (insert choice_def [of f "one (oncetd f)" "C z (x'#b')"]);
apply (case_tac "f (C z (x'#b')) = None");
prefer 2;
apply (force);
apply (frule oncetd_one_main_or_lemma [of f "C z (x'#b')" "oncetd f"]);
apply (frule one_main_or_lemma [of f x' "oncetd f" z b']);
apply (insert oncetd_reform [of f e]);
apply (frule choice_partial_fail_reform [of f _ "one (oncetd f)"]);
apply (insert oncetd_rule [of f]);
apply (auto);
done;


text {* oncebu_fun *}

lemma oncebu_fun_lemma: "oncebu_fun f e = choice (one (oncebu_fun f)) f e";
apply (insert once_choice_theorem [of f e]);
apply (auto);
done;

lemma oncebu_fun_not_fail_lemma: "f e ~= None ==> oncebu_fun f e ~= None";
apply (insert oncebu_fun_lemma [of f e]);
apply (unfold choice_def);
apply (unfold one_def);
apply (auto);
done;

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

lemma oncebu_fun_not_empty_lemma: "[|e = (C z (x#b)); f e ~= None|] ==> oncebu_fun f (C z (x#b)) ~= None";
apply (insert oncebu_fun_not_fail_lemma [of f "C z (x#b)"]);
apply (auto);
done;

lemma oncebu_fun_not_empty_none_lemma: "[|e = x; one (oncebu_fun f) x = None; f e ~= None|] ==> oncebu_fun f (C z (x#b)) ~= None";
apply (insert oncebu_fun_lemma [of f "C z (x#b)"]);
apply (frule choice_partial_fail_reform [of "one (oncebu_fun f)" x f]);
apply (insert oncebu_fun_lemma [of f x]);
apply (case_tac "oncebu_fun f x = None");
apply (force);
apply (frule postMapOne_main_lemma [of "oncebu_fun f" x b]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu_fun f" z]);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncebu_fun_not_empty_none_or_lemma: "[|e = x; one (oncebu_fun f) x ~= None; f e ~= None|] ==> oncebu_fun f (C z (x#b)) ~= None";
apply (insert oncebu_fun_lemma [of f "C z (x#b)"]);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" x f]);
apply (insert oncebu_fun_lemma [of f x]);
apply (case_tac "oncebu_fun f x = None");
apply (force);
apply (frule postMapOne_main_lemma [of "oncebu_fun f" x b]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu_fun f" z]);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncebu_fun_main_lemma: "f (C z b) ~= None ==> oncebu_fun f (C z b) ~= None";
apply (insert oncebu_fun_lemma [of f "C z b"]);
apply (case_tac "one (oncebu_fun f) (C z b) = None");
apply (frule choice_partial_fail_reform [of "one (oncebu_fun f)" "C z b"  f]);
apply (force);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" "C z b" f]);
apply (auto);
done;

lemma oncebu_fun_main_one_lemma: "f x ~= None ==> oncebu_fun f x ~= None";
apply (insert con_of_children_lemma [of x]);
apply (insert oncebu_fun_main_lemma [of f "con_of x" "children x"]);
apply (auto);
done;

lemma oncebu_fun_main_or_lemma: "[|oncebu_fun f (C z b) ~= None; f (C z b) = None|] ==> oncebu_fun f (C z (x#b)) ~= None";
apply (insert oncebu_fun_lemma [of f "C z b"]);
apply (case_tac "choice (one (oncebu_fun f)) f (C z b) = None");
apply (force);
apply (frule choice_none_or_lemma [of "one (oncebu_fun f)" f "C z b"]);
apply (force);
apply (case_tac "one (oncebu_fun f) (C z b) = None");
apply (force);
apply (frule one_postMapOne_reform [of "oncebu_fun f" z b]);
apply (frule postMapOne_or_lemma [of b "oncebu_fun f" x]);
apply (frule one_not_fail_reform [of "(x#b)" "oncebu_fun f" z]);
apply (insert oncebu_fun_lemma [of f "C z (x#b)"]);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncebu_fun_in_term_lemma: "[|e:(in_term (C z b)); f e ~= None; f (C z b) = None; (e:(in_term (C z b))) & f e ~= None  & f (C z b) = None --> oncebu_fun f (C z b) ~= None|] ==> oncebu_fun f (C z (x#b)) ~= None";
apply (insert oncebu_fun_lemma [of f "C z (x#b)"]);
apply (insert oncebu_fun_main_or_lemma [of f z b x]);
apply (auto);
done;

lemma oncebu_fun_in_term_or_lemma: "[|e:(in_term (C z b)); f e ~= None; e = (C z b)|] ==> oncebu_fun f (C z b) ~= None";
apply (insert oncebu_fun_main_lemma [of f z b]);
apply (auto);
done;

lemma oncebu_fun_main_in_term_or_lemma: "[|e:(in_term x); f e ~= None; e = x|] ==> oncebu_fun f x ~= None";
apply (insert con_of_children_lemma [of x]);
apply (insert oncebu_fun_in_term_or_lemma [of e "con_of x" "children x" f]);
apply (auto);
done;

lemma in_term_lemma: "[|e:(in_term (C z b)); e ~= (C z b)|] ==> (e:(\<Union> (e'::cterm). (if in_list e' (children (C z b)) then in_term e' else {})) | e:{C z b})";
apply (insert in_term_def [of "C z b"]);
apply (auto);
done;

lemma in_union_lemma: "e:(\<Union> (e'::cterm). A e') ==> (? (e'::cterm). e:(A e'))";
apply  (auto);
done;

lemma in_main_or_lemma: "(e:(if in_list e' b then in_term e' else {})) ==> (in_list e' b & e:(in_term e'))";
apply (case_tac "in_list e' b");
apply (auto);
done;

lemma in_aim_or_lemma: "(? (e'::cterm). e:(if in_list e' b then in_term e' else {})) ==> ((? (e'::cterm). in_list e' b & e:(in_term e')))";
apply (insert in_main_or_lemma [of e]);
apply (fast);
done;

lemma in_union_or_lemma: "e:(\<Union> (e'::cterm). (if in_list e' b then in_term e' else {})) ==> (? (e'::cterm). in_list e' b & e:(in_term e'))";
apply (frule in_union_lemma);
apply (frule in_aim_or_lemma);
apply (auto);
done;

lemma in_term_main_lemma: "[|e:(in_term (C z b)); e ~= (C z b)|] ==> (? (e'::cterm). in_list e' b & e:(in_term e'))";
apply (insert in_term_def [of "C z b"]);
apply (frule in_term_lemma [of e z b]);
apply (best);
apply (case_tac "e:(\<Union> (e'::cterm). (if in_list e' (children (C z b)) then in_term e' else {}))");
apply (frule in_union_or_lemma [of e]);
apply (auto);
done;

lemma in_term_main_or_lemma: "[|e:(in_term x); e ~= x|] ==> (? (e'::cterm). in_list e' (children x) & e:(in_term e'))";
apply (insert con_of_children_lemma [of x]);
apply (insert in_term_main_lemma [of e "con_of x" "children x"]);
apply (auto);
done;

lemma oncebu_fun_in_term_aim_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x); e:(in_term e'); \<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)|] ==> oncebu_fun f x ~= None";
apply (insert oncebu_fun_lemma [of f x]);
apply (frule_tac x=e' in spec);
apply (frule mp);
apply (force);
apply (frule mp);
back;
apply (best);
apply (frule one_in_list_lemma [of e' x "oncebu_fun f"]);
apply (force);
apply (frule choice_main_or_lemma [of "one (oncebu_fun f)" x f]);
apply (force);
done;

lemma in_lemma: "(\<forall> (e'::cterm). size e' < size (C (con_of x) (children x)) --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)) ==> (\<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None))";
apply (insert in_list_congr_main_lemma [of "children x" "con_of x"]);
apply (fast);
done;

lemma id_main_or_lemma: "(size e' < size (C (con_of x) (children x))) = (size e' < size x)";
apply (insert con_of_children_lemma [of x]);
apply (auto);
done;

lemma in_main_lemma: "(\<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)) ==> (\<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None))";
apply (insert id_main_or_lemma [of _ x]);
apply (insert in_lemma [of x e f]);
apply (fast);
done;

lemma oncebu_fun_in_term_aim_or_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x); e:(in_term e'); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)|] ==> oncebu_fun f x ~= None";
apply (frule in_main_lemma [of x e f]);
apply (frule oncebu_fun_in_term_aim_lemma [of e x f e']);
apply (force);
apply (force);
apply (force);
apply (best);
apply (force);
apply (force);
apply (force);
done;

lemma oncebu_fun_main_in_term_aim_or_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x) & e:(in_term e'); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)|] ==> oncebu_fun f x ~= None";
apply (insert oncebu_fun_in_term_aim_or_lemma [of e x f]);
apply (fast);
done;

lemma oncebu_fun_in_term_main_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; (? (e'::cterm). in_list e' (children x) & e:(in_term e')); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)|] ==> oncebu_fun f x ~= None";
apply (frule_tac someI_ex);
apply (frule oncebu_fun_main_in_term_aim_or_lemma [of e x f]);
apply (force);
apply (force);
apply (force);
apply (best);
apply (force);
apply (auto);
done;

lemma oncebu_fun_in_term_main_or_lemma: "[|e:(in_term x); f e ~= None; \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncebu_fun f e' ~= None)|] ==> oncebu_fun f x ~= None";
apply (case_tac "e = x");
apply (frule oncebu_fun_main_in_term_or_lemma [of e x f]);
apply (force);
apply (force);
apply (force);
apply (case_tac "f x = None");
apply (frule in_term_main_or_lemma [of e x]);
apply (force);
apply (frule oncebu_fun_in_term_main_lemma [of e x f]);
apply (force);
apply (best);
apply (force);
apply (best);
apply (force);
apply (best);
apply (frule oncebu_fun_main_one_lemma [of f x]);
apply (auto);
done;

lemma oncebu_fun_in_term_one_main_or_lemma: "(e:(in_term x) & f e ~= None) --> oncebu_fun f x ~= None";
apply (induct_tac x rule: measure_induct [of size]);
apply (insert oncebu_fun_in_term_main_or_lemma [of e _ f]);
apply (best);
done;


text {* oncetd *}

lemma oncetd_main_lemma: "f (C z b) ~= None ==> oncetd f (C z b) ~= None";
apply (insert oncetd_lemma [of f "C z b"]);
apply (frule choice_main_or_lemma [of f  "C z b" "one (oncetd f)"]);
apply (auto);
done;

lemma oncetd_main_one_lemma: "f x ~= None ==> oncetd f x ~= None";
apply (insert con_of_children_lemma [of x]);
apply (insert oncetd_main_lemma [of f "con_of x" "children x"]);
apply (auto);
done;

lemma oncetd_main_or_lemma: "[|oncetd f (C z b) ~= None; f (C z b) = None|] ==>oncetd f (C z (x#b)) ~= None";
apply (insert oncetd_lemma [of f "C z b"]);
apply (case_tac "choice f (one (oncetd f)) (C z b) = None");
apply (force);
apply (case_tac "one (oncetd f) (C z b) = None");
apply (frule choice_none_id_lemma [of f "C z b" "one (oncetd f)"]);
apply (force);
apply (frule one_postMapOne_reform [of "oncetd f" z b]);
apply (frule postMapOne_or_lemma [of b "oncetd f" x]);
apply (frule one_not_fail_reform [of "(x#b)" "oncetd f" z]);
apply (insert oncetd_lemma [of f "C z (x#b)"]);
apply (frule choice_main_lemma [of "one (oncetd f)" "C z (x#b)" f]);
apply (auto);
done;

lemma oncetd_in_term_lemma: "[|e:(in_term (C z b)); f e ~= None; f (C z b) = None; (e:(in_term (C z b))) & f e ~= None  & f (C z b) = None --> oncetd f (C z b) ~= None|] ==> oncetd f (C z (x#b)) ~= None";
apply (insert oncetd_lemma [of f "C z (x#b)"]);
apply (insert oncetd_main_or_lemma [of f z b x]);
apply (auto);
done;

lemma oncetd_in_term_or_lemma: "[|e:(in_term (C z b)); f e ~= None; e = (C z b)|] ==> oncetd f (C z b) ~= None";
apply (insert oncetd_main_lemma [of f z b]);
apply (auto);
done;

lemma oncetd_main_in_term_or_lemma: "[|e:(in_term x); f e ~= None; e = x|] ==> oncetd f x ~= None";
apply (insert con_of_children_lemma [of x]);
apply (insert oncetd_in_term_or_lemma [of e "con_of x" "children x" f]);
apply (auto);
done;

lemma oncetd_in_term_aim_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x); e:(in_term e'); \<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)|] ==> oncetd f x ~= None";
apply (insert oncetd_lemma [of f x]);
apply (frule_tac x=e' in spec);
apply (frule mp);
apply (force);
apply (frule mp);
back;
apply (best);
apply (frule one_in_list_lemma [of e' x "oncetd f"]);
apply (force);
apply (frule choice_main_lemma [of "one (oncetd f)" x f]);
apply (force);
done;

lemma in_aim_lemma: "(\<forall> (e'::cterm). size e' < size (C (con_of x) (children x)) --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)) ==> (\<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None))";
apply (insert in_list_congr_main_lemma [of "children x" "con_of x"]);
apply (fast);
done;

lemma in_oncetd_lemma: "(\<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)) ==> (\<forall> (e'::cterm). in_list e' (children x) --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None))";
apply (insert id_main_or_lemma [of _ x]);
apply (insert in_aim_lemma [of x e f]);
apply (fast);
done;

lemma oncetd_in_term_aim_or_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x); e:(in_term e'); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)|] ==> oncetd f x ~= None";
apply (frule in_oncetd_lemma [of x e f]);
apply (frule oncetd_in_term_aim_lemma [of e x f e']);
apply (force);
apply (force);
apply (force);
apply (best);
apply (force);
apply (force);
apply (force);
done;

lemma oncetd_main_in_term_aim_or_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; in_list e' (children x) & e:(in_term e'); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)|] ==> oncetd f x ~= None";
apply (insert oncetd_in_term_aim_or_lemma [of e x f]);
apply (fast);
done;

lemma oncetd_in_term_main_lemma: "[|e:(in_term x); f e ~= None; e ~= x; f x = None; (? (e'::cterm). in_list e' (children x) & e:(in_term e')); \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)|] ==>  oncetd f x ~= None";
apply (frule_tac someI_ex);
apply (frule oncetd_main_in_term_aim_or_lemma [of e x f]);
apply (force);
apply (force);
apply (force);
apply (best);
apply (force);
apply (auto);
done;

lemma oncetd_in_term_main_or_lemma: "[|e:(in_term x); f e ~= None; \<forall> (e'::cterm). size e' < size x --> (e:(in_term e') & f e ~= None --> oncetd f e' ~= None)|] ==> oncetd f x ~= None";
apply (case_tac "e = x");
apply (frule oncetd_main_in_term_or_lemma [of e x f]);
apply (force);
apply (force);
apply (force);
apply (case_tac "f x = None");
apply (frule in_term_main_or_lemma [of e x]);
apply (force);
apply (frule oncetd_in_term_main_lemma [of e x f]);
apply (force);
apply (best);
apply (force);
apply (best);
apply (force);
apply (best);
apply (frule oncetd_main_one_lemma [of f x]);
apply (auto);
done;

lemma oncetd_in_term_one_main_or_lemma: "(e:(in_term x) & f e ~= None) --> oncetd f x ~= None";
apply (induct_tac x rule: measure_induct [of size]);
apply (insert oncetd_in_term_main_or_lemma [of e _ f]);
apply (best);
done;

end