[isabelle-dev] Stymied by cryptic failure in Product_type.thy

[Josh Tilles]

I’m experimenting with separating the intuitionistic parts of HOL from the classical parts. (If anyone is interested, I’d be happy to describe my goals and/or motivations in more detail; for now I’ll stick to just the problem description)
Renaming HOL.thy to IHOL.thy did not cause any problems. I.e., `./bin/isabelle build HOL` still succeeded after commit 122bc618d6.
I then started extracting everything in (I)HOL.thy that depended on the axiom `True_or_False` to a file named CHOL.thy. Many of the ensuing failures I was able to handle, but I don’t know what to make of this one from Product_type.thy:

```
free_constructors case_prod for Pair fst snd
proof -
  fix P :: bool and p :: "'a × 'b"
  show "(⋀x1 x2. p = Pair x1 x2 ⟹ P) ⟹ P"
    by (cases p) (auto simp add: prod_def Pair_def Pair_Rep_def)
next
  fix a c :: 'a and b d :: 'b
  have "Pair_Rep a b = Pair_Rep c d ⟷ a = c ∧ b = d"
    by (auto simp add: Pair_Rep_def fun_eq_iff)
  moreover have "Pair_Rep a b ∈ prod" and "Pair_Rep c d ∈ prod"
    by (auto simp add: prod_def)
  ultimately show "Pair a b = Pair c d ⟷ a = c ∧ b = d"
    by (simp add: Pair_def Abs_prod_inject)
qed
```

jEdit underlines “qed” in red, claiming that:
```
Tactic failed
The error(s) above occurred for the goal statement:
P (local.prod.case_prod f prod) = (∀x1 x2. prod = Pair x1 x2 ⟶ P (f x1 x2))
```

You can get the code and run it yourself by running the following command:
git clone https://github.com/MerelyAPseudonym/isabelle.git --branch=IHOL-wip --depth=1


Thank you for any time you can spare,
--Josh
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140217/75e0da20/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140217/75e0da20/attachment.asc>