Isaac Oscar Gariano (Sep 30 2021 at 03:08): Isaac Oscar Gariano (Sep 30 2021 at 03:08):I am curious, would something like this be admissiable in HOL:
axiomatization Proptrue :: ‹prop ⇒ bool› where
prop_iff_bool [simp]: ‹Trueprop (Proptrue P) ≡ P›
Then you can use meta-propositions in HOL ones, e.g:
lemma ‹Proptrue(P ⟹ Q) ⟶ (P ⟶ Q)› by(auto)
Sorry if this is a very dumb idea/question, I'm new to Isabelle!
Kevin Kappelmann (Sep 30 2021 at 10:52):admissible is not the right word in this context since your axiomatisation adds theorems about a new constant that previously were not derivable (since the constant did not exist).
I suppose you are interested in whether this would introduce any inconsistencies. I think it would not but you better ask an expert on the mailing list if you want to be sure (or maybe @Simon Roßkopf knows a simple argument?)
In any case, it does not seem like a good idea to add such a constant. Reasoning in isar using meta level connectives is more convenient than using object level connectives.
Isaac Oscar Gariano (Sep 30 2021 at 21:36):Yes your right, I did mean to say consistent, although now I wonder if this would be provable:
lemma LPropTrue:
fixes p :: ‹prop›
obtains b :: ‹bool› where ‹Trueprop b ≡ p›
sorry
I have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)
I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.
Isaac Oscar Gariano (Sep 30 2021 at 21:56):Also, on a related note what got me thinking about Proptrue was me trying to make some syntax sugar, but it keeps wrapping things in Trueprop:
syntax "_foo" :: ‹prop ⇒ prop ⇒ prop'› (‹⫿_›)
parse_ast_translation ‹[("_foo", fn _ => fn [body] => body)]›
However prop ‹⫿P›, and even ‹(⫿(P :: prop)) :: prop› reports a type error
Operator: Trueprop :: bool ⇒ prop
Operand: P :: prop
Using declare [[syntax_ast_trace]] the AST is apparently:
("\<^const>HOL.Trueprop" ("_constrain" ("\<^const>HOL.Trueprop" ("_constrain" P <position>)) "\<^type>prop"))
Interstingly, if I don't use ML and instead do
translations "⫿P" ⇀ "P"
It works as expected, but that's not sufficient as I have more complicated desugarings I want to do.
Kevin Kappelmann (Sep 30 2021 at 23:02):Isaac Oscar Gariano said:
Yes your right, I did mean to say consistent, although now I wonder if this would be provable:
lemma LPropTrue: fixes p :: ‹prop› obtains b :: ‹bool› where ‹Trueprop b ≡ p› sorryI have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)
I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.
That lemma is unprovable. The best you can do, given your axiomatisation for Proptrue, is this:
axiomatization Proptrue :: ‹prop ⇒ bool› where
prop_iff_bool [simp]: ‹Trueprop (Proptrue (PROP P)) ≡ PROP P›
lemma
fixes p :: ‹prop›
obtains ‹Trueprop True ≡ p› | ‹Trueprop False ≡ p›
proof -
assume
h1 : "Trueprop True ≡ p ⟹ thesis" and
h2 : "Trueprop False ≡ p ⟹ thesis"
have p_eq: "Trueprop (Proptrue p) ≡ p" by simp
have
h1' : "Trueprop True ≡ Trueprop (Proptrue p) ⟹ thesis" and
h2' : "Trueprop False ≡ Trueprop (Proptrue p) ⟹ thesis" by
(subst(asm) p_eq | fact h1 | fact h2)+
show thesis
proof (cases "Proptrue p")
case True
have "Trueprop True ≡ Trueprop (Proptrue p)" by (simp add: True)
then show thesis by (rule h1')
next
case False
hence "Trueprop False ≡ Trueprop (Proptrue p)" by simp
then show thesis by (rule h2')
qed
qed
You can, in theory, axiomatise all HOL operators to live in prop but then you loose the distinction between meta-level and object level logic. You want to keep you meta logic simple and separate from your object logic
Last updated: Dec 21 2024 at 16:20 UTC