theory Terms imports Option Children begin


text {* a datatype for term expressions *}

types con = nat;
   
datatype cterm = C con "cterm list";

lemma postMapAll_none_map_lemma: "(\<forall> (e::'a). f e ~= None) --> postMapAll (map f b) ~= None";
apply (induct_tac b);
apply (insert postMapAll_none_map_not_empty_lemma [of f]);
apply (auto);
done;


text {* a datatype for rewriting results *}

types result = "cterm option";


text {* Term-processing helper functions *}

consts
con_of :: "cterm => con"
children :: "cterm => cterm list"

primrec
"con_of (C c ts) = c"

primrec
"children (C c ts) = ts"


lemma con_of_children_lemma: "t = C (con_of t) (children t)";
apply (case_tac t);
apply (auto);
done;

lemma con_of_children_main_lemma: "[|b = b'; b = (children e)|] ==> C (con_of e) b' = e"
apply (case_tac e);
apply (auto);
done;

lemma con_of_children_main_lemma: "[|b = b'; b = (children e)|] ==> C (con_of e) b' = e"
apply (case_tac e);
apply (auto);
done;


text {* nontrivial auxiliary concerning the size of terms *}

lemma ok_auto_lemma[simp]: "b' \<in> set b --> size b' < Suc (cterm_list_size b)";
apply (induct_tac b);
apply (auto);
done;

lemma ok_in_list_lemma: "in_list b' b --> size b' < Suc (cterm_list_size b)";
apply (insert in_list_congr_lemma [of b' b]);
apply (auto);
done;

lemma ok_cnr_in_list_lemma[rule_format]: "(e = C z b) --> (\<forall> (b'::cterm). in_list b' b --> size b' < size e)";
apply (case_tac e);
apply (insert ok_in_list_lemma);
apply (auto);
done;

lemma in_list_congr_main_lemma: "(\<forall> (e::cterm). in_list e b --> size e < size (C z b))" ;
apply (insert ok_in_list_lemma);
apply (auto);
done;

lemma in_list_run_lemma: "size b < Suc (cterm_list_size b)";
apply (induct_tac b);
apply (auto);
done;

lemma main_run_lemma: "size b < size (C z b)"
apply (insert in_list_run_lemma [of b]);
apply (auto);
done;

lemma map_congr_lemma: "(\<forall> (x::cterm). size x < size (C z b) --> f x = f' x) ==> map f b = map f' b";
apply (insert in_list_congr_main_lemma [of b z]);
apply (insert map_lemma [of b f f']);
apply (auto);
done;

lemma map_or_lemma: "[|\<forall> (x::cterm). size x < size (C z b) --> f x = f' x; postMapAll (map f' b) ~= e|] ==> postMapAll (map f b) ~= e";
apply (insert in_list_congr_main_lemma [of b z]);
apply (insert map_lemma [of b f f']);
apply (auto);
done;


text {* logic *}

lemma ok_fail_x_lemma: "\<forall> (e::cterm). f e ~= None ==> \<forall> (e::cterm). A --> f e ~= None";
apply (auto);
done;

lemma implication_lemma: "[|\<forall> (e::cterm). A --> f e ~= None; A|] ==> \<forall> (e::cterm). A \<and> f e ~= None";
apply (auto);
done;

lemma cjn_lemma: "[|\<forall> (e:: cterm). A e < A (C z b) --> f e ~= None; \<forall> (e::cterm). A' e r --> A e < A (C z b)|] ==> \<forall> (e::cterm). A' e r --> f e ~= None";
apply (auto);
done;

lemma gr_cjn_lemma: "[|\<forall> (e::cterm). A e < A (C z b) --> f e ~= None; \<forall> (e::cterm). A' e r --> A e < A (C z b)|] ==> \<forall> (e::cterm). A' e r --> f e ~= None";
apply (auto);
done;


end