# HG changeset patch # User paulson # Date 1080824704 -7200 # Node ID e2373489d3739c3a08898c55ca11f1908e980c4d # Parent 7a3d80e276d412c0ff49993661e37f3c427647b7 removal of Binary Trees examples prepratory to its going into AFP diff -r 7a3d80e276d4 -r e2373489d373 src/HOL/Induct/BinaryTree.thy --- a/src/HOL/Induct/BinaryTree.thy Thu Apr 01 10:54:32 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,795 +0,0 @@ -header {* Isar-style Reasoning for Binary Tree Operations *} -theory BinaryTree = Main: - -text {* We prove correctness of operations on - binary search tree implementing a set. - - This document is GPL. - - Author: Viktor Kuncak, MIT CSAIL, November 2003 *} - -(*============================================================*) -section {* Tree Definition *} -(*============================================================*) - -datatype 'a Tree = Tip | T "'a Tree" 'a "'a Tree" - -consts - setOf :: "'a Tree => 'a set" - -- {* set abstraction of a tree *} -primrec -"setOf Tip = {}" -"setOf (T t1 x t2) = (setOf t1) Un (setOf t2) Un {x}" - -types - -- {* we require index to have an irreflexive total order < *} - -- {* apart from that, we do not rely on index being int *} - index = int - -types -- {* hash function type *} - 'a hash = "'a => index" - -constdefs - eqs :: "'a hash => 'a => 'a set" - -- {* equivalence class of elements with the same hash code *} - "eqs h x == {y. h y = h x}" - -consts - sortedTree :: "'a hash => 'a Tree => bool" - -- {* check if a tree is sorted *} -primrec -"sortedTree h Tip = True" -"sortedTree h (T t1 x t2) = - (sortedTree h t1 & - (ALL l: setOf t1. h l < h x) & - (ALL r: setOf t2. h x < h r) & - sortedTree h t2)" - -lemma sortLemmaL: - "sortedTree h (T t1 x t2) ==> sortedTree h t1" by simp -lemma sortLemmaR: - "sortedTree h (T t1 x t2) ==> sortedTree h t2" by simp - -(*============================================================*) -section {* Tree Lookup *} -(*============================================================*) - -consts - tlookup :: "'a hash => index => 'a Tree => 'a option" -primrec -"tlookup h k Tip = None" -"tlookup h k (T t1 x t2) = - (if k < h x then tlookup h k t1 - else if h x < k then tlookup h k t2 - else Some x)" - -lemma tlookup_none: -"sortedTree h t & (tlookup h k t = None) --> - (ALL x:setOf t. h x ~= k)" -apply (induct t) -apply auto (* takes some time *) -done - -lemma tlookup_some: -"sortedTree h t & (tlookup h k t = Some x) --> - x:setOf t & h x = k" -apply (induct t) -apply auto (* takes some time *) -done - -constdefs - sorted_distinct_pred :: "'a hash => 'a => 'a => 'a Tree => bool" - -- {* No two elements have the same hash code *} - "sorted_distinct_pred h a b t == sortedTree h t & - a:setOf t & b:setOf t & h a = h b --> - a = b" - -declare sorted_distinct_pred_def [simp] - --- {* for case analysis on three cases *} -lemma cases3: "[| C1 ==> G; C2 ==> G; C3 ==> G; - C1 | C2 | C3 |] ==> G" -by auto - -text {* @{term sorted_distinct_pred} holds for out trees: *} - -lemma sorted_distinct: "sorted_distinct_pred h a b t" (is "?P t") -proof (induct t) - show "?P Tip" by simp - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof (unfold sorted_distinct_pred_def, safe) - assume s: "sortedTree h (T t1 x t2)" - assume adef: "a : setOf (T t1 x t2)" - assume bdef: "b : setOf (T t1 x t2)" - assume hahb: "h a = h b" - from s have s1: "sortedTree h t1" by auto - from s have s2: "sortedTree h t2" by auto - show "a = b" - -- {* We consider 9 cases for the position of a and b are in the tree *} - proof - - -- {* three cases for a *} - from adef have "a : setOf t1 | a = x | a : setOf t2" by auto - moreover { assume adef1: "a : setOf t1" - have ?thesis - proof - - -- {* three cases for b *} - from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto - moreover { assume bdef1: "b : setOf t1" - from s1 adef1 bdef1 hahb h1 have ?thesis by simp } - moreover { assume bdef1: "b = x" - from adef1 bdef1 s have "h a < h b" by auto - from this hahb have ?thesis by simp } - moreover { assume bdef1: "b : setOf t2" - from adef1 s have o1: "h a < h x" by auto - from bdef1 s have o2: "h x < h b" by auto - from o1 o2 have "h a < h b" by simp - from this hahb have ?thesis by simp } -- {* case impossible *} - ultimately show ?thesis by blast - qed - } - moreover { assume adef1: "a = x" - have ?thesis - proof - - -- {* three cases for b *} - from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto - moreover { assume bdef1: "b : setOf t1" - from this s have "h b < h x" by auto - from this adef1 have "h b < h a" by auto - from hahb this have ?thesis by simp } -- {* case impossible *} - moreover { assume bdef1: "b = x" - from adef1 bdef1 have ?thesis by simp } - moreover { assume bdef1: "b : setOf t2" - from this s have "h x < h b" by auto - from this adef1 have "h a < h b" by simp - from hahb this have ?thesis by simp } -- {* case impossible *} - ultimately show ?thesis by blast - qed - } - moreover { assume adef1: "a : setOf t2" - have ?thesis - proof - - -- {* three cases for b *} - from bdef have "b : setOf t1 | b = x | b : setOf t2" by auto - moreover { assume bdef1: "b : setOf t1" - from bdef1 s have o1: "h b < h x" by auto - from adef1 s have o2: "h x < h a" by auto - from o1 o2 have "h b < h a" by simp - from this hahb have ?thesis by simp } -- {* case impossible *} - moreover { assume bdef1: "b = x" - from adef1 bdef1 s have "h b < h a" by auto - from this hahb have ?thesis by simp } -- {* case impossible *} - moreover { assume bdef1: "b : setOf t2" - from s2 adef1 bdef1 hahb h2 have ?thesis by simp } - ultimately show ?thesis by blast - qed - } - ultimately show ?thesis by blast - qed - qed -qed - -lemma tlookup_finds: -- {* if a node is in the tree, lookup finds it *} -"sortedTree h t & y:setOf t --> - tlookup h (h y) t = Some y" -proof safe - assume s: "sortedTree h t" - assume yint: "y : setOf t" - show "tlookup h (h y) t = Some y" - proof (cases "tlookup h (h y) t") - case None note res = this - from s res have "sortedTree h t & (tlookup h (h y) t = None)" by simp - from this have o1: "ALL x:setOf t. h x ~= h y" by (simp add: tlookup_none) - from o1 yint have "h y ~= h y" by fastsimp (* auto does not work *) - from this show ?thesis by simp - next case (Some z) note res = this - have ls: "sortedTree h t & (tlookup h (h y) t = Some z) --> - z:setOf t & h z = h y" by (simp add: tlookup_some) - have sd: "sorted_distinct_pred h y z t" - by (insert sorted_distinct [of h y z t], simp) - (* for some reason simplifier would never guess this substitution *) - from s res ls have o1: "z:setOf t & h z = h y" by simp - from s yint o1 sd have "y = z" by auto - from this res show "tlookup h (h y) t = Some y" by simp - qed -qed - -subsection {* Tree membership as a special case of lookup *} - -constdefs - memb :: "'a hash => 'a => 'a Tree => bool" - "memb h x t == - (case (tlookup h (h x) t) of - None => False - | Some z => (x=z))" - -lemma assumes s: "sortedTree h t" - shows memb_spec: "memb h x t = (x : setOf t)" -proof (cases "tlookup h (h x) t") -case None note tNone = this - from tNone have res: "memb h x t = False" by (simp add: memb_def) - from s tNone tlookup_none have o1: "ALL y:setOf t. h y ~= h x" by fastsimp - have notIn: "x ~: setOf t" - proof - assume h: "x : setOf t" - from h o1 have "h x ~= h x" by fastsimp - from this show False by simp - qed - from res notIn show ?thesis by simp -next case (Some z) note tSome = this - from s tSome tlookup_some have zin: "z : setOf t" by fastsimp - show ?thesis - proof (cases "x=z") - case True note xez = this - from tSome xez have res: "memb h x t" by (simp add: memb_def) - from res zin xez show ?thesis by simp - next case False note xnez = this - from tSome xnez have res: "~ memb h x t" by (simp add: memb_def) - have "x ~: setOf t" - proof - assume xin: "x : setOf t" - from s tSome tlookup_some have hzhx: "h x = h z" by fastsimp - have o1: "sorted_distinct_pred h x z t" - by (insert sorted_distinct [of h x z t], simp) - from s xin zin hzhx o1 have "x = z" by fastsimp - from this xnez show False by simp - qed - from this res show ?thesis by simp - qed -qed - -declare sorted_distinct_pred_def [simp del] - -(*============================================================*) -section {* Insertion into a Tree *} -(*============================================================*) - -consts - binsert :: "'a hash => 'a => 'a Tree => 'a Tree" - -primrec -"binsert h e Tip = (T Tip e Tip)" -"binsert h e (T t1 x t2) = (if h e < h x then - (T (binsert h e t1) x t2) - else - (if h x < h e then - (T t1 x (binsert h e t2)) - else (T t1 e t2)))" - -text {* A technique for proving disjointness of sets. *} -lemma disjCond: "[| !! x. [| x:A; x:B |] ==> False |] ==> A Int B = {}" -by fastsimp - -text {* The following is a proof that insertion correctly implements - the set interface. - Compared to @{text BinaryTree_TacticStyle}, the claim is more - difficult, and this time we need to assume as a hypothesis - that the tree is sorted. *} - -lemma binsert_set: "sortedTree h t --> - setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}" - (is "?P t") -proof (induct t) - -- {* base case *} - show "?P Tip" by (simp add: eqs_def) - -- {* inductition step *} - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof - assume s: "sortedTree h (T t1 x t2)" - from s have s1: "sortedTree h t1" by (rule sortLemmaL) - from s1 and h1 have c1: "setOf (binsert h e t1) = setOf t1 - eqs h e Un {e}" by simp - from s have s2: "sortedTree h t2" by (rule sortLemmaR) - from s2 and h2 have c2: "setOf (binsert h e t2) = setOf t2 - eqs h e Un {e}" by simp - show "setOf (binsert h e (T t1 x t2)) = - setOf (T t1 x t2) - eqs h e Un {e}" - proof (cases "h e < h x") - case True note eLess = this - from eLess have res: "binsert h e (T t1 x t2) = (T (binsert h e t1) x t2)" by simp - show "setOf (binsert h e (T t1 x t2)) = - setOf (T t1 x t2) - eqs h e Un {e}" - proof (simp add: res eLess c1) - show "insert x (insert e (setOf t1 - eqs h e Un setOf t2)) = - insert e (insert x (setOf t1 Un setOf t2) - eqs h e)" - proof - - have eqsLessX: "ALL el: eqs h e. h el < h x" by (simp add: eqs_def eLess) - from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by fastsimp - from s have xLessT2: "ALL r: setOf t2. h x < h r" by auto - have eqsLessT2: "ALL el: eqs h e. ALL r: setOf t2. h el < h r" - proof safe - fix el assume hel: "el : eqs h e" - from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *) - fix r assume hr: "r : setOf t2" - from xLessT2 hr o1 eLess show "h el < h r" by auto - qed - from eqsLessT2 have eqsDisjT2: "ALL el: eqs h e. ALL r: setOf t2. h el ~= h r" - by fastsimp (* auto fails here *) - from eqsDisjX eqsDisjT2 show ?thesis by fastsimp - qed - qed - next case False note eNotLess = this - show "setOf (binsert h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e Un {e}" - proof (cases "h x < h e") - case True note xLess = this - from xLess have res: "binsert h e (T t1 x t2) = (T t1 x (binsert h e t2))" by simp - show "setOf (binsert h e (T t1 x t2)) = - setOf (T t1 x t2) - eqs h e Un {e}" - proof (simp add: res xLess eNotLess c2) - show "insert x (insert e (setOf t1 Un (setOf t2 - eqs h e))) = - insert e (insert x (setOf t1 Un setOf t2) - eqs h e)" - proof - - have XLessEqs: "ALL el: eqs h e. h x < h el" by (simp add: eqs_def xLess) - from this have eqsDisjX: "ALL el: eqs h e. h el ~= h x" by auto - from s have t1LessX: "ALL l: setOf t1. h l < h x" by auto - have T1lessEqs: "ALL el: eqs h e. ALL l: setOf t1. h l < h el" - proof safe - fix el assume hel: "el : eqs h e" - fix l assume hl: "l : setOf t1" - from hel eqs_def have o1: "h el = h e" by fastsimp (* auto fails here! *) - from t1LessX hl o1 xLess show "h l < h el" by auto - qed - from T1lessEqs have T1disjEqs: "ALL el: eqs h e. ALL l: setOf t1. h el ~= h l" - by fastsimp - from eqsDisjX T1lessEqs show ?thesis by auto - qed - qed - next case False note xNotLess = this - from xNotLess eNotLess have xeqe: "h x = h e" by simp - from xeqe have res: "binsert h e (T t1 x t2) = (T t1 e t2)" by simp - show "setOf (binsert h e (T t1 x t2)) = - setOf (T t1 x t2) - eqs h e Un {e}" - proof (simp add: res eNotLess xeqe) - show "insert e (setOf t1 Un setOf t2) = - insert e (insert x (setOf t1 Un setOf t2) - eqs h e)" - proof - - have "insert x (setOf t1 Un setOf t2) - eqs h e = - setOf t1 Un setOf t2" - proof - - have (* o1: *) "x : eqs h e" by (simp add: eqs_def xeqe) - moreover have (* o2: *) "(setOf t1) Int (eqs h e) = {}" - proof (rule disjCond) - fix w - assume whSet: "w : setOf t1" - assume whEq: "w : eqs h e" - from whSet s have o1: "h w < h x" by simp - from whEq eqs_def have o2: "h w = h e" by fastsimp - from o2 xeqe have o3: "~ h w < h x" by simp - from o1 o3 show False by contradiction - qed - moreover have (* o3: *) "(setOf t2) Int (eqs h e) = {}" - proof (rule disjCond) - fix w - assume whSet: "w : setOf t2" - assume whEq: "w : eqs h e" - from whSet s have o1: "h x < h w" by simp - from whEq eqs_def have o2: "h w = h e" by fastsimp - from o2 xeqe have o3: "~ h x < h w" by simp - from o1 o3 show False by contradiction - qed - ultimately show ?thesis by auto - qed - from this show ?thesis by simp - qed - qed - qed - qed - qed -qed - -text {* Using the correctness of set implementation, - preserving sortedness is still simple. *} -lemma binsert_sorted: "sortedTree h t --> sortedTree h (binsert h x t)" -by (induct t) (auto simp add: binsert_set) - -text {* We summarize the specification of binsert as follows. *} -corollary binsert_spec: "sortedTree h t --> - sortedTree h (binsert h x t) & - setOf (binsert h e t) = (setOf t) - (eqs h e) Un {e}" -by (simp add: binsert_set binsert_sorted) - -(*============================================================*) -section {* Removing an element from a tree *} -(*============================================================*) - -text {* These proofs are influenced by those in @{text BinaryTree_Tactic} *} - -consts - rm :: "'a hash => 'a Tree => 'a" - -- {* rightmost element of a tree *} -primrec -"rm h (T t1 x t2) = - (if t2=Tip then x else rm h t2)" - -consts - wrm :: "'a hash => 'a Tree => 'a Tree" - -- {* tree without the rightmost element *} -primrec -"wrm h (T t1 x t2) = - (if t2=Tip then t1 else (T t1 x (wrm h t2)))" - -consts - wrmrm :: "'a hash => 'a Tree => 'a Tree * 'a" - -- {* computing rightmost and removal in one pass *} -primrec -"wrmrm h (T t1 x t2) = - (if t2=Tip then (t1,x) - else (T t1 x (fst (wrmrm h t2)), - snd (wrmrm h t2)))" - -consts - remove :: "'a hash => 'a => 'a Tree => 'a Tree" - -- {* removal of an element from the tree *} -primrec -"remove h e Tip = Tip" -"remove h e (T t1 x t2) = - (if h e < h x then (T (remove h e t1) x t2) - else if h x < h e then (T t1 x (remove h e t2)) - else (if t1=Tip then t2 - else let (t1p,r) = wrmrm h t1 - in (T t1p r t2)))" - -theorem wrmrm_decomp: "t ~= Tip --> wrmrm h t = (wrm h t, rm h t)" -apply (induct_tac t) -apply simp_all -done - -lemma rm_set: "t ~= Tip & sortedTree h t --> rm h t : setOf t" -apply (induct_tac t) -apply simp_all -done - -lemma wrm_set: "t ~= Tip & sortedTree h t --> - setOf (wrm h t) = setOf t - {rm h t}" (is "?P t") -proof (induct t) - show "?P Tip" by simp - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof (rule impI, erule conjE) - assume s: "sortedTree h (T t1 x t2)" - show "setOf (wrm h (T t1 x t2)) = - setOf (T t1 x t2) - {rm h (T t1 x t2)}" - proof (cases "t2 = Tip") - case True note t2tip = this - from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp - from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp - from s have "x ~: setOf t1" by auto - from this rm_res wrm_res t2tip show ?thesis by simp - next case False note t2nTip = this - from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp - from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp - from s have s2: "sortedTree h t2" by simp - from h2 t2nTip s2 - have o1: "setOf (wrm h t2) = setOf t2 - {rm h t2}" by simp - show ?thesis - proof (simp add: rm_res wrm_res t2nTip h2 o1) - show "insert x (setOf t1 Un (setOf t2 - {rm h t2})) = - insert x (setOf t1 Un setOf t2) - {rm h t2}" - proof - - from s rm_set t2nTip have xOk: "h x < h (rm h t2)" by auto - have t1Ok: "ALL l:setOf t1. h l < h (rm h t2)" - proof safe - fix l :: 'a assume ldef: "l : setOf t1" - from ldef s have lx: "h l < h x" by auto - from lx xOk show "h l < h (rm h t2)" by auto - qed - from xOk t1Ok show ?thesis by auto - qed - qed - qed - qed -qed - -lemma wrm_set1: "t ~= Tip & sortedTree h t --> setOf (wrm h t) <= setOf t" -by (auto simp add: wrm_set) - -lemma wrm_sort: "t ~= Tip & sortedTree h t --> sortedTree h (wrm h t)" (is "?P t") -proof (induct t) - show "?P Tip" by simp - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof safe - assume s: "sortedTree h (T t1 x t2)" - show "sortedTree h (wrm h (T t1 x t2))" - proof (cases "t2 = Tip") - case True note t2tip = this - from t2tip have res: "wrm h (T t1 x t2) = t1" by simp - from res s show ?thesis by simp - next case False note t2nTip = this - from t2nTip have res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp - from s have s1: "sortedTree h t1" by simp - from s have s2: "sortedTree h t2" by simp - from s2 h2 t2nTip have o1: "sortedTree h (wrm h t2)" by simp - from s2 t2nTip wrm_set1 have o2: "setOf (wrm h t2) <= setOf t2" by auto - from s o2 have o3: "ALL r: setOf (wrm h t2). h x < h r" by auto - from s1 o1 o3 res s show "sortedTree h (wrm h (T t1 x t2))" by simp - qed - qed -qed - -lemma wrm_less_rm: - "t ~= Tip & sortedTree h t --> - (ALL l:setOf (wrm h t). h l < h (rm h t))" (is "?P t") -proof (induct t) - show "?P Tip" by simp - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof safe - fix l :: "'a" assume ldef: "l : setOf (wrm h (T t1 x t2))" - assume s: "sortedTree h (T t1 x t2)" - from s have s1: "sortedTree h t1" by simp - from s have s2: "sortedTree h t2" by simp - show "h l < h (rm h (T t1 x t2))" - proof (cases "t2 = Tip") - case True note t2tip = this - from t2tip have rm_res: "rm h (T t1 x t2) = x" by simp - from t2tip have wrm_res: "wrm h (T t1 x t2) = t1" by simp - from ldef wrm_res have o1: "l : setOf t1" by simp - from rm_res o1 s show ?thesis by simp - next case False note t2nTip = this - from t2nTip have rm_res: "rm h (T t1 x t2) = rm h t2" by simp - from t2nTip have wrm_res: "wrm h (T t1 x t2) = T t1 x (wrm h t2)" by simp - from ldef wrm_res - have l_scope: "l : {x} Un setOf t1 Un setOf (wrm h t2)" by simp - have hLess: "h l < h (rm h t2)" - proof (cases "l = x") - case True note lx = this - from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto - from lx o1 show ?thesis by simp - next case False note lnx = this - show ?thesis - proof (cases "l : setOf t1") - case True note l_in_t1 = this - from s t2nTip rm_set s2 have o1: "h x < h (rm h t2)" by auto - from l_in_t1 s have o2: "h l < h x" by auto - from o1 o2 show ?thesis by simp - next case False note l_notin_t1 = this - from l_scope lnx l_notin_t1 - have l_in_res: "l : setOf (wrm h t2)" by auto - from l_in_res h2 t2nTip s2 show ?thesis by auto - qed - qed - from rm_res hLess show ?thesis by simp - qed - qed -qed - -lemma remove_set: "sortedTree h t --> - setOf (remove h e t) = setOf t - eqs h e" (is "?P t") -proof (induct t) - show "?P Tip" by auto - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof - assume s: "sortedTree h (T t1 x t2)" - show "setOf (remove h e (T t1 x t2)) = setOf (T t1 x t2) - eqs h e" - proof (cases "h e < h x") - case True note elx = this - from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2" - by simp - from s have s1: "sortedTree h t1" by simp - from s1 h1 have o1: "setOf (remove h e t1) = setOf t1 - eqs h e" by simp - show ?thesis - proof (simp add: o1 elx) - show "insert x (setOf t1 - eqs h e Un setOf t2) = - insert x (setOf t1 Un setOf t2) - eqs h e" - proof - - have xOk: "x ~: eqs h e" - proof - assume h: "x : eqs h e" - from h have o1: "~ (h e < h x)" by (simp add: eqs_def) - from elx o1 show "False" by contradiction - qed - have t2Ok: "(setOf t2) Int (eqs h e) = {}" - proof (rule disjCond) - fix y :: 'a - assume y_in_t2: "y : setOf t2" - assume y_in_eq: "y : eqs h e" - from y_in_t2 s have xly: "h x < h y" by auto - from y_in_eq have eey: "h y = h e" by (simp add: eqs_def) (* must "add:" not "from" *) - from xly eey have nelx: "~ (h e < h x)" by simp - from nelx elx show False by contradiction - qed - from xOk t2Ok show ?thesis by auto - qed - qed - next case False note nelx = this - show ?thesis - proof (cases "h x < h e") - case True note xle = this - from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp - from s have s2: "sortedTree h t2" by simp - from s2 h2 have o1: "setOf (remove h e t2) = setOf t2 - eqs h e" by simp - show ?thesis - proof (simp add: o1 xle nelx) - show "insert x (setOf t1 Un (setOf t2 - eqs h e)) = - insert x (setOf t1 Un setOf t2) - eqs h e" - proof - - have xOk: "x ~: eqs h e" - proof - assume h: "x : eqs h e" - from h have o1: "~ (h x < h e)" by (simp add: eqs_def) - from xle o1 show "False" by contradiction - qed - have t1Ok: "(setOf t1) Int (eqs h e) = {}" - proof (rule disjCond) - fix y :: 'a - assume y_in_t1: "y : setOf t1" - assume y_in_eq: "y : eqs h e" - from y_in_t1 s have ylx: "h y < h x" by auto - from y_in_eq have eey: "h y = h e" by (simp add: eqs_def) - from ylx eey have nxle: "~ (h x < h e)" by simp - from nxle xle show False by contradiction - qed - from xOk t1Ok show ?thesis by auto - qed - qed - next case False note nxle = this - from nelx nxle have ex: "h e = h x" by simp - have t2Ok: "(setOf t2) Int (eqs h e) = {}" - proof (rule disjCond) - fix y :: 'a - assume y_in_t2: "y : setOf t2" - assume y_in_eq: "y : eqs h e" - from y_in_t2 s have xly: "h x < h y" by auto - from y_in_eq have eey: "h y = h e" by (simp add: eqs_def) - from y_in_eq ex eey have nxly: "~ (h x < h y)" by simp - from nxly xly show False by contradiction - qed - show ?thesis - proof (cases "t1 = Tip") - case True note t1tip = this - from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp - show ?thesis - proof (simp add: res t1tip ex) - show "setOf t2 = insert x (setOf t2) - eqs h e" - proof - - from ex have x_in_eqs: "x : eqs h e" by (simp add: eqs_def) - from x_in_eqs t2Ok show ?thesis by auto - qed - qed - next case False note t1nTip = this - from nelx nxle ex t1nTip - have res: "remove h e (T t1 x t2) = - T (wrm h t1) (rm h t1) t2" - by (simp add: Let_def wrmrm_decomp) - from res show ?thesis - proof simp - from s have s1: "sortedTree h t1" by simp - show "insert (rm h t1) (setOf (wrm h t1) Un setOf t2) = - insert x (setOf t1 Un setOf t2) - eqs h e" - proof (simp add: t1nTip s1 rm_set wrm_set) - show "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) = - insert x (setOf t1 Un setOf t2) - eqs h e" - proof - - from t1nTip s1 rm_set - have o1: "insert (rm h t1) (setOf t1 - {rm h t1} Un setOf t2) = - setOf t1 Un setOf t2" by auto - have o2: "insert x (setOf t1 Un setOf t2) - eqs h e = - setOf t1 Un setOf t2" - proof - - from ex have xOk: "x : eqs h e" by (simp add: eqs_def) - have t1Ok: "(setOf t1) Int (eqs h e) = {}" - proof (rule disjCond) - fix y :: 'a - assume y_in_t1: "y : setOf t1" - assume y_in_eq: "y : eqs h e" - from y_in_t1 s ex have o1: "h y < h e" by auto - from y_in_eq have o2: "~ (h y < h e)" by (simp add: eqs_def) - from o1 o2 show False by contradiction - qed - from xOk t1Ok t2Ok show ?thesis by auto - qed - from o1 o2 show ?thesis by simp - qed - qed - qed - qed - qed - qed - qed -qed - -lemma remove_sort: "sortedTree h t --> - sortedTree h (remove h e t)" (is "?P t") -proof (induct t) - show "?P Tip" by auto - fix t1 :: "'a Tree" assume h1: "?P t1" - fix t2 :: "'a Tree" assume h2: "?P t2" - fix x :: 'a - show "?P (T t1 x t2)" - proof - assume s: "sortedTree h (T t1 x t2)" - from s have s1: "sortedTree h t1" by simp - from s have s2: "sortedTree h t2" by simp - from h1 s1 have sr1: "sortedTree h (remove h e t1)" by simp - from h2 s2 have sr2: "sortedTree h (remove h e t2)" by simp - show "sortedTree h (remove h e (T t1 x t2))" - proof (cases "h e < h x") - case True note elx = this - from elx have res: "remove h e (T t1 x t2) = T (remove h e t1) x t2" - by simp - show ?thesis - proof (simp add: s sr1 s2 elx res) - let ?C1 = "ALL l:setOf (remove h e t1). h l < h x" - let ?C2 = "ALL r:setOf t2. h x < h r" - have o1: "?C1" - proof - - from s1 have "setOf (remove h e t1) = setOf t1 - eqs h e" by (simp add: remove_set) - from s this show ?thesis by auto - qed - from o1 s show "?C1 & ?C2" by auto - qed - next case False note nelx = this - show ?thesis - proof (cases "h x < h e") - case True note xle = this - from xle have res: "remove h e (T t1 x t2) = T t1 x (remove h e t2)" by simp - show ?thesis - proof (simp add: s s1 sr2 xle nelx res) - let ?C1 = "ALL l:setOf t1. h l < h x" - let ?C2 = "ALL r:setOf (remove h e t2). h x < h r" - have o2: "?C2" - proof - - from s2 have "setOf (remove h e t2) = setOf t2 - eqs h e" by (simp add: remove_set) - from s this show ?thesis by auto - qed - from o2 s show "?C1 & ?C2" by auto - qed - next case False note nxle = this - from nelx nxle have ex: "h e = h x" by simp - show ?thesis - proof (cases "t1 = Tip") - case True note t1tip = this - from ex t1tip have res: "remove h e (T t1 x t2) = t2" by simp - show ?thesis by (simp add: res t1tip ex s2) - next case False note t1nTip = this - from nelx nxle ex t1nTip - have res: "remove h e (T t1 x t2) = - T (wrm h t1) (rm h t1) t2" - by (simp add: Let_def wrmrm_decomp) - from res show ?thesis - proof simp - let ?C1 = "sortedTree h (wrm h t1)" - let ?C2 = "ALL l:setOf (wrm h t1). h l < h (rm h t1)" - let ?C3 = "ALL r:setOf t2. h (rm h t1) < h r" - let ?C4 = "sortedTree h t2" - from s1 t1nTip have o1: ?C1 by (simp add: wrm_sort) - from s1 t1nTip have o2: ?C2 by (simp add: wrm_less_rm) - have o3: ?C3 - proof - fix r :: 'a - assume rt2: "r : setOf t2" - from s rm_set s1 t1nTip have o1: "h (rm h t1) < h x" by auto - from rt2 s have o2: "h x < h r" by auto - from o1 o2 show "h (rm h t1) < h r" by simp - qed - from o1 o2 o3 s2 show "?C1 & ?C2 & ?C3 & ?C4" by simp - qed - qed - qed - qed - qed -qed - -text {* We summarize the specification of remove as follows. *} -corollary remove_spec: "sortedTree h t --> - sortedTree h (remove h e t) & - setOf (remove h e t) = setOf t - eqs h e" -by (simp add: remove_sort remove_set) - -generate_code ("BinaryTree_Code.ML") - test = "tlookup id 4 (remove id 3 (binsert id 4 (binsert id 3 Tip)))" - -end diff -r 7a3d80e276d4 -r e2373489d373 src/HOL/Induct/BinaryTree_Map.thy --- a/src/HOL/Induct/BinaryTree_Map.thy Thu Apr 01 10:54:32 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,257 +0,0 @@ -header {* Mostly Isar-style Reasoning for Binary Tree Operations *} -theory BinaryTree_Map = BinaryTree: - -text {* We prove correctness of map operations - implemented using binary search trees from BinaryTree. - - This document is GPL. - - Author: Viktor Kuncak, MIT CSAIL, November 2003 *} - - -(*============================================================*) -section {* Map implementation and an abstraction function *} -(*============================================================*) - -types - 'a tarray = "(index * 'a) Tree" - -constdefs - valid_tmap :: "'a tarray => bool" - "valid_tmap t == sortedTree fst t" - -declare valid_tmap_def [simp] - -constdefs - mapOf :: "'a tarray => index => 'a option" - -- {* the abstraction function from trees to maps *} - "mapOf t i == - (case (tlookup fst i t) of - None => None - | Some ia => Some (snd ia))" - -(*============================================================*) -section {* Auxiliary Properties of our Implementation *} -(*============================================================*) - -lemma mapOf_lookup1: "tlookup fst i t = None ==> mapOf t i = None" -by (simp add: mapOf_def) - -lemma mapOf_lookup2: "tlookup fst i t = Some (j,a) ==> mapOf t i = Some a" -by (simp add: mapOf_def) - -lemma assumes h: "mapOf t i = None" - shows mapOf_lookup3: "tlookup fst i t = None" -proof (cases "tlookup fst i t") -case None from this show ?thesis by assumption -next case (Some ia) note tsome = this - from this have o1: "tlookup fst i t = Some (fst ia, snd ia)" by simp - have "mapOf t i = Some (snd ia)" - by (insert mapOf_lookup2 [of i t "fst ia" "snd ia"], simp add: o1) - from this have "mapOf t i ~= None" by simp - from this h show ?thesis by simp -- {* contradiction *} -qed - -lemma assumes v: "valid_tmap t" - assumes h: "mapOf t i = Some a" - shows mapOf_lookup4: "tlookup fst i t = Some (i,a)" -proof (cases "tlookup fst i t") -case None - from this mapOf_lookup1 have "mapOf t i = None" by auto - from this h show ?thesis by simp -- {* contradiction *} -next case (Some ia) note tsome = this - have tlookup_some_inst: "sortedTree fst t & (tlookup fst i t = Some ia) --> - ia : setOf t & fst ia = i" by (simp add: tlookup_some) - from tlookup_some_inst tsome v have "ia : setOf t" by simp - from tsome have "mapOf t i = Some (snd ia)" by (simp add: mapOf_def) - from this h have o1: "snd ia = a" by simp - from tlookup_some_inst tsome v have o2: "fst ia = i" by simp - from o1 o2 have "ia = (i,a)" by auto - from this tsome show "tlookup fst i t = Some (i, a)" by simp -qed - -subsection {* Lemmas @{text mapset_none} and @{text mapset_some} establish - a relation between the set and map abstraction of the tree *} - -lemma assumes v: "valid_tmap t" - shows mapset_none: "(mapOf t i = None) = (ALL a. (i,a) ~: setOf t)" -proof - -- {* ==> *} - assume mapNone: "mapOf t i = None" - from v mapNone mapOf_lookup3 have lnone: "tlookup fst i t = None" by auto - show "ALL a. (i,a) ~: setOf t" - proof - fix a - show "(i,a) ~: setOf t" - proof - assume iain: "(i,a) : setOf t" - have tlookup_none_inst: - "sortedTree fst t & (tlookup fst i t = None) --> (ALL x:setOf t. fst x ~= i)" - by (insert tlookup_none [of "fst" "t" "i"], assumption) - from v lnone tlookup_none_inst have "ALL x : setOf t. fst x ~= i" by simp - from this iain have "fst (i,a) ~= i" by fastsimp - from this show False by simp - qed - qed - -- {* <== *} - next assume h: "ALL a. (i,a) ~: setOf t" - show "mapOf t i = None" - proof (cases "mapOf t i") - case None show ?thesis by assumption - next case (Some a) note mapsome = this - from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4) - (* moving mapOf_lookup4 to assumption does not work, although it uses - no == !! *) - from tlookup_some have tlookup_some_inst: - "sortedTree fst t & tlookup fst i t = Some (i,a) --> - (i,a) : setOf t & fst (i,a) = i" - by (insert tlookup_some [of fst t i "(i,a)"], assumption) - from v o1 this have "(i,a) : setOf t" by simp - from this h show ?thesis by auto -- {* contradiction *} - qed -qed - -lemma assumes v: "valid_tmap t" - shows mapset_some: "(mapOf t i = Some a) = ((i,a) : setOf t)" -proof - -- {* ==> *} - assume mapsome: "mapOf t i = Some a" - from v mapsome have o1: "tlookup fst i t = Some (i,a)" by (simp add: mapOf_lookup4) - from tlookup_some have tlookup_some_inst: - "sortedTree fst t & tlookup fst i t = Some (i,a) --> - (i,a) : setOf t & fst (i,a) = i" - by (insert tlookup_some [of fst t i "(i,a)"], assumption) - from v o1 this show "(i,a) : setOf t" by simp - -- {* <== *} - next assume iain: "(i,a) : setOf t" - from v iain tlookup_finds have "tlookup fst (fst (i,a)) t = Some (i,a)" by fastsimp - from this have "tlookup fst i t = Some (i,a)" by simp - from this show "mapOf t i = Some a" by (simp add: mapOf_def) -qed - -(*============================================================*) -section {* Empty Map *} -(*============================================================*) - -lemma mnew_spec_valid: "valid_tmap Tip" -by (simp add: mapOf_def) - -lemma mtip_spec_empty: "mapOf Tip k = None" -by (simp add: mapOf_def) - - -(*============================================================*) -section {* Map Update Operation *} -(*============================================================*) - -constdefs - mupdate :: "index => 'a => 'a tarray => 'a tarray" - "mupdate i a t == binsert fst (i,a) t" - -lemma assumes v: "valid_tmap t" - shows mupdate_map: "mapOf (mupdate i a t) = (mapOf t)(i |-> a)" -proof - fix i2 - let ?tr = "binsert fst (i,a) t" - have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def) - from v binsert_set - have setSpec: "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}" by fastsimp - from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp - show "mapOf (mupdate i a t) i2 = ((mapOf t)(i |-> a)) i2" - proof (cases "i = i2") - case True note i2ei = this - from i2ei have rhs_res: "((mapOf t)(i |-> a)) i2 = Some a" by simp - have lhs_res: "mapOf (mupdate i a t) i = Some a" - proof - - have will_find: "tlookup fst i ?tr = Some (i,a)" - proof - - from setSpec have kvin: "(i,a) : setOf ?tr" by simp - have binsert_sorted_inst: "sortedTree fst t --> - sortedTree fst ?tr" - by (insert binsert_sorted [of "fst" "t" "(i,a)"], assumption) - from v binsert_sorted_inst have rs: "sortedTree fst ?tr" by simp - have tlookup_finds_inst: "sortedTree fst ?tr & (i,a) : setOf ?tr --> - tlookup fst i ?tr = Some (i,a)" - by (insert tlookup_finds [of "fst" "?tr" "(i,a)"], simp) - from rs kvin tlookup_finds_inst show ?thesis by simp - qed - from upres will_find show ?thesis by (simp add: mapOf_def) - qed - from lhs_res rhs_res i2ei show ?thesis by simp - next case False note i2nei = this - from i2nei have rhs_res: "((mapOf t)(i |-> a)) i2 = mapOf t i2" by auto - have lhs_res: "mapOf (mupdate i a t) i2 = mapOf t i2" - proof (cases "mapOf t i2") - case None from this have mapNone: "mapOf t i2 = None" by simp - from v mapNone mapset_none have i2nin: "ALL a. (i2,a) ~: setOf t" by fastsimp - have noneIn: "ALL b. (i2,b) ~: setOf ?tr" - proof - fix b - from v binsert_set - have "setOf ?tr = setOf t - eqs fst (i,a) Un {(i,a)}" - by fastsimp - from this i2nei i2nin show "(i2,b) ~: setOf ?tr" by fastsimp - qed - have mapset_none_inst: - "valid_tmap ?tr --> (mapOf ?tr i2 = None) = (ALL a. (i2, a) ~: setOf ?tr)" - by (insert mapset_none [of "?tr" i2], simp) - from vr noneIn mapset_none_inst have "mapOf ?tr i2 = None" by fastsimp - from this upres mapNone show ?thesis by simp - next case (Some z) from this have mapSome: "mapOf t i2 = Some z" by simp - from v mapSome mapset_some have "(i2,z) : setOf t" by fastsimp - from this setSpec i2nei have "(i2,z) : setOf ?tr" by (simp add: eqs_def) - from this vr mapset_some have "mapOf ?tr i2 = Some z" by fastsimp - from this upres mapSome show ?thesis by simp - qed - from lhs_res rhs_res show ?thesis by simp - qed -qed - -lemma assumes v: "valid_tmap t" - shows mupdate_valid: "valid_tmap (mupdate i a t)" -proof - - let ?tr = "binsert fst (i,a) t" - have upres: "mupdate i a t = ?tr" by (simp add: mupdate_def) - from v binsert_sorted have vr: "valid_tmap ?tr" by fastsimp - from vr upres show ?thesis by simp -qed - -(*============================================================*) -section {* Map Remove Operation *} -(*============================================================*) - -constdefs - mremove :: "index => 'a tarray => 'a tarray" - "mremove i t == remove fst (i, arbitrary) t" - -lemma assumes v: "valid_tmap t" - shows mremove_valid: "valid_tmap (mremove i t)" -proof (simp add: mremove_def) - from v remove_sort - show "sortedTree fst (remove fst (i,arbitrary) t)" by fastsimp -qed - -lemma assumes v: "valid_tmap t" - shows mremove_map: "mapOf (mremove i t) i = None" -proof (simp add: mremove_def) - let ?tr = "remove fst (i,arbitrary) t" - show "mapOf ?tr i = None" - proof - - from v remove_spec - have remSet: "setOf ?tr = setOf t - eqs fst (i,arbitrary)" - by fastsimp - have noneIn: "ALL a. (i,a) ~: setOf ?tr" - proof - fix a - from remSet show "(i,a) ~: setOf ?tr" by (simp add: eqs_def) - qed - from v remove_sort have vr: "valid_tmap ?tr" by fastsimp - have mapset_none_inst: "valid_tmap ?tr ==> - (mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)" - by (insert mapset_none [of "?tr" "i"], simp) - from vr this have "(mapOf ?tr i = None) = (ALL a. (i,a) ~: setOf ?tr)" by fastsimp - from this noneIn show "mapOf ?tr i = None" by simp - qed -qed - -end diff -r 7a3d80e276d4 -r e2373489d373 src/HOL/Induct/BinaryTree_TacticStyle.thy --- a/src/HOL/Induct/BinaryTree_TacticStyle.thy Thu Apr 01 10:54:32 2004 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,141 +0,0 @@ -header {* Tactic-Style Reasoning for Binary Tree Operations *} -theory BinaryTree_TacticStyle = Main: - -text {* This example theory illustrates automated proofs of correctness - for binary tree operations using tactic-style reasoning. - The current proofs for remove operation are by Tobias Nipkow, - some modifications and the remaining tree operations are - by Viktor Kuncak. *} - -(*============================================================*) -section {* Definition of a sorted binary tree *} -(*============================================================*) - -datatype tree = Tip | Nd tree nat tree - -consts set_of :: "tree => nat set" --- {* The set of nodes stored in a tree. *} -primrec -"set_of Tip = {}" -"set_of(Nd l x r) = set_of l Un set_of r Un {x}" - -consts sorted :: "tree => bool" --- {* Tree is sorted *} -primrec -"sorted Tip = True" -"sorted(Nd l y r) = - (sorted l & sorted r & (ALL x:set_of l. x < y) & (ALL z:set_of r. y < z))" - -(*============================================================*) -section {* Tree Membership *} -(*============================================================*) - -consts - memb :: "nat => tree => bool" -primrec -"memb e Tip = False" -"memb e (Nd t1 x t2) = - (if e < x then memb e t1 - else if x < e then memb e t2 - else True)" - -lemma member_set: "sorted t --> memb e t = (e : set_of t)" -by (induct t, auto) - -(*============================================================*) -section {* Insertion operation *} -(*============================================================*) - -consts binsert :: "nat => tree => tree" --- {* Insert a node into sorted tree. *} -primrec -"binsert x Tip = (Nd Tip x Tip)" -"binsert x (Nd t1 y t2) = (if x < y then - (Nd (binsert x t1) y t2) - else - (if y < x then - (Nd t1 y (binsert x t2)) - else (Nd t1 y t2)))" - -theorem set_of_binsert [simp]: "set_of (binsert x t) = set_of t Un {x}" -by (induct_tac t, auto) - -theorem binsert_sorted: "sorted t --> sorted (binsert x t)" -by (induct_tac t, auto simp add: set_of_binsert) - -corollary binsert_spec: (* summary specification of binsert *) -"sorted t ==> - sorted (binsert x t) & - set_of (binsert x t) = set_of t Un {x}" -by (simp add: binsert_sorted) - -(*============================================================*) -section {* Remove operation *} -(*============================================================*) - -consts - remove:: "nat => tree => tree" -- {* remove a node from sorted tree *} - -- {* auxiliary operations: *} - rm :: "tree => nat" -- {* find the rightmost element in the tree *} - rem :: "tree => tree" -- {* find the tree without the rightmost element *} -primrec -"rm(Nd l x r) = (if r = Tip then x else rm r)" -primrec -"rem(Nd l x r) = (if r=Tip then l else Nd l x (rem r))" -primrec -"remove x Tip = Tip" -"remove x (Nd l y r) = - (if x < y then Nd (remove x l) y r else - if y < x then Nd l y (remove x r) else - if l = Tip then r - else Nd (rem l) (rm l) r)" - -lemma rm_in_set_of: "t ~= Tip ==> rm t : set_of t" -by (induct t) auto - -lemma set_of_rem: "t ~= Tip ==> set_of t = set_of(rem t) Un {rm t}" -by (induct t) auto - -lemma [simp]: "[| t ~= Tip; sorted t |] ==> sorted(rem t)" -by (induct t) (auto simp add:set_of_rem) - -lemma sorted_rem: "[| t ~= Tip; x \<in> set_of(rem t); sorted t |] ==> x < rm t" -by (induct t) (auto simp add:set_of_rem split:if_splits) - -theorem set_of_remove [simp]: "sorted t ==> set_of(remove x t) = set_of t - {x}" -apply(induct t) - apply simp -apply simp -apply(rule conjI) - apply fastsimp -apply(rule impI) -apply(rule conjI) - apply fastsimp -apply(fastsimp simp:set_of_rem) -done - -theorem remove_sorted: "sorted t ==> sorted(remove x t)" -by (induct t) (auto intro: less_trans rm_in_set_of sorted_rem) - -corollary remove_spec: -- {* summary specification of remove *} -"sorted t ==> - sorted (remove x t) & - set_of (remove x t) = set_of t - {x}" -by (simp add: remove_sorted) - -text {* Finally, note that rem and rm can be computed - using a single tree traversal given by remrm. *} - -consts remrm :: "tree => tree * nat" -primrec -"remrm(Nd l x r) = (if r=Tip then (l,x) else - let (r',y) = remrm r in (Nd l x r',y))" - -lemma "t ~= Tip ==> remrm t = (rem t, rm t)" -by (induct t) (auto simp:Let_def) - -text {* We can test this implementation by generating code. *} -generate_code ("BinaryTree_TacticStyle_Code.ML") - test = "memb 4 (remove (3::nat) (binsert 4 (binsert 3 Tip)))" - -end diff -r 7a3d80e276d4 -r e2373489d373 src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Thu Apr 01 10:54:32 2004 +0200 +++ b/src/HOL/Induct/ROOT.ML Thu Apr 01 15:05:04 2004 +0200 @@ -10,5 +10,3 @@ time_use_thy "SList"; time_use_thy "LFilter"; -time_use_thy "BinaryTree_Map"; -time_use_thy "BinaryTree_TacticStyle"; diff -r 7a3d80e276d4 -r e2373489d373 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Apr 01 10:54:32 2004 +0200 +++ b/src/HOL/IsaMakefile Thu Apr 01 15:05:04 2004 +0200 @@ -202,8 +202,6 @@ HOL-Induct: HOL $(LOG)/HOL-Induct.gz $(LOG)/HOL-Induct.gz: $(OUT)/HOL \ - Induct/BinaryTree.thy Induct/BinaryTree_Map.thy\ - Induct/BinaryTree_TacticStyle.thy\ Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \ Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \ Induct/PropLog.thy Induct/ROOT.ML \