# HG changeset patch # User berghofe # Date 1184144679 -7200 # Node ID d7f18c837ce7f1f0b9c4362f55d8a5aae124be22 # Parent c5ead5df7f358df28a3649781840fbeb0a8163cb Adapted to new package for inductive sets. diff -r c5ead5df7f35 -r d7f18c837ce7 src/HOL/List.thy --- a/src/HOL/List.thy Wed Jul 11 11:03:11 2007 +0200 +++ b/src/HOL/List.thy Wed Jul 11 11:04:39 2007 +0200 @@ -2386,33 +2386,20 @@ subsubsection {* @{text lists}: the list-forming operator over sets *} -inductive2 - listsp :: "('a \ bool) \ 'a list \ bool" - for A :: "'a \ bool" -where - Nil [intro!]: "listsp A []" - | Cons [intro!]: "[| A a; listsp A l |] ==> listsp A (a # l)" - -constdefs +inductive_set lists :: "'a set => 'a list set" - "lists A == Collect (listsp (member A))" - -lemma listsp_lists_eq [pred_set_conv]: "listsp (member A) = member (lists A)" - by (simp add: lists_def) - -lemmas lists_intros [intro!] = listsp.intros [to_set] - -lemmas lists_induct [consumes 1, case_names Nil Cons, induct set: lists] = - listsp.induct [to_set] - -inductive_cases2 listspE [elim!]: "listsp A (x # l)" - -lemmas listsE [elim!] = listspE [to_set] - -lemma listsp_mono [mono2]: "A \ B ==> listsp A \ listsp B" + for A :: "'a set" +where + Nil [intro!]: "[]: lists A" + | Cons [intro!]: "[| a: A;l: lists A|] ==> a#l : lists A" + +inductive_cases listsE [elim!]: "x#l : lists A" +inductive_cases listspE [elim!]: "listsp A (x # l)" + +lemma listsp_mono [mono]: "A \ B ==> listsp A \ listsp B" by (clarify, erule listsp.induct, blast+) -lemmas lists_mono [mono] = listsp_mono [to_set] +lemmas lists_mono = listsp_mono [to_set] lemma listsp_infI: assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l @@ -2459,7 +2446,7 @@ subsubsection{* Inductive definition for membership *} -inductive2 ListMem :: "'a \ 'a list \ bool" +inductive ListMem :: "'a \ 'a list \ bool" where elem: "ListMem x (x # xs)" | insert: "ListMem x xs \ ListMem x (y # xs)" @@ -2711,73 +2698,60 @@ subsubsection{*Lifting a Relation on List Elements to the Lists*} -inductive2 - list_all2' :: "('a \ 'b \ bool) \ 'a list \ 'b list \ bool" - for r :: "'a \ 'b \ bool" +inductive_set + listrel :: "('a * 'a)set => ('a list * 'a list)set" + for r :: "('a * 'a)set" where - Nil: "list_all2' r [] []" - | Cons: "[| r x y; list_all2' r xs ys |] ==> list_all2' r (x#xs) (y#ys)" - -constdefs - listrel :: "('a * 'b) set => ('a list * 'b list) set" - "listrel r == Collect2 (list_all2' (member2 r))" - -lemma list_all2_listrel_eq [pred_set_conv]: - "list_all2' (member2 r) = member2 (listrel r)" - by (simp add: listrel_def) - -lemmas listrel_induct [consumes 1, case_names Nil Cons, induct set: listrel] = - list_all2'.induct [to_set] - -lemmas listrel_intros = list_all2'.intros [to_set] - -inductive_cases2 listrel_Nil1 [to_set, elim!]: "list_all2' r [] xs" -inductive_cases2 listrel_Nil2 [to_set, elim!]: "list_all2' r xs []" -inductive_cases2 listrel_Cons1 [to_set, elim!]: "list_all2' r (y#ys) xs" -inductive_cases2 listrel_Cons2 [to_set, elim!]: "list_all2' r xs (y#ys)" + Nil: "([],[]) \ listrel r" + | Cons: "[| (x,y) \ r; (xs,ys) \ listrel r |] ==> (x#xs, y#ys) \ listrel r" + +inductive_cases listrel_Nil1 [elim!]: "([],xs) \ listrel r" +inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \ listrel r" +inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \ listrel r" +inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \ listrel r" lemma listrel_mono: "r \ s \ listrel r \ listrel s" apply clarify -apply (erule listrel_induct) -apply (blast intro: listrel_intros)+ +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ done lemma listrel_subset: "r \ A \ A \ listrel r \ lists A \ lists A" apply clarify -apply (erule listrel_induct, auto) +apply (erule listrel.induct, auto) done lemma listrel_refl: "refl A r \ refl (lists A) (listrel r)" apply (simp add: refl_def listrel_subset Ball_def) apply (rule allI) apply (induct_tac x) -apply (auto intro: listrel_intros) +apply (auto intro: listrel.intros) done lemma listrel_sym: "sym r \ sym (listrel r)" apply (auto simp add: sym_def) -apply (erule listrel_induct) -apply (blast intro: listrel_intros)+ +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ done lemma listrel_trans: "trans r \ trans (listrel r)" apply (simp add: trans_def) apply (intro allI) apply (rule impI) -apply (erule listrel_induct) -apply (blast intro: listrel_intros)+ +apply (erule listrel.induct) +apply (blast intro: listrel.intros)+ done theorem equiv_listrel: "equiv A r \ equiv (lists A) (listrel r)" by (simp add: equiv_def listrel_refl listrel_sym listrel_trans) lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}" -by (blast intro: listrel_intros) +by (blast intro: listrel.intros) lemma listrel_Cons: "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"; -by (auto simp add: set_Cons_def intro: listrel_intros) +by (auto simp add: set_Cons_def intro: listrel.intros) subsection{*Miscellany*} @@ -2875,7 +2849,7 @@ subsubsection {* Generation of efficient code *} consts - memberl :: "'a \ 'a list \ bool" (infixl "mem" 55) + member :: "'a \ 'a list \ bool" (infixl "mem" 55) null:: "'a list \ bool" list_inter :: "'a list \ 'a list \ 'a list" list_ex :: "('a \ bool) \ 'a list \ bool" diff -r c5ead5df7f35 -r d7f18c837ce7 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Wed Jul 11 11:03:11 2007 +0200 +++ b/src/HOL/Nat.thy Wed Jul 11 11:04:39 2007 +0200 @@ -34,18 +34,17 @@ text {* Type definition *} -inductive2 Nat :: "ind \ bool" +inductive_set Nat :: "ind set" where - Zero_RepI: "Nat Zero_Rep" - | Suc_RepI: "Nat i ==> Nat (Suc_Rep i)" + Zero_RepI: "Zero_Rep : Nat" + | Suc_RepI: "i : Nat ==> Suc_Rep i : Nat" global typedef (open Nat) - nat = "Collect Nat" + nat = Nat proof - from Nat.Zero_RepI - show "Zero_Rep : Collect Nat" .. + show "Zero_Rep : Nat" by (rule Nat.Zero_RepI) qed text {* Abstract constants and syntax *} @@ -72,23 +71,17 @@ text {* Induction *} -lemma Rep_Nat': "Nat (Rep_Nat x)" - by (rule Rep_Nat [simplified mem_Collect_eq]) - -lemma Abs_Nat_inverse': "Nat y \ Rep_Nat (Abs_Nat y) = y" - by (rule Abs_Nat_inverse [simplified mem_Collect_eq]) - theorem nat_induct: "P 0 ==> (!!n. P n ==> P (Suc n)) ==> P n" apply (unfold Zero_nat_def Suc_def) apply (rule Rep_Nat_inverse [THEN subst]) -- {* types force good instantiation *} - apply (erule Rep_Nat' [THEN Nat.induct]) - apply (iprover elim: Abs_Nat_inverse' [THEN subst]) + apply (erule Rep_Nat [THEN Nat.induct]) + apply (iprover elim: Abs_Nat_inverse [THEN subst]) done text {* Distinctness of constructors *} lemma Suc_not_Zero [iff]: "Suc m \ 0" - by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat' Suc_RepI Zero_RepI + by (simp add: Zero_nat_def Suc_def Abs_Nat_inject Rep_Nat Suc_RepI Zero_RepI Suc_Rep_not_Zero_Rep) lemma Zero_not_Suc [iff]: "0 \ Suc m" @@ -103,7 +96,7 @@ text {* Injectiveness of @{term Suc} *} lemma inj_Suc[simp]: "inj_on Suc N" - by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat' Suc_RepI + by (simp add: Suc_def inj_on_def Abs_Nat_inject Rep_Nat Suc_RepI inj_Suc_Rep [THEN inj_eq] Rep_Nat_inject) lemma Suc_inject: "Suc x = Suc y ==> x = y"