theory Basic imports Main begin

text {* logic *}

lemma or_lemma: "A ==> A \<or> Z";
apply (auto);
done;

lemma equivalence_or_lemma: "[|A == A'; A'|] ==> A";
apply (auto);
done;

lemma equivalence_main_or_lemma: "[|(A = e) == A'; A'; Z = e|] ==> Z = A";
apply (auto);
done;

lemma equivalence_main_lemma: "[|A = A'; A|] ==> A'";
apply (auto);
done;

lemma equality_lemma: "[|A = A'; e = e'; A' = Z e; Z e' ~= None|] ==> A ~= None";
apply (auto);
done;

lemma condition_form_lemma: "[|(\<forall> (x::'a). B x --> Z x) ==> A; \<forall> (x::'a). B x --> B' x|] ==> ((\<forall> (x::'a). B' x --> Z x) ==> A)";
apply (auto);
done;

lemma arrow_lemma: "[|A ==> A'; A' --> A|] ==> (A = A')";
apply (auto);
done;

lemma arrow_or_lemma: "[|A --> A'; A' --> A|] ==> (A = A')";
apply (auto);
done;

lemma arrow_main_lemma: "(A = A') ==> (A == A')";
apply (auto);
done;

lemma arrow_main_id_lemma: "[|A ==> A'; A' --> A|] ==> (A == A')";
apply (insert arrow_lemma [of A A']);
apply (rule arrow_main_lemma [of A A']);
apply (auto);
done;

lemma arrow_main_or_lemma: "[|A --> A'; A' --> A|] ==> (A == A')";
apply (insert arrow_lemma [of A A']);
apply (rule arrow_main_lemma [of A A']);
apply (auto);
done;


text {* easy properties *}

lemma one_lemma: "(0 < (i::nat)) = (1 <= i)";
apply (auto);
done;

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

lemma gr_form_lemma: "[|size x <= size y; size y <= size z|] ==> size x <= size z";
apply (auto);
done;

lemma gr_aim_lemma: "[|x = y; z = b; size y <= size b|] ==> size x <= size z";
apply (auto);
done;

lemma gr_expr_or_lemma: "[|size e < size x; size x' <= size e|] ==> size x' < size x";
apply (auto);
done;


end