# HG changeset patch # User krauss # Date 1267459557 -3600 # Node ID d78659d1723e5a847ced672fe0d3e5dcaf1ace82 # Parent 83b0f75810f02f121bb1055ee539778ab517b09e more recdef (and old primrec) hunting diff -r 83b0f75810f0 -r d78659d1723e src/HOL/Hoare/Pointer_Examples.thy --- a/src/HOL/Hoare/Pointer_Examples.thy Mon Mar 01 16:42:45 2010 +0100 +++ b/src/HOL/Hoare/Pointer_Examples.thy Mon Mar 01 17:05:57 2010 +0100 @@ -222,13 +222,11 @@ definition cand :: "bool \ bool \ bool" where "cand P Q == if P then Q else False" -consts merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" - -recdef merge "measure(%(xs,ys,f). size xs + size ys)" +fun merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" where "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) - else y # merge(x#xs,ys,f))" -"merge(x#xs,[],f) = x # merge(xs,[],f)" -"merge([],y#ys,f) = y # merge([],ys,f)" + else y # merge(x#xs,ys,f))" | +"merge(x#xs,[],f) = x # merge(xs,[],f)" | +"merge([],y#ys,f) = y # merge([],ys,f)" | "merge([],[],f) = []" text{* Simplifies the proof a little: *} diff -r 83b0f75810f0 -r d78659d1723e src/HOL/Hoare/Pointers0.thy --- a/src/HOL/Hoare/Pointers0.thy Mon Mar 01 16:42:45 2010 +0100 +++ b/src/HOL/Hoare/Pointers0.thy Mon Mar 01 17:05:57 2010 +0100 @@ -320,13 +320,11 @@ text"This is still a bit rough, especially the proof." -consts merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" - -recdef merge "measure(%(xs,ys,f). size xs + size ys)" +fun merge :: "'a list * 'a list * ('a \ 'a \ bool) \ 'a list" where "merge(x#xs,y#ys,f) = (if f x y then x # merge(xs,y#ys,f) - else y # merge(x#xs,ys,f))" -"merge(x#xs,[],f) = x # merge(xs,[],f)" -"merge([],y#ys,f) = y # merge([],ys,f)" + else y # merge(x#xs,ys,f))" | +"merge(x#xs,[],f) = x # merge(xs,[],f)" | +"merge([],y#ys,f) = y # merge([],ys,f)" | "merge([],[],f) = []" lemma imp_disjCL: "(P|Q \ R) = ((P \ R) \ (~P \ Q \ R))" diff -r 83b0f75810f0 -r d78659d1723e src/HOL/Induct/Tree.thy --- a/src/HOL/Induct/Tree.thy Mon Mar 01 16:42:45 2010 +0100 +++ b/src/HOL/Induct/Tree.thy Mon Mar 01 17:05:57 2010 +0100 @@ -13,20 +13,20 @@ Atom 'a | Branch "nat => 'a tree" -consts +primrec map_tree :: "('a => 'b) => 'a tree => 'b tree" -primrec +where "map_tree f (Atom a) = Atom (f a)" - "map_tree f (Branch ts) = Branch (\x. map_tree f (ts x))" +| "map_tree f (Branch ts) = Branch (\x. map_tree f (ts x))" lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \ f) t" by (induct t) simp_all -consts +primrec exists_tree :: "('a => bool) => 'a tree => bool" -primrec +where "exists_tree P (Atom a) = P a" - "exists_tree P (Branch ts) = (\x. exists_tree P (ts x))" +| "exists_tree P (Branch ts) = (\x. exists_tree P (ts x))" lemma exists_map: "(!!x. P x ==> Q (f x)) ==> @@ -39,23 +39,23 @@ datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer" text{*Addition of ordinals*} -consts +primrec add :: "[brouwer,brouwer] => brouwer" -primrec +where "add i Zero = i" - "add i (Succ j) = Succ (add i j)" - "add i (Lim f) = Lim (%n. add i (f n))" +| "add i (Succ j) = Succ (add i j)" +| "add i (Lim f) = Lim (%n. add i (f n))" lemma add_assoc: "add (add i j) k = add i (add j k)" by (induct k) auto text{*Multiplication of ordinals*} -consts +primrec mult :: "[brouwer,brouwer] => brouwer" -primrec +where "mult i Zero = Zero" - "mult i (Succ j) = add (mult i j) i" - "mult i (Lim f) = Lim (%n. mult i (f n))" +| "mult i (Succ j) = add (mult i j) i" +| "mult i (Lim f) = Lim (%n. mult i (f n))" lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)" by (induct k) (auto simp add: add_assoc) @@ -83,7 +83,7 @@ lemma wf_brouwer_pred: "wf brouwer_pred" by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+) -lemma wf_brouwer_order: "wf brouwer_order" +lemma wf_brouwer_order[simp]: "wf brouwer_order" by(unfold brouwer_order_def, rule wf_trancl[OF wf_brouwer_pred]) lemma [simp]: "(j, Succ j) : brouwer_order" @@ -92,14 +92,16 @@ lemma [simp]: "(f n, Lim f) : brouwer_order" by(auto simp add: brouwer_order_def brouwer_pred_def) -text{*Example of a recdef*} -consts +text{*Example of a general function*} + +function add2 :: "(brouwer*brouwer) => brouwer" -recdef add2 "inv_image brouwer_order (\ (x,y). y)" +where "add2 (i, Zero) = i" - "add2 (i, (Succ j)) = Succ (add2 (i, j))" - "add2 (i, (Lim f)) = Lim (\ n. add2 (i, (f n)))" - (hints recdef_wf: wf_brouwer_order) +| "add2 (i, (Succ j)) = Succ (add2 (i, j))" +| "add2 (i, (Lim f)) = Lim (\ n. add2 (i, (f n)))" +by pat_completeness auto +termination by (relation "inv_image brouwer_order snd") auto lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))" by (induct k) auto diff -r 83b0f75810f0 -r d78659d1723e src/HOL/ex/ReflectionEx.thy --- a/src/HOL/ex/ReflectionEx.thy Mon Mar 01 16:42:45 2010 +0100 +++ b/src/HOL/ex/ReflectionEx.thy Mon Mar 01 17:05:57 2010 +0100 @@ -69,28 +69,29 @@ oops text{* Let's perform NNF. This is a version that tends to generate disjunctions *} -consts fmsize :: "fm \ nat" -primrec +primrec fmsize :: "fm \ nat" where "fmsize (At n) = 1" - "fmsize (NOT p) = 1 + fmsize p" - "fmsize (And p q) = 1 + fmsize p + fmsize q" - "fmsize (Or p q) = 1 + fmsize p + fmsize q" - "fmsize (Imp p q) = 2 + fmsize p + fmsize q" - "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q" +| "fmsize (NOT p) = 1 + fmsize p" +| "fmsize (And p q) = 1 + fmsize p + fmsize q" +| "fmsize (Or p q) = 1 + fmsize p + fmsize q" +| "fmsize (Imp p q) = 2 + fmsize p + fmsize q" +| "fmsize (Iff p q) = 2 + 2* fmsize p + 2* fmsize q" + +lemma [measure_function]: "is_measure fmsize" .. -consts nnf :: "fm \ fm" -recdef nnf "measure fmsize" +fun nnf :: "fm \ fm" +where "nnf (At n) = At n" - "nnf (And p q) = And (nnf p) (nnf q)" - "nnf (Or p q) = Or (nnf p) (nnf q)" - "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)" - "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))" - "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))" - "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))" - "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))" - "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))" - "nnf (NOT (NOT p)) = nnf p" - "nnf (NOT p) = NOT p" +| "nnf (And p q) = And (nnf p) (nnf q)" +| "nnf (Or p q) = Or (nnf p) (nnf q)" +| "nnf (Imp p q) = Or (nnf (NOT p)) (nnf q)" +| "nnf (Iff p q) = Or (And (nnf p) (nnf q)) (And (nnf (NOT p)) (nnf (NOT q)))" +| "nnf (NOT (And p q)) = Or (nnf (NOT p)) (nnf (NOT q))" +| "nnf (NOT (Or p q)) = And (nnf (NOT p)) (nnf (NOT q))" +| "nnf (NOT (Imp p q)) = And (nnf p) (nnf (NOT q))" +| "nnf (NOT (Iff p q)) = Or (And (nnf p) (nnf (NOT q))) (And (nnf (NOT p)) (nnf q))" +| "nnf (NOT (NOT p)) = nnf p" +| "nnf (NOT p) = NOT p" text{* The correctness theorem of nnf: it preserves the semantics of fm *} lemma nnf[reflection]: "Ifm (nnf p) vs = Ifm p vs" @@ -113,22 +114,22 @@ datatype num = C nat | Add num num | Mul nat num | Var nat | CN nat nat num text{* This is just technical to make recursive definitions easier. *} -consts num_size :: "num \ nat" -primrec +primrec num_size :: "num \ nat" +where "num_size (C c) = 1" - "num_size (Var n) = 1" - "num_size (Add a b) = 1 + num_size a + num_size b" - "num_size (Mul c a) = 1 + num_size a" - "num_size (CN n c a) = 4 + num_size a " +| "num_size (Var n) = 1" +| "num_size (Add a b) = 1 + num_size a + num_size b" +| "num_size (Mul c a) = 1 + num_size a" +| "num_size (CN n c a) = 4 + num_size a " text{* The semantics of num *} -consts Inum:: "num \ nat list \ nat" -primrec +primrec Inum:: "num \ nat list \ nat" +where Inum_C : "Inum (C i) vs = i" - Inum_Var: "Inum (Var n) vs = vs!n" - Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs " - Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs " - Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs " +| Inum_Var: "Inum (Var n) vs = vs!n" +| Inum_Add: "Inum (Add s t) vs = Inum s vs + Inum t vs " +| Inum_Mul: "Inum (Mul c t) vs = c * Inum t vs " +| Inum_CN : "Inum (CN n c t) vs = c*(vs!n) + Inum t vs " text{* Let's reify some nat expressions \dots *} @@ -168,39 +169,41 @@ apply (reify Inum_eqs' ("1 * (2*x + (y::nat) + 0 + 1)")) oops text{* Okay, let's try reflection. Some simplifications on num follow. You can skim until the main theorem @{text linum} *} -consts lin_add :: "num \ num \ num" -recdef lin_add "measure (\(x,y). ((size x) + (size y)))" - "lin_add (CN n1 c1 r1,CN n2 c2 r2) = +fun lin_add :: "num \ num \ num" +where + "lin_add (CN n1 c1 r1) (CN n2 c2 r2) = (if n1=n2 then (let c = c1 + c2 - in (if c=0 then lin_add(r1,r2) else CN n1 c (lin_add (r1,r2)))) - else if n1 \ n2 then (CN n1 c1 (lin_add (r1,CN n2 c2 r2))) - else (CN n2 c2 (lin_add (CN n1 c1 r1,r2))))" - "lin_add (CN n1 c1 r1,t) = CN n1 c1 (lin_add (r1, t))" - "lin_add (t,CN n2 c2 r2) = CN n2 c2 (lin_add (t,r2))" - "lin_add (C b1, C b2) = C (b1+b2)" - "lin_add (a,b) = Add a b" -lemma lin_add: "Inum (lin_add (t,s)) bs = Inum (Add t s) bs" + in (if c=0 then lin_add r1 r2 else CN n1 c (lin_add r1 r2))) + else if n1 \ n2 then (CN n1 c1 (lin_add r1 (CN n2 c2 r2))) + else (CN n2 c2 (lin_add (CN n1 c1 r1) r2)))" +| "lin_add (CN n1 c1 r1) t = CN n1 c1 (lin_add r1 t)" +| "lin_add t (CN n2 c2 r2) = CN n2 c2 (lin_add t r2)" +| "lin_add (C b1) (C b2) = C (b1+b2)" +| "lin_add a b = Add a b" +lemma lin_add: "Inum (lin_add t s) bs = Inum (Add t s) bs" apply (induct t s rule: lin_add.induct, simp_all add: Let_def) apply (case_tac "c1+c2 = 0",case_tac "n1 \ n2", simp_all) by (case_tac "n1 = n2", simp_all add: algebra_simps) -consts lin_mul :: "num \ nat \ num" -recdef lin_mul "measure size " - "lin_mul (C j) = (\ i. C (i*j))" - "lin_mul (CN n c a) = (\ i. if i=0 then (C 0) else CN n (i*c) (lin_mul a i))" - "lin_mul t = (\ i. Mul i t)" +fun lin_mul :: "num \ nat \ num" +where + "lin_mul (C j) i = C (i*j)" +| "lin_mul (CN n c a) i = (if i=0 then (C 0) else CN n (i*c) (lin_mul a i))" +| "lin_mul t i = (Mul i t)" lemma lin_mul: "Inum (lin_mul t i) bs = Inum (Mul i t) bs" -by (induct t arbitrary: i rule: lin_mul.induct, auto simp add: algebra_simps) +by (induct t i rule: lin_mul.induct, auto simp add: algebra_simps) -consts linum:: "num \ num" -recdef linum "measure num_size" +lemma [measure_function]: "is_measure num_size" .. + +fun linum:: "num \ num" +where "linum (C b) = C b" - "linum (Var n) = CN n 1 (C 0)" - "linum (Add t s) = lin_add (linum t, linum s)" - "linum (Mul c t) = lin_mul (linum t) c" - "linum (CN n c t) = lin_add (linum (Mul c (Var n)),linum t)" +| "linum (Var n) = CN n 1 (C 0)" +| "linum (Add t s) = lin_add (linum t) (linum s)" +| "linum (Mul c t) = lin_mul (linum t) c" +| "linum (CN n c t) = lin_add (linum (Mul c (Var n))) (linum t)" lemma linum[reflection] : "Inum (linum t) bs = Inum t bs" by (induct t rule: linum.induct, simp_all add: lin_mul lin_add) @@ -214,30 +217,32 @@ datatype aform = Lt num num | Eq num num | Ge num num | NEq num num | Conj aform aform | Disj aform aform | NEG aform | T | F -consts linaformsize:: "aform \ nat" -recdef linaformsize "measure size" + +primrec linaformsize:: "aform \ nat" +where "linaformsize T = 1" - "linaformsize F = 1" - "linaformsize (Lt a b) = 1" - "linaformsize (Ge a b) = 1" - "linaformsize (Eq a b) = 1" - "linaformsize (NEq a b) = 1" - "linaformsize (NEG p) = 2 + linaformsize p" - "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q" - "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q" +| "linaformsize F = 1" +| "linaformsize (Lt a b) = 1" +| "linaformsize (Ge a b) = 1" +| "linaformsize (Eq a b) = 1" +| "linaformsize (NEq a b) = 1" +| "linaformsize (NEG p) = 2 + linaformsize p" +| "linaformsize (Conj p q) = 1 + linaformsize p + linaformsize q" +| "linaformsize (Disj p q) = 1 + linaformsize p + linaformsize q" +lemma [measure_function]: "is_measure linaformsize" .. -consts is_aform :: "aform => nat list => bool" -primrec +primrec is_aform :: "aform => nat list => bool" +where "is_aform T vs = True" - "is_aform F vs = False" - "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)" - "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)" - "is_aform (Ge a b) vs = (Inum a vs \ Inum b vs)" - "is_aform (NEq a b) vs = (Inum a vs \ Inum b vs)" - "is_aform (NEG p) vs = (\ (is_aform p vs))" - "is_aform (Conj p q) vs = (is_aform p vs \ is_aform q vs)" - "is_aform (Disj p q) vs = (is_aform p vs \ is_aform q vs)" +| "is_aform F vs = False" +| "is_aform (Lt a b) vs = (Inum a vs < Inum b vs)" +| "is_aform (Eq a b) vs = (Inum a vs = Inum b vs)" +| "is_aform (Ge a b) vs = (Inum a vs \ Inum b vs)" +| "is_aform (NEq a b) vs = (Inum a vs \ Inum b vs)" +| "is_aform (NEG p) vs = (\ (is_aform p vs))" +| "is_aform (Conj p q) vs = (is_aform p vs \ is_aform q vs)" +| "is_aform (Disj p q) vs = (is_aform p vs \ is_aform q vs)" text{* Let's reify and do reflection *} lemma "(3::nat)*x + t < 0 \ (2 * x + y \ 17)" @@ -250,24 +255,25 @@ oops text{* For reflection we now define a simple transformation on aform: NNF + linum on atoms *} -consts linaform:: "aform \ aform" -recdef linaform "measure linaformsize" + +fun linaform:: "aform \ aform" +where "linaform (Lt s t) = Lt (linum s) (linum t)" - "linaform (Eq s t) = Eq (linum s) (linum t)" - "linaform (Ge s t) = Ge (linum s) (linum t)" - "linaform (NEq s t) = NEq (linum s) (linum t)" - "linaform (Conj p q) = Conj (linaform p) (linaform q)" - "linaform (Disj p q) = Disj (linaform p) (linaform q)" - "linaform (NEG T) = F" - "linaform (NEG F) = T" - "linaform (NEG (Lt a b)) = Ge a b" - "linaform (NEG (Ge a b)) = Lt a b" - "linaform (NEG (Eq a b)) = NEq a b" - "linaform (NEG (NEq a b)) = Eq a b" - "linaform (NEG (NEG p)) = linaform p" - "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))" - "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))" - "linaform p = p" +| "linaform (Eq s t) = Eq (linum s) (linum t)" +| "linaform (Ge s t) = Ge (linum s) (linum t)" +| "linaform (NEq s t) = NEq (linum s) (linum t)" +| "linaform (Conj p q) = Conj (linaform p) (linaform q)" +| "linaform (Disj p q) = Disj (linaform p) (linaform q)" +| "linaform (NEG T) = F" +| "linaform (NEG F) = T" +| "linaform (NEG (Lt a b)) = Ge a b" +| "linaform (NEG (Ge a b)) = Lt a b" +| "linaform (NEG (Eq a b)) = NEq a b" +| "linaform (NEG (NEq a b)) = Eq a b" +| "linaform (NEG (NEG p)) = linaform p" +| "linaform (NEG (Conj p q)) = Disj (linaform (NEG p)) (linaform (NEG q))" +| "linaform (NEG (Disj p q)) = Conj (linaform (NEG p)) (linaform (NEG q))" +| "linaform p = p" lemma linaform: "is_aform (linaform p) vs = is_aform p vs" by (induct p rule: linaform.induct) (auto simp add: linum) @@ -283,11 +289,11 @@ text{* We now give an example where Interpretaions have 0 or more than only one envornement of different types and show that automatic reification also deals with binding *} datatype rb = BC bool| BAnd rb rb | BOr rb rb -consts Irb :: "rb \ bool" -primrec +primrec Irb :: "rb \ bool" +where "Irb (BC p) = p" - "Irb (BAnd s t) = (Irb s \ Irb t)" - "Irb (BOr s t) = (Irb s \ Irb t)" +| "Irb (BAnd s t) = (Irb s \ Irb t)" +| "Irb (BOr s t) = (Irb s \ Irb t)" lemma "A \ (B \ D \ B) \ A \ (B \ D \ B) \ A \ (B \ D \ B) \ A \ (B \ D \ B)" apply (reify Irb.simps) @@ -295,14 +301,14 @@ datatype rint = IC int| IVar nat | IAdd rint rint | IMult rint rint | INeg rint | ISub rint rint -consts Irint :: "rint \ int list \ int" -primrec -Irint_Var: "Irint (IVar n) vs = vs!n" -Irint_Neg: "Irint (INeg t) vs = - Irint t vs" -Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs" -Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs" -Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs" -Irint_C: "Irint (IC i) vs = i" +primrec Irint :: "rint \ int list \ int" +where + Irint_Var: "Irint (IVar n) vs = vs!n" +| Irint_Neg: "Irint (INeg t) vs = - Irint t vs" +| Irint_Add: "Irint (IAdd s t) vs = Irint s vs + Irint t vs" +| Irint_Sub: "Irint (ISub s t) vs = Irint s vs - Irint t vs" +| Irint_Mult: "Irint (IMult s t) vs = Irint s vs * Irint t vs" +| Irint_C: "Irint (IC i) vs = i" lemma Irint_C0: "Irint (IC 0) vs = 0" by simp lemma Irint_C1: "Irint (IC 1) vs = 1" @@ -314,12 +320,12 @@ apply (reify Irint_simps ("(3::int) * x + y*y - 9 + (- z)")) oops datatype rlist = LVar nat| LEmpty| LCons rint rlist | LAppend rlist rlist -consts Irlist :: "rlist \ int list \ (int list) list \ (int list)" -primrec +primrec Irlist :: "rlist \ int list \ (int list) list \ (int list)" +where "Irlist (LEmpty) is vs = []" - "Irlist (LVar n) is vs = vs!n" - "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))" - "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)" +| "Irlist (LVar n) is vs = vs!n" +| "Irlist (LCons i t) is vs = ((Irint i is)#(Irlist t is vs))" +| "Irlist (LAppend s t) is vs = (Irlist s is vs) @ (Irlist t is vs)" lemma "[(1::int)] = []" apply (reify Irlist.simps Irint_simps ("[1]:: int list")) oops @@ -329,16 +335,16 @@ oops datatype rnat = NC nat| NVar nat| NSuc rnat | NAdd rnat rnat | NMult rnat rnat | NNeg rnat | NSub rnat rnat | Nlgth rlist -consts Irnat :: "rnat \ int list \ (int list) list \ nat list \ nat" -primrec -Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)" -Irnat_Var: "Irnat (NVar n) is ls vs = vs!n" -Irnat_Neg: "Irnat (NNeg t) is ls vs = 0" -Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs" -Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs" -Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs" -Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)" -Irnat_C: "Irnat (NC i) is ls vs = i" +primrec Irnat :: "rnat \ int list \ (int list) list \ nat list \ nat" +where + Irnat_Suc: "Irnat (NSuc t) is ls vs = Suc (Irnat t is ls vs)" +| Irnat_Var: "Irnat (NVar n) is ls vs = vs!n" +| Irnat_Neg: "Irnat (NNeg t) is ls vs = 0" +| Irnat_Add: "Irnat (NAdd s t) is ls vs = Irnat s is ls vs + Irnat t is ls vs" +| Irnat_Sub: "Irnat (NSub s t) is ls vs = Irnat s is ls vs - Irnat t is ls vs" +| Irnat_Mult: "Irnat (NMult s t) is ls vs = Irnat s is ls vs * Irnat t is ls vs" +| Irnat_lgth: "Irnat (Nlgth rxs) is ls vs = length (Irlist rxs is ls)" +| Irnat_C: "Irnat (NC i) is ls vs = i" lemma Irnat_C0: "Irnat (NC 0) is ls vs = 0" by simp lemma Irnat_C1: "Irnat (NC 1) is ls vs = 1" @@ -356,26 +362,26 @@ | RNEX rifm | RIEX rifm| RLEX rifm | RNALL rifm | RIALL rifm| RLALL rifm | RBEX rifm | RBALL rifm -consts Irifm :: "rifm \ bool list \ int list \ (int list) list \ nat list \ bool" -primrec -"Irifm RT ps is ls ns = True" -"Irifm RF ps is ls ns = False" -"Irifm (RVar n) ps is ls ns = ps!n" -"Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)" -"Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)" -"Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)" -"Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" -"Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" -"Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" -"Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)" -"Irifm (RNEX p) ps is ls ns = (\x. Irifm p ps is ls (x#ns))" -"Irifm (RIEX p) ps is ls ns = (\x. Irifm p ps (x#is) ls ns)" -"Irifm (RLEX p) ps is ls ns = (\x. Irifm p ps is (x#ls) ns)" -"Irifm (RBEX p) ps is ls ns = (\x. Irifm p (x#ps) is ls ns)" -"Irifm (RNALL p) ps is ls ns = (\x. Irifm p ps is ls (x#ns))" -"Irifm (RIALL p) ps is ls ns = (\x. Irifm p ps (x#is) ls ns)" -"Irifm (RLALL p) ps is ls ns = (\x. Irifm p ps is (x#ls) ns)" -"Irifm (RBALL p) ps is ls ns = (\x. Irifm p (x#ps) is ls ns)" +primrec Irifm :: "rifm \ bool list \ int list \ (int list) list \ nat list \ bool" +where + "Irifm RT ps is ls ns = True" +| "Irifm RF ps is ls ns = False" +| "Irifm (RVar n) ps is ls ns = ps!n" +| "Irifm (RNLT s t) ps is ls ns = (Irnat s is ls ns < Irnat t is ls ns)" +| "Irifm (RNILT s t) ps is ls ns = (int (Irnat s is ls ns) < Irint t is)" +| "Irifm (RNEQ s t) ps is ls ns = (Irnat s is ls ns = Irnat t is ls ns)" +| "Irifm (RAnd p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" +| "Irifm (ROr p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" +| "Irifm (RImp p q) ps is ls ns = (Irifm p ps is ls ns \ Irifm q ps is ls ns)" +| "Irifm (RIff p q) ps is ls ns = (Irifm p ps is ls ns = Irifm q ps is ls ns)" +| "Irifm (RNEX p) ps is ls ns = (\x. Irifm p ps is ls (x#ns))" +| "Irifm (RIEX p) ps is ls ns = (\x. Irifm p ps (x#is) ls ns)" +| "Irifm (RLEX p) ps is ls ns = (\x. Irifm p ps is (x#ls) ns)" +| "Irifm (RBEX p) ps is ls ns = (\x. Irifm p (x#ps) is ls ns)" +| "Irifm (RNALL p) ps is ls ns = (\x. Irifm p ps is ls (x#ns))" +| "Irifm (RIALL p) ps is ls ns = (\x. Irifm p ps (x#is) ls ns)" +| "Irifm (RLALL p) ps is ls ns = (\x. Irifm p ps is (x#ls) ns)" +| "Irifm (RBALL p) ps is ls ns = (\x. Irifm p (x#ps) is ls ns)" lemma " \x. \n. ((Suc n) * length (([(3::int) * x + (f t)*y - 9 + (- z)] @ []) @ xs) = length xs) \ m < 5*n - length (xs @ [2,3,4,x*z + 8 - y]) \ (\p. \q. p \ q \ r)" apply (reify Irifm.simps Irnat_simps Irlist.simps Irint_simps) @@ -385,28 +391,28 @@ (* An example for equations containing type variables *) datatype prod = Zero | One | Var nat | Mul prod prod | Pw prod nat | PNM nat nat prod -consts Iprod :: " prod \ ('a::{linordered_idom}) list \'a" -primrec +primrec Iprod :: " prod \ ('a::{linordered_idom}) list \'a" +where "Iprod Zero vs = 0" - "Iprod One vs = 1" - "Iprod (Var n) vs = vs!n" - "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)" - "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)" - "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs" +| "Iprod One vs = 1" +| "Iprod (Var n) vs = vs!n" +| "Iprod (Mul a b) vs = (Iprod a vs * Iprod b vs)" +| "Iprod (Pw a n) vs = ((Iprod a vs) ^ n)" +| "Iprod (PNM n k t) vs = (vs ! n)^k * Iprod t vs" consts prodmul:: "prod \ prod \ prod" datatype sgn = Pos prod | Neg prod | ZeroEq prod | NZeroEq prod | Tr | F | Or sgn sgn | And sgn sgn -consts Isgn :: " sgn \ ('a::{linordered_idom}) list \bool" -primrec +primrec Isgn :: " sgn \ ('a::{linordered_idom}) list \bool" +where "Isgn Tr vs = True" - "Isgn F vs = False" - "Isgn (ZeroEq t) vs = (Iprod t vs = 0)" - "Isgn (NZeroEq t) vs = (Iprod t vs \ 0)" - "Isgn (Pos t) vs = (Iprod t vs > 0)" - "Isgn (Neg t) vs = (Iprod t vs < 0)" - "Isgn (And p q) vs = (Isgn p vs \ Isgn q vs)" - "Isgn (Or p q) vs = (Isgn p vs \ Isgn q vs)" +| "Isgn F vs = False" +| "Isgn (ZeroEq t) vs = (Iprod t vs = 0)" +| "Isgn (NZeroEq t) vs = (Iprod t vs \ 0)" +| "Isgn (Pos t) vs = (Iprod t vs > 0)" +| "Isgn (Neg t) vs = (Iprod t vs < 0)" +| "Isgn (And p q) vs = (Isgn p vs \ Isgn q vs)" +| "Isgn (Or p q) vs = (Isgn p vs \ Isgn q vs)" lemmas eqs = Isgn.simps Iprod.simps diff -r 83b0f75810f0 -r d78659d1723e src/HOL/ex/ThreeDivides.thy --- a/src/HOL/ex/ThreeDivides.thy Mon Mar 01 16:42:45 2010 +0100 +++ b/src/HOL/ex/ThreeDivides.thy Mon Mar 01 17:05:57 2010 +0100 @@ -149,10 +149,10 @@ The function @{text "nlen"} returns the number of digits in a natural number n. *} -consts nlen :: "nat \ nat" -recdef nlen "measure id" +fun nlen :: "nat \ nat" +where "nlen 0 = 0" - "nlen x = 1 + nlen (x div 10)" +| "nlen x = 1 + nlen (x div 10)" text {* The function @{text "sumdig"} returns the sum of all digits in some number n. *}