equal
deleted
inserted
replaced
260 (* ARITY CLAUSE *) |
260 (* ARITY CLAUSE *) |
261 fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = |
261 fun m_arity_cls (TConsLit ((c, _), (t, _), args)) = |
262 metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] |
262 metis_lit true c [Metis_Term.Fn(t, map (Metis_Term.Var o fst) args)] |
263 | m_arity_cls (TVarLit ((c, _), (s, _))) = |
263 | m_arity_cls (TVarLit ((c, _), (s, _))) = |
264 metis_lit false c [Metis_Term.Var s] |
264 metis_lit false c [Metis_Term.Var s] |
265 (*TrueI is returned as the Isabelle counterpart because there isn't any.*) |
265 (* TrueI is returned as the Isabelle counterpart because there isn't any. *) |
266 fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) = |
266 fun arity_cls ({prem_lits, concl_lits, ...} : arity_clause) = |
267 (TrueI, |
267 (TrueI, |
268 Metis_Thm.axiom (Metis_LiteralSet.fromList |
268 Metis_Thm.axiom (Metis_LiteralSet.fromList |
269 (map m_arity_cls (concl_lits :: prem_lits)))); |
269 (map m_arity_cls (concl_lits :: prem_lits)))); |
270 |
270 |