From e6473c383b479610cee4c0119e5811a12a938cf9 Mon Sep 17 00:00:00 2001 From: Josh Chen Date: Tue, 14 Aug 2018 17:43:03 +0200 Subject: Well-formation rules are back in the methods; new theory synthesizing the natural number predecessor function. --- Equal.thy | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'Equal.thy') diff --git a/Equal.thy b/Equal.thy index 93f623f..9fc478a 100644 --- a/Equal.thy +++ b/Equal.thy @@ -46,17 +46,21 @@ and a: A \ \ ind\<^sub>=(f)(refl(a)) \ f(a)" + text "Admissible inference rules for equality type formation:" -(* + axiomatization where Equal_form_cond1: "a =\<^sub>A b: U(i) \ A: U(i)" and Equal_form_cond2: "a =\<^sub>A b: U(i) \ a: A" and Equal_form_cond3: "a =\<^sub>A b: U(i) \ b: A" -*) + + +text "Rule declarations:" + lemmas Equal_rules [intro] = Equal_form Equal_intro Equal_elim Equal_comp -(*lemmas Equal_wellform [intro] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3*) +lemmas Equal_wellform [wellform] = Equal_form_cond1 Equal_form_cond2 Equal_form_cond3 lemmas Equal_comps [comp] = Equal_comp -- cgit v1.2.3