# HG changeset patch # User wenzelm # Date 1248805599 -7200 # Node ID 99711ef9d582249ab73e9e93374fe8c0b8c3b05d # Parent b1c2110ae6810b00fa4db5338aad8a3d9d6ff9b4# Parent 8b03a3daba5da3faed6fe405553468a8cd2f57f2 merged diff -r 8b03a3daba5d -r 99711ef9d582 NEWS --- a/NEWS Tue Jul 28 19:49:42 2009 +0200 +++ b/NEWS Tue Jul 28 20:26:39 2009 +0200 @@ -18,6 +18,8 @@ *** HOL *** +* Set.UNIV and Set.empty are mere abbreviations for top and bot. INCOMPATIBILITY. + * More convenient names for set intersection and union. INCOMPATIBILITY: Set.Int ~> Set.inter diff -r 8b03a3daba5d -r 99711ef9d582 doc-src/Main/Docs/document/Main_Doc.tex --- a/doc-src/Main/Docs/document/Main_Doc.tex Tue Jul 28 19:49:42 2009 +0200 +++ b/doc-src/Main/Docs/document/Main_Doc.tex Tue Jul 28 20:26:39 2009 +0200 @@ -231,7 +231,7 @@ \begin{supertabular}{@ {} l @ {~::~} l @ {}} \isa{converse} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ -\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}c\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ +\isa{op\ O} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}c{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}c{\isacharparenright}\ set}\\ \isa{op\ {\isacharbackquote}{\isacharbackquote}} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharprime}b\ set}\\ \isa{inv{\isacharunderscore}image} & \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}a{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}b\ {\isasymtimes}\ {\isacharprime}b{\isacharparenright}\ set}\\ \isa{Id{\isacharunderscore}on} & \isa{{\isacharprime}a\ set\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set}\\ diff -r 8b03a3daba5d -r 99711ef9d582 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 19:49:42 2009 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Tue Jul 28 20:26:39 2009 +0200 @@ -841,6 +841,8 @@ (*Apply rules to break down assumptions of the form Y \ parts(insert X H) and Y \ analz(insert X H) *) +fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) + val Fake_insert_tac = dresolve_tac [impOfSubs Fake_analz_insert, impOfSubs Fake_parts_insert] THEN' diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/MicroJava/BV/Listn.thy --- a/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/MicroJava/BV/Listn.thy Tue Jul 28 20:26:39 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/MicroJava/BV/Listn.thy - ID: $Id$ Author: Tobias Nipkow Copyright 2000 TUM @@ -8,7 +7,9 @@ header {* \isaheader{Fixed Length Lists} *} -theory Listn imports Err begin +theory Listn +imports Err +begin constdefs @@ -317,6 +318,10 @@ apply (simp add: nth_Cons split: nat.split) done +lemma equals0I_aux: + "(\y. A y \ False) \ A = bot_class.bot" + by (rule equals0I) (auto simp add: mem_def) + lemma acc_le_listI [intro!]: "\ order r; acc r \ \ acc(Listn.le r)" apply (unfold acc_def) @@ -330,7 +335,7 @@ apply (rename_tac m n) apply (case_tac "m=n") apply simp - apply (fast intro!: equals0I [to_pred bot_empty_eq pred_equals_eq] dest: not_sym) + apply (fast intro!: equals0I_aux dest: not_sym) apply clarify apply (rename_tac n) apply (induct_tac n) diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/NatTransfer.thy --- a/src/HOL/NatTransfer.thy Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/NatTransfer.thy Tue Jul 28 20:26:39 2009 +0200 @@ -382,7 +382,7 @@ lemma UNIV_apply: "UNIV x = True" - by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq) + by (simp add: top_fun_eq top_bool_eq) declare TransferMorphism_int_nat[transfer add return: transfer_int_nat_numerals diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Set.thy Tue Jul 28 20:26:39 2009 +0200 @@ -100,8 +100,8 @@ text {* Set enumerations *} -definition empty :: "'a set" ("{}") where - bot_set_eq [symmetric]: "{} = bot" +abbreviation empty :: "'a set" ("{}") where + "{} \ bot" definition insert :: "'a \ 'a set \ 'a set" where insert_compr: "insert a B = {x. x = a \ x \ B}" @@ -541,12 +541,12 @@ subsubsection {* The universal set -- UNIV *} -definition UNIV :: "'a set" where - top_set_eq [symmetric]: "UNIV = top" +abbreviation UNIV :: "'a set" where + "UNIV \ top" lemma UNIV_def: "UNIV = {x. True}" - by (simp add: top_set_eq [symmetric] top_fun_eq top_bool_eq Collect_def) + by (simp add: top_fun_eq top_bool_eq Collect_def) lemma UNIV_I [simp]: "x : UNIV" by (simp add: UNIV_def) @@ -579,7 +579,7 @@ lemma empty_def: "{} = {x. False}" - by (simp add: bot_set_eq [symmetric] bot_fun_eq bot_bool_eq Collect_def) + by (simp add: bot_fun_eq bot_bool_eq Collect_def) lemma empty_iff [simp]: "(c : {}) = False" by (simp add: empty_def) diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Jul 28 20:26:39 2009 +0200 @@ -428,7 +428,7 @@ in fun provein x S = case term_of S of - Const(@{const_name Set.empty}, _) => error "Unexpected error in Cooper, please email Amine Chaieb" + Const(@{const_name Orderings.bot}, _) => error "Unexpected error in Cooper, please email Amine Chaieb" | Const(@{const_name insert}, _) $ y $ _ => let val (cy,S') = Thm.dest_binop S in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Tue Jul 28 20:26:39 2009 +0200 @@ -99,7 +99,7 @@ in fun provein x S = case term_of S of - Const(@{const_name Set.empty}, _) => raise CTERM ("provein : not a member!", [S]) + Const(@{const_name Orderings.bot}, _) => raise CTERM ("provein : not a member!", [S]) | Const(@{const_name insert}, _) $ y $_ => let val (cy,S') = Thm.dest_binop S in if term_of x aconv y then instantiate' [] [SOME x, SOME S'] insI1 diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Tools/Qelim/langford.ML --- a/src/HOL/Tools/Qelim/langford.ML Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Tools/Qelim/langford.ML Tue Jul 28 20:26:39 2009 +0200 @@ -15,7 +15,7 @@ let fun h acc ct = case term_of ct of - Const (@{const_name Set.empty}, _) => acc + Const (@{const_name Orderings.bot}, _) => acc | Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct) in h [] end; @@ -48,11 +48,11 @@ in (ne, f) end val qe = case (term_of L, term_of U) of - (Const (@{const_name Set.empty}, _),_) => + (Const (@{const_name Orderings.bot}, _),_) => let val (neU,fU) = proveneF U in simp_rule (transitive ths (dlo_qeth_nolb OF [neU, fU])) end - | (_,Const (@{const_name Set.empty}, _)) => + | (_,Const (@{const_name Orderings.bot}, _)) => let val (neL,fL) = proveneF L in simp_rule (transitive ths (dlo_qeth_noub OF [neL, fL])) end diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Tue Jul 28 20:26:39 2009 +0200 @@ -153,13 +153,13 @@ fun mk_set T ts = let val sT = mk_setT T; - val empty = Const ("Set.empty", sT); + val empty = Const ("Orderings.bot_class.bot", sT); fun insert t u = Const ("Set.insert", T --> sT --> sT) $ t $ u; in fold_rev insert ts empty end; -fun mk_UNIV T = Const ("Set.UNIV", mk_setT T); +fun mk_UNIV T = Const ("Orderings.top_class.top", mk_setT T); -fun dest_set (Const ("Set.empty", _)) = [] +fun dest_set (Const ("Orderings.bot_class.bot", _)) = [] | dest_set (Const ("Set.insert", _) $ t $ u) = t :: dest_set u | dest_set t = raise TERM ("dest_set", [t]); diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Tools/res_clause.ML Tue Jul 28 20:26:39 2009 +0200 @@ -99,20 +99,10 @@ val const_trans_table = Symtab.make [(@{const_name "op ="}, "equal"), (@{const_name HOL.less_eq}, "lessequals"), - (@{const_name HOL.less}, "less"), (@{const_name "op &"}, "and"), (@{const_name "op |"}, "or"), - (@{const_name HOL.plus}, "plus"), - (@{const_name HOL.minus}, "minus"), - (@{const_name HOL.times}, "times"), - (@{const_name Divides.div}, "div"), - (@{const_name HOL.divide}, "divide"), (@{const_name "op -->"}, "implies"), - (@{const_name Set.empty}, "emptyset"), (@{const_name "op :"}, "in"), - (@{const_name union}, "union"), - (@{const_name inter}, "inter"), - ("List.append", "append"), ("ATP_Linkup.fequal", "fequal"), ("ATP_Linkup.COMBI", "COMBI"), ("ATP_Linkup.COMBK", "COMBK"), diff -r 8b03a3daba5d -r 99711ef9d582 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Tue Jul 28 19:49:42 2009 +0200 +++ b/src/HOL/Wellfounded.thy Tue Jul 28 20:26:39 2009 +0200 @@ -283,8 +283,10 @@ apply (blast elim!: allE) done -lemmas wfP_SUP = wf_UN [where I=UNIV and r="\i. {(x, y). r i x y}", - to_pred SUP_UN_eq2 bot_empty_eq pred_equals_eq, simplified, standard] +lemma wfP_SUP: + "\i. wfP (r i) \ \i j. r i \ r j \ inf (DomainP (r i)) (RangeP (r j)) = bot \ wfP (SUPR UNIV r)" + by (rule wf_UN [where I=UNIV and r="\i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq]) + (simp_all add: bot_fun_eq bot_bool_eq) lemma wf_Union: "[| ALL r:R. wf r;