SeLFiE: Print_Is_Free, Print_Is_Var, Print_Is_Bound does not work for variables with question marks.

data61 / PSL

Other

65 stars 9 forks source link

SeLFiE: Print_Is_Free, Print_Is_Var, Print_Is_Bound does not work for variables with question marks. #179

Open yutakang opened 3 years ago

yutakang commented 3 years ago

In Hybrid_Logic.thy,

ML‹ try (Syntax.read_term @{context}) "?g" › lemma soundness': ‹n ⊢ branch ⟹ M, g ⊨⇩Θ branch ⟹ False›(!) assert_SeLFiE_true generalize_arguments_used_in_recursion_deep [on["branch"], arb["g"], rule["ST.induct"]] assert_SeLFiE_false generalize_arguments_used_in_recursion_deep [on["branch"], arb[ ], rule["ST.induct"]]

It was caused by is_variable.

yutakang commented 3 years ago

I am not sure what the right fix would be to this issue.

Should I remove the question marks?
Should I avoid using Is_Free, Is_Bound, Is_Var at least for inner cases?