removed Isar_examples/Minimal;
authorwenzelm
Thu Jan 20 17:57:59 2000 +0100 (2000-01-20)
changeset 8137fb6fe34060ca
parent 8136 8c65f3ca13f2
child 8138 1e4cb069b19d
removed Isar_examples/Minimal;
src/HOL/IsaMakefile
src/HOL/Isar_examples/Minimal.thy
src/HOL/Isar_examples/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Tue Jan 18 11:33:31 2000 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Jan 20 17:57:59 2000 +0100
     1.3 @@ -420,7 +420,7 @@
     1.4    Isar_examples/Cantor.ML Isar_examples/Cantor.thy \
     1.5    Isar_examples/ExprCompiler.thy Isar_examples/Fibonacci.thy \
     1.6    Isar_examples/Group.thy Isar_examples/KnasterTarski.thy \
     1.7 -  Isar_examples/MultisetOrder.thy Isar_examples/Minimal.thy \
     1.8 +  Isar_examples/MultisetOrder.thy \
     1.9    Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \
    1.10    Isar_examples/Puzzle.thy Isar_examples/Summation.thy \
    1.11    Isar_examples/ROOT.ML Isar_examples/W_correct.thy \
     2.1 --- a/src/HOL/Isar_examples/Minimal.thy	Tue Jan 18 11:33:31 2000 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,49 +0,0 @@
     2.4 -
     2.5 -header {* The mimimality principle *};
     2.6 -
     2.7 -theory Minimal = Main:;
     2.8 -
     2.9 -consts
    2.10 -  rel :: "'a => 'a => bool"  (infixl "<<" 50);
    2.11 -axioms
    2.12 -  induct: "(ALL m. m << n --> P m ==> P n) ==> P n";
    2.13 -
    2.14 -theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)"
    2.15 -  (concl is "Ex ?minimal");
    2.16 -proof -;
    2.17 -  assume "A ~= {}";
    2.18 -  hence "EX n. n:A"; by blast;
    2.19 -  thus ?thesis;
    2.20 -  proof;
    2.21 -    fix n; assume h: "n:A";
    2.22 -    have "n:A --> Ex ?minimal" (is "?P n");
    2.23 -    proof (rule induct [of n]);
    2.24 -      fix m;
    2.25 -      assume hyp: "ALL m. m << n --> ?P m";
    2.26 -      show "?P n";
    2.27 -      proof;
    2.28 -	show "Ex ?minimal";
    2.29 -	proof (rule case_split);
    2.30 -	  assume "EX m. m << n & m:A";
    2.31 -	  with hyp; show ?thesis; by blast;
    2.32 -	next;
    2.33 -	  assume "~ (EX m. m << n & m:A)";
    2.34 -	  with h; have "?minimal n"; by blast;
    2.35 -	  thus ?thesis; ..;
    2.36 -	qed;
    2.37 -      qed;
    2.38 -    qed;
    2.39 -    thus ?thesis; ..;
    2.40 -  qed;
    2.41 -qed;
    2.42 -
    2.43 -text {* \medskip Prefer a short, tactic script-style proof? *};
    2.44 -
    2.45 -theorem "A ~= {} ==> EX n. n:A & (ALL m. m << n --> m ~: A)";
    2.46 -proof -;
    2.47 -  assume "A ~= {}";
    2.48 -  {{; fix n; have "n:A --> ?thesis"; by (rule induct [of n]) blast; }};
    2.49 -  thus ?thesis; by (force! simp add: not_empty);
    2.50 -qed;
    2.51 -
    2.52 -end;
     3.1 --- a/src/HOL/Isar_examples/ROOT.ML	Tue Jan 18 11:33:31 2000 +0100
     3.2 +++ b/src/HOL/Isar_examples/ROOT.ML	Thu Jan 20 17:57:59 2000 +0100
     3.3 @@ -17,4 +17,3 @@
     3.4  with_path "../W0" time_use_thy "W_correct";
     3.5  with_path "../ex" time_use_thy "Fibonacci";
     3.6  time_use_thy "Puzzle";
     3.7 -time_use_thy "Minimal";