# [isabelle] How to apply a theorem?

Hi,
I am a novice to Isabelle.
The below theory does not verify at the point of "by (unfold bij_converse_bij)". What it should be replaced to? Which document to read about this kind of questions I ask?
Before presenting my theory I want to explain what I am trying to achieve: Suppose (in ZF) we have two sets 'small' and 'big' (not necessarily disjoint) and an injection 'embed' from small to big. I want to replace 'big' with 'newbig' so that 'newbig' would bijectively correspond to 'big' but 'small' would become a subset of 'newbig'. Example: 'small' are integers, 'big' are reals, we want to embed the set of integers into the (another) set of reals. Another example: 'small' is the powerset of some set, 'big' is the set of filters on 'small', 'embed' maps every set to the corresponding principal filter; so filters are considered as a generalization of sets.
Well, below my theory:
---------------------------------------
theory embedding
imports ZF Perm
begin
locale embedding2 =
fixes big::i and small::i
fixes embed
assumes is_inj: "embded: inj(small, big)"
begin
(* <a,b> == {{a,a}, {a,b}} *)
definition "newbig == big" (*to be replaced with the real definition*)
definition "move == 0" (*to be replaced with the real definition*)
definition "ret == converse(move)"
theorem "small <= newbig"
sorry
theorem "move: bij(big, newbig)"
sorry
theorem "ret: bij(newbig, big)"
by (unfold bij_converse_bij)
end
end

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*