theory Option imports Main begin


lemma result_lemma: "x = Some e ==> x ~= None"
apply (auto);
done;

lemma result_form_lemma: "x ~= None ==> (?(e::'a). x = Some e)";
apply (case_tac x);
apply (auto);
done;

lemma result_reform: "\<forall> (e::'a). (f::'a =>'a option) e ~= None ==> (\<forall> (e::'a). (?(e'::'a). f e = Some e'))";
apply (insert result_form_lemma);
apply (auto);
done;

lemma con_of_result_lemma: "Some x = Some x' ==> con_of x = con_of x'";
apply (auto);
done;

lemma equal_result_lemma: "[|z = Some x; z = Some x'|] ==>  x = x'";
apply (auto);
done;

lemma option_lemma: "[|\<forall> (e::'a). f e ~= None; \<forall> (e::'a). f' e ~= None|] ==> (? (e'::'a). (? (e''::'a). f e = Some e' &  f' e' = Some e''))";
apply (insert result_form_lemma);
apply (auto);
done;


end