--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Sexp.ML Mon May 08 20:59:30 2000 +0200
@@ -0,0 +1,130 @@
+(* Title: HOL/Sexp
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+S-expressions, general binary trees for defining recursive data structures
+*)
+
+open Sexp;
+
+(** sexp_case **)
+
+Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
+by (Blast_tac 1);
+qed "sexp_case_Leaf";
+
+Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
+by (Blast_tac 1);
+qed "sexp_case_Numb";
+
+Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
+by (Blast_tac 1);
+qed "sexp_case_Scons";
+
+Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
+
+
+(** Introduction rules for sexp constructors **)
+
+val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+qed "sexp_In0I";
+
+val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
+by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
+qed "sexp_In1I";
+
+AddIs sexp.intrs;
+
+Goal "range(Leaf) <= sexp";
+by (Blast_tac 1);
+qed "range_Leaf_subset_sexp";
+
+val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
+by (rtac (major RS setup_induction) 1);
+by (etac sexp.induct 1);
+by (ALLGOALS Blast_tac);
+qed "Scons_D";
+
+(** Introduction rules for 'pred_sexp' **)
+
+Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
+by (Blast_tac 1);
+qed "pred_sexp_subset_Sigma";
+
+(* (a,b) : pred_sexp^+ ==> a : sexp *)
+val trancl_pred_sexpD1 =
+ pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
+and trancl_pred_sexpD2 =
+ pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
+
+Goalw [pred_sexp_def]
+ "!!M. [| M: sexp; N: sexp |] ==> (M, Scons M N) : pred_sexp";
+by (Blast_tac 1);
+qed "pred_sexpI1";
+
+Goalw [pred_sexp_def]
+ "!!M. [| M: sexp; N: sexp |] ==> (N, Scons M N) : pred_sexp";
+by (Blast_tac 1);
+qed "pred_sexpI2";
+
+(*Combinations involving transitivity and the rules above*)
+val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
+and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
+
+val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
+and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
+
+(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
+Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
+ pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
+
+val major::prems = goalw Sexp.thy [pred_sexp_def]
+ "[| p : pred_sexp; \
+\ !!M N. [| p = (M, Scons M N); M: sexp; N: sexp |] ==> R; \
+\ !!M N. [| p = (N, Scons M N); M: sexp; N: sexp |] ==> R \
+\ |] ==> R";
+by (cut_facts_tac [major] 1);
+by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
+qed "pred_sexpE";
+
+Goal "wf(pred_sexp)";
+by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
+by (etac sexp.induct 1);
+by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
+qed "wf_pred_sexp";
+
+
+(*** sexp_rec -- by wf recursion on pred_sexp ***)
+
+Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
+ \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
+by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+
+(* sexp_rec a c d e =
+ sexp_case c d
+ (%N1 N2.
+ e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
+ (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
+*)
+bind_thm("sexp_rec_unfold",
+ [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
+
+(** conversion rules **)
+
+Goal "sexp_rec (Leaf a) c d h = c(a)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Leaf 1);
+qed "sexp_rec_Leaf";
+
+Goal "sexp_rec (Numb k) c d h = d(k)";
+by (stac sexp_rec_unfold 1);
+by (rtac sexp_case_Numb 1);
+qed "sexp_rec_Numb";
+
+Goal "[| M: sexp; N: sexp |] ==> \
+\ sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
+by (rtac (sexp_rec_unfold RS trans) 1);
+by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
+qed "sexp_rec_Scons";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Sexp.thy Mon May 08 20:59:30 2000 +0200
@@ -0,0 +1,41 @@
+(* Title: HOL/Induct/Sexp.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+S-expressions, general binary trees for defining recursive data
+structures by hand.
+*)
+
+Sexp = Univ + Inductive +
+consts
+ sexp :: 'a item set
+
+ sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
+ 'a item] => 'b"
+
+ sexp_rec :: "['a item, 'a=>'b, nat=>'b,
+ ['a item, 'a item, 'b, 'b]=>'b] => 'b"
+
+ pred_sexp :: "('a item * 'a item)set"
+
+inductive sexp
+ intrs
+ LeafI "Leaf(a): sexp"
+ NumbI "Numb(i): sexp"
+ SconsI "[| M: sexp; N: sexp |] ==> Scons M N : sexp"
+
+defs
+
+ sexp_case_def
+ "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))
+ | (? k. M=Numb(k) & z=d(k))
+ | (? N1 N2. M = Scons N1 N2 & z=e N1 N2)"
+
+ pred_sexp_def
+ "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
+
+ sexp_rec_def
+ "sexp_rec M c d e == wfrec pred_sexp
+ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
+end
--- a/src/HOL/IsaMakefile Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/IsaMakefile Mon May 08 20:59:30 2000 +0200
@@ -31,40 +31,40 @@
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
-$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
- $(SRC)/Provers/Arith/cancel_sums.ML \
- $(SRC)/Provers/Arith/assoc_fold.ML \
- $(SRC)/Provers/Arith/combine_numerals.ML \
- $(SRC)/Provers/Arith/cancel_numerals.ML \
- $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
- $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
- $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
- $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
- $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
- $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
- $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
- $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
- $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
- Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
- Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
- HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
- Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
- Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
- Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
- Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
- Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
- Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
- Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
- Relation.ML Relation.thy Set.ML Set.thy Sexp.ML Sexp.thy String.thy \
- SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
- Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
- Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
- Tools/induct_method.ML Tools/inductive_package.ML \
- Tools/numeral_syntax.ML Tools/primrec_package.ML \
- Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
- Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
- Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
- cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
+$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
+ $(SRC)/Provers/Arith/cancel_sums.ML \
+ $(SRC)/Provers/Arith/assoc_fold.ML \
+ $(SRC)/Provers/Arith/combine_numerals.ML \
+ $(SRC)/Provers/Arith/cancel_numerals.ML \
+ $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML \
+ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
+ $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
+ $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
+ $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
+ $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
+ $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
+ $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
+ $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
+ Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
+ Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
+ HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
+ Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
+ Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
+ Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
+ Integ/NatSimprocs.ML Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
+ Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
+ Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
+ Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
+ Relation.ML Relation.thy Set.ML Set.thy String.thy SVC_Oracle.ML \
+ SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
+ Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
+ Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
+ Tools/induct_method.ML Tools/inductive_package.ML \
+ Tools/numeral_syntax.ML Tools/primrec_package.ML \
+ Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
+ Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
+ Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
+ cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
simpdata.ML subset.ML subset.thy thy_syntax.ML
@$(ISATOOL) usedir -b $(OUT)/Pure HOL
@@ -133,11 +133,11 @@
Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
Induct/LList.ML Induct/LList.thy Induct/Mutil.ML Induct/Mutil.thy \
- Induct/Multiset0.ML Induct/Multiset0.thy \
- Induct/Multiset.ML Induct/Multiset.thy \
- Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML Induct/PropLog.thy \
- Induct/ROOT.ML Induct/SList.ML Induct/SList.thy Induct/ABexp.ML \
- Induct/ABexp.thy Induct/Term.ML Induct/Term.thy
+ Induct/Multiset0.ML Induct/Multiset0.thy Induct/Multiset.ML \
+ Induct/Multiset.thy Induct/Perm.ML Induct/Perm.thy Induct/PropLog.ML \
+ Induct/PropLog.thy Induct/ROOT.ML Induct/Sexp.ML Induct/Sexp.thy \
+ Induct/SList.ML Induct/SList.thy Induct/ABexp.ML Induct/ABexp.thy \
+ Induct/Term.ML Induct/Term.thy
@$(ISATOOL) usedir $(OUT)/HOL Induct
--- a/src/HOL/PreList.thy Mon May 08 20:58:49 2000 +0200
+++ b/src/HOL/PreList.thy Mon May 08 20:59:30 2000 +0200
@@ -8,8 +8,7 @@
*)
theory PreList =
- Option + WF_Rel + NatBin + Recdef + Record + RelPow + Sexp + Calculation
- + SVC_Oracle
+ Option + WF_Rel + NatBin + Recdef + Record + RelPow + Calculation + SVC_Oracle
files "Integ/NatSimprocs.ML":
end
--- a/src/HOL/Sexp.ML Mon May 08 20:58:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(* Title: HOL/Sexp
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1994 University of Cambridge
-
-S-expressions, general binary trees for defining recursive data structures
-*)
-
-open Sexp;
-
-(** sexp_case **)
-
-Goalw [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
-by (Blast_tac 1);
-qed "sexp_case_Leaf";
-
-Goalw [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
-by (Blast_tac 1);
-qed "sexp_case_Numb";
-
-Goalw [sexp_case_def] "sexp_case c d e (Scons M N) = e M N";
-by (Blast_tac 1);
-qed "sexp_case_Scons";
-
-Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
-
-
-(** Introduction rules for sexp constructors **)
-
-val [prem] = goalw Sexp.thy [In0_def] "M: sexp ==> In0(M) : sexp";
-by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-qed "sexp_In0I";
-
-val [prem] = goalw Sexp.thy [In1_def] "M: sexp ==> In1(M) : sexp";
-by (rtac (prem RS (sexp.NumbI RS sexp.SconsI)) 1);
-qed "sexp_In1I";
-
-AddIs sexp.intrs;
-
-Goal "range(Leaf) <= sexp";
-by (Blast_tac 1);
-qed "range_Leaf_subset_sexp";
-
-val [major] = goal Sexp.thy "Scons M N : sexp ==> M: sexp & N: sexp";
-by (rtac (major RS setup_induction) 1);
-by (etac sexp.induct 1);
-by (ALLGOALS Blast_tac);
-qed "Scons_D";
-
-(** Introduction rules for 'pred_sexp' **)
-
-Goalw [pred_sexp_def] "pred_sexp <= sexp <*> sexp";
-by (Blast_tac 1);
-qed "pred_sexp_subset_Sigma";
-
-(* (a,b) : pred_sexp^+ ==> a : sexp *)
-val trancl_pred_sexpD1 =
- pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD1
-and trancl_pred_sexpD2 =
- pred_sexp_subset_Sigma RS trancl_subset_Sigma RS subsetD RS SigmaD2;
-
-Goalw [pred_sexp_def]
- "!!M. [| M: sexp; N: sexp |] ==> (M, Scons M N) : pred_sexp";
-by (Blast_tac 1);
-qed "pred_sexpI1";
-
-Goalw [pred_sexp_def]
- "!!M. [| M: sexp; N: sexp |] ==> (N, Scons M N) : pred_sexp";
-by (Blast_tac 1);
-qed "pred_sexpI2";
-
-(*Combinations involving transitivity and the rules above*)
-val pred_sexp_t1 = pred_sexpI1 RS r_into_trancl
-and pred_sexp_t2 = pred_sexpI2 RS r_into_trancl;
-
-val pred_sexp_trans1 = pred_sexp_t1 RSN (2, trans_trancl RS transD)
-and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
-
-(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
-Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
- pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
-
-val major::prems = goalw Sexp.thy [pred_sexp_def]
- "[| p : pred_sexp; \
-\ !!M N. [| p = (M, Scons M N); M: sexp; N: sexp |] ==> R; \
-\ !!M N. [| p = (N, Scons M N); M: sexp; N: sexp |] ==> R \
-\ |] ==> R";
-by (cut_facts_tac [major] 1);
-by (REPEAT (eresolve_tac ([asm_rl,emptyE,insertE,UN_E]@prems) 1));
-qed "pred_sexpE";
-
-Goal "wf(pred_sexp)";
-by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
-by (etac sexp.induct 1);
-by (ALLGOALS (blast_tac (claset() addSEs [allE, pred_sexpE])));
-qed "wf_pred_sexp";
-
-
-(*** sexp_rec -- by wf recursion on pred_sexp ***)
-
-Goal "(%M. sexp_rec M c d e) = wfrec pred_sexp \
- \ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
-by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
-
-(* sexp_rec a c d e =
- sexp_case c d
- (%N1 N2.
- e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
- (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
-*)
-bind_thm("sexp_rec_unfold",
- [result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
-
-(** conversion rules **)
-
-Goal "sexp_rec (Leaf a) c d h = c(a)";
-by (stac sexp_rec_unfold 1);
-by (rtac sexp_case_Leaf 1);
-qed "sexp_rec_Leaf";
-
-Goal "sexp_rec (Numb k) c d h = d(k)";
-by (stac sexp_rec_unfold 1);
-by (rtac sexp_case_Numb 1);
-qed "sexp_rec_Numb";
-
-Goal "[| M: sexp; N: sexp |] ==> \
-\ sexp_rec (Scons M N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
-by (rtac (sexp_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
-qed "sexp_rec_Scons";
--- a/src/HOL/Sexp.thy Mon May 08 20:58:49 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* Title: HOL/Sexp
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1992 University of Cambridge
-
-S-expressions, general binary trees for defining recursive data structures
-*)
-
-Sexp = Univ + Inductive +
-consts
- sexp :: 'a item set
-
- sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b,
- 'a item] => 'b"
-
- sexp_rec :: "['a item, 'a=>'b, nat=>'b,
- ['a item, 'a item, 'b, 'b]=>'b] => 'b"
-
- pred_sexp :: "('a item * 'a item)set"
-
-inductive sexp
- intrs
- LeafI "Leaf(a): sexp"
- NumbI "Numb(i): sexp"
- SconsI "[| M: sexp; N: sexp |] ==> Scons M N : sexp"
-
-defs
-
- sexp_case_def
- "sexp_case c d e M == @ z. (? x. M=Leaf(x) & z=c(x))
- | (? k. M=Numb(k) & z=d(k))
- | (? N1 N2. M = Scons N1 N2 & z=e N1 N2)"
-
- pred_sexp_def
- "pred_sexp == UN M: sexp. UN N: sexp. {(M, Scons M N), (N, Scons M N)}"
-
- sexp_rec_def
- "sexp_rec M c d e == wfrec pred_sexp
- (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2))) M"
-end