# HG changeset patch # User wenzelm # Date 1149715315 -7200 # Node ID 14de4d05d27524bff74c055daf5d1856e3b791cc # Parent 5c5c1208a3fa53137f7e9bed7f755378f5a9227f removed obsolete ML files; diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Wed Jun 07 16:55:39 2006 +0200 +++ b/src/FOL/IsaMakefile Wed Jun 07 23:21:55 2006 +0200 @@ -45,9 +45,9 @@ $(LOG)/FOL-ex.gz: $(OUT)/FOL$(ML_SUFFIX) ex/First_Order_Logic.thy \ ex/If.thy ex/IffOracle.thy ex/List.ML ex/List.thy ex/LocaleTest.thy \ - ex/Nat.ML ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \ - ex/Prolog.ML ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\ - ex/foundn.ML ex/Intuitionistic.thy ex/intro.ML ex/prop.ML ex/quant.ML + ex/Nat.thy ex/Nat2.ML ex/Nat2.thy ex/Natural_Numbers.thy \ + ex/Prolog.thy ex/ROOT.ML ex/Classical.thy ex/document/root.tex\ + ex/Foundation.thy ex/Intuitionistic.thy ex/Intro.thy ex/prop.ML ex/quant.ML @$(ISATOOL) usedir $(OUT)/FOL ex diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Foundation.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Foundation.thy Wed Jun 07 23:21:55 2006 +0200 @@ -0,0 +1,135 @@ +(* Title: FOL/ex/Foundation.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge +*) + +header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover" + +theory Foundation +imports IFOL +begin + +lemma "A&B --> (C-->A&C)" +apply (rule impI) +apply (rule impI) +apply (rule conjI) +prefer 2 apply assumption +apply (rule conjunct1) +apply assumption +done + +text {*A form of conj-elimination*} +lemma + assumes "A & B" + and "A ==> B ==> C" + shows C +apply (rule prems) +apply (rule conjunct1) +apply (rule prems) +apply (rule conjunct2) +apply (rule prems) +done + +lemma + assumes "!!A. ~ ~A ==> A" + shows "B | ~B" +apply (rule prems) +apply (rule notI) +apply (rule_tac P = "~B" in notE) +apply (rule_tac [2] notI) +apply (rule_tac [2] P = "B | ~B" in notE) +prefer 2 apply assumption +apply (rule_tac [2] disjI1) +prefer 2 apply assumption +apply (rule notI) +apply (rule_tac P = "B | ~B" in notE) +apply assumption +apply (rule disjI2) +apply assumption +done + +lemma + assumes "!!A. ~ ~A ==> A" + shows "B | ~B" +apply (rule prems) +apply (rule notI) +apply (rule notE) +apply (rule_tac [2] notI) +apply (erule_tac [2] notE) +apply (erule_tac [2] disjI1) +apply (rule notI) +apply (erule notE) +apply (erule disjI2) +done + + +lemma + assumes "A | ~A" + and "~ ~A" + shows A +apply (rule disjE) +apply (rule prems) +apply assumption +apply (rule FalseE) +apply (rule_tac P = "~A" in notE) +apply (rule prems) +apply assumption +done + + +subsection "Examples with quantifiers" + +lemma + assumes "ALL z. G(z)" + shows "ALL z. G(z)|H(z)" +apply (rule allI) +apply (rule disjI1) +apply (rule prems [THEN spec]) +done + +lemma "ALL x. EX y. x=y" +apply (rule allI) +apply (rule exI) +apply (rule refl) +done + +lemma "EX y. ALL x. x=y" +apply (rule exI) +apply (rule allI) +apply (rule refl)? +oops + +text {* Parallel lifting example. *} +lemma "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)" +apply (rule exI allI) +apply (rule exI allI) +apply (rule exI allI) +apply (rule exI allI) +apply (rule exI allI) +oops + +lemma + assumes "(EX z. F(z)) & B" + shows "EX z. F(z) & B" +apply (rule conjE) +apply (rule prems) +apply (rule exE) +apply assumption +apply (rule exI) +apply (rule conjI) +apply assumption +apply assumption +done + +text {* A bigger demonstration of quantifiers -- not in the paper. *} +lemma "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))" +apply (rule impI) +apply (rule allI) +apply (rule exE, assumption) +apply (rule exI) +apply (rule allE, assumption) +apply assumption +done + +end diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Intro.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FOL/ex/Intro.thy Wed Jun 07 23:21:55 2006 +0200 @@ -0,0 +1,102 @@ +(* Title: FOL/ex/Intro.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Derives some inference rules, illustrating the use of definitions. +*) + +header {* Examples for the manual ``Introduction to Isabelle'' *} + +theory Intro +imports FOL +begin + +subsubsection {* Some simple backward proofs *} + +lemma mythm: "P|P --> P" +apply (rule impI) +apply (rule disjE) +prefer 3 apply (assumption) +prefer 2 apply (assumption) +apply assumption +done + +lemma "(P & Q) | R --> (P | R)" +apply (rule impI) +apply (erule disjE) +apply (drule conjunct1) +apply (rule disjI1) +apply (rule_tac [2] disjI2) +apply assumption+ +done + +(*Correct version, delaying use of "spec" until last*) +lemma "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))" +apply (rule impI) +apply (rule allI) +apply (rule allI) +apply (drule spec) +apply (drule spec) +apply assumption +done + + +subsubsection {* Demonstration of @{text "fast"} *} + +lemma "(EX y. ALL x. J(y,x) <-> ~J(x,x)) + --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))" +apply fast +done + + +lemma "ALL x. P(x,f(x)) <-> + (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))" +apply fast +done + + +subsubsection {* Derivation of conjunction elimination rule *} + +lemma + assumes major: "P&Q" + and minor: "[| P; Q |] ==> R" + shows R +apply (rule minor) +apply (rule major [THEN conjunct1]) +apply (rule major [THEN conjunct2]) +done + + +subsection {* Derived rules involving definitions *} + +text {* Derivation of negation introduction *} + +lemma + assumes "P ==> False" + shows "~ P" +apply (unfold not_def) +apply (rule impI) +apply (rule prems) +apply assumption +done + +lemma + assumes major: "~P" + and minor: P + shows R +apply (rule FalseE) +apply (rule mp) +apply (rule major [unfolded not_def]) +apply (rule minor) +done + +text {* Alternative proof of the result above *} +lemma + assumes major: "~P" + and minor: P + shows R +apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]]) +done + +end diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Nat.ML --- a/src/FOL/ex/Nat.ML Wed Jun 07 16:55:39 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,64 +0,0 @@ -(* Title: FOL/ex/Nat.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Proofs about the natural numbers. - -To generate similar output to manual, execute these commands: - Pretty.setmargin 72; print_depth 0; -*) - -Goal "Suc(k) ~= k"; -by (res_inst_tac [("n","k")] induct 1); -by (rtac notI 1); -by (etac Suc_neq_0 1); -by (rtac notI 1); -by (etac notE 1); -by (etac Suc_inject 1); -qed "Suc_n_not_n"; - - -Goal "(k+m)+n = k+(m+n)"; -prths ([induct] RL [topthm()]); (*prints all 14 next states!*) -by (rtac induct 1); -back(); -back(); -back(); -back(); -back(); -back(); - -Goalw [add_def] "0+n = n"; -by (rtac rec_0 1); -qed "add_0"; - -Goalw [add_def] "Suc(m)+n = Suc(m+n)"; -by (rtac rec_Suc 1); -qed "add_Suc"; - -Addsimps [add_0, add_Suc]; - -Goal "(k+m)+n = k+(m+n)"; -by (res_inst_tac [("n","k")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_assoc"; - -Goal "m+0 = m"; -by (res_inst_tac [("n","m")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_0_right"; - -Goal "m+Suc(n) = Suc(m+n)"; -by (res_inst_tac [("n","m")] induct 1); -by (ALLGOALS (Asm_simp_tac)); -qed "add_Suc_right"; - -(*Example used in Reference Manual, Doc/Ref/simplifier.tex*) -val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; -by (res_inst_tac [("n","i")] induct 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [prem]) 1); -result(); diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Nat.thy --- a/src/FOL/ex/Nat.thy Wed Jun 07 16:55:39 2006 +0200 +++ b/src/FOL/ex/Nat.thy Wed Jun 07 23:21:55 2006 +0200 @@ -25,8 +25,65 @@ Suc_neq_0: "Suc(m)=0 ==> R" rec_0: "rec(0,a,f) = a" rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))" + +defs add_def: "m+n == rec(m, n, %x y. Suc(y))" -ML {* use_legacy_bindings (the_context ()) *} + +subsection {* Proofs about the natural numbers *} + +lemma Suc_n_not_n: "Suc(k) ~= k" +apply (rule_tac n = k in induct) +apply (rule notI) +apply (erule Suc_neq_0) +apply (rule notI) +apply (erule notE) +apply (erule Suc_inject) +done + +lemma "(k+m)+n = k+(m+n)" +apply (rule induct) +back +back +back +back +back +back +oops + +lemma add_0 [simp]: "0+n = n" +apply (unfold add_def) +apply (rule rec_0) +done + +lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" +apply (unfold add_def) +apply (rule rec_Suc) +done + +lemma add_assoc: "(k+m)+n = k+(m+n)" +apply (rule_tac n = k in induct) +apply simp +apply simp +done + +lemma add_0_right: "m+0 = m" +apply (rule_tac n = m in induct) +apply simp +apply simp +done + +lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" +apply (rule_tac n = m in induct) +apply simp_all +done + +lemma + assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" + shows "f(i+j) = i+f(j)" +apply (rule_tac n = i in induct) +apply simp +apply (simp add: prem) +done end diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/NatClass.ML --- a/src/FOL/ex/NatClass.ML Wed Jun 07 16:55:39 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,59 +0,0 @@ -(* Title: FOL/ex/NatClass.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -This is Nat.ML trivially modified to make it work with NatClass.thy. -*) - -Goal "Suc(k) ~= (k::'a::nat)"; -by (res_inst_tac [("n","k")] induct 1); -by (rtac notI 1); -by (etac Suc_neq_0 1); -by (rtac notI 1); -by (etac notE 1); -by (etac Suc_inject 1); -qed "Suc_n_not_n"; - - -Goal "(k+m)+n = k+(m+n)"; -prths ([induct] RL [topthm()]); (*prints all 14 next states!*) -by (rtac induct 1); -back(); -back(); -back(); -back(); -back(); -back(); - -Goalw [add_def] "0+n = n"; -by (rtac rec_0 1); -qed "add_0"; - -Goalw [add_def] "Suc(m)+n = Suc(m+n)"; -by (rtac rec_Suc 1); -qed "add_Suc"; - -Addsimps [add_0, add_Suc]; - -Goal "(k+m)+n = k+(m+n)"; -by (res_inst_tac [("n","k")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_assoc"; - -Goal "m+0 = m"; -by (res_inst_tac [("n","m")] induct 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "add_0_right"; - -Goal "m+Suc(n) = Suc(m+n)"; -by (res_inst_tac [("n","m")] induct 1); -by (ALLGOALS (Asm_simp_tac)); -qed "add_Suc_right"; - -val [prem] = goal (the_context ()) "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; -by (res_inst_tac [("n","i")] induct 1); -by (Simp_tac 1); -by (asm_simp_tac (simpset() addsimps [prem]) 1); -result(); diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/NatClass.thy --- a/src/FOL/ex/NatClass.thy Wed Jun 07 16:55:39 2006 +0200 +++ b/src/FOL/ex/NatClass.thy Wed Jun 07 23:21:55 2006 +0200 @@ -29,11 +29,62 @@ rec_0: "rec(0, a, f) = a" rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))" -constdefs +definition add :: "['a::nat, 'a] => 'a" (infixl "+" 60) - "m + n == rec(m, n, %x y. Suc(y))" + "m + n = rec(m, n, %x y. Suc(y))" + +lemma Suc_n_not_n: "Suc(k) ~= (k::'a::nat)" +apply (rule_tac n = k in induct) +apply (rule notI) +apply (erule Suc_neq_0) +apply (rule notI) +apply (erule notE) +apply (erule Suc_inject) +done + +lemma "(k+m)+n = k+(m+n)" +apply (rule induct) +back +back +back +back +back +back +oops + +lemma add_0 [simp]: "0+n = n" +apply (unfold add_def) +apply (rule rec_0) +done -ML {* use_legacy_bindings (the_context ()) *} -ML {* open nat_class *} +lemma add_Suc [simp]: "Suc(m)+n = Suc(m+n)" +apply (unfold add_def) +apply (rule rec_Suc) +done + +lemma add_assoc: "(k+m)+n = k+(m+n)" +apply (rule_tac n = k in induct) +apply simp +apply simp +done + +lemma add_0_right: "m+0 = m" +apply (rule_tac n = m in induct) +apply simp +apply simp +done + +lemma add_Suc_right: "m+Suc(n) = Suc(m+n)" +apply (rule_tac n = m in induct) +apply simp_all +done + +lemma + assumes prem: "!!n. f(Suc(n)) = Suc(f(n))" + shows "f(i+j) = i+f(j)" +apply (rule_tac n = i in induct) +apply simp +apply (simp add: prem) +done end diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Prolog.ML --- a/src/FOL/ex/Prolog.ML Wed Jun 07 16:55:39 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: FOL/ex/prolog.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge -*) - -Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; -by (resolve_tac [appNil,appCons] 1); -by (resolve_tac [appNil,appCons] 1); -by (resolve_tac [appNil,appCons] 1); -by (resolve_tac [appNil,appCons] 1); -prth (result()); - -Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; -by (REPEAT (resolve_tac [appNil,appCons] 1)); -result(); - - -Goal "app(?x, ?y, a:b:c:d:Nil)"; -by (REPEAT (resolve_tac [appNil,appCons] 1)); -back(); -back(); -back(); -back(); -result(); - - -(*app([x1,...,xn], y, ?z) requires (n+1) inferences*) -(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) - -Goal "rev(a:b:c:d:Nil, ?x)"; -val rules = [appNil,appCons,revNil,revCons]; -by (REPEAT (resolve_tac rules 1)); -result(); - -Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; -by (REPEAT (resolve_tac rules 1)); -result(); - -Goal "rev(?x, a:b:c:Nil)"; -by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*) -back(); -back(); - -(*backtracking version*) -val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac rules 1); - -choplev 0; -by prolog_tac; -result(); - -Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; -by prolog_tac; -result(); - -(*rev([a..p], ?w) requires 153 inferences *) -Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)"; -by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); -(*Poly/ML: 4 secs >> 38 lips*) -result(); - -(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences; - total inferences = 2 + 1 + 17 + 561 = 581*) -Goal - "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"; -by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1)); -(*Poly/ML: 29 secs >> 20 lips*) -result(); diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/Prolog.thy --- a/src/FOL/ex/Prolog.thy Wed Jun 07 16:55:39 2006 +0200 +++ b/src/FOL/ex/Prolog.thy Wed Jun 07 23:21:55 2006 +0200 @@ -23,6 +23,66 @@ revNil: "rev(Nil,Nil)" revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)" -ML {* use_legacy_bindings (the_context ()) *} +lemma "app(a:b:c:Nil, d:e:Nil, ?x)" +apply (rule appNil appCons) +apply (rule appNil appCons) +apply (rule appNil appCons) +apply (rule appNil appCons) +done + +lemma "app(?x, c:d:Nil, a:b:c:d:Nil)" +apply (rule appNil appCons)+ +done + +lemma "app(?x, ?y, a:b:c:d:Nil)" +apply (rule appNil appCons)+ +back +back +back +back +done + +(*app([x1,...,xn], y, ?z) requires (n+1) inferences*) +(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*) + +lemmas rules = appNil appCons revNil revCons + +lemma "rev(a:b:c:d:Nil, ?x)" +apply (rule rules)+ +done + +lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)" +apply (rule rules)+ +done + +lemma "rev(?x, a:b:c:Nil)" +apply (rule rules)+ -- {* does not solve it directly! *} +back +back +done + +(*backtracking version*) +ML {* +val prolog_tac = DEPTH_FIRST (has_fewer_prems 1) (resolve_tac (thms "rules") 1) +*} + +lemma "rev(?x, a:b:c:Nil)" +apply (tactic prolog_tac) +done + +lemma "rev(a:?x:c:?y:Nil, d:?z:b:?u)" +apply (tactic prolog_tac) +done + +(*rev([a..p], ?w) requires 153 inferences *) +lemma "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)" +apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *}) +done + +(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences + total inferences = 2 + 1 + 17 + 561 = 581*) +lemma "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)" +apply (tactic {* DEPTH_SOLVE (resolve_tac ([refl, conjI] @ thms "rules") 1) *}) +done end diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/ROOT.ML --- a/src/FOL/ex/ROOT.ML Wed Jun 07 16:55:39 2006 +0200 +++ b/src/FOL/ex/ROOT.ML Wed Jun 07 23:21:55 2006 +0200 @@ -8,12 +8,11 @@ time_use_thy "First_Order_Logic"; time_use_thy "Natural_Numbers"; -time_use "intro.ML"; +time_use_thy "Intro"; time_use_thy "Nat"; -time_use "foundn.ML"; +time_use_thy "Foundation"; time_use_thy "Prolog"; -writeln"\n** Intuitionistic examples **\n"; time_use_thy "Intuitionistic"; val thy = IFOL.thy and tac = IntPr.fast_tac 1; @@ -35,7 +34,6 @@ time_use_thy "Nat2"; time_use_thy "List"; -writeln"\n** How to declare an oracle **\n"; time_use_thy "IffOracle"; (*regression test for locales -- sets several global flags!*) diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/foundn.ML --- a/src/FOL/ex/foundn.ML Wed Jun 07 16:55:39 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,129 +0,0 @@ -(* Title: FOL/ex/foundn.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1991 University of Cambridge - -Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover -*) - -goal IFOL.thy "A&B --> (C-->A&C)"; -by (rtac impI 1); -by (rtac impI 1); -by (rtac conjI 1); -by (assume_tac 2); -by (rtac conjunct1 1); -by (assume_tac 1); -result(); - -(*A form of conj-elimination*) -val prems = -goal IFOL.thy "A&B ==> ([| A; B |] ==> C) ==> C"; -by (resolve_tac prems 1); -by (rtac conjunct1 1); -by (resolve_tac prems 1); -by (rtac conjunct2 1); -by (resolve_tac prems 1); -result(); - - -val prems = -goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B"; -by (resolve_tac prems 1); -by (rtac notI 1); -by (res_inst_tac [ ("P", "~B") ] notE 1); -by (rtac notI 2); -by (res_inst_tac [ ("P", "B | ~B") ] notE 2); -by (assume_tac 2); -by (rtac disjI1 2); -by (assume_tac 2); -by (rtac notI 1); -by (res_inst_tac [ ("P", "B | ~B") ] notE 1); -by (assume_tac 1); -by (rtac disjI2 1); -by (assume_tac 1); -result(); - - -val prems = -goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B"; -by (resolve_tac prems 1); -by (rtac notI 1); -by (rtac notE 1); -by (rtac notI 2); -by (etac notE 2); -by (etac disjI1 2); -by (rtac notI 1); -by (etac notE 1); -by (etac disjI2 1); -result(); - - -val prems = -goal IFOL.thy "[| A | ~A; ~ ~A |] ==> A"; -by (rtac disjE 1); -by (resolve_tac prems 1); -by (assume_tac 1); -by (rtac FalseE 1); -by (res_inst_tac [ ("P", "~A") ] notE 1); -by (resolve_tac prems 1); -by (assume_tac 1); -result(); - - -writeln"Examples with quantifiers"; - -val prems = -goal IFOL.thy "ALL z. G(z) ==> ALL z. G(z)|H(z)"; -by (rtac allI 1); -by (rtac disjI1 1); -by (resolve_tac (prems RL [spec]) 1); - (*can use instead - by (rtac spec 1); by (resolve_tac prems 1); *) -result(); - - -goal IFOL.thy "ALL x. EX y. x=y"; -by (rtac allI 1); -by (rtac exI 1); -by (rtac refl 1); -result(); - - -goal IFOL.thy "EX y. ALL x. x=y"; -by (rtac exI 1); -by (rtac allI 1); -by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected"; -getgoal 1; - - -(*Parallel lifting example. *) -goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; -by (resolve_tac [exI, allI] 1); -by (resolve_tac [exI, allI] 1); -by (resolve_tac [exI, allI] 1); -by (resolve_tac [exI, allI] 1); -by (resolve_tac [exI, allI] 1); - - -val prems = -goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)"; -by (rtac conjE 1); -by (resolve_tac prems 1); -by (rtac exE 1); -by (assume_tac 1); -by (rtac exI 1); -by (rtac conjI 1); -by (assume_tac 1); -by (assume_tac 1); -result(); - - -(*A bigger demonstration of quantifiers -- not in the paper*) -goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; -by (rtac impI 1); -by (rtac allI 1); -by (rtac exE 1 THEN assume_tac 1); -by (rtac exI 1); -by (rtac allE 1 THEN assume_tac 1); -by (assume_tac 1); -result(); diff -r 5c5c1208a3fa -r 14de4d05d275 src/FOL/ex/intro.ML --- a/src/FOL/ex/intro.ML Wed Jun 07 16:55:39 2006 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -(* Title: FOL/ex/intro - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1992 University of Cambridge - -Examples for the manual "Introduction to Isabelle" - -Derives some inference rules, illustrating the use of definitions - -To generate similar output to manual, execute these commands: - Pretty.setmargin 72; print_depth 0; -*) - - -context FOL.thy; - -(**** Some simple backward proofs ****) - -Goal "P|P --> P"; -by (rtac impI 1); -by (rtac disjE 1); -by (assume_tac 3); -by (assume_tac 2); -by (assume_tac 1); -qed "mythm"; - -Goal "(P & Q) | R --> (P | R)"; -by (rtac impI 1); -by (etac disjE 1); -by (dtac conjunct1 1); -by (rtac disjI1 1); -by (rtac disjI2 2); -by (REPEAT (assume_tac 1)); -result(); - -(*Correct version, delaying use of "spec" until last*) -Goal "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"; -by (rtac impI 1); -by (rtac allI 1); -by (rtac allI 1); -by (dtac spec 1); -by (dtac spec 1); -by (assume_tac 1); -result(); - - -(**** Demonstration of Fast_tac ****) - -Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ -\ --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; -by (Fast_tac 1); -result(); - -Goal "ALL x. P(x,f(x)) <-> \ -\ (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; -by (Fast_tac 1); -result(); - - -(**** Derivation of conjunction elimination rule ****) - -val [major,minor] = Goal "[| P&Q; [| P; Q |] ==> R |] ==> R"; -by (rtac minor 1); -by (resolve_tac [major RS conjunct1] 1); -by (resolve_tac [major RS conjunct2] 1); -prth (topthm()); -result(); - - -(**** Derived rules involving definitions ****) - -(** Derivation of negation introduction **) - -val prems = Goal "(P ==> False) ==> ~P"; -by (rewtac not_def); -by (rtac impI 1); -by (resolve_tac prems 1); -by (assume_tac 1); -result(); - -val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; -by (rtac FalseE 1); -by (rtac mp 1); -by (resolve_tac [rewrite_rule [not_def] major] 1); -by (rtac minor 1); -result(); - -(*Alternative proof of the result above*) -val [major,minor] = goalw FOL.thy [not_def] - "[| ~P; P |] ==> R"; -by (resolve_tac [minor RS (major RS mp RS FalseE)] 1); -result(); - -writeln"Reached end of file.";