9 *)

    10 

    11 ML {*

    12 val ctxt0 = @{context}

    13 val ty = Syntax.read_typ ctxt0 "bool"  

    14 val ctxt1 = Variable.declare_typ ty ctxt0 

    15 val trm = Syntax.parse_term ctxt1 "A \<and> B"

    16 val trm' = Syntax.type_constraint ty trm

    17 val trm'' = Syntax.check_term ctxt1 trm'

    18 val ctxt2 = Variable.declare_term trm'' ctxt1 

    19 *}

    20 

    21 term "split"

    22 

    23 term "Ex1 (\<lambda>(x, y). P x y)" 

    24 

    25 lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"

    26 apply(erule ex1E)

    27 apply(case_tac x)

    28 apply(clarify)

    29 apply(rule_tac a="aa" in ex1I)

    30 apply(rule ex1I)

    31 apply(assumption)

    32 apply(blast)

    33 apply(blast)

    34 done

    35 

    36 (*

    37 lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"

    38 apply(erule ex1E)

    39 apply(erule ex1E)

    40 apply(rule_tac a="(x, y)" in ex1I)

    41 apply(clarify)

    42 apply(case_tac xa)

    43 apply(clarify)

    44 

    45 apply(rule ex1I)

    46 apply(assumption)

    47 apply(blast)

    48 apply(blast)

    49 done

    50 

    51 apply(metis)