[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.