Commit 2c43d3de by Jean-Christophe

### new theory list.Distinct

`new theory number for... number theory`
parent f259ae47
 (* Tree relabelling. Given a tree t, with values at the leaves, build a new tree with the same structure and leaves labelled with distinct integers. *) module Relabel use import list.Mem use import list.Append use import list.Distinct type tree 'a = | Leaf 'a ... ... @@ -14,11 +21,11 @@ module Relabel end lemma labels_Leaf : forall x y : 'a. mem x (labels (Leaf y)) <-> x=y forall x y : 'a. mem x (labels (Leaf y)) <-> x=y lemma labels_Node : forall x : 'a, l r : tree 'a. mem x (labels (Node l r)) <-> (mem x (labels l) or mem x (labels r)) forall x : 'a, l r : tree 'a. mem x (labels (Node l r)) <-> (mem x (labels l) or mem x (labels r)) inductive same_shape (t1 : tree 'a) (t2 : tree 'b) = | same_shape_Leaf : ... ... @@ -29,25 +36,13 @@ module Relabel same_shape l1 l2 -> same_shape r1 r2 -> same_shape (Node l1 r1) (Node l2 r2) (* should be in the library? *) inductive distinct (l : list 'a) = | distinct_zero : distinct (Nil : list 'a) | distinct_one : forall x:'a. distinct (Cons x Nil) | distinct_many : forall x :'a, l : list 'a. not (mem x l) -> distinct l -> distinct (Cons x l) lemma distinct_append : forall l1 l2 : list 'a. distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) use import int.Int use import module stdlib.Ref parameter r : ref int let fresh () = {} r := !r + 1; !r { r = old r + 1 and result = r } let fresh () = {} r := !r + 1; !r { r = old r + 1 and result = r } let rec relabel (t : tree 'a) : tree int = {} ... ...
 ... ... @@ -2,7 +2,6 @@ (* graph theory *) theory Path use import list.Mem type graph ... ... @@ -18,18 +17,39 @@ theory Path path g src v1 -> edge g v1 v2 -> path g v2 dst -> path g src dst lemma path_left_extension : forall g : graph, v1 v2 v3 : vertex. edge g v1 v2 -> path g v2 v3 -> path g v1 v3 lemma path_right_extension : forall g : graph, v1 v2 v3 : vertex. path g v1 v2 -> edge g v2 v3 -> path g v1 v3 end (* theory SimplePath use import list.List use import list.Mem type graph type vertex logic edge graph vertex vertex (* [simple_path g src [x1;...;xn] dst] is a path src --> x1 --> x2 --> ... --> xn --> dst without repetition. *) inductive simple_path graph vertex (list vertex) vertex = | Path_empty : forall g:graph, v:vertex. simple_path g v (Nil : list vertex) v | Path_cons : forall g:graph, src v dst : vertex, l : list vertex. simple_path g v l dst -> edge g src v -> not mem v l -> edge g src v -> src <> v -> simple_path g v l dst -> not mem src l -> simple_path g src (Cons v l) dst logic simple_cycle(g : graph, v : vertex) = logic simple_cycle (g : graph) (v : vertex) = exists l : list vertex. l <> Nil and simple_path g v l v *) end
 ... ... @@ -197,6 +197,27 @@ theory Permut end theory Distinct use import List use import Mem inductive distinct (l : list 'a) = | distinct_zero : distinct (Nil : list 'a) | distinct_one : forall x:'a. distinct (Cons x Nil) | distinct_many : forall x :'a, l : list 'a. not (mem x l) -> distinct l -> distinct (Cons x l) use import Append lemma distinct_append : forall l1 l2 : list 'a. distinct l1 -> distinct l2 -> (forall x:'a. mem x l1 -> not (mem x l2)) -> distinct (l1 ++ l2) end theory Induction use import List ... ... @@ -243,3 +264,9 @@ theory ListRich use export NumOcc use export Permut end (* Local Variables: compile-command: "make -C .. theories/list" End: *)
 (* number theory *) theory Divisibility use export int.Int logic divides (d:int) (n:int) = exists q:int. n = q * d lemma divides_refl : forall n:int. divides n n lemma divides_1 : forall n:int. divides 1 n lemma divides_0 : forall n:int. divides n 0 lemma divides_left : forall a b c : int. divides a b -> divides (c*a) (c*b) lemma divides_right: forall a b c : int. divides a b -> divides (a*c) (b*c) lemma divides_oppr: forall a b : int. divides a b -> divides a (-b) lemma divides_oppl: forall a b : int. divides a b -> divides (-a) b lemma divides_oppr_rev: forall a b : int. divides (-a) b -> divides a b lemma divides_oppl_rev: forall a b : int. divides a (-b) -> divides a b lemma divides_plusr: forall a b c : int. divides a b -> divides a c -> divides a (b + c) lemma divides_minusr: forall a b c : int. divides a b -> divides a c -> divides a (b - c) lemma divides_multl: forall a b c : int. divides a b -> divides a (c * b) lemma divides_multr: forall a b c : int. divides a b -> divides a (b * c) lemma divides_factorl: forall a b : int. divides a (b * a) lemma divides_factorr: forall a b : int. divides a (a * b) lemma divides1 : forall x : int. divides x 1 -> x = 1 or x = -1 lemma divides_antisym : forall a b : int. divides a b -> divides b a -> a = b or a = -b lemma divides_trans : forall a b c : int. divides a b -> divides b c -> divides a c use import int.Abs lemma divides_bounds : forall a b : int. divides a b -> b <> 0 -> abs a <= abs b use import int.EuclideanDivision lemma mod_divides : forall a b : int. b <> 0 -> mod a b = 0 -> divides b a lemma divides_mod : forall a b : int. b <> 0 -> divides b a -> mod a b = 0 end theory Gcd use export int.Int use import Divisibility logic gcd int int : int axiom gcd_nonneg : forall a b : int. 0 <= gcd a b axiom gcd_def1 : forall a b : int. divides (gcd a b) a axiom gcd_def2 : forall a b : int. divides (gcd a b) b axiom gcd_def3 : forall a b x : int. divides x a -> divides x b -> divides x (gcd a b) (* TODO: lemmas *) clone algebra.AC with type t = int, logic op = gcd end theory Prime use export int.Int use import Divisibility use import Gcd logic rel_prime (a b : int) = gcd a b = 1 logic prime (p : int) = 2 <= p && forall n:int. 1 <= n < p -> rel_prime n p lemma prime_divisors : forall p : int. prime p -> forall d : int. divides d p -> d = 1 or d = -1 or d = p or d = -p lemma not_prime_1 : not (prime 1) lemma prime_2 : prime 2 lemma prime_3 : prime 3 lemma prime_alt_def : forall p : int. prime p <-> 2 <= p and forall n : int. 1 not (divides n p) end (* Local Variables: compile-command: "make -C .. theories/number" End: *)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!