# HG changeset patch # User wenzelm # Date 957812370 -7200 # Node ID 18b76c137c41a9e29ecd4b6d1b7aff845feb26ea # Parent 31da5b9790c00b39112489bd1fe5166269a98897 moved theory Sexp to Induct examples; diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Induct/Sexp.ML --- /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"; diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Induct/Sexp.thy --- /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 diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/IsaMakefile --- 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 diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/PreList.thy --- 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 diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Sexp.ML --- 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"; diff -r 31da5b9790c0 -r 18b76c137c41 src/HOL/Sexp.thy --- 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