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