TFL/WF1.ML
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
(*  Title: 	HOL/WF.ML
paulson@2112
     2
    ID:         $Id$
paulson@2112
     3
    Author: 	Konrad Slind
paulson@2112
     4
    Copyright   1996  TU Munich
paulson@2112
     5
paulson@2112
     6
For WF1.thy.  
paulson@2112
     7
*)
paulson@2112
     8
paulson@2112
     9
open WF1;
paulson@2112
    10
paulson@2112
    11
(* TFL variants *)
paulson@2112
    12
goal WF.thy
paulson@2112
    13
    "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
paulson@2112
    14
by (strip_tac 1);
paulson@2112
    15
by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
paulson@2112
    16
by (assume_tac 1);
paulson@2112
    17
by (fast_tac HOL_cs 1);
paulson@2112
    18
qed"tfl_wf_induct";
paulson@2112
    19
paulson@2112
    20
goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
paulson@2112
    21
by (strip_tac 1);
paulson@2112
    22
by (rtac cut_apply 1);
paulson@2112
    23
by (assume_tac 1);
paulson@2112
    24
qed"tfl_cut_apply";
paulson@2112
    25
paulson@2112
    26
goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
paulson@2112
    27
by (strip_tac 1);
paulson@2112
    28
by (res_inst_tac [("r","R"), ("H","M"),
paulson@2112
    29
                  ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
paulson@2112
    30
by (assume_tac 1);
paulson@2112
    31
by (assume_tac 1);
paulson@2112
    32
qed "tfl_wfrec";
paulson@2112
    33
paulson@2112
    34
(*----------------------------------------------------------------------------
paulson@2112
    35
 * Proof that the inverse image into a wellfounded relation is wellfounded.
paulson@2112
    36
 * The proof is relatively sloppy - I map to another version of 
paulson@2112
    37
 * wellfoundedness (every n.e. set has an R-minimal element) and transport 
paulson@2112
    38
 * the proof for that formulation over. I also didn't remember the existence
paulson@2112
    39
 *  of "set_cs" so no doubt the proof can be dramatically shortened!
paulson@2112
    40
 *---------------------------------------------------------------------------*)
paulson@2112
    41
goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))";
paulson@2112
    42
by (fast_tac HOL_cs 1);
paulson@2112
    43
val th1 = result();
paulson@2112
    44
paulson@2112
    45
goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))";
paulson@2112
    46
by (fast_tac HOL_cs 1);
paulson@2112
    47
val th2 = result();
paulson@2112
    48
paulson@2112
    49
goal HOL.thy "(~(x-->y)) = (x & (~ y))";
paulson@2112
    50
by (fast_tac HOL_cs 1);
paulson@2112
    51
val th3 = result();
paulson@2112
    52
paulson@2112
    53
goal HOL.thy "((~ x) | y) = (x --> y)";
paulson@2112
    54
by (fast_tac HOL_cs 1);
paulson@2112
    55
val th4 = result();
paulson@2112
    56
paulson@2112
    57
goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))";
paulson@2112
    58
by (fast_tac HOL_cs 1);
paulson@2112
    59
val th5 = result();
paulson@2112
    60
paulson@2112
    61
goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))";
paulson@2112
    62
by (fast_tac HOL_cs 1);
paulson@2112
    63
val th6 = result();
paulson@2112
    64
paulson@2112
    65
goal HOL.thy "(~(~x)) = x";
paulson@2112
    66
by (fast_tac HOL_cs 1);
paulson@2112
    67
val th7 = result();
paulson@2112
    68
paulson@2112
    69
(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *)
paulson@2112
    70
val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7];
paulson@2112
    71
paulson@2112
    72
(* The name "contrapos" is already taken. *)
paulson@2112
    73
goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))";
paulson@2112
    74
by (fast_tac HOL_cs 1);
paulson@2112
    75
val ol_contrapos = result();
paulson@2112
    76
paulson@2112
    77
(* Maps to another version of wellfoundedness *)
paulson@2112
    78
val [p1] = goalw WF.thy [wf_def]
paulson@2112
    79
"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
paulson@2112
    80
by (rtac allI 1);
paulson@2112
    81
by (rtac (ol_contrapos RS ssubst) 1);
paulson@2112
    82
by (rewrite_tac NNF_rews);
paulson@2112
    83
by (rtac impI 1);
paulson@2112
    84
by (rtac ((p1 RS spec) RS mp) 1);
paulson@2112
    85
by (fast_tac HOL_cs 1);
paulson@2112
    86
val wf_minimal = result();
paulson@2112
    87
paulson@2112
    88
goalw WF.thy [wf_def]
paulson@2112
    89
"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R";
paulson@2112
    90
by (rtac impI 1);
paulson@2112
    91
by (rtac allI 1);
paulson@2112
    92
by (rtac (ol_contrapos RS ssubst) 1);
paulson@2112
    93
by (rewrite_tac NNF_rews);
paulson@2112
    94
by (rtac impI 1);
paulson@2112
    95
by (etac allE 1);
paulson@2112
    96
by (dtac mp 1);
paulson@2112
    97
by (assume_tac 1);
paulson@2112
    98
by (fast_tac HOL_cs 1);
paulson@2112
    99
val minimal_wf = result();
paulson@2112
   100
paulson@2112
   101
val wf_eq_minimal = 
paulson@2112
   102
  standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym);
paulson@2112
   103
paulson@2112
   104
goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection] 
paulson@2112
   105
"wf(R) --> wf(inv_image R (f::'a=>'b))"; 
paulson@2112
   106
by (strip_tac 1);
paulson@2112
   107
by (etac exE 1);
paulson@2112
   108
by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1);
paulson@2112
   109
by (rtac exI 2);
paulson@2112
   110
by (rtac exI 2);
paulson@2112
   111
by (rtac conjI 2);
paulson@2112
   112
by (assume_tac 2);
paulson@2112
   113
by (rtac refl 2);
paulson@2112
   114
paulson@2112
   115
by (etac allE 1);
paulson@2112
   116
by (dtac mp 1);
paulson@2112
   117
by (assume_tac 1);
paulson@2112
   118
by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \
paulson@2112
   119
                \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1);
paulson@2112
   120
by (etac thin_rl 1);
paulson@2112
   121
by (etac thin_rl 1);
paulson@2112
   122
by (rewrite_tac NNF_rews);
paulson@2112
   123
by (rtac impI 1);
paulson@2112
   124
by (etac exE 1);
paulson@2112
   125
by (etac conjE 1);
paulson@2112
   126
by (etac exE 1);
paulson@2112
   127
by (rtac exI 1);
paulson@2112
   128
by (etac conjE 1);
paulson@2112
   129
by (rtac conjI 1);
paulson@2112
   130
by (assume_tac 1);
paulson@2112
   131
by (hyp_subst_tac 1);
paulson@2112
   132
by (rtac allI 1);
paulson@2112
   133
by (rtac impI 1);
paulson@2112
   134
by (etac CollectE 1);
paulson@2112
   135
by (etac allE 1);
paulson@2112
   136
by (dtac mp 1);
paulson@2112
   137
by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]);
paulson@2112
   138
by (assume_tac 1);
paulson@2112
   139
by (fast_tac HOL_cs 1);
paulson@2112
   140
val wf_inv_image = result() RS mp;
paulson@2112
   141
paulson@2112
   142
(* from Nat.ML *)
paulson@2112
   143
goalw WF1.thy [wf_def] "wf(pred_nat)";
paulson@2112
   144
by (strip_tac 1);
paulson@2112
   145
by (nat_ind_tac "x" 1);
paulson@2112
   146
by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
paulson@2112
   147
                             make_elim Suc_inject]) 2);
paulson@2112
   148
by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
paulson@2112
   149
val wf_pred_nat = result();
paulson@2112
   150
paulson@2112
   151
goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)";
paulson@2112
   152
by (strip_tac 1);
paulson@2112
   153
by (List.list.induct_tac "x" 1);
paulson@2112
   154
by (etac allE 1);
paulson@2112
   155
by (etac impE 1);
paulson@2112
   156
by (assume_tac 2);
paulson@2112
   157
by (strip_tac 1);
paulson@2112
   158
by (etac CollectE 1);
paulson@2112
   159
by (asm_full_simp_tac (!simpset) 1);
paulson@2112
   160
paulson@2112
   161
by (etac allE 1);
paulson@2112
   162
by (etac impE 1);
paulson@2112
   163
by (assume_tac 2);
paulson@2112
   164
by (strip_tac 1);
paulson@2112
   165
by (etac CollectE 1);
paulson@2112
   166
by (etac exE 1);
paulson@2112
   167
by (asm_full_simp_tac (!simpset) 1);
paulson@2112
   168
by (etac conjE 1);
paulson@2112
   169
by (hyp_subst_tac 1);
paulson@2112
   170
by (assume_tac 1);
paulson@2112
   171
qed "wf_pred_list";
paulson@2112
   172
paulson@2112
   173
(*----------------------------------------------------------------------------
paulson@2112
   174
 * All measures are wellfounded.
paulson@2112
   175
 *---------------------------------------------------------------------------*)
paulson@2112
   176
paulson@2112
   177
goalw WF1.thy [measure_def] "wf (measure f)";
paulson@2112
   178
by (rtac wf_inv_image 1);
paulson@2112
   179
by (rtac wf_trancl 1);
paulson@2112
   180
by (rtac wf_pred_nat 1);
paulson@2112
   181
qed "wf_measure";
paulson@2112
   182
paulson@2112
   183
(*----------------------------------------------------------------------------
paulson@2112
   184
 * Wellfoundedness of lexicographic combinations
paulson@2112
   185
 *---------------------------------------------------------------------------*)
paulson@2112
   186
paulson@2112
   187
val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)";
paulson@2112
   188
by (cut_facts_tac prems 1);
paulson@2112
   189
by (rtac allI 1);
paulson@2112
   190
by (rtac (surjective_pairing RS ssubst) 1);
paulson@2112
   191
by (fast_tac HOL_cs 1);
paulson@2112
   192
qed "split_all_pair";
paulson@2112
   193
paulson@2112
   194
val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def]
paulson@2112
   195
 "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
paulson@2112
   196
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
paulson@2112
   197
by (rtac (wfa RS spec RS mp) 1);
paulson@2112
   198
by (EVERY1 [rtac allI,rtac impI]);
paulson@2112
   199
by (rtac (wfb RS spec RS mp) 1);
paulson@2112
   200
by (fast_tac (set_cs addSEs [Pair_inject]) 1);
paulson@2112
   201
qed "wf_lex_prod";
paulson@2112
   202
paulson@2112
   203
(*----------------------------------------------------------------------------
paulson@2112
   204
 * Wellfoundedness of relational product
paulson@2112
   205
 *---------------------------------------------------------------------------*)
paulson@2112
   206
val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def]
paulson@2112
   207
 "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
paulson@2112
   208
by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
paulson@2112
   209
by (rtac (wfa RS spec RS mp) 1);
paulson@2112
   210
by (EVERY1 [rtac allI,rtac impI]);
paulson@2112
   211
by (rtac (wfb RS spec RS mp) 1);
paulson@2112
   212
by (fast_tac (set_cs addSEs [Pair_inject]) 1);
paulson@2112
   213
qed "wf_rel_prod";
paulson@2112
   214
paulson@2112
   215
paulson@2112
   216
(*---------------------------------------------------------------------------
paulson@2112
   217
 * Wellfoundedness of subsets
paulson@2112
   218
 *---------------------------------------------------------------------------*)
paulson@2112
   219
paulson@2112
   220
goalw WF1.thy [wf_eq_minimal RS eq_reflection] 
paulson@2112
   221
     "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)";
paulson@2112
   222
by (fast_tac set_cs 1);
paulson@2112
   223
qed "wf_subset";
paulson@2112
   224
paulson@2112
   225
(*---------------------------------------------------------------------------
paulson@2112
   226
 * Wellfoundedness of the empty relation.
paulson@2112
   227
 *---------------------------------------------------------------------------*)
paulson@2112
   228
paulson@2112
   229
goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def] 
paulson@2112
   230
     "wf(emptyr)";
paulson@2112
   231
by (fast_tac set_cs 1);
paulson@2112
   232
qed "wf_emptyr";