eliminated some legacy ML files;
authorwenzelm
Sun Jan 27 20:04:32 2008 +0100 (2008-01-27 ago)
changeset 2599131b38a39e589
parent 25990 d98da4a40a79
child 25992 928594f50893
eliminated some legacy ML files;
src/FOLP/IsaMakefile
src/FOLP/ex/Foundation.thy
src/FOLP/ex/If.ML
src/FOLP/ex/If.thy
src/FOLP/ex/Intro.thy
src/FOLP/ex/Nat.ML
src/FOLP/ex/Nat.thy
src/FOLP/ex/ROOT.ML
src/FOLP/ex/foundn.ML
src/FOLP/ex/intro.ML
src/FOLP/ex/prop.ML
     1.1 --- a/src/FOLP/IsaMakefile	Sun Jan 27 20:04:31 2008 +0100
     1.2 +++ b/src/FOLP/IsaMakefile	Sun Jan 27 20:04:32 2008 +0100
     1.3 @@ -35,8 +35,8 @@
     1.4  
     1.5  FOLP-ex: FOLP $(LOG)/FOLP-ex.gz
     1.6  
     1.7 -$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/foundn.ML \
     1.8 -  ex/If.ML ex/If.thy ex/int.ML ex/intro.ML ex/Nat.ML ex/Nat.thy \
     1.9 +$(LOG)/FOLP-ex.gz: $(OUT)/FOLP ex/ROOT.ML ex/cla.ML ex/Foundation.thy \
    1.10 +  ex/If.thy ex/int.ML ex/Intro.thy ex/Nat.thy \
    1.11    ex/Prolog.ML ex/Prolog.thy ex/prop.ML ex/quant.ML
    1.12  	@$(ISATOOL) usedir $(OUT)/FOLP ex
    1.13  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/FOLP/ex/Foundation.thy	Sun Jan 27 20:04:32 2008 +0100
     2.3 @@ -0,0 +1,135 @@
     2.4 +(*  Title:      FOLP/ex/Foundation.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1991  University of Cambridge
     2.8 +*)
     2.9 +
    2.10 +header "Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover"
    2.11 +
    2.12 +theory Foundation
    2.13 +imports IFOLP
    2.14 +begin
    2.15 +
    2.16 +lemma "?p : A&B  --> (C-->A&C)"
    2.17 +apply (rule impI)
    2.18 +apply (rule impI)
    2.19 +apply (rule conjI)
    2.20 +prefer 2 apply assumption
    2.21 +apply (rule conjunct1)
    2.22 +apply assumption
    2.23 +done
    2.24 +
    2.25 +text {*A form of conj-elimination*}
    2.26 +lemma
    2.27 +  assumes "p : A & B"
    2.28 +    and "!!x y. x : A ==> y : B ==> f(x, y) : C"
    2.29 +  shows "?p : C"
    2.30 +apply (rule prems)
    2.31 +apply (rule conjunct1)
    2.32 +apply (rule prems)
    2.33 +apply (rule conjunct2)
    2.34 +apply (rule prems)
    2.35 +done
    2.36 +
    2.37 +lemma
    2.38 +  assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    2.39 +  shows "?p : B | ~B"
    2.40 +apply (rule prems)
    2.41 +apply (rule notI)
    2.42 +apply (rule_tac P = "~B" in notE)
    2.43 +apply (rule_tac [2] notI)
    2.44 +apply (rule_tac [2] P = "B | ~B" in notE)
    2.45 +prefer 2 apply assumption
    2.46 +apply (rule_tac [2] disjI1)
    2.47 +prefer 2 apply assumption
    2.48 +apply (rule notI)
    2.49 +apply (rule_tac P = "B | ~B" in notE)
    2.50 +apply assumption
    2.51 +apply (rule disjI2)
    2.52 +apply assumption
    2.53 +done
    2.54 +
    2.55 +lemma
    2.56 +  assumes "!!A x. x : ~ ~A ==> cla(x) : A"
    2.57 +  shows "?p : B | ~B"
    2.58 +apply (rule prems)
    2.59 +apply (rule notI)
    2.60 +apply (rule notE)
    2.61 +apply (rule_tac [2] notI)
    2.62 +apply (erule_tac [2] notE)
    2.63 +apply (erule_tac [2] disjI1)
    2.64 +apply (rule notI)
    2.65 +apply (erule notE)
    2.66 +apply (erule disjI2)
    2.67 +done
    2.68 +
    2.69 +
    2.70 +lemma
    2.71 +  assumes "p : A | ~A"
    2.72 +    and "q : ~ ~A"
    2.73 +  shows "?p : A"
    2.74 +apply (rule disjE)
    2.75 +apply (rule prems)
    2.76 +apply assumption
    2.77 +apply (rule FalseE)
    2.78 +apply (rule_tac P = "~A" in notE)
    2.79 +apply (rule prems)
    2.80 +apply assumption
    2.81 +done
    2.82 +
    2.83 +
    2.84 +subsection "Examples with quantifiers"
    2.85 +
    2.86 +lemma
    2.87 +  assumes "p : ALL z. G(z)"
    2.88 +  shows "?p : ALL z. G(z)|H(z)"
    2.89 +apply (rule allI)
    2.90 +apply (rule disjI1)
    2.91 +apply (rule prems [THEN spec])
    2.92 +done
    2.93 +
    2.94 +lemma "?p : ALL x. EX y. x=y"
    2.95 +apply (rule allI)
    2.96 +apply (rule exI)
    2.97 +apply (rule refl)
    2.98 +done
    2.99 +
   2.100 +lemma "?p : EX y. ALL x. x=y"
   2.101 +apply (rule exI)
   2.102 +apply (rule allI)
   2.103 +apply (rule refl)?
   2.104 +oops
   2.105 +
   2.106 +text {* Parallel lifting example. *}
   2.107 +lemma "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
   2.108 +apply (rule exI allI)
   2.109 +apply (rule exI allI)
   2.110 +apply (rule exI allI)
   2.111 +apply (rule exI allI)
   2.112 +apply (rule exI allI)
   2.113 +oops
   2.114 +
   2.115 +lemma
   2.116 +  assumes "p : (EX z. F(z)) & B"
   2.117 +  shows "?p : EX z. F(z) & B"
   2.118 +apply (rule conjE)
   2.119 +apply (rule prems)
   2.120 +apply (rule exE)
   2.121 +apply assumption
   2.122 +apply (rule exI)
   2.123 +apply (rule conjI)
   2.124 +apply assumption
   2.125 +apply assumption
   2.126 +done
   2.127 +
   2.128 +text {* A bigger demonstration of quantifiers -- not in the paper. *}
   2.129 +lemma "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
   2.130 +apply (rule impI)
   2.131 +apply (rule allI)
   2.132 +apply (rule exE, assumption)
   2.133 +apply (rule exI)
   2.134 +apply (rule allE, assumption)
   2.135 +apply assumption
   2.136 +done
   2.137 +
   2.138 +end
     3.1 --- a/src/FOLP/ex/If.ML	Sun Jan 27 20:04:31 2008 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,36 +0,0 @@
     3.4 -(*  Title:      FOLP/ex/If.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 -    Copyright   1991  University of Cambridge
     3.8 -*)
     3.9 -
    3.10 -val prems = goalw (the_context ()) [if_def]
    3.11 -    "[| !!x. x:P ==> f(x):Q; !!x. x:~P ==> g(x):R |] ==> ?p:if(P,Q,R)";
    3.12 -by (fast_tac (FOLP_cs addIs prems) 1);
    3.13 -val ifI = result();
    3.14 -
    3.15 -val major::prems = goalw (the_context ()) [if_def]
    3.16 -   "[| p:if(P,Q,R);  !!x y.[| x:P; y:Q |] ==> f(x,y):S; \
    3.17 -\                    !!x y.[| x:~P; y:R |] ==> g(x,y):S |] ==> ?p:S";
    3.18 -by (cut_facts_tac [major] 1);
    3.19 -by (fast_tac (FOLP_cs addIs prems) 1);
    3.20 -val ifE = result();
    3.21 -
    3.22 -
    3.23 -Goal
    3.24 -    "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
    3.25 -by (rtac iffI 1);
    3.26 -by (etac ifE 1);
    3.27 -by (etac ifE 1);
    3.28 -by (rtac ifI 1);
    3.29 -by (rtac ifI 1);
    3.30 -
    3.31 -choplev 0;
    3.32 -val if_cs = FOLP_cs addSIs [ifI] addSEs[ifE];
    3.33 -by (fast_tac if_cs 1);
    3.34 -val if_commute = result();
    3.35 -
    3.36 -
    3.37 -Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
    3.38 -by (fast_tac if_cs 1);
    3.39 -val nested_ifs = result();
     4.1 --- a/src/FOLP/ex/If.thy	Sun Jan 27 20:04:31 2008 +0100
     4.2 +++ b/src/FOLP/ex/If.thy	Sun Jan 27 20:04:32 2008 +0100
     4.3 @@ -8,6 +8,39 @@
     4.4    "if" :: "[o,o,o]=>o"
     4.5    "if(P,Q,R) == P&Q | ~P&R"
     4.6  
     4.7 -ML {* use_legacy_bindings (the_context ()) *}
     4.8 +lemma ifI:
     4.9 +  assumes "!!x. x : P ==> f(x) : Q"  "!!x. x : ~P ==> g(x) : R"
    4.10 +  shows "?p : if(P,Q,R)"
    4.11 +apply (unfold if_def)
    4.12 +apply (tactic {* fast_tac (FOLP_cs addIs @{thms assms}) 1 *})
    4.13 +done
    4.14 +
    4.15 +lemma ifE:
    4.16 +  assumes 1: "p : if(P,Q,R)" and
    4.17 +    2: "!!x y. [| x : P; y : Q |] ==> f(x, y) : S" and
    4.18 +    3: "!!x y. [| x : ~P; y : R |] ==> g(x, y) : S"
    4.19 +  shows "?p : S"
    4.20 +apply (insert 1)
    4.21 +apply (unfold if_def)
    4.22 +apply (tactic {* fast_tac (FOLP_cs addIs [@{thm 2}, @{thm 3}]) 1 *})
    4.23 +done
    4.24 +
    4.25 +lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    4.26 +apply (rule iffI)
    4.27 +apply (erule ifE)
    4.28 +apply (erule ifE)
    4.29 +apply (rule ifI)
    4.30 +apply (rule ifI)
    4.31 +oops
    4.32 +
    4.33 +ML {* val if_cs = FOLP_cs addSIs [@{thm ifI}] addSEs [@{thm ifE}] *}
    4.34 +
    4.35 +lemma if_commute: "?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
    4.36 +apply (tactic {* fast_tac if_cs 1 *})
    4.37 +done
    4.38 +
    4.39 +lemma nested_ifs: "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
    4.40 +apply (tactic {* fast_tac if_cs 1 *})
    4.41 +done
    4.42  
    4.43  end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/FOLP/ex/Intro.thy	Sun Jan 27 20:04:32 2008 +0100
     5.3 @@ -0,0 +1,102 @@
     5.4 +(*  Title:      FOLP/ex/Intro.thy
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1992  University of Cambridge
     5.8 +
     5.9 +Derives some inference rules, illustrating the use of definitions.
    5.10 +*)
    5.11 +
    5.12 +header {* Examples for the manual ``Introduction to Isabelle'' *}
    5.13 +
    5.14 +theory Intro
    5.15 +imports FOLP
    5.16 +begin
    5.17 +
    5.18 +subsubsection {* Some simple backward proofs *}
    5.19 +
    5.20 +lemma mythm: "?p : P|P --> P"
    5.21 +apply (rule impI)
    5.22 +apply (rule disjE)
    5.23 +prefer 3 apply (assumption)
    5.24 +prefer 2 apply (assumption)
    5.25 +apply assumption
    5.26 +done
    5.27 +
    5.28 +lemma "?p : (P & Q) | R --> (P | R)"
    5.29 +apply (rule impI)
    5.30 +apply (erule disjE)
    5.31 +apply (drule conjunct1)
    5.32 +apply (rule disjI1)
    5.33 +apply (rule_tac [2] disjI2)
    5.34 +apply assumption+
    5.35 +done
    5.36 +
    5.37 +(*Correct version, delaying use of "spec" until last*)
    5.38 +lemma "?p : (ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
    5.39 +apply (rule impI)
    5.40 +apply (rule allI)
    5.41 +apply (rule allI)
    5.42 +apply (drule spec)
    5.43 +apply (drule spec)
    5.44 +apply assumption
    5.45 +done
    5.46 +
    5.47 +
    5.48 +subsubsection {* Demonstration of @{text "fast"} *}
    5.49 +
    5.50 +lemma "?p : (EX y. ALL x. J(y,x) <-> ~J(x,x))
    5.51 +        -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
    5.52 +apply (tactic {* fast_tac FOLP_cs 1 *})
    5.53 +done
    5.54 +
    5.55 +
    5.56 +lemma "?p : ALL x. P(x,f(x)) <->
    5.57 +        (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
    5.58 +apply (tactic {* fast_tac FOLP_cs 1 *})
    5.59 +done
    5.60 +
    5.61 +
    5.62 +subsubsection {* Derivation of conjunction elimination rule *}
    5.63 +
    5.64 +lemma
    5.65 +  assumes major: "p : P&Q"
    5.66 +    and minor: "!!x y. [| x : P; y : Q |] ==> f(x, y) : R"
    5.67 +  shows "?p : R"
    5.68 +apply (rule minor)
    5.69 +apply (rule major [THEN conjunct1])
    5.70 +apply (rule major [THEN conjunct2])
    5.71 +done
    5.72 +
    5.73 +
    5.74 +subsection {* Derived rules involving definitions *}
    5.75 +
    5.76 +text {* Derivation of negation introduction *}
    5.77 +
    5.78 +lemma
    5.79 +  assumes "!!x. x : P ==> f(x) : False"
    5.80 +  shows "?p : ~ P"
    5.81 +apply (unfold not_def)
    5.82 +apply (rule impI)
    5.83 +apply (rule prems)
    5.84 +apply assumption
    5.85 +done
    5.86 +
    5.87 +lemma
    5.88 +  assumes major: "p : ~P"
    5.89 +    and minor: "q : P"
    5.90 +  shows "?p : R"
    5.91 +apply (rule FalseE)
    5.92 +apply (rule mp)
    5.93 +apply (rule major [unfolded not_def])
    5.94 +apply (rule minor)
    5.95 +done
    5.96 +
    5.97 +text {* Alternative proof of the result above *}
    5.98 +lemma
    5.99 +  assumes major: "p : ~P"
   5.100 +    and minor: "q : P"
   5.101 +  shows "?p : R"
   5.102 +apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
   5.103 +done
   5.104 +
   5.105 +end
     6.1 --- a/src/FOLP/ex/Nat.ML	Sun Jan 27 20:04:31 2008 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,72 +0,0 @@
     6.4 -(*  Title:      FOLP/ex/Nat.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1992  University of Cambridge
     6.8 -*)
     6.9 -
    6.10 -Goal "?p : ~ (Suc(k) = k)";
    6.11 -by (res_inst_tac [("n","k")] induct 1);
    6.12 -by (rtac notI 1);
    6.13 -by (etac Suc_neq_0 1);
    6.14 -by (rtac notI 1);
    6.15 -by (etac notE 1);
    6.16 -by (etac Suc_inject 1);
    6.17 -val Suc_n_not_n = result();
    6.18 -
    6.19 -
    6.20 -Goal "?p : (k+m)+n = k+(m+n)";
    6.21 -prths ([induct] RL [topthm()]);  (*prints all 14 next states!*)
    6.22 -by (rtac induct 1);
    6.23 -back();
    6.24 -back();
    6.25 -back();
    6.26 -back();
    6.27 -back();
    6.28 -back();
    6.29 -
    6.30 -Goalw [add_def] "?p : 0+n = n";
    6.31 -by (rtac rec_0 1);
    6.32 -val add_0 = result();
    6.33 -
    6.34 -Goalw [add_def] "?p : Suc(m)+n = Suc(m+n)";
    6.35 -by (rtac rec_Suc 1);
    6.36 -val add_Suc = result();
    6.37 -
    6.38 -(*
    6.39 -val nat_congs = mk_congs (the_context ()) ["Suc", "op +"];
    6.40 -prths nat_congs;
    6.41 -*)
    6.42 -val prems = goal (the_context ()) "p: x=y ==> ?p : Suc(x) = Suc(y)";
    6.43 -by (resolve_tac (prems RL [subst]) 1);
    6.44 -by (rtac refl 1);
    6.45 -val Suc_cong = result();
    6.46 -
    6.47 -val prems = goal (the_context ()) "[| p : a=x;  q: b=y |] ==> ?p : a+b=x+y";
    6.48 -by (resolve_tac (prems RL [subst]) 1 THEN resolve_tac (prems RL [subst]) 1 THEN
    6.49 -    rtac refl 1);
    6.50 -val Plus_cong = result();
    6.51 -
    6.52 -val nat_congs = [Suc_cong,Plus_cong];
    6.53 -
    6.54 -
    6.55 -val add_ss = FOLP_ss  addcongs nat_congs
    6.56 -                     addrews  [add_0, add_Suc];
    6.57 -
    6.58 -Goal "?p : (k+m)+n = k+(m+n)";
    6.59 -by (res_inst_tac [("n","k")] induct 1);
    6.60 -by (SIMP_TAC add_ss 1);
    6.61 -by (ASM_SIMP_TAC add_ss 1);
    6.62 -val add_assoc = result();
    6.63 -
    6.64 -Goal "?p : m+0 = m";
    6.65 -by (res_inst_tac [("n","m")] induct 1);
    6.66 -by (SIMP_TAC add_ss 1);
    6.67 -by (ASM_SIMP_TAC add_ss 1);
    6.68 -val add_0_right = result();
    6.69 -
    6.70 -Goal "?p : m+Suc(n) = Suc(m+n)";
    6.71 -by (res_inst_tac [("n","m")] induct 1);
    6.72 -by (ALLGOALS (ASM_SIMP_TAC add_ss));
    6.73 -val add_Suc_right = result();
    6.74 -
    6.75 -(*mk_typed_congs appears not to work with FOLP's version of subst*)
     7.1 --- a/src/FOLP/ex/Nat.thy	Sun Jan 27 20:04:31 2008 +0100
     7.2 +++ b/src/FOLP/ex/Nat.thy	Sun Jan 27 20:04:32 2008 +0100
     7.3 @@ -11,18 +11,20 @@
     7.4  begin
     7.5  
     7.6  typedecl nat
     7.7 -arities nat         :: "term"
     7.8 -consts  "0"         :: "nat"    ("0")
     7.9 -        Suc         :: "nat=>nat"
    7.10 -        rec         :: "[nat, 'a, [nat,'a]=>'a] => 'a"
    7.11 -        "+"         :: "[nat, nat] => nat"              (infixl 60)
    7.12 +arities nat :: "term"
    7.13 +
    7.14 +consts
    7.15 +  0 :: nat    ("0")
    7.16 +  Suc :: "nat => nat"
    7.17 +  rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    7.18 +  add :: "[nat, nat] => nat"    (infixl "+" 60)
    7.19  
    7.20    (*Proof terms*)
    7.21 -       nrec         :: "[nat,p,[nat,p]=>p]=>p"
    7.22 -       ninj         :: "p=>p"
    7.23 -       nneq         :: "p=>p"
    7.24 -       rec0         :: "p"
    7.25 -       recSuc       :: "p"
    7.26 +  nrec :: "[nat, p, [nat, p] => p] => p"
    7.27 +  ninj :: "p => p"
    7.28 +  nneq :: "p => p"
    7.29 +  rec0 :: "p"
    7.30 +  recSuc :: "p"
    7.31  
    7.32  axioms
    7.33    induct:     "[| b:P(0); !!x u. u:P(x) ==> c(x,u):P(Suc(x))
    7.34 @@ -32,11 +34,79 @@
    7.35    Suc_neq_0:  "p:Suc(m)=0      ==> nneq(p) : R"
    7.36    rec_0:      "rec0 : rec(0,a,f) = a"
    7.37    rec_Suc:    "recSuc : rec(Suc(m), a, f) = f(m, rec(m,a,f))"
    7.38 +
    7.39 +defs
    7.40    add_def:    "m+n == rec(m, n, %x y. Suc(y))"
    7.41  
    7.42 +axioms
    7.43    nrecB0:     "b: A ==> nrec(0,b,c) = b : A"
    7.44    nrecBSuc:   "c(n,nrec(n,b,c)) : A ==> nrec(Suc(n),b,c) = c(n,nrec(n,b,c)) : A"
    7.45  
    7.46 -ML {* use_legacy_bindings (the_context ()) *}
    7.47 +
    7.48 +subsection {* Proofs about the natural numbers *}
    7.49 +
    7.50 +lemma Suc_n_not_n: "?p : ~ (Suc(k) = k)"
    7.51 +apply (rule_tac n = k in induct)
    7.52 +apply (rule notI)
    7.53 +apply (erule Suc_neq_0)
    7.54 +apply (rule notI)
    7.55 +apply (erule notE)
    7.56 +apply (erule Suc_inject)
    7.57 +done
    7.58 +
    7.59 +lemma "?p : (k+m)+n = k+(m+n)"
    7.60 +apply (rule induct)
    7.61 +back
    7.62 +back
    7.63 +back
    7.64 +back
    7.65 +back
    7.66 +back
    7.67 +oops
    7.68 +
    7.69 +lemma add_0 [simp]: "?p : 0+n = n"
    7.70 +apply (unfold add_def)
    7.71 +apply (rule rec_0)
    7.72 +done
    7.73 +
    7.74 +lemma add_Suc [simp]: "?p : Suc(m)+n = Suc(m+n)"
    7.75 +apply (unfold add_def)
    7.76 +apply (rule rec_Suc)
    7.77 +done
    7.78 +
    7.79 +
    7.80 +lemma Suc_cong: "p : x = y \<Longrightarrow> ?p : Suc(x) = Suc(y)"
    7.81 +  apply (erule subst)
    7.82 +  apply (rule refl)
    7.83 +  done
    7.84 +
    7.85 +lemma Plus_cong: "[| p : a = x;  q: b = y |] ==> ?p : a + b = x + y"
    7.86 +  apply (erule subst, erule subst, rule refl)
    7.87 +  done
    7.88 +
    7.89 +lemmas nat_congs = Suc_cong Plus_cong
    7.90 +
    7.91 +ML {*
    7.92 +  val add_ss = FOLP_ss addcongs @{thms nat_congs} addrews [@{thm add_0}, @{thm add_Suc}]
    7.93 +*}
    7.94 +
    7.95 +lemma add_assoc: "?p : (k+m)+n = k+(m+n)"
    7.96 +apply (rule_tac n = k in induct)
    7.97 +apply (tactic {* SIMP_TAC add_ss 1 *})
    7.98 +apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
    7.99 +done
   7.100 +
   7.101 +lemma add_0_right: "?p : m+0 = m"
   7.102 +apply (rule_tac n = m in induct)
   7.103 +apply (tactic {* SIMP_TAC add_ss 1 *})
   7.104 +apply (tactic {* ASM_SIMP_TAC add_ss 1 *})
   7.105 +done
   7.106 +
   7.107 +lemma add_Suc_right: "?p : m+Suc(n) = Suc(m+n)"
   7.108 +apply (rule_tac n = m in induct)
   7.109 +apply (tactic {* ALLGOALS (ASM_SIMP_TAC add_ss) *})
   7.110 +done
   7.111 +
   7.112 +(*mk_typed_congs appears not to work with FOLP's version of subst*)
   7.113  
   7.114  end
     8.1 --- a/src/FOLP/ex/ROOT.ML	Sun Jan 27 20:04:31 2008 +0100
     8.2 +++ b/src/FOLP/ex/ROOT.ML	Sun Jan 27 20:04:32 2008 +0100
     8.3 @@ -6,9 +6,12 @@
     8.4  Examples for First-Order Logic. 
     8.5  *)
     8.6  
     8.7 -time_use     "intro.ML";
     8.8 -time_use_thy "Nat";
     8.9 -time_use     "foundn.ML";
    8.10 +use_thys [
    8.11 +  "Intro",
    8.12 +  "Nat",
    8.13 +  "Foundation",
    8.14 +  "If"
    8.15 +];
    8.16  
    8.17  writeln"\n** Intuitionistic examples **\n";
    8.18  time_use     "int.ML";
    8.19 @@ -19,7 +22,6 @@
    8.20  
    8.21  writeln"\n** Classical examples **\n";
    8.22  time_use     "cla.ML";
    8.23 -time_use_thy "If";
    8.24  
    8.25  val thy = theory "FOLP"  and  tac = Cla.fast_tac FOLP_cs 1;
    8.26  time_use     "prop.ML";
     9.1 --- a/src/FOLP/ex/foundn.ML	Sun Jan 27 20:04:31 2008 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,129 +0,0 @@
     9.4 -(*  Title:      FOLP/ex/foundn.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1991  University of Cambridge
     9.8 -
     9.9 -Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
    9.10 -*)
    9.11 -
    9.12 -goal (theory "IFOLP") "?p : A&B  --> (C-->A&C)";
    9.13 -by (rtac impI 1);
    9.14 -by (rtac impI 1);
    9.15 -by (rtac conjI 1);
    9.16 -by (assume_tac 2);
    9.17 -by (rtac conjunct1 1);
    9.18 -by (assume_tac 1);
    9.19 -result();
    9.20 -
    9.21 -(*A form of conj-elimination*)
    9.22 -val prems = 
    9.23 -goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A;  y:B |] ==> f(x,y):C) ==> ?p:C";
    9.24 -by (resolve_tac prems 1);
    9.25 -by (rtac conjunct1 1);
    9.26 -by (resolve_tac prems 1);
    9.27 -by (rtac conjunct2 1);
    9.28 -by (resolve_tac prems 1);
    9.29 -result();
    9.30 -
    9.31 -
    9.32 -val prems = 
    9.33 -goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    9.34 -by (resolve_tac prems 1);
    9.35 -by (rtac notI 1);
    9.36 -by (res_inst_tac [ ("P", "~B") ]  notE  1);
    9.37 -by (rtac notI 2);
    9.38 -by (res_inst_tac [ ("P", "B | ~B") ]  notE  2);
    9.39 -by (assume_tac 2);
    9.40 -by (rtac disjI1 2);
    9.41 -by (assume_tac 2);
    9.42 -by (rtac notI 1);
    9.43 -by (res_inst_tac [ ("P", "B | ~B") ]  notE  1);
    9.44 -by (assume_tac 1);
    9.45 -by (rtac disjI2 1);
    9.46 -by (assume_tac 1);
    9.47 -result();
    9.48 -
    9.49 -
    9.50 -val prems = 
    9.51 -goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
    9.52 -by (resolve_tac prems 1);
    9.53 -by (rtac notI 1);
    9.54 -by (rtac notE 1);
    9.55 -by (rtac notI 2);
    9.56 -by (etac notE 2);
    9.57 -by (etac disjI1 2);
    9.58 -by (rtac notI 1);
    9.59 -by (etac notE 1);
    9.60 -by (etac disjI2 1);
    9.61 -result();
    9.62 -
    9.63 -
    9.64 -val prems = 
    9.65 -goal (theory "IFOLP") "[| p:A | ~A;  q:~ ~A |] ==> ?p:A";
    9.66 -by (rtac disjE 1);
    9.67 -by (resolve_tac prems 1);
    9.68 -by (assume_tac 1);
    9.69 -by (rtac FalseE 1);
    9.70 -by (res_inst_tac [ ("P", "~A") ]  notE  1);
    9.71 -by (resolve_tac prems 1);
    9.72 -by (assume_tac 1);
    9.73 -result();
    9.74 -
    9.75 -
    9.76 -writeln"Examples with quantifiers";
    9.77 -
    9.78 -val prems =
    9.79 -goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
    9.80 -by (rtac allI 1);
    9.81 -by (rtac disjI1 1);
    9.82 -by (resolve_tac (prems RL [spec]) 1); 
    9.83 -  (*can use instead
    9.84 -    by (rtac spec 1);  by (resolve_tac prems 1); *)
    9.85 -result();
    9.86 -
    9.87 -
    9.88 -goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
    9.89 -by (rtac allI 1);
    9.90 -by (rtac exI 1);
    9.91 -by (rtac refl 1);
    9.92 -result();
    9.93 -
    9.94 -
    9.95 -goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
    9.96 -by (rtac exI 1);
    9.97 -by (rtac allI 1);
    9.98 -by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected";  
    9.99 -getgoal 1; 
   9.100 -
   9.101 -
   9.102 -(*Parallel lifting example. *)
   9.103 -goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
   9.104 -by (resolve_tac [exI, allI] 1);
   9.105 -by (resolve_tac [exI, allI] 1);
   9.106 -by (resolve_tac [exI, allI] 1);
   9.107 -by (resolve_tac [exI, allI] 1);
   9.108 -by (resolve_tac [exI, allI] 1);
   9.109 -
   9.110 -
   9.111 -val prems =
   9.112 -goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
   9.113 -by (rtac conjE 1);
   9.114 -by (resolve_tac prems 1);
   9.115 -by (rtac exE 1);
   9.116 -by (assume_tac 1);
   9.117 -by (rtac exI 1);
   9.118 -by (rtac conjI 1);
   9.119 -by (assume_tac 1);
   9.120 -by (assume_tac 1);
   9.121 -result();
   9.122 -
   9.123 -
   9.124 -(*A bigger demonstration of quantifiers -- not in the paper*)
   9.125 -goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
   9.126 -by (rtac impI 1);
   9.127 -by (rtac allI 1);
   9.128 -by (rtac exE 1 THEN assume_tac 1);
   9.129 -by (rtac exI 1);
   9.130 -by (rtac allE 1 THEN assume_tac 1);
   9.131 -by (assume_tac 1);
   9.132 -result();  
    10.1 --- a/src/FOLP/ex/intro.ML	Sun Jan 27 20:04:31 2008 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,90 +0,0 @@
    10.4 -(*  Title:      FOLP/ex/intro.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   1992  University of Cambridge
    10.8 -
    10.9 -Examples for the manual "Introduction to Isabelle"
   10.10 -
   10.11 -Derives some inference rules, illustrating the use of definitions
   10.12 -
   10.13 -To generate similar output to manual, execute these commands:
   10.14 -    Pretty.setmargin 72; print_depth 0;
   10.15 -*)
   10.16 -
   10.17 -
   10.18 -(**** Some simple backward proofs ****)
   10.19 -
   10.20 -goal (theory "FOLP") "?p:P|P --> P";
   10.21 -by (rtac impI 1);
   10.22 -by (rtac disjE 1);
   10.23 -by (assume_tac 3);
   10.24 -by (assume_tac 2);
   10.25 -by (assume_tac 1);
   10.26 -val mythm = result();
   10.27 -
   10.28 -goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
   10.29 -by (rtac impI 1);
   10.30 -by (etac disjE 1);
   10.31 -by (dtac conjunct1 1);
   10.32 -by (rtac disjI1 1);
   10.33 -by (rtac disjI2 2);
   10.34 -by (REPEAT (assume_tac 1));
   10.35 -result();
   10.36 -
   10.37 -(*Correct version, delaying use of "spec" until last*)
   10.38 -goal (theory "FOLP") "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
   10.39 -by (rtac impI 1);
   10.40 -by (rtac allI 1);
   10.41 -by (rtac allI 1);
   10.42 -by (dtac spec 1);
   10.43 -by (dtac spec 1);
   10.44 -by (assume_tac 1);
   10.45 -result();
   10.46 -
   10.47 -
   10.48 -(**** Demonstration of fast_tac ****)
   10.49 -
   10.50 -goal (theory "FOLP") "?p:(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
   10.51 -\       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
   10.52 -by (fast_tac FOLP_cs 1);
   10.53 -result();
   10.54 -
   10.55 -goal (theory "FOLP") "?p:ALL x. P(x,f(x)) <-> \
   10.56 -\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   10.57 -by (fast_tac FOLP_cs 1);
   10.58 -result();
   10.59 -
   10.60 -
   10.61 -(**** Derivation of conjunction elimination rule ****)
   10.62 -
   10.63 -val [major,minor] = goal (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
   10.64 -by (rtac minor 1);
   10.65 -by (resolve_tac [major RS conjunct1] 1);
   10.66 -by (resolve_tac [major RS conjunct2] 1);
   10.67 -prth (topthm());
   10.68 -result();
   10.69 -
   10.70 -
   10.71 -(**** Derived rules involving definitions ****)
   10.72 -
   10.73 -(** Derivation of negation introduction **)
   10.74 -
   10.75 -val prems = goal (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
   10.76 -by (rewtac not_def);
   10.77 -by (rtac impI 1);
   10.78 -by (resolve_tac prems 1);
   10.79 -by (assume_tac 1);
   10.80 -result();
   10.81 -
   10.82 -val [major,minor] = goal (theory "FOLP") "[| p:~P;  q:P |] ==> ?p:R";
   10.83 -by (rtac FalseE 1);
   10.84 -by (rtac mp 1);
   10.85 -by (resolve_tac [rewrite_rule [not_def] major] 1);
   10.86 -by (rtac minor 1);
   10.87 -result();
   10.88 -
   10.89 -(*Alternative proof of above result*)
   10.90 -val [major,minor] = goalw (theory "FOLP") [not_def]
   10.91 -    "[| p:~P;  q:P |] ==> ?p:R";
   10.92 -by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
   10.93 -result();
    11.1 --- a/src/FOLP/ex/prop.ML	Sun Jan 27 20:04:31 2008 +0100
    11.2 +++ b/src/FOLP/ex/prop.ML	Sun Jan 27 20:04:32 2008 +0100
    11.3 @@ -7,6 +7,9 @@
    11.4  Needs declarations of the theory "thy" and the tactic "tac"
    11.5  *)
    11.6  
    11.7 +ML_Context.set_context (SOME (Context.Theory thy));
    11.8 +
    11.9 +
   11.10  writeln"commutative laws of & and | ";
   11.11  Goal "?p : P & Q  -->  Q & P";
   11.12  by tac;