src/HOL/WF_Rel.ML
author paulson
Tue, 20 May 1997 11:40:28 +0200
changeset 3237 4da86d44de33
parent 3193 fafc7e815b70
child 3296 2ee6c397003d
permissions -rw-r--r--
Relation "less_than" internalizes "<" for easy use of TFL
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     1
(*  Title: 	HOL/WF_Rel
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     2
    ID:         $Id$
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     3
    Author: 	Konrad Slind
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     4
    Copyright   1996  TU Munich
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     5
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     6
Derived wellfounded relations: inverse image, relational product, measure, ...
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     7
*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     8
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
     9
open WF_Rel;
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    10
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    11
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    12
(*----------------------------------------------------------------------------
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    13
 * "Less than" on the natural numbers
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    14
 *---------------------------------------------------------------------------*)
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    15
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    16
goalw thy [less_than_def] "wf less_than"; 
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    17
by (rtac (wf_pred_nat RS wf_trancl) 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    18
qed "wf_less_than";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    19
AddIffs [wf_less_than];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    20
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    21
goalw thy [less_than_def] "trans less_than"; 
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    22
by (rtac trans_trancl 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    23
qed "trans_less_than";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    24
AddIffs [trans_less_than];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    25
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    26
goalw thy [less_than_def, less_def] "((x,y): less_than) = (x<y)"; 
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    27
by (Simp_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    28
qed "less_than_iff";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    29
AddIffs [less_than_iff];
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    30
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    31
(*----------------------------------------------------------------------------
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    32
 * The inverse image into a wellfounded relation is wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    33
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    34
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    35
goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    36
by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    37
by (Step_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    38
by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    39
by (blast_tac (!claset delrules [allE]) 2);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    40
by (etac allE 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    41
by (mp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    42
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    43
qed "wf_inv_image";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    44
AddSIs [wf_inv_image];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    45
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    46
goalw thy [trans_def,inv_image_def]
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    47
    "!!r. trans r ==> trans (inv_image r f)";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    48
by (Simp_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    49
by (Blast_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    50
qed "trans_inv_image";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    51
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    52
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    53
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    54
 * All measures are wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    55
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    56
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    57
goalw thy [measure_def] "wf (measure f)";
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
    58
by (rtac (wf_less_than RS wf_inv_image) 1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    59
qed "wf_measure";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    60
AddIffs [wf_measure];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    61
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    62
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    63
 * Wellfoundedness of lexicographic combinations
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    64
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    65
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    66
goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    67
by (rtac allI 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    68
by (rtac (surjective_pairing RS ssubst) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    69
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    70
qed "split_all_pair";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    71
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    72
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    73
 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    74
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    75
by (rtac (wfa RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    76
by (EVERY1 [rtac allI,rtac impI]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    77
by (rtac (wfb RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    78
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    79
qed "wf_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    80
AddSIs [wf_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    81
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    82
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    83
 * Wellfoundedness of relational product
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    84
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    85
val [wfa,wfb] = goalw thy [wf_def,rprod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    86
 "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    87
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    88
by (rtac (wfa RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    89
by (EVERY1 [rtac allI,rtac impI]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    90
by (rtac (wfb RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    91
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    92
qed "wf_rel_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    93
AddSIs [wf_rel_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    94
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    95
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    96
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    97
 * Wellfoundedness of subsets
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    98
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    99
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   100
goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   101
by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   102
by (Fast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   103
qed "wf_subset";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   104
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   105
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   106
 * Wellfoundedness of the empty relation.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   107
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   108
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   109
goal thy "wf({})";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   110
by (simp_tac (!simpset addsimps [wf_def]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   111
qed "wf_empty";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   112
AddSIs [wf_empty];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   113
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   114
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   115
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   116
 * Transitivity of WF combinators.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   117
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   118
goalw thy [trans_def, lex_prod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   119
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   120
by (Simp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   121
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   122
qed "trans_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   123
AddSIs [trans_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   124
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   125
goalw thy [trans_def, rprod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   126
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   127
by (Simp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   128
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   129
qed "trans_rprod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   130
AddSIs [trans_rprod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   131
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   132
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   133
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   134
 * Wellfoundedness of proper subset on finite sets.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   135
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   136
goalw thy [finite_psubset_def] "wf(finite_psubset)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   137
by (rtac (wf_measure RS wf_subset) 1);
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   138
by (simp_tac (!simpset addsimps [measure_def, inv_image_def, less_than_def,
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   139
				 symmetric less_def])1);
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   140
by (fast_tac (!claset addIs [psubset_card]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   141
qed "wf_finite_psubset";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   142
3237
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   143
goalw thy [finite_psubset_def, trans_def] "trans finite_psubset";
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   144
by (simp_tac (!simpset addsimps [psubset_def]) 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   145
by (Blast_tac 1);
4da86d44de33 Relation "less_than" internalizes "<" for easy use of TFL
paulson
parents: 3193
diff changeset
   146
qed "trans_finite_psubset";
3193
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   147