--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/WF_Rel.ML Thu May 15 12:45:42 1997 +0200
@@ -0,0 +1,119 @@
+(* Title: HOL/WF_Rel
+ ID: $Id$
+ Author: Konrad Slind
+ Copyright 1996 TU Munich
+
+Derived wellfounded relations: inverse image, relational product, measure, ...
+*)
+
+open WF_Rel;
+
+
+(*----------------------------------------------------------------------------
+ * The inverse image into a wellfounded relation is wellfounded.
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))";
+by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
+by (Step_tac 1);
+by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
+by (blast_tac (!claset delrules [allE]) 2);
+by (etac allE 1);
+by (mp_tac 1);
+by (Blast_tac 1);
+qed "wf_inv_image";
+AddSIs [wf_inv_image];
+
+(*----------------------------------------------------------------------------
+ * All measures are wellfounded.
+ *---------------------------------------------------------------------------*)
+
+goalw thy [measure_def] "wf (measure f)";
+by (rtac wf_inv_image 1);
+by (rtac wf_trancl 1);
+by (rtac wf_pred_nat 1);
+qed "wf_measure";
+AddIffs [wf_measure];
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of lexicographic combinations
+ *---------------------------------------------------------------------------*)
+
+goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)";
+by (rtac allI 1);
+by (rtac (surjective_pairing RS ssubst) 1);
+by (Blast_tac 1);
+qed "split_all_pair";
+
+val [wfa,wfb] = goalw thy [wf_def,lex_prod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(ra**rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (Blast_tac 1);
+qed "wf_lex_prod";
+AddSIs [wf_lex_prod];
+
+(*----------------------------------------------------------------------------
+ * Wellfoundedness of relational product
+ *---------------------------------------------------------------------------*)
+val [wfa,wfb] = goalw thy [wf_def,rprod_def]
+ "[| wf(ra); wf(rb) |] ==> wf(rprod ra rb)";
+by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]);
+by (rtac (wfa RS spec RS mp) 1);
+by (EVERY1 [rtac allI,rtac impI]);
+by (rtac (wfb RS spec RS mp) 1);
+by (Blast_tac 1);
+qed "wf_rel_prod";
+AddSIs [wf_rel_prod];
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of subsets
+ *---------------------------------------------------------------------------*)
+
+goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)";
+by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by (Fast_tac 1);
+qed "wf_subset";
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of the empty relation.
+ *---------------------------------------------------------------------------*)
+
+goal thy "wf({})";
+by (simp_tac (!simpset addsimps [wf_def]) 1);
+qed "wf_empty";
+AddSIs [wf_empty];
+
+
+(*---------------------------------------------------------------------------
+ * Transitivity of WF combinators.
+ *---------------------------------------------------------------------------*)
+goalw thy [trans_def, lex_prod_def]
+ "!!R1 R2. [| trans R1; trans R2 |] ==> trans (R1 ** R2)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_lex_prod";
+AddSIs [trans_lex_prod];
+
+goalw thy [trans_def, rprod_def]
+ "!!R1 R2. [| trans R1; trans R2 |] ==> trans (rprod R1 R2)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "trans_rprod";
+AddSIs [trans_rprod];
+
+
+(*---------------------------------------------------------------------------
+ * Wellfoundedness of proper subset on finite sets.
+ *---------------------------------------------------------------------------*)
+goalw thy [finite_psubset_def] "wf(finite_psubset)";
+by (rtac (wf_measure RS wf_subset) 1);
+by (simp_tac (!simpset addsimps[measure_def, inv_image_def,
+ symmetric less_def])1);
+by (fast_tac (!claset addIs [psubset_card]) 1);
+qed "wf_finite_psubset";
+
+