# HG changeset patch # User paulson # Date 863693142 -7200 # Node ID fafc7e815b70b03d284612a4214532581e299ef6 # Parent a75558a4ed3773790bb894b3119f054472ce7fb5 New theories used by TFL diff -r a75558a4ed37 -r fafc7e815b70 src/HOL/Psubset.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Psubset.ML Thu May 15 12:45:42 1997 +0200 @@ -0,0 +1,83 @@ +(* Title: Psubset.ML + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Properties of subsets and empty sets. +*) + +open Psubset; + +(*********) + +(*** Rules for subsets ***) + +goal Set.thy "A <= B = (! t.t:A --> t:B)"; +by (Blast_tac 1); +qed "subset_iff"; + +goalw thy [psubset_def] "!!A::'a set. [| A <= B; A ~= B |] ==> A A ~= B"; +by (Blast_tac 1); +qed "insert_lim"; + +(* This is an adaptation of the proof for the "<=" version in Finite. *) + +goalw thy [psubset_def] +"!!B. finite B ==> !A. A < B --> card(A) < card(B)"; +by (etac finite_induct 1); +by (Simp_tac 1); +by (Blast_tac 1); +by (strip_tac 1); +by (etac conjE 1); +by (case_tac "x:A" 1); +(*1*) +by (dtac mk_disjoint_insert 1); +by (etac exE 1); +by (etac conjE 1); +by (hyp_subst_tac 1); +by (rotate_tac ~1 1); +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); +by (dtac insert_lim 1); +by (Asm_full_simp_tac 1); +(*2*) +by (rotate_tac ~1 1); +by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); +by (case_tac "A=F" 1); +by (Asm_simp_tac 1); +by (Asm_simp_tac 1); +by (subgoal_tac "card A <= card F" 1); +by (Asm_simp_tac 2); +by (Auto_tac()); +qed_spec_mp "psubset_card" ; + + +goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))"; +by (Blast_tac 1); +qed "set_eq_subset"; + + +goalw thy [psubset_def] "~ (A < {})"; +by (Blast_tac 1); +qed "not_psubset_empty"; + +AddIffs [not_psubset_empty]; + +goalw thy [psubset_def] + "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x} A Un C < B Un D + even for finite sets: consider A={1}, C={2}, B=D={1,2} *) + + diff -r a75558a4ed37 -r fafc7e815b70 src/HOL/Psubset.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Psubset.thy Thu May 15 12:45:42 1997 +0200 @@ -0,0 +1,14 @@ +(* Title: Psubset.thy + Author: Martin Coen, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +The "Proper Subset" relation +*) + +Psubset = Finite + + +rules (*not allowed as "defs" because < is overloaded*) + + psubset_def "A < B == A <= B & ~ A=B" + +end diff -r a75558a4ed37 -r fafc7e815b70 src/HOL/WF_Rel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/WF_Rel.ML Thu May 15 12:45:42 1997 +0200 @@ -0,0 +1,119 @@ +(* Title: HOL/WF_Rel + ID: $Id$ + Author: Konrad Slind + Copyright 1996 TU Munich + +Derived wellfounded relations: inverse image, relational product, measure, ... +*) + +open WF_Rel; + + +(*---------------------------------------------------------------------------- + * The inverse image into a wellfounded relation is wellfounded. + *---------------------------------------------------------------------------*) + +goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; +by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1); +by (Step_tac 1); +by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1); +by (blast_tac (!claset delrules [allE]) 2); +by (etac allE 1); +by (mp_tac 1); +by (Blast_tac 1); +qed "wf_inv_image"; +AddSIs [wf_inv_image]; + +(*---------------------------------------------------------------------------- + * All measures are wellfounded. + *---------------------------------------------------------------------------*) + +goalw thy [measure_def] "wf (measure f)"; +by (rtac wf_inv_image 1); +by (rtac wf_trancl 1); +by (rtac wf_pred_nat 1); +qed "wf_measure"; +AddIffs [wf_measure]; + +(*---------------------------------------------------------------------------- + * Wellfoundedness of lexicographic combinations + *---------------------------------------------------------------------------*) + +goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)"; +by (rtac allI 1); +by (rtac (surjective_pairing RS ssubst) 1); +by (Blast_tac 1); +qed "split_all_pair"; + +val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] + "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); +by (rtac (wfa RS spec RS mp) 1); +by (EVERY1 [rtac allI,rtac impI]); +by (rtac (wfb RS spec RS mp) 1); +by (Blast_tac 1); +qed "wf_lex_prod"; +AddSIs [wf_lex_prod]; + +(*---------------------------------------------------------------------------- + * Wellfoundedness of relational product + *---------------------------------------------------------------------------*) +val [wfa,wfb] = goalw thy [wf_def,rprod_def] + "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)"; +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); +by (rtac (wfa RS spec RS mp) 1); +by (EVERY1 [rtac allI,rtac impI]); +by (rtac (wfb RS spec RS mp) 1); +by (Blast_tac 1); +qed "wf_rel_prod"; +AddSIs [wf_rel_prod]; + + +(*--------------------------------------------------------------------------- + * Wellfoundedness of subsets + *---------------------------------------------------------------------------*) + +goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; +by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); +by (Fast_tac 1); +qed "wf_subset"; + +(*--------------------------------------------------------------------------- + * Wellfoundedness of the empty relation. + *---------------------------------------------------------------------------*) + +goal thy "wf({})"; +by (simp_tac (!simpset addsimps [wf_def]) 1); +qed "wf_empty"; +AddSIs [wf_empty]; + + +(*--------------------------------------------------------------------------- + * Transitivity of WF combinators. + *---------------------------------------------------------------------------*) +goalw thy [trans_def, lex_prod_def] + "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)"; +by (Simp_tac 1); +by (Blast_tac 1); +qed "trans_lex_prod"; +AddSIs [trans_lex_prod]; + +goalw thy [trans_def, rprod_def] + "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)"; +by (Simp_tac 1); +by (Blast_tac 1); +qed "trans_rprod"; +AddSIs [trans_rprod]; + + +(*--------------------------------------------------------------------------- + * Wellfoundedness of proper subset on finite sets. + *---------------------------------------------------------------------------*) +goalw thy [finite_psubset_def] "wf(finite_psubset)"; +by (rtac (wf_measure RS wf_subset) 1); +by (simp_tac (!simpset addsimps[measure_def, inv_image_def, + symmetric less_def])1); +by (fast_tac (!claset addIs [psubset_card]) 1); +qed "wf_finite_psubset"; + + diff -r a75558a4ed37 -r fafc7e815b70 src/HOL/WF_Rel.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/WF_Rel.thy Thu May 15 12:45:42 1997 +0200 @@ -0,0 +1,32 @@ +(* Title: HOL/WF_Rel + ID: $Id$ + Author: Konrad Slind + Copyright 1995 TU Munich + +Derived wellfounded relations: inverse image, relational product, measure, ... +*) + +WF_Rel = WF + Psubset + +consts + inv_image :: "('b * 'b)set => ('a => 'b) => ('a * 'a)set" + measure :: "('a => nat) => ('a * 'a)set" + "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) + rprod :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" + finite_psubset :: "('a set * 'a set) set" + +defs + inv_image_def "inv_image r f == {(x,y). (f(x), f(y)) : r}" + + measure_def "measure == inv_image (trancl pred_nat)" + + lex_prod_def "ra**rb == {p. ? a a' b b'. + p = ((a,b),(a',b')) & + ((a,a') : ra | a=a' & (b,b') : rb)}" + + rprod_def "rprod ra rb == {p. ? a a' b b'. + p = ((a,b),(a',b')) & + ((a,a') : ra & (b,b') : rb)}" + + (* finite proper subset*) + finite_psubset_def "finite_psubset == {(A,B). A < B & finite B}" +end