1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Isar_examples/Minimal.thy	Mon Nov 29 11:21:50 1999 +0100
     1.3 @@ -0,0 +1,49 @@
     1.4 +
     1.5 +header {* The mimimality principle *};
     1.6 +
     1.7 +theory Minimal = Main:;
     1.8 +
     1.9 +consts
    1.10 +  rel :: "'a => 'a => bool"  (infixl "<<" 50);
    1.11 +axioms
    1.12 +  induct: "(ALL m. m << n --> P m ==> P n) ==> P n";
    1.13 +
    1.14 +theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)"
    1.15 +  (concl is "Ex ?minimal");
    1.16 +proof -;
    1.17 +  assume "A ~= {}";
    1.18 +  hence "EX n. n:A"; by blast;
    1.19 +  thus ?thesis;
    1.20 +  proof;
    1.21 +    fix n; assume h: "n:A";
    1.22 +    have "n:A --> Ex ?minimal" (is "?P n");
    1.23 +    proof (rule induct [of n]);
    1.24 +      fix m;
    1.25 +      assume hyp: "ALL m. m << n --> ?P m";
    1.26 +      show "?P n";
    1.27 +      proof;
    1.28 +	show "Ex ?minimal";
    1.29 +	proof (rule case_split);
    1.30 +	  assume "EX m. m << n & m:A";
    1.31 +	  with hyp; show ?thesis; by blast;
    1.32 +	next;
    1.33 +	  assume "~ (EX m. m << n & m:A)";
    1.34 +	  with h; have "?minimal n"; by blast;
    1.35 +	  thus ?thesis; ..;
    1.36 +	qed;
    1.37 +      qed;
    1.38 +    qed;
    1.39 +    thus ?thesis; ..;
    1.40 +  qed;
    1.41 +qed;
    1.42 +
    1.43 +text {* \medskip Prefer a short, tactic script-style proof? *};
    1.44 +
    1.45 +theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)";
    1.46 +proof -;
    1.47 +  assume "A ~= {}";
    1.48 +  {{; fix n; have "n:A --> ?thesis"; by (rule induct [of n]) blast; }};
    1.49 +  thus ?thesis; by (force! simp add: not_empty);
    1.50 +qed;
    1.51 +
    1.52 +end;

     2.1 --- a/src/HOL/Isar_examples/ROOT.ML	Mon Nov 29 11:21:44 1999 +0100
     2.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Mon Nov 29 11:21:50 1999 +0100
     2.3 @@ -16,3 +16,4 @@
     2.4  with_path "../Induct" time_use_thy "MultisetOrder";
     2.5  with_path "../W0" time_use_thy "W_correct";
     2.6  time_use_thy "Puzzle";
     2.7 +time_use_thy "Minimal";