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
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
