theory week05A_demo imports Main begin text \ In higher-order logic, we distinguish between *definitions* and *axioms*. When you make an Isabelle/HOL development, you can introduce both as you go along. Definitions are logically well-behaved. We expect our logic to satisfy some properties: - consistent (you can't prove false) - conservative (if you make a definition, and you prove a theorem whose statement doesn't mention the definition, then you could have proven your theorem without the definition) We want definitions to preserve consistency and be conservative. Axioms don't have be either. \ (* Now, our logic is inconsistent *) (* axiomatization b :: bool where b_def: "b \ \b" lemma False using b_def by blast *) text \ Isabelle (and other provers in the HOL family) have safeguards to make sure that definitions cannot introduce inconsistencies. In particular: the RHS of the definition must be a term that consists only of things that were already previously defined. In other words: definitions can't be self-referential. Therefore: inductive (and recursive) definitions don't exist. \ (* This def is rejected because we can't define things in terms of themselves *) definition b :: bool where "b \ \b" (* Q: so no recursive definitions -> no inconsistency? A: You can still make inconsistent logics without recursion. But most logical paradoxes tend to rely on self-reference (Russell's paradox) By removing self-reference, we remove a lot of footguns from the design of the logic. *) text \ The definition of Even must use the primitive definition mechanism as a backend somehow. Therefore, it can't *really* be an inductive definition, because that's self-referential. *) \ inductive Even where Even0[simp,intro!]: "Even 0" | EvenSuc[intro!]: "Even n \ Even (Suc (Suc n))" print_theorems term Even text \ Therefore, it must be defined in some other way than what it looks like. Then, the user is presented with an abstraction that looks like induction but really is defined in terms of something else. But what? Now: let's try to define the set Even, without induction. \ (* R is going to be the *characteristic functional* of the inference rules for Even. R(X) is the judgements I can conclude with a single application of the inference rules for Even, if I'm allowed to use premises from X. x \ X ______ _________ Suc(Suc x) \ R(X) 0 \ R(X) *) definition R :: "nat set \ nat set" where "R X \ {0} \ {Suc(Suc n) | n. n \ X}" value "R {}" value "R {0}" value "R(R {})" value "R(R(R {}))" value "R(R(R(R {})))" value "R {0}" value "R {1}" (* A set X if *consistent* with the inference rules of Even if, by a single application of the inference rules, we cannot escape X. *) definition R_consistent :: "nat set \ bool" where "R_consistent X \ R(X) \ X" lemma "R_consistent UNIV" by(simp add: R_consistent_def) (* We want an inductive definition with characteristic functional R to be the *least* R-consistent set. *) definition my_even :: "nat set" where "my_even \ \{X | X. R_consistent X}" (* The way we get the *least* R_consistent set is to take the intersection of all R_consistent sets. This intersection is (by definition) smaller than all of them, but we don't necessarily know if it's itself R_consistent. *) text \ We should be able to prove that the new @{term my_even} defined in terms of @{term R} is equivalent to the @{term Even} we defined using "inductive". \ lemma even_imp_my_even: assumes "Even x" shows "x \ my_even" using assms apply(induct rule: Even.induct) apply(simp add: my_even_def R_consistent_def R_def) apply(clarsimp simp add: my_even_def R_consistent_def R_def subset_eq) done lemma my_even_imp_even: assumes "x \ my_even" shows "Even x" using assms apply(clarsimp simp add: my_even_def R_consistent_def) apply(drule spec[where x="{n | n. Even n}"]) apply simp apply(erule mp) apply(simp add: subset_eq R_def) (* try also: apply clarify *) apply(rule allI) apply(rule impI) apply(erule exE) apply(erule conjE) apply(drule EvenSuc) apply simp done lemma my_even_eq_even: "x \ my_even \ Even x" (* FIXME *) find_theorems intro oops (* Example of a rule with a side condition *) inductive Something where "Something 0" | "\Something n; n \ 1\ \ Something (Suc (Suc n))" thm Even.induct Something.induct text \ Now here is a fixpoint-based characterisation of @{term my_even} in terms of @{term R}. \ definition my_second_even :: "nat set" where "my_second_even \ lfp R" (* A *fixed point* of a function f is an x such that f(x) = x The *least* fixed point is the intersection of all the fixed points. lfp has properties such as: lfp(f) = f(lfp(f)) *) lemma "my_second_even = my_even" (* FIXME *) oops text \ Example of an (incomplete) lattice: The natural numbers ordered by the standard \ nat is the carrier set \ is a pre-order (it is reflexive and transitive) therefore (nat, \) is a lattice Every finite set of numbers X has a a greatest lower bound: a number n s.t. forall x \ X, n \ x *and* for all other lower bounds m of X, m \ n. {2,3,4} has lower bounds: 0, 1 and 2. But, of all these lower bounds, 2 is the *greatest* lower bound. Similarly, every finite set of numbers has a least upper bound. That shows you that the natural numbers form a lattice, but they don't form a *complete* lattice. *Infinite* subsets of natural numbers have no least upper bound (there is no largest natural number). \ text \ Example of a complete lattice: The *sets* of natural numbers ordered by \ (As in our running example with R) nat set is the carrier set \ is a pre-order (it is reflexive and transitive) therefore (nat set, \) is a lattice It is a *complete* lattice because every subset of nat set has both a greatest lower bound and a least upper bound. Consequently (by the Knaster-Tarski Fixpoint Theorem) its fixpoints also have a greatest lower bound and least upper bound. This is what matters for us in defining X as the lfp of R. \ text \ We can also prove that @{term my_even} is @{term R_consistent}, using that it is monotonic. \ (* A function R is monotonic if X \ Y implies R(X) \ R(Y) *) lemma R_mono: "mono R" apply(simp add: mono_def subset_eq Ball_def R_def) apply blast done lemma "R_consistent(my_even)" unfolding R_consistent_def my_even_def apply(clarsimp simp add: subset_eq Ball_def) subgoal for y X using R_mono apply - apply(drule monoD[where x="my_even" and y=X]) apply(simp add: add: my_even_def R_consistent_def) apply blast apply(drule spec[where x=y]) apply(erule mp) apply(erule subsetD) apply(simp add: my_even_def R_consistent_def subset_eq Ball_def) done done end