4 

     5 ML_command "ProofContext.debug := false"

     6 ML_command "ProofContext.verbose := false"

     7 

     8 ML {*

     9 val ctxt0 = @{context}

    10 val ty = Syntax.read_typ ctxt0 "bool"  

    11 val ctxt1 = Variable.declare_typ ty ctxt0 

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

    13 val trm' = Syntax.type_constraint ty trm

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

    15 val ctxt2 = Variable.declare_term trm'' ctxt1 

    16 *}

    17 

    18 term "split"

    19 

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

    21 

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

    23 apply(erule ex1E)

    24 apply(case_tac x)

    25 apply(clarify)

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

    27 apply(rule ex1I)

    28 apply(assumption)

    29 apply(blast)

    30 apply(blast)

    31 done

    32 

    33 (*

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

    35 apply(erule ex1E)

    36 apply(erule ex1E)

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

    38 apply(clarify)

    39 apply(case_tac xa)

    40 apply(clarify)

    41 

    42 apply(rule ex1I)

    43 apply(assumption)

    44 apply(blast)

    45 apply(blast)

    46 done

    47 

    48 apply(metis)

    49 *)