TFL/WF1.ML
changeset 2112 3902e9af752f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/WF1.ML	Fri Oct 18 12:41:04 1996 +0200
     1.3 @@ -0,0 +1,232 @@
     1.4 +(*  Title: 	HOL/WF.ML
     1.5 +    ID:         $Id$
     1.6 +    Author: 	Konrad Slind
     1.7 +    Copyright   1996  TU Munich
     1.8 +
     1.9 +For WF1.thy.  
    1.10 +*)
    1.11 +
    1.12 +open WF1;
    1.13 +
    1.14 +(* TFL variants *)
    1.15 +goal WF.thy
    1.16 +    "!R. wf R --> (!P. (!x. (!y. (y,x):R --> P y) --> P x) --> (!x. P x))";
    1.17 +by (strip_tac 1);
    1.18 +by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1);
    1.19 +by (assume_tac 1);
    1.20 +by (fast_tac HOL_cs 1);
    1.21 +qed"tfl_wf_induct";
    1.22 +
    1.23 +goal WF.thy "!f R. (x,a):R --> (cut f R a)(x) = f(x)";
    1.24 +by (strip_tac 1);
    1.25 +by (rtac cut_apply 1);
    1.26 +by (assume_tac 1);
    1.27 +qed"tfl_cut_apply";
    1.28 +
    1.29 +goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
    1.30 +by (strip_tac 1);
    1.31 +by (res_inst_tac [("r","R"), ("H","M"),
    1.32 +                  ("a","x"), ("f","f")] (eq_reflection RS def_wfrec) 1);
    1.33 +by (assume_tac 1);
    1.34 +by (assume_tac 1);
    1.35 +qed "tfl_wfrec";
    1.36 +
    1.37 +(*----------------------------------------------------------------------------
    1.38 + * Proof that the inverse image into a wellfounded relation is wellfounded.
    1.39 + * The proof is relatively sloppy - I map to another version of 
    1.40 + * wellfoundedness (every n.e. set has an R-minimal element) and transport 
    1.41 + * the proof for that formulation over. I also didn't remember the existence
    1.42 + *  of "set_cs" so no doubt the proof can be dramatically shortened!
    1.43 + *---------------------------------------------------------------------------*)
    1.44 +goal HOL.thy "(~(!x. P x)) = (? x. ~(P x))";
    1.45 +by (fast_tac HOL_cs 1);
    1.46 +val th1 = result();
    1.47 +
    1.48 +goal HOL.thy "(~(? x. P x)) = (!x. ~(P x))";
    1.49 +by (fast_tac HOL_cs 1);
    1.50 +val th2 = result();
    1.51 +
    1.52 +goal HOL.thy "(~(x-->y)) = (x & (~ y))";
    1.53 +by (fast_tac HOL_cs 1);
    1.54 +val th3 = result();
    1.55 +
    1.56 +goal HOL.thy "((~ x) | y) = (x --> y)";
    1.57 +by (fast_tac HOL_cs 1);
    1.58 +val th4 = result();
    1.59 +
    1.60 +goal HOL.thy "(~(x & y)) = ((~ x) | (~ y))";
    1.61 +by (fast_tac HOL_cs 1);
    1.62 +val th5 = result();
    1.63 +
    1.64 +goal HOL.thy "(~(x | y)) = ((~ x) & (~ y))";
    1.65 +by (fast_tac HOL_cs 1);
    1.66 +val th6 = result();
    1.67 +
    1.68 +goal HOL.thy "(~(~x)) = x";
    1.69 +by (fast_tac HOL_cs 1);
    1.70 +val th7 = result();
    1.71 +
    1.72 +(* Using [th1,th2,th3,th4,th5,th6,th7] as rewrites drives negation inwards. *)
    1.73 +val NNF_rews = map (fn th => th RS eq_reflection)[th1,th2,th3,th4,th5,th6,th7];
    1.74 +
    1.75 +(* The name "contrapos" is already taken. *)
    1.76 +goal HOL.thy "(P --> Q) = ((~ Q) --> (~ P))";
    1.77 +by (fast_tac HOL_cs 1);
    1.78 +val ol_contrapos = result();
    1.79 +
    1.80 +(* Maps to another version of wellfoundedness *)
    1.81 +val [p1] = goalw WF.thy [wf_def]
    1.82 +"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
    1.83 +by (rtac allI 1);
    1.84 +by (rtac (ol_contrapos RS ssubst) 1);
    1.85 +by (rewrite_tac NNF_rews);
    1.86 +by (rtac impI 1);
    1.87 +by (rtac ((p1 RS spec) RS mp) 1);
    1.88 +by (fast_tac HOL_cs 1);
    1.89 +val wf_minimal = result();
    1.90 +
    1.91 +goalw WF.thy [wf_def]
    1.92 +"(!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b)))) --> wf R";
    1.93 +by (rtac impI 1);
    1.94 +by (rtac allI 1);
    1.95 +by (rtac (ol_contrapos RS ssubst) 1);
    1.96 +by (rewrite_tac NNF_rews);
    1.97 +by (rtac impI 1);
    1.98 +by (etac allE 1);
    1.99 +by (dtac mp 1);
   1.100 +by (assume_tac 1);
   1.101 +by (fast_tac HOL_cs 1);
   1.102 +val minimal_wf = result();
   1.103 +
   1.104 +val wf_eq_minimal = 
   1.105 +  standard ((wf_minimal COMP ((minimal_wf RS mp) COMP iffI)) RS sym);
   1.106 +
   1.107 +goalw WF1.thy [inv_image_def,wf_eq_minimal RS eq_reflection] 
   1.108 +"wf(R) --> wf(inv_image R (f::'a=>'b))"; 
   1.109 +by (strip_tac 1);
   1.110 +by (etac exE 1);
   1.111 +by (subgoal_tac "? (w::'b). ? (x::'a). Q x & (f x = w)" 1);
   1.112 +by (rtac exI 2);
   1.113 +by (rtac exI 2);
   1.114 +by (rtac conjI 2);
   1.115 +by (assume_tac 2);
   1.116 +by (rtac refl 2);
   1.117 +
   1.118 +by (etac allE 1);
   1.119 +by (dtac mp 1);
   1.120 +by (assume_tac 1);
   1.121 +by (eres_inst_tac [("P","? min. (? x. Q x & f x = min) & \
   1.122 +                \ (! b. (b, min) : R --> ~ (? x. Q x & f x = b))")] rev_mp 1);
   1.123 +by (etac thin_rl 1);
   1.124 +by (etac thin_rl 1);
   1.125 +by (rewrite_tac NNF_rews);
   1.126 +by (rtac impI 1);
   1.127 +by (etac exE 1);
   1.128 +by (etac conjE 1);
   1.129 +by (etac exE 1);
   1.130 +by (rtac exI 1);
   1.131 +by (etac conjE 1);
   1.132 +by (rtac conjI 1);
   1.133 +by (assume_tac 1);
   1.134 +by (hyp_subst_tac 1);
   1.135 +by (rtac allI 1);
   1.136 +by (rtac impI 1);
   1.137 +by (etac CollectE 1);
   1.138 +by (etac allE 1);
   1.139 +by (dtac mp 1);
   1.140 +by (rewrite_tac[fst_conv RS eq_reflection,snd_conv RS eq_reflection]);
   1.141 +by (assume_tac 1);
   1.142 +by (fast_tac HOL_cs 1);
   1.143 +val wf_inv_image = result() RS mp;
   1.144 +
   1.145 +(* from Nat.ML *)
   1.146 +goalw WF1.thy [wf_def] "wf(pred_nat)";
   1.147 +by (strip_tac 1);
   1.148 +by (nat_ind_tac "x" 1);
   1.149 +by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, 
   1.150 +                             make_elim Suc_inject]) 2);
   1.151 +by (fast_tac (HOL_cs addSEs [mp, pred_natE, Pair_inject, Zero_neq_Suc]) 1);
   1.152 +val wf_pred_nat = result();
   1.153 +
   1.154 +goalw WF1.thy [wf_def,pred_list_def] "wf(pred_list)";
   1.155 +by (strip_tac 1);
   1.156 +by (List.list.induct_tac "x" 1);
   1.157 +by (etac allE 1);
   1.158 +by (etac impE 1);
   1.159 +by (assume_tac 2);
   1.160 +by (strip_tac 1);
   1.161 +by (etac CollectE 1);
   1.162 +by (asm_full_simp_tac (!simpset) 1);
   1.163 +
   1.164 +by (etac allE 1);
   1.165 +by (etac impE 1);
   1.166 +by (assume_tac 2);
   1.167 +by (strip_tac 1);
   1.168 +by (etac CollectE 1);
   1.169 +by (etac exE 1);
   1.170 +by (asm_full_simp_tac (!simpset) 1);
   1.171 +by (etac conjE 1);
   1.172 +by (hyp_subst_tac 1);
   1.173 +by (assume_tac 1);
   1.174 +qed "wf_pred_list";
   1.175 +
   1.176 +(*----------------------------------------------------------------------------
   1.177 + * All measures are wellfounded.
   1.178 + *---------------------------------------------------------------------------*)
   1.179 +
   1.180 +goalw WF1.thy [measure_def] "wf (measure f)";
   1.181 +by (rtac wf_inv_image 1);
   1.182 +by (rtac wf_trancl 1);
   1.183 +by (rtac wf_pred_nat 1);
   1.184 +qed "wf_measure";
   1.185 +
   1.186 +(*----------------------------------------------------------------------------
   1.187 + * Wellfoundedness of lexicographic combinations
   1.188 + *---------------------------------------------------------------------------*)
   1.189 +
   1.190 +val prems = goal Prod.thy "!a b. P((a,b)) ==> !p. P(p)";
   1.191 +by (cut_facts_tac prems 1);
   1.192 +by (rtac allI 1);
   1.193 +by (rtac (surjective_pairing RS ssubst) 1);
   1.194 +by (fast_tac HOL_cs 1);
   1.195 +qed "split_all_pair";
   1.196 +
   1.197 +val [wfa,wfb] = goalw WF1.thy [wf_def,lex_prod_def]
   1.198 + "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
   1.199 +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
   1.200 +by (rtac (wfa RS spec RS mp) 1);
   1.201 +by (EVERY1 [rtac allI,rtac impI]);
   1.202 +by (rtac (wfb RS spec RS mp) 1);
   1.203 +by (fast_tac (set_cs addSEs [Pair_inject]) 1);
   1.204 +qed "wf_lex_prod";
   1.205 +
   1.206 +(*----------------------------------------------------------------------------
   1.207 + * Wellfoundedness of relational product
   1.208 + *---------------------------------------------------------------------------*)
   1.209 +val [wfa,wfb] = goalw WF1.thy [wf_def,rprod_def]
   1.210 + "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
   1.211 +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
   1.212 +by (rtac (wfa RS spec RS mp) 1);
   1.213 +by (EVERY1 [rtac allI,rtac impI]);
   1.214 +by (rtac (wfb RS spec RS mp) 1);
   1.215 +by (fast_tac (set_cs addSEs [Pair_inject]) 1);
   1.216 +qed "wf_rel_prod";
   1.217 +
   1.218 +
   1.219 +(*---------------------------------------------------------------------------
   1.220 + * Wellfoundedness of subsets
   1.221 + *---------------------------------------------------------------------------*)
   1.222 +
   1.223 +goalw WF1.thy [wf_eq_minimal RS eq_reflection] 
   1.224 +     "wf(r) --> (!x y. (x,y):p --> (x,y):r) --> wf(p)";
   1.225 +by (fast_tac set_cs 1);
   1.226 +qed "wf_subset";
   1.227 +
   1.228 +(*---------------------------------------------------------------------------
   1.229 + * Wellfoundedness of the empty relation.
   1.230 + *---------------------------------------------------------------------------*)
   1.231 +
   1.232 +goalw WF1.thy [wf_eq_minimal RS eq_reflection,emptyr_def] 
   1.233 +     "wf(emptyr)";
   1.234 +by (fast_tac set_cs 1);
   1.235 +qed "wf_emptyr";