<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">On 17.02.2014 19:55, Josh Tilles wrote:<br>
</div>
<blockquote
cite="mid:DEFC23DE-91BA-4D90-8D10-509E9CE75463@gmail.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html;
charset=ISO-8859-1">
<div>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)</div>
<div>Renaming HOL.thy to IHOL.thy did not cause any problems.
I.e., `./bin/isabelle build HOL` still succeeded after commit <a
moz-do-not-send="true"
href="https://github.com/MerelyAPseudonym/isabelle/tree/122bc618d65927d16877b1107e91224ba3bfbaf8">122bc618d6</a>.</div>
<div>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:</div>
<div><br>
</div>
<div>```</div>
<blockquote style="margin: 0 0 0 40px; border: none; padding:
0px;">
<div>free_constructors case_prod for Pair fst snd</div>
<div>proof -</div>
<div> fix P :: bool and p :: "'a × 'b"</div>
<div> show "(⋀x1 x2. p = Pair x1 x2 ⟹ P) ⟹ P"</div>
<div> by (cases p) (auto simp add: prod_def Pair_def
Pair_Rep_def)</div>
<div>next</div>
<div> fix a c :: 'a and b d :: 'b</div>
<div> have "Pair_Rep a b = Pair_Rep c d ⟷ a = c ∧ b = d"</div>
<div> by (auto simp add: Pair_Rep_def fun_eq_iff)</div>
<div> moreover have "Pair_Rep a b ∈ prod" and "Pair_Rep c d ∈
prod"</div>
<div> by (auto simp add: prod_def)</div>
<div> ultimately show "Pair a b = Pair c d ⟷ a = c ∧ b = d"</div>
<div> by (simp add: Pair_def Abs_prod_inject)</div>
<div>qed</div>
</blockquote>
<div>```</div>
<div><br>
</div>
<div>jEdit underlines “qed” in red, claiming that:</div>
<div>```</div>
<blockquote style="margin: 0 0 0 40px; border: none; padding:
0px;">
<div>Tactic failed</div>
<div>The error(s) above occurred for the goal statement:</div>
<div>P (local.prod.case_prod f prod) = (∀x1 x2. prod = Pair x1
x2 ⟶ P (f x1 x2))</div>
</blockquote>
```<br>
</blockquote>
The position of the error message is a bit misleading. It is not the
qed which fails. Instead, after finishing the proof, the
free_constructors command tries to prove something on its own -- and
fails. Probably, its internal tactics depend on the choice axiom.<br>
<br>
BTW: Whoever wrote this proof: The first case would be better stated
as<br>
<br>
assume "⋀x1 x2. p = Pair x1 x2 ⟹ P" then show "P"<br>
<br>
because meta-implication in show-statements may lead to
counter-intuitive behaviour.<br>
<br>
Best regards,<br>
Lars<br>
</body>
</html>