src/HOL/WF_Rel.ML
author paulson
Thu, 15 May 1997 12:45:42 +0200
changeset 3193 fafc7e815b70
child 3237 4da86d44de33
permissions -rw-r--r--
New theories used by 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
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    13
 * The inverse image into a wellfounded relation is wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    14
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    15
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    16
goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    17
by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    18
by (Step_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    19
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
    20
by (blast_tac (!claset delrules [allE]) 2);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    21
by (etac allE 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    22
by (mp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    23
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    24
qed "wf_inv_image";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    25
AddSIs [wf_inv_image];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    26
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    27
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    28
 * All measures are wellfounded.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    29
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    30
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    31
goalw thy [measure_def] "wf (measure f)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    32
by (rtac wf_inv_image 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    33
by (rtac wf_trancl 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    34
by (rtac wf_pred_nat 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    35
qed "wf_measure";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    36
AddIffs [wf_measure];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    37
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    38
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    39
 * Wellfoundedness of lexicographic combinations
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    40
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    41
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    42
goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    43
by (rtac allI 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    44
by (rtac (surjective_pairing RS ssubst) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    45
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    46
qed "split_all_pair";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    47
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    48
val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    49
 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    50
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    51
by (rtac (wfa RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    52
by (EVERY1 [rtac allI,rtac impI]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    53
by (rtac (wfb RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    54
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    55
qed "wf_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    56
AddSIs [wf_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    57
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    58
(*----------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    59
 * Wellfoundedness of relational product
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    60
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    61
val [wfa,wfb] = goalw thy [wf_def,rprod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    62
 "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    63
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    64
by (rtac (wfa RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    65
by (EVERY1 [rtac allI,rtac impI]);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    66
by (rtac (wfb RS spec RS mp) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    67
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    68
qed "wf_rel_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    69
AddSIs [wf_rel_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    70
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    71
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    72
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    73
 * Wellfoundedness of subsets
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    74
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    75
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    76
goal thy "!!r. [| wf(r);  p<=r |] ==> wf(p)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    77
by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    78
by (Fast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    79
qed "wf_subset";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    80
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    81
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    82
 * Wellfoundedness of the empty relation.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    83
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    84
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    85
goal thy "wf({})";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    86
by (simp_tac (!simpset addsimps [wf_def]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    87
qed "wf_empty";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    88
AddSIs [wf_empty];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    89
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    90
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    91
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    92
 * Transitivity of WF combinators.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    93
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    94
goalw thy [trans_def, lex_prod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    95
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    96
by (Simp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    97
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    98
qed "trans_lex_prod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
    99
AddSIs [trans_lex_prod];
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   100
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   101
goalw thy [trans_def, rprod_def]
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   102
    "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   103
by (Simp_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   104
by (Blast_tac 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   105
qed "trans_rprod";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   106
AddSIs [trans_rprod];
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
(*---------------------------------------------------------------------------
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   110
 * Wellfoundedness of proper subset on finite sets.
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   111
 *---------------------------------------------------------------------------*)
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   112
goalw thy [finite_psubset_def] "wf(finite_psubset)";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   113
by (rtac (wf_measure RS wf_subset) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   114
by (simp_tac (!simpset addsimps[measure_def, inv_image_def,
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   115
				symmetric less_def])1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   116
by (fast_tac (!claset addIs [psubset_card]) 1);
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   117
qed "wf_finite_psubset";
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   118
fafc7e815b70 New theories used by TFL
paulson
parents:
diff changeset
   119