# HG changeset patch # User clasohm # Date 795872554 -3600 # Node ID b051e2fc2e340bb12e77793473a63d3d07cb9666 # Parent 3cdaa87241757cde87670648c63e83e72dd02823 converted ex with curried function application diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Acc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Acc.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,63 @@ +(* Title: HOL/ex/Acc + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +open Acc; + +(*The intended introduction rule*) +val prems = goal Acc.thy + "[| !!b. :r ==> b: acc(r) |] ==> a: acc(r)"; +by (fast_tac (set_cs addIs (prems @ + map (rewrite_rule [pred_def]) acc.intrs)) 1); +qed "accI"; + +goal Acc.thy "!!a b r. [| b: acc(r); : r |] ==> a: acc(r)"; +by (etac acc.elim 1); +by (rewtac pred_def); +by (fast_tac set_cs 1); +qed "acc_downward"; + +val [major,indhyp] = goal Acc.thy + "[| a : acc(r); \ +\ !!x. [| x: acc(r); ALL y. :r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (rtac (major RS acc.induct) 1); +by (rtac indhyp 1); +by (resolve_tac acc.intrs 1); +by (rewtac pred_def); +by (fast_tac set_cs 2); +be (Int_lower1 RS Pow_mono RS subsetD) 1; +qed "acc_induct"; + + +val [major] = goal Acc.thy "r <= Sigma (acc r) (%u. acc(r)) ==> wf(r)"; +by (rtac (major RS wfI) 1); +by (etac acc.induct 1); +by (rewtac pred_def); +by (fast_tac set_cs 1); +qed "acc_wfI"; + +val [major] = goal Acc.thy "wf(r) ==> ALL x. : r | :r --> y: acc(r)"; +by (rtac (major RS wf_induct) 1); +br (impI RS allI) 1; +br accI 1; +by (fast_tac set_cs 1); +qed "acc_wfD_lemma"; + +val [major] = goal Acc.thy "wf(r) ==> r <= Sigma (acc r) (%u. acc(r))"; +by (rtac subsetI 1); +by (res_inst_tac [("p", "x")] PairE 1); +by (fast_tac (set_cs addSIs [SigmaI, + major RS acc_wfD_lemma RS spec RS mp]) 1); +qed "acc_wfD"; + +goal Acc.thy "wf(r) = (r <= Sigma (acc r) (%u. acc(r)))"; +by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); +qed "wf_acc_iff"; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Acc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Acc.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,26 @@ +(* Title: HOL/ex/Acc.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +Acc = WF + + +consts + pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) + acc :: "('a * 'a)set => 'a set" (*Accessible part*) + +defs + pred_def "pred x r == {y. :r}" + +inductive "acc(r)" + intrs + pred "pred a r: Pow(acc(r)) ==> a: acc(r)" + monos "[Pow_mono]" + +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/InSort.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/InSort.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,46 @@ +(* Title: HOL/ex/insort.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Correctness proof of insertion sort. +*) + +val insort_ss = sorting_ss addsimps + [InSort.ins_Nil,InSort.ins_Cons,InSort.insort_Nil,InSort.insort_Cons]; + +goalw InSort.thy [Sorting.total_def] + "!!f. [| total(f); ~f x y |] ==> f y x"; +by(fast_tac HOL_cs 1); +qed "totalD"; + +goalw InSort.thy [Sorting.transf_def] + "!!f. [| transf(f); f b a |] ==> !x. f a x --> f b x"; +by(fast_tac HOL_cs 1); +qed "transfD"; + +goal InSort.thy "list_all p (ins f x xs) = (list_all p xs & p(x))"; +by(list.induct_tac "xs" 1); +by(asm_simp_tac insort_ss 1); +by(asm_simp_tac (insort_ss setloop (split_tac [expand_if])) 1); +by(fast_tac HOL_cs 1); +val insort_ss = insort_ss addsimps [result()]; + +goal InSort.thy "(!x. p(x) --> q(x)) --> list_all p xs --> list_all q xs"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if])))); +qed "list_all_imp"; + +val prems = goal InSort.thy + "[| total(f); transf(f) |] ==> sorted f (ins f x xs) = sorted f xs"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (insort_ss setloop (split_tac [expand_if])))); +by(cut_facts_tac prems 1); +by(cut_inst_tac [("p","f(a)"),("q","f(x)")] list_all_imp 1); +by(fast_tac (HOL_cs addDs [totalD,transfD]) 1); +val insort_ss = insort_ss addsimps [result()]; + +goal InSort.thy "!!f. [| total(f); transf(f) |] ==> sorted f (insort f xs)"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac insort_ss)); +result(); diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/InSort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/InSort.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,21 @@ +(* Title: HOL/ex/insort.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Insertion sort +*) + +InSort = Sorting + + +consts + ins :: "[['a,'a]=>bool, 'a, 'a list] => 'a list" + insort :: "[['a,'a]=>bool, 'a list] => 'a list" + +primrec ins List.list + ins_Nil "ins f x [] = [x]" + ins_Cons "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))" +primrec insort List.list + insort_Nil "insort f [] = []" + insort_Cons "insort f (x#xs) = ins f x (insort f xs)" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/LList.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LList.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,880 @@ +(* Title: HOL/llist + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)? +*) + +open LList; + +(** Simplification **) + +val llist_ss = univ_ss addcongs [split_weak_cong, sum_case_weak_cong] + setloop split_tac [expand_split, expand_sum_case]; + +(*For adding _eqI rules to a simpset; we must remove Pair_eq because + it may turn an instance of reflexivity into a conjunction!*) +fun add_eqI ss = ss addsimps [range_eqI, image_eqI] + delsimps [Pair_eq]; + + +(*This justifies using llist in other recursive type definitions*) +goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)"; +by (rtac gfp_mono 1); +by (REPEAT (ares_tac basic_monos 1)); +qed "llist_mono"; + + +goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))"; +let val rew = rewrite_rule [NIL_def, CONS_def] in +by (fast_tac (univ_cs addSIs (equalityI :: map rew llist.intrs) + addEs [rew llist.elim]) 1) +end; +qed "llist_unfold"; + + +(*** Type checking by coinduction, using list_Fun + THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! +***) + +goalw LList.thy [list_Fun_def] + "!!M. [| M : X; X <= list_Fun A (X Un llist(A)) |] ==> M : llist(A)"; +be llist.coinduct 1; +be (subsetD RS CollectD) 1; +ba 1; +qed "llist_coinduct"; + +goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X"; +by (fast_tac set_cs 1); +qed "list_Fun_NIL_I"; + +goalw LList.thy [list_Fun_def,CONS_def] + "!!M N. [| M: A; N: X |] ==> CONS M N : list_Fun A X"; +by (fast_tac set_cs 1); +qed "list_Fun_CONS_I"; + +(*Utilise the "strong" part, i.e. gfp(f)*) +goalw LList.thy (llist.defs @ [list_Fun_def]) + "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))"; +by (etac (llist.mono RS gfp_fun_UnI2) 1); +qed "list_Fun_llist_I"; + +(*** LList_corec satisfies the desired recurion equation ***) + +(*A continuity result?*) +goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))"; +by (simp_tac (univ_ss addsimps [In1_UN1, Scons_UN1_y]) 1); +qed "CONS_UN1"; + +(*UNUSED; obsolete? +goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))"; +by (simp_tac (prod_ss setloop (split_tac [expand_split])) 1); +qed "split_UN1"; + +goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))"; +by (simp_tac (sum_ss setloop (split_tac [expand_sum_case])) 1); +qed "sum_case2_UN1"; +*) + +val prems = goalw LList.thy [CONS_def] + "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'"; +by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1)); +qed "CONS_mono"; + +val corec_fun_simps = [LList_corec_fun_def RS def_nat_rec_0, + LList_corec_fun_def RS def_nat_rec_Suc]; +val corec_fun_ss = llist_ss addsimps corec_fun_simps; + +(** The directions of the equality are proved separately **) + +goalw LList.thy [LList_corec_def] + "LList_corec a f <= sum_case (%u.NIL) \ +\ (split(%z w. CONS z (LList_corec w f))) (f a)"; +by (rtac UN1_least 1); +by (res_inst_tac [("n","k")] natE 1); +by (ALLGOALS (asm_simp_tac corec_fun_ss)); +by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1)); +qed "LList_corec_subset1"; + +goalw LList.thy [LList_corec_def] + "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \ +\ LList_corec a f"; +by (simp_tac (corec_fun_ss addsimps [CONS_UN1]) 1); +by (safe_tac set_cs); +by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' + asm_simp_tac corec_fun_ss)); +qed "LList_corec_subset2"; + +(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*) +goal LList.thy + "LList_corec a f = sum_case (%u. NIL) \ +\ (split(%z w. CONS z (LList_corec w f))) (f a)"; +by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, + LList_corec_subset2] 1)); +qed "LList_corec"; + +(*definitional version of same*) +val [rew] = goal LList.thy + "[| !!x. h(x) == LList_corec x f |] ==> \ +\ h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)"; +by (rewtac rew); +by (rtac LList_corec 1); +qed "def_LList_corec"; + +(*A typical use of co-induction to show membership in the gfp. + Bisimulation is range(%x. LList_corec x f) *) +goal LList.thy "LList_corec a f : llist({u.True})"; +by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (stac LList_corec 1); +by (simp_tac (llist_ss addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI] + |> add_eqI) 1); +qed "LList_corec_type"; + +(*Lemma for the proof of llist_corec*) +goal LList.thy + "LList_corec a (%z.sum_case Inl (split(%v w.Inr())) (f z)) : \ +\ llist(range(Leaf))"; +by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (stac LList_corec 1); +by (asm_simp_tac (llist_ss addsimps [list_Fun_NIL_I]) 1); +by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); +qed "LList_corec_type2"; + + +(**** llist equality as a gfp; the bisimulation principle ****) + +(*This theorem is actually used, unlike the many similar ones in ZF*) +goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))"; +let val rew = rewrite_rule [NIL_def, CONS_def] in +by (fast_tac (univ_cs addSIs (equalityI :: map rew LListD.intrs) + addEs [rew LListD.elim]) 1) +end; +qed "LListD_unfold"; + +goal LList.thy "!M N. : LListD(diag(A)) --> ntrunc k M = ntrunc k N"; +by (res_inst_tac [("n", "k")] less_induct 1); +by (safe_tac set_cs); +by (etac LListD.elim 1); +by (safe_tac (prod_cs addSEs [diagE])); +by (res_inst_tac [("n", "n")] natE 1); +by (asm_simp_tac (univ_ss addsimps [ntrunc_0]) 1); +by (rename_tac "n'" 1); +by (res_inst_tac [("n", "n'")] natE 1); +by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_one_In1]) 1); +by (asm_simp_tac (univ_ss addsimps [CONS_def, ntrunc_In1, ntrunc_Scons]) 1); +qed "LListD_implies_ntrunc_equality"; + +(*The domain of the LListD relation*) +goalw LList.thy (llist.defs @ [NIL_def, CONS_def]) + "fst``LListD(diag(A)) <= llist(A)"; +by (rtac gfp_upperbound 1); +(*avoids unfolding LListD on the rhs*) +by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1); +by (simp_tac fst_image_ss 1); +by (fast_tac univ_cs 1); +qed "fst_image_LListD"; + +(*This inclusion justifies the use of coinduction to show M=N*) +goal LList.thy "LListD(diag(A)) <= diag(llist(A))"; +by (rtac subsetI 1); +by (res_inst_tac [("p","x")] PairE 1); +by (safe_tac HOL_cs); +by (rtac diag_eqI 1); +by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS + ntrunc_equality) 1); +by (assume_tac 1); +by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1); +qed "LListD_subset_diag"; + +(** Coinduction, using LListD_Fun + THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS! + **) + +goalw LList.thy [LListD_Fun_def] + "!!M. [| M : X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M : LListD(r)"; +be LListD.coinduct 1; +be (subsetD RS CollectD) 1; +ba 1; +qed "LListD_coinduct"; + +goalw LList.thy [LListD_Fun_def,NIL_def] " : LListD_Fun r s"; +by (fast_tac set_cs 1); +qed "LListD_Fun_NIL_I"; + +goalw LList.thy [LListD_Fun_def,CONS_def] + "!!x. [| x:A; :s |] ==> : LListD_Fun (diag A) s"; +by (fast_tac univ_cs 1); +qed "LListD_Fun_CONS_I"; + +(*Utilise the "strong" part, i.e. gfp(f)*) +goalw LList.thy (LListD.defs @ [LListD_Fun_def]) + "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))"; +by (etac (LListD.mono RS gfp_fun_UnI2) 1); +qed "LListD_Fun_LListD_I"; + + +(*This converse inclusion helps to strengthen LList_equalityI*) +goal LList.thy "diag(llist(A)) <= LListD(diag(A))"; +by (rtac subsetI 1); +by (etac LListD_coinduct 1); +by (rtac subsetI 1); +by (eresolve_tac [diagE] 1); +by (eresolve_tac [ssubst] 1); +by (eresolve_tac [llist.elim] 1); +by (ALLGOALS + (asm_simp_tac (llist_ss addsimps [diagI, LListD_Fun_NIL_I, + LListD_Fun_CONS_I]))); +qed "diag_subset_LListD"; + +goal LList.thy "LListD(diag(A)) = diag(llist(A))"; +by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, + diag_subset_LListD] 1)); +qed "LListD_eq_diag"; + +goal LList.thy + "!!M N. M: llist(A) ==> : LListD_Fun (diag A) (X Un diag(llist(A)))"; +by (rtac (LListD_eq_diag RS subst) 1); +br LListD_Fun_LListD_I 1; +by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag, diagI]) 1); +qed "LListD_Fun_diag_I"; + + +(** To show two LLists are equal, exhibit a bisimulation! + [also admits true equality] + Replace "A" by some particular set, like {x.True}??? *) +goal LList.thy + "!!r. [| : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \ +\ |] ==> M=N"; +by (rtac (LListD_subset_diag RS subsetD RS diagE) 1); +by (etac LListD_coinduct 1); +by (asm_simp_tac (HOL_ss addsimps [LListD_eq_diag]) 1); +by (safe_tac prod_cs); +qed "LList_equalityI"; + + +(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***) + +(*abstract proof using a bisimulation*) +val [prem1,prem2] = goal LList.thy + "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \ +\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\ +\ ==> h1=h2"; +by (rtac ext 1); +(*next step avoids an unknown (and flexflex pair) in simplification*) +by (res_inst_tac [("A", "{u.True}"), + ("r", "range(%u. )")] LList_equalityI 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (stac prem1 1); +by (stac prem2 1); +by (simp_tac (llist_ss addsimps [LListD_Fun_NIL_I, + CollectI RS LListD_Fun_CONS_I] + |> add_eqI) 1); +qed "LList_corec_unique"; + +val [prem] = goal LList.thy + "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \ +\ ==> h = (%x.LList_corec x f)"; +by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1); +qed "equals_LList_corec"; + + +(** Obsolete LList_corec_unique proof: complete induction, not coinduction **) + +goalw LList.thy [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}"; +by (rtac ntrunc_one_In1 1); +qed "ntrunc_one_CONS"; + +goalw LList.thy [CONS_def] + "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"; +by (simp_tac (HOL_ss addsimps [ntrunc_Scons,ntrunc_In1]) 1); +qed "ntrunc_CONS"; + +val [prem1,prem2] = goal LList.thy + "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \ +\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\ +\ ==> h1=h2"; +by (rtac (ntrunc_equality RS ext) 1); +by (res_inst_tac [("x", "x")] spec 1); +by (res_inst_tac [("n", "k")] less_induct 1); +by (rtac allI 1); +by (stac prem1 1); +by (stac prem2 1); +by (simp_tac (sum_ss setloop (split_tac [expand_split,expand_sum_case])) 1); +by (strip_tac 1); +by (res_inst_tac [("n", "n")] natE 1); +by (res_inst_tac [("n", "xc")] natE 2); +by (ALLGOALS(asm_simp_tac(nat_ss addsimps + [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS]))); +result(); + + +(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***) + +goal LList.thy "mono(CONS(M))"; +by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1)); +qed "Lconst_fun_mono"; + +(* Lconst(M) = CONS M (Lconst M) *) +bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski))); + +(*A typical use of co-induction to show membership in the gfp. + The containing set is simply the singleton {Lconst(M)}. *) +goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)"; +by (rtac (singletonI RS llist_coinduct) 1); +by (safe_tac set_cs); +by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1); +by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1)); +qed "Lconst_type"; + +goal LList.thy "Lconst(M) = LList_corec M (%x.Inr())"; +by (rtac (equals_LList_corec RS fun_cong) 1); +by (simp_tac sum_ss 1); +by (rtac Lconst 1); +qed "Lconst_eq_LList_corec"; + +(*Thus we could have used gfp in the definition of Lconst*) +goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr())"; +by (rtac (equals_LList_corec RS fun_cong) 1); +by (simp_tac sum_ss 1); +by (rtac (Lconst_fun_mono RS gfp_Tarski) 1); +qed "gfp_Lconst_eq_LList_corec"; + + +(*** Isomorphisms ***) + +goal LList.thy "inj(Rep_llist)"; +by (rtac inj_inverseI 1); +by (rtac Rep_llist_inverse 1); +qed "inj_Rep_llist"; + +goal LList.thy "inj_onto Abs_llist (llist(range(Leaf)))"; +by (rtac inj_onto_inverseI 1); +by (etac Abs_llist_inverse 1); +qed "inj_onto_Abs_llist"; + +(** Distinctness of constructors **) + +goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil"; +by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1)); +qed "LCons_not_LNil"; + +bind_thm ("LNil_not_LCons", (LCons_not_LNil RS not_sym)); + +bind_thm ("LCons_neq_LNil", (LCons_not_LNil RS notE)); +val LNil_neq_LCons = sym RS LCons_neq_LNil; + +(** llist constructors **) + +goalw LList.thy [LNil_def] + "Rep_llist(LNil) = NIL"; +by (rtac (llist.NIL_I RS Abs_llist_inverse) 1); +qed "Rep_llist_LNil"; + +goalw LList.thy [LCons_def] + "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)"; +by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse, + rangeI, Rep_llist] 1)); +qed "Rep_llist_LCons"; + +(** Injectiveness of CONS and LCons **) + +goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')"; +by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1); +qed "CONS_CONS_eq"; + +bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE)); + + +(*For reasoning about abstract llist constructors*) +val llist_cs = set_cs addIs [Rep_llist]@llist.intrs + addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] + addSDs [inj_onto_Abs_llist RS inj_ontoD, + inj_Rep_llist RS injD, Leaf_inject]; + +goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)"; +by (fast_tac llist_cs 1); +qed "LCons_LCons_eq"; +bind_thm ("LCons_inject", (LCons_LCons_eq RS iffD1 RS conjE)); + +val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)"; +by (rtac (major RS llist.elim) 1); +by (etac CONS_neq_NIL 1); +by (fast_tac llist_cs 1); +qed "CONS_D"; + + +(****** Reasoning about llist(A) ******) + +(*Don't use llist_ss, as it does case splits!*) +val List_case_ss = univ_ss addsimps [List_case_NIL, List_case_CONS]; + +(*A special case of list_equality for functions over lazy lists*) +val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy + "[| M: llist(A); g(NIL): llist(A); \ +\ f(NIL)=g(NIL); \ +\ !!x l. [| x:A; l: llist(A) |] ==> \ +\ : \ +\ LListD_Fun (diag A) ((%u.)``llist(A) Un \ +\ diag(llist(A))) \ +\ |] ==> f(M) = g(M)"; +by (rtac LList_equalityI 1); +br (Mlist RS imageI) 1; +by (rtac subsetI 1); +by (etac imageE 1); +by (etac ssubst 1); +by (etac llist.elim 1); +by (etac ssubst 1); +by (stac NILcase 1); +br (gMlist RS LListD_Fun_diag_I) 1; +by (etac ssubst 1); +by (REPEAT (ares_tac [CONScase] 1)); +qed "LList_fun_equalityI"; + + +(*** The functional "Lmap" ***) + +goal LList.thy "Lmap f NIL = NIL"; +by (rtac (Lmap_def RS def_LList_corec RS trans) 1); +by (simp_tac List_case_ss 1); +qed "Lmap_NIL"; + +goal LList.thy "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"; +by (rtac (Lmap_def RS def_LList_corec RS trans) 1); +by (simp_tac List_case_ss 1); +qed "Lmap_CONS"; + +(*Another type-checking proof by coinduction*) +val [major,minor] = goal LList.thy + "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)"; +by (rtac (major RS imageI RS llist_coinduct) 1); +by (safe_tac set_cs); +by (etac llist.elim 1); +by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, + minor, imageI, UnI1] 1)); +qed "Lmap_type"; + +(*This type checking rule synthesises a sufficiently large set for f*) +val [major] = goal LList.thy "M: llist(A) ==> Lmap f M: llist(f``A)"; +by (rtac (major RS Lmap_type) 1); +by (etac imageI 1); +qed "Lmap_type2"; + +(** Two easy results about Lmap **) + +val [prem] = goalw LList.thy [o_def] + "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"; +by (rtac (prem RS imageI RS LList_equalityI) 1); +by (safe_tac set_cs); +by (etac llist.elim 1); +by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1, + rangeI RS LListD_Fun_CONS_I] 1)); +qed "Lmap_compose"; + +val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M"; +by (rtac (prem RS imageI RS LList_equalityI) 1); +by (safe_tac set_cs); +by (etac llist.elim 1); +by (ALLGOALS (asm_simp_tac (HOL_ss addsimps [Lmap_NIL,Lmap_CONS]))); +by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1, + rangeI RS LListD_Fun_CONS_I] 1)); +qed "Lmap_ident"; + + +(*** Lappend -- its two arguments cause some complications! ***) + +goalw LList.thy [Lappend_def] "Lappend NIL NIL = NIL"; +by (rtac (LList_corec RS trans) 1); +by (simp_tac List_case_ss 1); +qed "Lappend_NIL_NIL"; + +goalw LList.thy [Lappend_def] + "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"; +by (rtac (LList_corec RS trans) 1); +by (simp_tac List_case_ss 1); +qed "Lappend_NIL_CONS"; + +goalw LList.thy [Lappend_def] + "Lappend (CONS M M') N = CONS M (Lappend M' N)"; +by (rtac (LList_corec RS trans) 1); +by (simp_tac List_case_ss 1); +qed "Lappend_CONS"; + +val Lappend_ss = + List_case_ss addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS, + Lappend_CONS, LListD_Fun_CONS_I] + |> add_eqI; + +goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M"; +by (etac LList_fun_equalityI 1); +by (ALLGOALS (asm_simp_tac Lappend_ss)); +qed "Lappend_NIL"; + +goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M"; +by (etac LList_fun_equalityI 1); +by (ALLGOALS (asm_simp_tac Lappend_ss)); +qed "Lappend_NIL2"; + +(** Alternative type-checking proofs for Lappend **) + +(*weak co-induction: bisimulation and case analysis on both variables*) +goal LList.thy + "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)"; +by (res_inst_tac + [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1); +by (fast_tac set_cs 1); +by (safe_tac set_cs); +by (eres_inst_tac [("a", "u")] llist.elim 1); +by (eres_inst_tac [("a", "v")] llist.elim 1); +by (ALLGOALS + (asm_simp_tac Lappend_ss THEN' + fast_tac (set_cs addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I]))); +qed "Lappend_type"; + +(*strong co-induction: bisimulation and case analysis on one variable*) +goal LList.thy + "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)"; +by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1); +be imageI 1; +br subsetI 1; +be imageE 1; +by (eres_inst_tac [("a", "u")] llist.elim 1); +by (asm_simp_tac (Lappend_ss addsimps [Lappend_NIL, list_Fun_llist_I]) 1); +by (asm_simp_tac Lappend_ss 1); +by (fast_tac (set_cs addSIs [list_Fun_CONS_I]) 1); +qed "Lappend_type"; + +(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****) + +(** llist_case: case analysis for 'a llist **) + +val Rep_llist_simps = + [List_case_NIL, List_case_CONS, + Abs_llist_inverse, Rep_llist_inverse, + Rep_llist, rangeI, inj_Leaf, Inv_f_f] + @ llist.intrs; +val Rep_llist_ss = llist_ss addsimps Rep_llist_simps; + +goalw LList.thy [llist_case_def,LNil_def] "llist_case c d LNil = c"; +by (simp_tac Rep_llist_ss 1); +qed "llist_case_LNil"; + +goalw LList.thy [llist_case_def,LCons_def] + "llist_case c d (LCons M N) = d M N"; +by (simp_tac Rep_llist_ss 1); +qed "llist_case_LCons"; + +(*Elimination is case analysis, not induction.*) +val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def] + "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P \ +\ |] ==> P"; +by (rtac (Rep_llist RS llist.elim) 1); +by (rtac (inj_Rep_llist RS injD RS prem1) 1); +by (stac Rep_llist_LNil 1); +by (assume_tac 1); +by (etac rangeE 1); +by (rtac (inj_Rep_llist RS injD RS prem2) 1); +by (asm_simp_tac (HOL_ss addsimps [Rep_llist_LCons]) 1); +by (etac (Abs_llist_inverse RS ssubst) 1); +by (rtac refl 1); +qed "llistE"; + +(** llist_corec: corecursion for 'a llist **) + +goalw LList.thy [llist_corec_def,LNil_def,LCons_def] + "llist_corec a f = sum_case (%u. LNil) \ +\ (split(%z w. LCons z (llist_corec w f))) (f a)"; +by (stac LList_corec 1); +by (res_inst_tac [("s","f(a)")] sumE 1); +by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); +by (res_inst_tac [("p","y")] PairE 1); +by (asm_simp_tac (llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1); +(*FIXME: correct case splits usd to be found automatically: +by (ASM_SIMP_TAC(llist_ss addsimps [LList_corec_type2,Abs_llist_inverse]) 1);*) +qed "llist_corec"; + +(*definitional version of same*) +val [rew] = goal LList.thy + "[| !!x. h(x) == llist_corec x f |] ==> \ +\ h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)"; +by (rewtac rew); +by (rtac llist_corec 1); +qed "def_llist_corec"; + +(**** Proofs about type 'a llist functions ****) + +(*** Deriving llist_equalityI -- llist equality is a bisimulation ***) + +goalw LList.thy [LListD_Fun_def] + "!!r A. r <= Sigma (llist A) (%x.llist(A)) ==> \ +\ LListD_Fun (diag A) r <= Sigma (llist A) (%x.llist(A))"; +by (stac llist_unfold 1); +by (simp_tac (HOL_ss addsimps [NIL_def, CONS_def]) 1); +by (fast_tac univ_cs 1); +qed "LListD_Fun_subset_Sigma_llist"; + +goal LList.thy + "prod_fun Rep_llist Rep_llist `` r <= \ +\ Sigma (llist(range(Leaf))) (%x.llist(range(Leaf)))"; +by (fast_tac (prod_cs addIs [Rep_llist]) 1); +qed "subset_Sigma_llist"; + +val [prem] = goal LList.thy + "r <= Sigma (llist(range Leaf)) (%x.llist(range Leaf)) ==> \ +\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r"; +by (safe_tac prod_cs); +by (rtac (prem RS subsetD RS SigmaE2) 1); +by (assume_tac 1); +by (asm_simp_tac (HOL_ss addsimps [o_def,prod_fun,Abs_llist_inverse]) 1); +qed "prod_fun_lemma"; + +goal LList.thy + "prod_fun Rep_llist Rep_llist `` range(%x. ) = \ +\ diag(llist(range(Leaf)))"; +br equalityI 1; +by (fast_tac (univ_cs addIs [Rep_llist]) 1); +by (fast_tac (univ_cs addSEs [Abs_llist_inverse RS subst]) 1); +qed "prod_fun_range_eq_diag"; + +(** To show two llists are equal, exhibit a bisimulation! + [also admits true equality] **) +val [prem1,prem2] = goalw LList.thy [llistD_Fun_def] + "[| : r; r <= llistD_Fun(r Un range(%x.)) |] ==> l1=l2"; +by (rtac (inj_Rep_llist RS injD) 1); +by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"), + ("A", "range(Leaf)")] + LList_equalityI 1); +by (rtac (prem1 RS prod_fun_imageI) 1); +by (rtac (prem2 RS image_mono RS subset_trans) 1); +by (rtac (image_compose RS subst) 1); +by (rtac (prod_fun_compose RS subst) 1); +by (rtac (image_Un RS ssubst) 1); +by (stac prod_fun_range_eq_diag 1); +by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1); +by (rtac (subset_Sigma_llist RS Un_least) 1); +by (rtac diag_subset_Sigma 1); +qed "llist_equalityI"; + +(** Rules to prove the 2nd premise of llist_equalityI **) +goalw LList.thy [llistD_Fun_def,LNil_def] " : llistD_Fun(r)"; +by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1); +qed "llistD_Fun_LNil_I"; + +val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def] + ":r ==> : llistD_Fun(r)"; +by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1); +by (rtac (prem RS prod_fun_imageI) 1); +qed "llistD_Fun_LCons_I"; + +(*Utilise the "strong" part, i.e. gfp(f)*) +goalw LList.thy [llistD_Fun_def] + "!!l. : llistD_Fun(r Un range(%x.))"; +br (Rep_llist_inverse RS subst) 1; +br prod_fun_imageI 1; +by (rtac (image_Un RS ssubst) 1); +by (stac prod_fun_range_eq_diag 1); +br (Rep_llist RS LListD_Fun_diag_I) 1; +qed "llistD_Fun_range_I"; + +(*A special case of list_equality for functions over lazy lists*) +val [prem1,prem2] = goal LList.thy + "[| f(LNil)=g(LNil); \ +\ !!x l. : \ +\ llistD_Fun(range(%u. ) Un range(%v. )) \ +\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"; +by (res_inst_tac [("r", "range(%u. )")] llist_equalityI 1); +by (rtac rangeI 1); +by (rtac subsetI 1); +by (etac rangeE 1); +by (etac ssubst 1); +by (res_inst_tac [("l", "u")] llistE 1); +by (etac ssubst 1); +by (stac prem1 1); +by (rtac llistD_Fun_range_I 1); +by (etac ssubst 1); +by (rtac prem2 1); +qed "llist_fun_equalityI"; + +(*simpset for llist bisimulations*) +val llistD_simps = [llist_case_LNil, llist_case_LCons, + llistD_Fun_LNil_I, llistD_Fun_LCons_I]; +(*Don't use llist_ss, as it does case splits!*) +val llistD_ss = univ_ss addsimps llistD_simps |> add_eqI; + + +(*** The functional "lmap" ***) + +goal LList.thy "lmap f LNil = LNil"; +by (rtac (lmap_def RS def_llist_corec RS trans) 1); +by (simp_tac llistD_ss 1); +qed "lmap_LNil"; + +goal LList.thy "lmap f (LCons M N) = LCons (f M) (lmap f N)"; +by (rtac (lmap_def RS def_llist_corec RS trans) 1); +by (simp_tac llistD_ss 1); +qed "lmap_LCons"; + + +(** Two easy results about lmap **) + +goal LList.thy "lmap (f o g) l = lmap f (lmap g l)"; +by (res_inst_tac [("l","l")] llist_fun_equalityI 1); +by (ALLGOALS (simp_tac (llistD_ss addsimps [lmap_LNil, lmap_LCons]))); +qed "lmap_compose"; + +goal LList.thy "lmap (%x.x) l = l"; +by (res_inst_tac [("l","l")] llist_fun_equalityI 1); +by (ALLGOALS (simp_tac (llistD_ss addsimps [lmap_LNil, lmap_LCons]))); +qed "lmap_ident"; + + +(*** iterates -- llist_fun_equalityI cannot be used! ***) + +goal LList.thy "iterates f x = LCons x (iterates f (f x))"; +by (rtac (iterates_def RS def_llist_corec RS trans) 1); +by (simp_tac sum_ss 1); +qed "iterates"; + +goal LList.thy "lmap f (iterates f x) = iterates f (f x)"; +by (res_inst_tac [("r", "range(%u.)")] + llist_equalityI 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1); +by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1); +by (simp_tac (llistD_ss addsimps [lmap_LCons]) 1); +qed "lmap_iterates"; + +goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))"; +br (lmap_iterates RS ssubst) 1; +br iterates 1; +qed "iterates_lmap"; + +(*** A rather complex proof about iterates -- cf Andy Pitts ***) + +(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **) + +goal LList.thy + "nat_rec n (LCons b l) (%m. lmap(f)) = \ +\ LCons (nat_rec n b (%m. f)) (nat_rec n l (%m. lmap(f)))"; +by (nat_ind_tac "n" 1); +by (ALLGOALS (asm_simp_tac (nat_ss addsimps [lmap_LCons]))); +qed "fun_power_lmap"; + +goal Nat.thy "nat_rec n (g x) (%m. g) = nat_rec (Suc n) x (%m. g)"; +by (nat_ind_tac "n" 1); +by (ALLGOALS (asm_simp_tac nat_ss)); +qed "fun_power_Suc"; + +val Pair_cong = read_instantiate_sg (sign_of Prod.thy) + [("f","Pair")] (standard(refl RS cong RS cong)); + +(*The bisimulation consists of {} + for all u and all n::nat.*) +val [prem] = goal LList.thy + "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"; +br ext 1; +by (res_inst_tac [("r", + "UN u. range(%n. )")] + llist_equalityI 1); +by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1)); +by (safe_tac set_cs); +by (stac iterates 1); +by (stac prem 1); +by (stac fun_power_lmap 1); +by (stac fun_power_lmap 1); +br llistD_Fun_LCons_I 1; +by (rtac (lmap_iterates RS subst) 1); +by (stac fun_power_Suc 1); +by (stac fun_power_Suc 1); +br (UN1_I RS UnI1) 1; +br rangeI 1; +qed "iterates_equality"; + + +(*** lappend -- its two arguments cause some complications! ***) + +goalw LList.thy [lappend_def] "lappend LNil LNil = LNil"; +by (rtac (llist_corec RS trans) 1); +by (simp_tac llistD_ss 1); +qed "lappend_LNil_LNil"; + +goalw LList.thy [lappend_def] + "lappend LNil (LCons l l') = LCons l (lappend LNil l')"; +by (rtac (llist_corec RS trans) 1); +by (simp_tac llistD_ss 1); +qed "lappend_LNil_LCons"; + +goalw LList.thy [lappend_def] + "lappend (LCons l l') N = LCons l (lappend l' N)"; +by (rtac (llist_corec RS trans) 1); +by (simp_tac llistD_ss 1); +qed "lappend_LCons"; + +goal LList.thy "lappend LNil l = l"; +by (res_inst_tac [("l","l")] llist_fun_equalityI 1); +by (ALLGOALS + (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LNil_LCons]))); +qed "lappend_LNil"; + +goal LList.thy "lappend l LNil = l"; +by (res_inst_tac [("l","l")] llist_fun_equalityI 1); +by (ALLGOALS + (simp_tac (llistD_ss addsimps [lappend_LNil_LNil, lappend_LCons]))); +qed "lappend_LNil2"; + +(*The infinite first argument blocks the second*) +goal LList.thy "lappend (iterates f x) N = iterates f x"; +by (res_inst_tac [("r", "range(%u.)")] + llist_equalityI 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (stac iterates 1); +by (simp_tac (llistD_ss addsimps [lappend_LCons]) 1); +qed "lappend_iterates"; + +(** Two proofs that lmap distributes over lappend **) + +(*Long proof requiring case analysis on both both arguments*) +goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; +by (res_inst_tac + [("r", + "UN n. range(%l.)")] + llist_equalityI 1); +by (rtac UN1_I 1); +by (rtac rangeI 1); +by (safe_tac set_cs); +by (res_inst_tac [("l", "l")] llistE 1); +by (res_inst_tac [("l", "n")] llistE 1); +by (ALLGOALS (asm_simp_tac (llistD_ss addsimps + [lappend_LNil_LNil,lappend_LCons,lappend_LNil_LCons, + lmap_LNil,lmap_LCons]))); +by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI])); +by (rtac range_eqI 1); +by (rtac (refl RS Pair_cong) 1); +by (stac lmap_LNil 1); +by (rtac refl 1); +qed "lmap_lappend_distrib"; + +(*Shorter proof of theorem above using llist_equalityI as strong coinduction*) +goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"; +by (res_inst_tac [("l","l")] llist_fun_equalityI 1); +by (simp_tac (llistD_ss addsimps [lappend_LNil, lmap_LNil])1); +by (simp_tac (llistD_ss addsimps [lappend_LCons, lmap_LCons]) 1); +qed "lmap_lappend_distrib"; + +(*Without strong coinduction, three case analyses might be needed*) +goal LList.thy "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"; +by (res_inst_tac [("l","l1")] llist_fun_equalityI 1); +by (simp_tac (llistD_ss addsimps [lappend_LNil])1); +by (simp_tac (llistD_ss addsimps [lappend_LCons]) 1); +qed "lappend_assoc"; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/LList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LList.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,145 @@ +(* Title: HOL/LList.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Definition of type 'a llist by a greatest fixed point + +Shares NIL, CONS, List_case with List.thy + +Still needs filter and flatten functions -- hard because they need +bounds on the amount of lookahead required. + +Could try (but would it work for the gfp analogue of term?) + LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)" + +A nice but complex example would be [ML for the Working Programmer, page 176] + from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1)))) + +Previous definition of llistD_Fun was explicit: + llistD_Fun_def + "llistD_Fun(r) == \ +\ {} Un \ +\ (UN x. (split(%l1 l2.))``r)" +*) + +LList = Gfp + SList + + +types + 'a llist + +arities + llist :: (term)term + +consts + list_Fun :: "['a item set, 'a item set] => 'a item set" + LListD_Fun :: + "[('a item * 'a item)set, ('a item * 'a item)set] => \ +\ ('a item * 'a item)set" + + llist :: "'a item set => 'a item set" + LListD :: "('a item * 'a item)set => ('a item * 'a item)set" + llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set" + + Rep_llist :: "'a llist => 'a item" + Abs_llist :: "'a item => 'a llist" + LNil :: "'a llist" + LCons :: "['a, 'a llist] => 'a llist" + + llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b" + + LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item" + LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item" + llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist" + + Lmap :: "('a item => 'b item) => ('a item => 'b item)" + lmap :: "('a=>'b) => ('a llist => 'b llist)" + + iterates :: "['a => 'a, 'a] => 'a llist" + + Lconst :: "'a item => 'a item" + Lappend :: "['a item, 'a item] => 'a item" + lappend :: "['a llist, 'a llist] => 'a llist" + + +coinductive "llist(A)" + intrs + NIL_I "NIL: llist(A)" + CONS_I "[| a: A; M: llist(A) |] ==> CONS a M : llist(A)" + +coinductive "LListD(r)" + intrs + NIL_I " : LListD(r)" + CONS_I "[| : r; : LListD(r) \ +\ |] ==> : LListD(r)" + +defs + (*Now used exclusively for abbreviating the coinduction rule*) + list_Fun_def "list_Fun A X == \ +\ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}" + + LListD_Fun_def "LListD_Fun r X == \ +\ {z. z = | \ +\ (? M N a b. z = & \ +\ : r & : X)}" + + (*defining the abstract constructors*) + LNil_def "LNil == Abs_llist(NIL)" + LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))" + + llist_case_def + "llist_case c d l == \ +\ List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)" + + LList_corec_fun_def + "LList_corec_fun k f == \ +\ nat_rec k (%x. {}) \ +\ (%j r x. sum_case (%u.NIL) (split(%z w. CONS z (r w))) (f x))" + + LList_corec_def + "LList_corec a f == UN k. LList_corec_fun k f a" + + llist_corec_def + "llist_corec a f == \ +\ Abs_llist(LList_corec a (%z.sum_case (%x.Inl(x)) \ +\ (split(%v w. Inr())) (f z)))" + + llistD_Fun_def + "llistD_Fun(r) == \ +\ prod_fun Abs_llist Abs_llist `` \ +\ LListD_Fun (diag(range Leaf)) \ +\ (prod_fun Rep_llist Rep_llist `` r)" + + Lconst_def "Lconst(M) == lfp(%N. CONS M N)" + + Lmap_def + "Lmap f M == LList_corec M (List_case (Inl Unity) (%x M'. Inr()))" + + lmap_def + "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr()))" + + iterates_def "iterates f a == llist_corec a (%x. Inr())" + +(*Append generates its result by applying f, where + f() = Inl(Unity) + f() = Inr() + f() = Inr() +*) + + Lappend_def + "Lappend M N == LList_corec \ +\ (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(>))) \ +\ (%M1 M2 N. Inr(>))))" + + lappend_def + "lappend l n == llist_corec \ +\ (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(>))) \ +\ (%l1 l2 n. Inr(>))))" + +rules + (*faking a type definition...*) + Rep_llist "Rep_llist(xs): llist(range(Leaf))" + Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs" + Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M" + +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/LexProd.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LexProd.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,24 @@ +(* Title: HOL/ex/lex-prod.ML + ID: $Id$ + Author: Tobias Nipkow, TU Munich + Copyright 1993 TU Munich + +For lex-prod.thy. +The lexicographic product of two wellfounded relations is again wellfounded. +*) + +val prems = goal Prod.thy "!a b. P() ==> !p.P(p)"; +by (cut_facts_tac prems 1); +by (rtac allI 1); +by (rtac (surjective_pairing RS ssubst) 1); +by (fast_tac HOL_cs 1); +qed "split_all_pair"; + +val [wfa,wfb] = goalw LexProd.thy [wf_def,LexProd.lex_prod_def] + "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; +by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); +by (rtac (wfa RS spec RS mp) 1); +by (EVERY1 [rtac allI,rtac impI]); +by (rtac (wfb RS spec RS mp) 1); +by (fast_tac (set_cs addSEs [Pair_inject]) 1); +qed "wf_lex_prod"; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/LexProd.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/LexProd.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,15 @@ +(* Title: HOL/ex/lex-prod.thy + ID: $Id$ + Author: Tobias Nipkow, TU Munich + Copyright 1993 TU Munich + +The lexicographic product of two relations. +*) + +LexProd = WF + Prod + +consts "**" :: "[('a*'a)set, ('b*'b)set] => (('a*'b)*('a*'b))set" (infixl 70) +rules +lex_prod_def "ra**rb == {p. ? a a' b b'. \ +\ p = <,> & ( : ra | a=a' & : rb)}" +end + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/MT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/MT.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,826 @@ +(* Title: HOL/ex/mt.ML + ID: $Id$ + Author: Jacob Frost, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Based upon the article + Robin Milner and Mads Tofte, + Co-induction in Relational Semantics, + Theoretical Computer Science 87 (1991), pages 209-220. + +Written up as + Jacob Frost, A Case Study of Co-induction in Isabelle/HOL + Report 308, Computer Lab, University of Cambridge (1993). +*) + +open MT; + +val prems = goal MT.thy "~a:{b} ==> ~a=b"; +by (cut_facts_tac prems 1); +by (rtac notI 1); +by (dtac notE 1); +by (hyp_subst_tac 1); +by (rtac singletonI 1); +by (assume_tac 1); +qed "notsingletonI"; + +val prems = goalw MT.thy [Un_def] + "[| c : A Un B; c : A & ~c : B ==> P; c : B ==> P |] ==> P"; +by (cut_facts_tac prems 1);bd CollectD 1;be disjE 1; +by (cut_facts_tac [excluded_middle] 1);be disjE 1; +by (resolve_tac prems 1);br conjI 1;ba 1;ba 1; +by (eresolve_tac prems 1); +by (eresolve_tac prems 1); +qed "UnSE"; + +(* ############################################################ *) +(* Inference systems *) +(* ############################################################ *) + +val infsys_mono_tac = + (rewtac subset_def) THEN (safe_tac HOL_cs) THEN (rtac ballI 1) THEN + (rtac CollectI 1) THEN (dtac CollectD 1) THEN + REPEAT + ( (TRY ((etac disjE 1) THEN (rtac disjI2 2) THEN (rtac disjI1 1))) THEN + (REPEAT (etac exE 1)) THEN (REPEAT (rtac exI 1)) THEN (fast_tac set_cs 1) + ); + +val prems = goal MT.thy "P a b ==> P (fst ) (snd )"; +by (rtac (fst_conv RS ssubst) 1); +by (rtac (snd_conv RS ssubst) 1); +by (resolve_tac prems 1); +qed "infsys_p1"; + +val prems = goal MT.thy "P (fst ) (snd ) ==> P a b"; +by (cut_facts_tac prems 1); +by (dtac (fst_conv RS subst) 1); +by (dtac (snd_conv RS subst) 1); +by (assume_tac 1); +qed "infsys_p2"; + +val prems = goal MT.thy + "P a b c ==> P (fst(fst <,c>)) (snd(fst <,c>)) (snd <,c>)"; +by (rtac (fst_conv RS ssubst) 1); +by (rtac (fst_conv RS ssubst) 1); +by (rtac (snd_conv RS ssubst) 1); +by (rtac (snd_conv RS ssubst) 1); +by (resolve_tac prems 1); +qed "infsys_pp1"; + +val prems = goal MT.thy + "P (fst(fst <,c>)) (snd(fst <,c>)) (snd <,c>) ==> P a b c"; +by (cut_facts_tac prems 1); +by (dtac (fst_conv RS subst) 1); +by (dtac (fst_conv RS subst) 1); +by (dtac (snd_conv RS subst) 1); +by (dtac (snd_conv RS subst) 1); +by (assume_tac 1); +qed "infsys_pp2"; + +(* ############################################################ *) +(* Fixpoints *) +(* ############################################################ *) + +(* Least fixpoints *) + +val prems = goal MT.thy "[| mono(f); x:f(lfp(f)) |] ==> x:lfp(f)"; +by (rtac subsetD 1); +by (rtac lfp_lemma2 1); +by (resolve_tac prems 1);brs prems 1; +qed "lfp_intro2"; + +val prems = goal MT.thy + " [| x:lfp(f); mono(f); !!y. y:f(lfp(f)) ==> P(y) |] ==> \ +\ P(x)"; +by (cut_facts_tac prems 1); +by (resolve_tac prems 1);br subsetD 1; +by (rtac lfp_lemma3 1);ba 1;ba 1; +qed "lfp_elim2"; + +val prems = goal MT.thy + " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x.P(x)}) ==> P(y) |] ==> \ +\ P(x)"; +by (cut_facts_tac prems 1); +by (etac induct 1);ba 1; +by (eresolve_tac prems 1); +qed "lfp_ind2"; + +(* Greatest fixpoints *) + +(* Note : "[| x:S; S <= f(S Un gfp(f)); mono(f) |] ==> x:gfp(f)" *) + +val [cih,monoh] = goal MT.thy "[| x:f({x} Un gfp(f)); mono(f) |] ==> x:gfp(f)"; +by (rtac (cih RSN (2,gfp_upperbound RS subsetD)) 1); +by (rtac (monoh RS monoD) 1); +by (rtac (UnE RS subsetI) 1);ba 1; +by (fast_tac (set_cs addSIs [cih]) 1); +by (rtac (monoh RS monoD RS subsetD) 1); +by (rtac Un_upper2 1); +by (etac (monoh RS gfp_lemma2 RS subsetD) 1); +qed "gfp_coind2"; + +val [gfph,monoh,caseh] = goal MT.thy + "[| x:gfp(f); mono(f); !! y. y:f(gfp(f)) ==> P(y) |] ==> P(x)"; +by (rtac caseh 1);br subsetD 1;br gfp_lemma2 1;br monoh 1;br gfph 1; +qed "gfp_elim2"; + +(* ############################################################ *) +(* Expressions *) +(* ############################################################ *) + +val e_injs = [e_const_inj, e_var_inj, e_fn_inj, e_fix_inj, e_app_inj]; + +val e_disjs = + [ e_disj_const_var, + e_disj_const_fn, + e_disj_const_fix, + e_disj_const_app, + e_disj_var_fn, + e_disj_var_fix, + e_disj_var_app, + e_disj_fn_fix, + e_disj_fn_app, + e_disj_fix_app + ]; + +val e_disj_si = e_disjs @ (e_disjs RL [not_sym]); +val e_disj_se = (e_disj_si RL [notE]); + +fun e_ext_cs cs = cs addSIs e_disj_si addSEs e_disj_se addSDs e_injs; + +(* ############################################################ *) +(* Values *) +(* ############################################################ *) + +val v_disjs = [v_disj_const_clos]; +val v_disj_si = v_disjs @ (v_disjs RL [not_sym]); +val v_disj_se = (v_disj_si RL [notE]); + +val v_injs = [v_const_inj, v_clos_inj]; + +fun v_ext_cs cs = cs addSIs v_disj_si addSEs v_disj_se addSDs v_injs; + +(* ############################################################ *) +(* Evaluations *) +(* ############################################################ *) + +(* Monotonicity of eval_fun *) + +goalw MT.thy [mono_def, eval_fun_def] "mono(eval_fun)"; +by infsys_mono_tac; +qed "eval_fun_mono"; + +(* Introduction rules *) + +goalw MT.thy [eval_def, eval_rel_def] "ve |- e_const(c) ---> v_const(c)"; +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI1 1; +by (fast_tac HOL_cs 1); +qed "eval_const"; + +val prems = goalw MT.thy [eval_def, eval_rel_def] + "ev:ve_dom(ve) ==> ve |- e_var(ev) ---> ve_app ve ev"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "eval_var"; + +val prems = goalw MT.thy [eval_def, eval_rel_def] + "ve |- fn ev => e ---> v_clos(<|ev,e,ve|>)"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "eval_fn"; + +val prems = goalw MT.thy [eval_def, eval_rel_def] + " cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ +\ ve |- fix ev2(ev1) = e ---> v_clos(cl)"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "eval_fix"; + +val prems = goalw MT.thy [eval_def, eval_rel_def] + " [| ve |- e1 ---> v_const(c1); ve |- e2 ---> v_const(c2) |] ==> \ +\ ve |- e1 @ e2 ---> v_const(c_app c1 c2)"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "eval_app1"; + +val prems = goalw MT.thy [eval_def, eval_rel_def] + " [| ve |- e1 ---> v_clos(<|xm,em,vem|>); \ +\ ve |- e2 ---> v2; \ +\ vem + {xm |-> v2} |- em ---> v \ +\ |] ==> \ +\ ve |- e1 @ e2 ---> v"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1; +by (fast_tac HOL_cs 1); +qed "eval_app2"; + +(* Strong elimination, induction on evaluations *) + +val prems = goalw MT.thy [eval_def, eval_rel_def] + " [| ve |- e ---> v; \ +\ !!ve c. P(<,v_const(c)>); \ +\ !!ev ve. ev:ve_dom(ve) ==> P(<,ve_app ve ev>); \ +\ !!ev ve e. P(< e>,v_clos(<|ev,e,ve|>)>); \ +\ !!ev1 ev2 ve cl e. \ +\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ +\ P(<,v_clos(cl)>); \ +\ !!ve c1 c2 e1 e2. \ +\ [| P(<,v_const(c1)>); P(<,v_const(c2)>) |] ==> \ +\ P(<,v_const(c_app c1 c2)>); \ +\ !!ve vem xm e1 e2 em v v2. \ +\ [| P(<,v_clos(<|xm,em,vem|>)>); \ +\ P(<,v2>); \ +\ P(< v2},em>,v>) \ +\ |] ==> \ +\ P(<,v>) \ +\ |] ==> \ +\ P(<,v>)"; +by (resolve_tac (prems RL [lfp_ind2]) 1); +by (rtac eval_fun_mono 1); +by (rewtac eval_fun_def); +by (dtac CollectD 1); +by (safe_tac HOL_cs); +by (ALLGOALS (resolve_tac prems)); +by (ALLGOALS (fast_tac set_cs)); +qed "eval_ind0"; + +val prems = goal MT.thy + " [| ve |- e ---> v; \ +\ !!ve c. P ve (e_const c) (v_const c); \ +\ !!ev ve. ev:ve_dom(ve) ==> P ve (e_var ev) (ve_app ve ev); \ +\ !!ev ve e. P ve (fn ev => e) (v_clos <|ev,e,ve|>); \ +\ !!ev1 ev2 ve cl e. \ +\ cl = <| ev1, e, ve + {ev2 |-> v_clos(cl)} |> ==> \ +\ P ve (fix ev2(ev1) = e) (v_clos cl); \ +\ !!ve c1 c2 e1 e2. \ +\ [| P ve e1 (v_const c1); P ve e2 (v_const c2) |] ==> \ +\ P ve (e1 @ e2) (v_const(c_app c1 c2)); \ +\ !!ve vem evm e1 e2 em v v2. \ +\ [| P ve e1 (v_clos <|evm,em,vem|>); \ +\ P ve e2 v2; \ +\ P (vem + {evm |-> v2}) em v \ +\ |] ==> P ve (e1 @ e2) v \ +\ |] ==> P ve e v"; +by (res_inst_tac [("P","P")] infsys_pp2 1); +by (rtac eval_ind0 1); +by (ALLGOALS (rtac infsys_pp1)); +by (ALLGOALS (resolve_tac prems)); +by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); +qed "eval_ind"; + +(* ############################################################ *) +(* Elaborations *) +(* ############################################################ *) + +goalw MT.thy [mono_def, elab_fun_def] "mono(elab_fun)"; +by infsys_mono_tac; +qed "elab_fun_mono"; + +(* Introduction rules *) + +val prems = goalw MT.thy [elab_def, elab_rel_def] + "c isof ty ==> te |- e_const(c) ===> ty"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (rtac CollectI 1);br disjI1 1; +by (fast_tac HOL_cs 1); +qed "elab_const"; + +val prems = goalw MT.thy [elab_def, elab_rel_def] + "x:te_dom(te) ==> te |- e_var(x) ===> te_app te x"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "elab_var"; + +val prems = goalw MT.thy [elab_def, elab_rel_def] + "te + {x |=> ty1} |- e ===> ty2 ==> te |- fn x => e ===> ty1->ty2"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "elab_fn"; + +val prems = goalw MT.thy [elab_def, elab_rel_def] + " te + {f |=> ty1->ty2} + {x |=> ty1} |- e ===> ty2 ==> \ +\ te |- fix f(x) = e ===> ty1->ty2"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI1 1; +by (fast_tac HOL_cs 1); +qed "elab_fix"; + +val prems = goalw MT.thy [elab_def, elab_rel_def] + " [| te |- e1 ===> ty1->ty2; te |- e2 ===> ty1 |] ==> \ +\ te |- e1 @ e2 ===> ty2"; +by (cut_facts_tac prems 1); +by (rtac lfp_intro2 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (rtac CollectI 1);br disjI2 1;br disjI2 1;br disjI2 1;br disjI2 1; +by (fast_tac HOL_cs 1); +qed "elab_app"; + +(* Strong elimination, induction on elaborations *) + +val prems = goalw MT.thy [elab_def, elab_rel_def] + " [| te |- e ===> t; \ +\ !!te c t. c isof t ==> P(<,t>); \ +\ !!te x. x:te_dom(te) ==> P(<,te_app te x>); \ +\ !!te x e t1 t2. \ +\ [| te + {x |=> t1} |- e ===> t2; P(< t1},e>,t2>) |] ==> \ +\ P(< e>,t1->t2>); \ +\ !!te f x e t1 t2. \ +\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \ +\ P(< t1->t2} + {x |=> t1},e>,t2>) \ +\ |] ==> \ +\ P(<,t1->t2>); \ +\ !!te e1 e2 t1 t2. \ +\ [| te |- e1 ===> t1->t2; P(<,t1->t2>); \ +\ te |- e2 ===> t1; P(<,t1>) \ +\ |] ==> \ +\ P(<,t2>) \ +\ |] ==> \ +\ P(<,t>)"; +by (resolve_tac (prems RL [lfp_ind2]) 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (dtac CollectD 1); +by (safe_tac HOL_cs); +by (ALLGOALS (resolve_tac prems)); +by (ALLGOALS (fast_tac set_cs)); +qed "elab_ind0"; + +val prems = goal MT.thy + " [| te |- e ===> t; \ +\ !!te c t. c isof t ==> P te (e_const c) t; \ +\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \ +\ !!te x e t1 t2. \ +\ [| te + {x |=> t1} |- e ===> t2; P (te + {x |=> t1}) e t2 |] ==> \ +\ P te (fn x => e) (t1->t2); \ +\ !!te f x e t1 t2. \ +\ [| te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2; \ +\ P (te + {f |=> t1->t2} + {x |=> t1}) e t2 \ +\ |] ==> \ +\ P te (fix f(x) = e) (t1->t2); \ +\ !!te e1 e2 t1 t2. \ +\ [| te |- e1 ===> t1->t2; P te e1 (t1->t2); \ +\ te |- e2 ===> t1; P te e2 t1 \ +\ |] ==> \ +\ P te (e1 @ e2) t2 \ +\ |] ==> \ +\ P te e t"; +by (res_inst_tac [("P","P")] infsys_pp2 1); +by (rtac elab_ind0 1); +by (ALLGOALS (rtac infsys_pp1)); +by (ALLGOALS (resolve_tac prems)); +by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); +qed "elab_ind"; + +(* Weak elimination, case analysis on elaborations *) + +val prems = goalw MT.thy [elab_def, elab_rel_def] + " [| te |- e ===> t; \ +\ !!te c t. c isof t ==> P(<,t>); \ +\ !!te x. x:te_dom(te) ==> P(<,te_app te x>); \ +\ !!te x e t1 t2. \ +\ te + {x |=> t1} |- e ===> t2 ==> P(< e>,t1->t2>); \ +\ !!te f x e t1 t2. \ +\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \ +\ P(<,t1->t2>); \ +\ !!te e1 e2 t1 t2. \ +\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \ +\ P(<,t2>) \ +\ |] ==> \ +\ P(<,t>)"; +by (resolve_tac (prems RL [lfp_elim2]) 1); +by (rtac elab_fun_mono 1); +by (rewtac elab_fun_def); +by (dtac CollectD 1); +by (safe_tac HOL_cs); +by (ALLGOALS (resolve_tac prems)); +by (ALLGOALS (fast_tac set_cs)); +qed "elab_elim0"; + +val prems = goal MT.thy + " [| te |- e ===> t; \ +\ !!te c t. c isof t ==> P te (e_const c) t; \ +\ !!te x. x:te_dom(te) ==> P te (e_var x) (te_app te x); \ +\ !!te x e t1 t2. \ +\ te + {x |=> t1} |- e ===> t2 ==> P te (fn x => e) (t1->t2); \ +\ !!te f x e t1 t2. \ +\ te + {f |=> t1->t2} + {x |=> t1} |- e ===> t2 ==> \ +\ P te (fix f(x) = e) (t1->t2); \ +\ !!te e1 e2 t1 t2. \ +\ [| te |- e1 ===> t1->t2; te |- e2 ===> t1 |] ==> \ +\ P te (e1 @ e2) t2 \ +\ |] ==> \ +\ P te e t"; +by (res_inst_tac [("P","P")] infsys_pp2 1); +by (rtac elab_elim0 1); +by (ALLGOALS (rtac infsys_pp1)); +by (ALLGOALS (resolve_tac prems)); +by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_pp2 1))); +qed "elab_elim"; + +(* Elimination rules for each expression *) + +fun elab_e_elim_tac p = + ( (rtac elab_elim 1) THEN + (resolve_tac p 1) THEN + (REPEAT (fast_tac (e_ext_cs HOL_cs) 1)) + ); + +val prems = goal MT.thy "te |- e ===> t ==> (e = e_const(c) --> c isof t)"; +by (elab_e_elim_tac prems); +qed "elab_const_elim_lem"; + +val prems = goal MT.thy "te |- e_const(c) ===> t ==> c isof t"; +by (cut_facts_tac prems 1); +by (dtac elab_const_elim_lem 1); +by (fast_tac prop_cs 1); +qed "elab_const_elim"; + +val prems = goal MT.thy + "te |- e ===> t ==> (e = e_var(x) --> t=te_app te x & x:te_dom(te))"; +by (elab_e_elim_tac prems); +qed "elab_var_elim_lem"; + +val prems = goal MT.thy + "te |- e_var(ev) ===> t ==> t=te_app te ev & ev : te_dom(te)"; +by (cut_facts_tac prems 1); +by (dtac elab_var_elim_lem 1); +by (fast_tac prop_cs 1); +qed "elab_var_elim"; + +val prems = goal MT.thy + " te |- e ===> t ==> \ +\ ( e = fn x1 => e1 --> \ +\ (? t1 t2.t=t_fun t1 t2 & te + {x1 |=> t1} |- e1 ===> t2) \ +\ )"; +by (elab_e_elim_tac prems); +qed "elab_fn_elim_lem"; + +val prems = goal MT.thy + " te |- fn x1 => e1 ===> t ==> \ +\ (? t1 t2. t=t1->t2 & te + {x1 |=> t1} |- e1 ===> t2)"; +by (cut_facts_tac prems 1); +by (dtac elab_fn_elim_lem 1); +by (fast_tac prop_cs 1); +qed "elab_fn_elim"; + +val prems = goal MT.thy + " te |- e ===> t ==> \ +\ (e = fix f(x) = e1 --> \ +\ (? t1 t2. t=t1->t2 & te + {f |=> t1->t2} + {x |=> t1} |- e1 ===> t2))"; +by (elab_e_elim_tac prems); +qed "elab_fix_elim_lem"; + +val prems = goal MT.thy + " te |- fix ev1(ev2) = e1 ===> t ==> \ +\ (? t1 t2. t=t1->t2 & te + {ev1 |=> t1->t2} + {ev2 |=> t1} |- e1 ===> t2)"; +by (cut_facts_tac prems 1); +by (dtac elab_fix_elim_lem 1); +by (fast_tac prop_cs 1); +qed "elab_fix_elim"; + +val prems = goal MT.thy + " te |- e ===> t2 ==> \ +\ (e = e1 @ e2 --> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1))"; +by (elab_e_elim_tac prems); +qed "elab_app_elim_lem"; + +val prems = goal MT.thy + "te |- e1 @ e2 ===> t2 ==> (? t1 . te |- e1 ===> t1->t2 & te |- e2 ===> t1)"; +by (cut_facts_tac prems 1); +by (dtac elab_app_elim_lem 1); +by (fast_tac prop_cs 1); +qed "elab_app_elim"; + +(* ############################################################ *) +(* The extended correspondence relation *) +(* ############################################################ *) + +(* Monotonicity of hasty_fun *) + +goalw MT.thy [mono_def,MT.hasty_fun_def] "mono(hasty_fun)"; +by infsys_mono_tac; +bind_thm("mono_hasty_fun", result()); + +(* + Because hasty_rel has been defined as the greatest fixpoint of hasty_fun it + enjoys two strong indtroduction (co-induction) rules and an elimination rule. +*) + +(* First strong indtroduction (co-induction) rule for hasty_rel *) + +val prems = goalw MT.thy [hasty_rel_def] "c isof t ==> : hasty_rel"; +by (cut_facts_tac prems 1); +by (rtac gfp_coind2 1); +by (rewtac MT.hasty_fun_def); +by (rtac CollectI 1);br disjI1 1; +by (fast_tac HOL_cs 1); +by (rtac mono_hasty_fun 1); +qed "hasty_rel_const_coind"; + +(* Second strong introduction (co-induction) rule for hasty_rel *) + +val prems = goalw MT.thy [hasty_rel_def] + " [| te |- fn ev => e ===> t; \ +\ ve_dom(ve) = te_dom(te); \ +\ ! ev1. \ +\ ev1:ve_dom(ve) --> \ +\ : {),t>} Un hasty_rel \ +\ |] ==> \ +\ ),t> : hasty_rel"; +by (cut_facts_tac prems 1); +by (rtac gfp_coind2 1); +by (rewtac hasty_fun_def); +by (rtac CollectI 1);br disjI2 1; +by (fast_tac HOL_cs 1); +by (rtac mono_hasty_fun 1); +qed "hasty_rel_clos_coind"; + +(* Elimination rule for hasty_rel *) + +val prems = goalw MT.thy [hasty_rel_def] + " [| !! c t.c isof t ==> P(); \ +\ !! te ev e t ve. \ +\ [| te |- fn ev => e ===> t; \ +\ ve_dom(ve) = te_dom(te); \ +\ !ev1.ev1:ve_dom(ve) --> : hasty_rel \ +\ |] ==> P(),t>); \ +\ : hasty_rel \ +\ |] ==> P()"; +by (cut_facts_tac prems 1); +by (etac gfp_elim2 1); +by (rtac mono_hasty_fun 1); +by (rewtac hasty_fun_def); +by (dtac CollectD 1); +by (fold_goals_tac [hasty_fun_def]); +by (safe_tac HOL_cs); +by (ALLGOALS (resolve_tac prems)); +by (ALLGOALS (fast_tac set_cs)); +qed "hasty_rel_elim0"; + +val prems = goal MT.thy + " [| : hasty_rel; \ +\ !! c t.c isof t ==> P (v_const c) t; \ +\ !! te ev e t ve. \ +\ [| te |- fn ev => e ===> t; \ +\ ve_dom(ve) = te_dom(te); \ +\ !ev1.ev1:ve_dom(ve) --> : hasty_rel \ +\ |] ==> P (v_clos <|ev,e,ve|>) t \ +\ |] ==> P v t"; +by (res_inst_tac [("P","P")] infsys_p2 1); +by (rtac hasty_rel_elim0 1); +by (ALLGOALS (rtac infsys_p1)); +by (ALLGOALS (resolve_tac prems)); +by (REPEAT ((assume_tac 1) ORELSE (dtac infsys_p2 1))); +qed "hasty_rel_elim"; + +(* Introduction rules for hasty *) + +val prems = goalw MT.thy [hasty_def] "c isof t ==> v_const(c) hasty t"; +by (resolve_tac (prems RL [hasty_rel_const_coind]) 1); +qed "hasty_const"; + +val prems = goalw MT.thy [hasty_def,hasty_env_def] + "te |- fn ev => e ===> t & ve hastyenv te ==> v_clos(<|ev,e,ve|>) hasty t"; +by (cut_facts_tac prems 1); +by (rtac hasty_rel_clos_coind 1); +by (ALLGOALS (fast_tac set_cs)); +qed "hasty_clos"; + +(* Elimination on constants for hasty *) + +val prems = goalw MT.thy [hasty_def] + "v hasty t ==> (!c.(v = v_const(c) --> c isof t))"; +by (cut_facts_tac prems 1); +by (rtac hasty_rel_elim 1); +by (ALLGOALS (fast_tac (v_ext_cs HOL_cs))); +qed "hasty_elim_const_lem"; + +val prems = goal MT.thy "v_const(c) hasty t ==> c isof t"; +by (cut_facts_tac (prems RL [hasty_elim_const_lem]) 1); +by (fast_tac HOL_cs 1); +qed "hasty_elim_const"; + +(* Elimination on closures for hasty *) + +val prems = goalw MT.thy [hasty_env_def,hasty_def] + " v hasty t ==> \ +\ ! x e ve. \ +\ v=v_clos(<|x,e,ve|>) --> (? te.te |- fn x => e ===> t & ve hastyenv te)"; +by (cut_facts_tac prems 1); +by (rtac hasty_rel_elim 1); +by (ALLGOALS (fast_tac (v_ext_cs HOL_cs))); +qed "hasty_elim_clos_lem"; + +val prems = goal MT.thy + "v_clos(<|ev,e,ve|>) hasty t ==> ? te.te |- fn ev => e ===> t & ve hastyenv te "; +by (cut_facts_tac (prems RL [hasty_elim_clos_lem]) 1); +by (fast_tac HOL_cs 1); +qed "hasty_elim_clos"; + +(* ############################################################ *) +(* The pointwise extension of hasty to environments *) +(* ############################################################ *) + +val prems = goal MT.thy + "[| ve hastyenv te; v hasty t |] ==> \ +\ ve + {ev |-> v} hastyenv te + {ev |=> t}"; +by (cut_facts_tac prems 1); +by (SELECT_GOAL (rewtac hasty_env_def) 1); +by (safe_tac HOL_cs); +by (rtac (ve_dom_owr RS ssubst) 1); +by (rtac (te_dom_owr RS ssubst) 1); +by (etac subst 1);br refl 1; + +by (dtac (ve_dom_owr RS subst) 1);back();back();back(); +by (etac UnSE 1);be conjE 1; +by (dtac notsingletonI 1);bd not_sym 1; +by (rtac (ve_app_owr2 RS ssubst) 1);ba 1; +by (rtac (te_app_owr2 RS ssubst) 1);ba 1; +by (fast_tac HOL_cs 1); +by (dtac singletonD 1);by (hyp_subst_tac 1); + +by (rtac (ve_app_owr1 RS ssubst) 1); +by (rtac (te_app_owr1 RS ssubst) 1); +by (assume_tac 1); +qed "hasty_env1"; + +(* ############################################################ *) +(* The Consistency theorem *) +(* ############################################################ *) + +val prems = goal MT.thy + "[| ve hastyenv te ; te |- e_const(c) ===> t |] ==> v_const(c) hasty t"; +by (cut_facts_tac prems 1); +by (dtac elab_const_elim 1); +by (etac hasty_const 1); +qed "consistency_const"; + +val prems = goalw MT.thy [hasty_env_def] + " [| ev : ve_dom(ve); ve hastyenv te ; te |- e_var(ev) ===> t |] ==> \ +\ ve_app ve ev hasty t"; +by (cut_facts_tac prems 1); +by (dtac elab_var_elim 1); +by (fast_tac HOL_cs 1); +qed "consistency_var"; + +val prems = goal MT.thy + " [| ve hastyenv te ; te |- fn ev => e ===> t |] ==> \ +\ v_clos(<| ev, e, ve |>) hasty t"; +by (cut_facts_tac prems 1); +by (rtac hasty_clos 1); +by (fast_tac prop_cs 1); +qed "consistency_fn"; + +val prems = goalw MT.thy [hasty_env_def,hasty_def] + " [| cl = <| ev1, e, ve + { ev2 |-> v_clos(cl) } |>; \ +\ ve hastyenv te ; \ +\ te |- fix ev2 ev1 = e ===> t \ +\ |] ==> \ +\ v_clos(cl) hasty t"; +by (cut_facts_tac prems 1); +by (dtac elab_fix_elim 1); +by (safe_tac HOL_cs); +by ((forward_tac [ssubst] 1) THEN (assume_tac 2) THEN + (rtac hasty_rel_clos_coind 1)); +by (etac elab_fn 1); + +by (rtac (ve_dom_owr RS ssubst) 1); +by (rtac (te_dom_owr RS ssubst) 1); +by ((etac subst 1) THEN (rtac refl 1)); + +by (rtac (ve_dom_owr RS ssubst) 1); +by (safe_tac HOL_cs); +by (dtac (Un_commute RS subst) 1); +by (etac UnSE 1); + +by (safe_tac HOL_cs); +by (dtac notsingletonI 1);bd not_sym 1; +by (rtac (ve_app_owr2 RS ssubst) 1);ba 1; +by (rtac (te_app_owr2 RS ssubst) 1);ba 1; +by (fast_tac set_cs 1); + +by (etac singletonE 1); +by (hyp_subst_tac 1); +by (rtac (ve_app_owr1 RS ssubst) 1); +by (rtac (te_app_owr1 RS ssubst) 1); +by (etac subst 1); +by (fast_tac set_cs 1); +qed "consistency_fix"; + +val prems = goal MT.thy + " [| ! t te. ve hastyenv te --> te |- e1 ===> t --> v_const(c1) hasty t; \ +\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v_const(c2) hasty t; \ +\ ve hastyenv te ; te |- e1 @ e2 ===> t \ +\ |] ==> \ +\ v_const(c_app c1 c2) hasty t"; +by (cut_facts_tac prems 1); +by (dtac elab_app_elim 1); +by (safe_tac HOL_cs); +by (rtac hasty_const 1); +by (rtac isof_app 1); +by (rtac hasty_elim_const 1); +by (fast_tac HOL_cs 1); +by (rtac hasty_elim_const 1); +by (fast_tac HOL_cs 1); +qed "consistency_app1"; + +val prems = goal MT.thy + " [| ! t te. \ +\ ve hastyenv te --> \ +\ te |- e1 ===> t --> v_clos(<|evm, em, vem|>) hasty t; \ +\ ! t te. ve hastyenv te --> te |- e2 ===> t --> v2 hasty t; \ +\ ! t te. \ +\ vem + { evm |-> v2 } hastyenv te --> te |- em ===> t --> v hasty t; \ +\ ve hastyenv te ; \ +\ te |- e1 @ e2 ===> t \ +\ |] ==> \ +\ v hasty t"; +by (cut_facts_tac prems 1); +by (dtac elab_app_elim 1); +by (safe_tac HOL_cs); +by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1; +by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));ba 1;be impE 1;ba 1; +by (dtac hasty_elim_clos 1); +by (safe_tac HOL_cs); +by (dtac elab_fn_elim 1); +by (safe_tac HOL_cs); +by (dtac t_fun_inj 1); +by (safe_tac prop_cs); +by ((dtac hasty_env1 1) THEN (assume_tac 1) THEN (fast_tac HOL_cs 1)); +qed "consistency_app2"; + +val prems = goal MT.thy + "ve |- e ---> v ==> (! t te. ve hastyenv te --> te |- e ===> t --> v hasty t)"; + +(* Proof by induction on the structure of evaluations *) + +by (resolve_tac (prems RL [eval_ind]) 1); +by (safe_tac HOL_cs); + +by (rtac consistency_const 1);ba 1;ba 1; +by (rtac consistency_var 1);ba 1;ba 1;ba 1; +by (rtac consistency_fn 1);ba 1;ba 1; +by (rtac consistency_fix 1);ba 1;ba 1;ba 1; +by (rtac consistency_app1 1);ba 1;ba 1;ba 1;ba 1; +by (rtac consistency_app2 1);ba 5;ba 4;ba 3;ba 2;ba 1; +qed "consistency"; + +(* ############################################################ *) +(* The Basic Consistency theorem *) +(* ############################################################ *) + +val prems = goalw MT.thy [isof_env_def,hasty_env_def] + "ve isofenv te ==> ve hastyenv te"; +by (cut_facts_tac prems 1); +by (safe_tac HOL_cs); +by (etac allE 1);be impE 1;ba 1;be exE 1;be conjE 1; +by (dtac hasty_const 1); +by ((rtac ssubst 1) THEN (assume_tac 1) THEN (assume_tac 1)); +qed "basic_consistency_lem"; + +val prems = goal MT.thy + "[| ve isofenv te; ve |- e ---> v_const(c); te |- e ===> t |] ==> c isof t"; +by (cut_facts_tac prems 1); +by (rtac hasty_elim_const 1); +by (dtac consistency 1); +by (fast_tac (HOL_cs addSIs [basic_consistency_lem]) 1); +qed "basic_consistency"; + + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/MT.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/MT.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,278 @@ +(* Title: HOL/ex/mt.thy + ID: $Id$ + Author: Jacob Frost, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Based upon the article + Robin Milner and Mads Tofte, + Co-induction in Relational Semantics, + Theoretical Computer Science 87 (1991), pages 209-220. + +Written up as + Jacob Frost, A Case Study of Co_induction in Isabelle/HOL + Report 308, Computer Lab, University of Cambridge (1993). +*) + +MT = Gfp + Sum + + +types + Const + + ExVar + Ex + + TyConst + Ty + + Clos + Val + + ValEnv + TyEnv + +arities + Const :: term + + ExVar :: term + Ex :: term + + TyConst :: term + Ty :: term + + Clos :: term + Val :: term + + ValEnv :: term + TyEnv :: term + +consts + c_app :: "[Const, Const] => Const" + + e_const :: "Const => Ex" + e_var :: "ExVar => Ex" + e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000) + e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000) + e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000) + e_const_fst :: "Ex => Const" + + t_const :: "TyConst => Ty" + t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000) + + v_const :: "Const => Val" + v_clos :: "Clos => Val" + + ve_emp :: "ValEnv" + ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50) + ve_dom :: "ValEnv => ExVar set" + ve_app :: "[ValEnv, ExVar] => Val" + + clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000) + + te_emp :: "TyEnv" + te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50) + te_app :: "[TyEnv, ExVar] => Ty" + te_dom :: "TyEnv => ExVar set" + + eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set" + eval_rel :: "((ValEnv * Ex) * Val) set" + eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50) + + elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set" + elab_rel :: "((TyEnv * Ex) * Ty) set" + elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50) + + isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50) + isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _") + + hasty_fun :: "(Val * Ty) set => (Val * Ty) set" + hasty_rel :: "(Val * Ty) set" + hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50) + hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35) + +rules + +(* + Expression constructors must be injective, distinct and it must be possible + to do induction over expressions. +*) + +(* All the constructors are injective *) + + e_const_inj "e_const(c1) = e_const(c2) ==> c1 = c2" + e_var_inj "e_var(ev1) = e_var(ev2) ==> ev1 = ev2" + e_fn_inj "fn ev1 => e1 = fn ev2 => e2 ==> ev1 = ev2 & e1 = e2" + e_fix_inj + " fix ev11e(v12) = e1 = fix ev21(ev22) = e2 ==> \ +\ ev11 = ev21 & ev12 = ev22 & e1 = e2 \ +\ " + e_app_inj "e11 @ e12 = e21 @ e22 ==> e11 = e21 & e12 = e22" + +(* All constructors are distinct *) + + e_disj_const_var "~e_const(c) = e_var(ev)" + e_disj_const_fn "~e_const(c) = fn ev => e" + e_disj_const_fix "~e_const(c) = fix ev1(ev2) = e" + e_disj_const_app "~e_const(c) = e1 @ e2" + e_disj_var_fn "~e_var(ev1) = fn ev2 => e" + e_disj_var_fix "~e_var(ev) = fix ev1(ev2) = e" + e_disj_var_app "~e_var(ev) = e1 @ e2" + e_disj_fn_fix "~fn ev1 => e1 = fix ev21(ev22) = e2" + e_disj_fn_app "~fn ev1 => e1 = e21 @ e22" + e_disj_fix_app "~fix ev11(ev12) = e1 = e21 @ e22" + +(* Strong elimination, induction on expressions *) + + e_ind + " [| !!ev. P(e_var(ev)); \ +\ !!c. P(e_const(c)); \ +\ !!ev e. P(e) ==> P(fn ev => e); \ +\ !!ev1 ev2 e. P(e) ==> P(fix ev1(ev2) = e); \ +\ !!e1 e2. P(e1) ==> P(e2) ==> P(e1 @ e2) \ +\ |] ==> \ +\ P(e) \ +\ " + +(* Types - same scheme as for expressions *) + +(* All constructors are injective *) + + t_const_inj "t_const(c1) = t_const(c2) ==> c1 = c2" + t_fun_inj "t11 -> t12 = t21 -> t22 ==> t11 = t21 & t12 = t22" + +(* All constructors are distinct, not needed so far ... *) + +(* Strong elimination, induction on types *) + + t_ind + "[| !!p. P(t_const p); !!t1 t2. P(t1) ==> P(t2) ==> P(t_fun t1 t2) |] \ +\ ==> P(t)" + + +(* Values - same scheme again *) + +(* All constructors are injective *) + + v_const_inj "v_const(c1) = v_const(c2) ==> c1 = c2" + v_clos_inj + " v_clos(<|ev1,e1,ve1|>) = v_clos(<|ev2,e2,ve2|>) ==> \ +\ ev1 = ev2 & e1 = e2 & ve1 = ve2" + +(* All constructors are distinct *) + + v_disj_const_clos "~v_const(c) = v_clos(cl)" + +(* Strong elimination, induction on values, not needed yet ... *) + + +(* + Value environments bind variables to values. Only the following trivial + properties are needed. +*) + + ve_dom_owr "ve_dom(ve + {ev |-> v}) = ve_dom(ve) Un {ev}" + + ve_app_owr1 "ve_app (ve + {ev |-> v}) ev=v" + ve_app_owr2 "~ev1=ev2 ==> ve_app (ve+{ev1 |-> v}) ev2=ve_app ve ev2" + + +(* Type Environments bind variables to types. The following trivial +properties are needed. *) + + te_dom_owr "te_dom(te + {ev |=> t}) = te_dom(te) Un {ev}" + + te_app_owr1 "te_app (te + {ev |=> t}) ev=t" + te_app_owr2 "~ev1=ev2 ==> te_app (te+{ev1 |=> t}) ev2=te_app te ev2" + + +(* The dynamic semantics is defined inductively by a set of inference +rules. These inference rules allows one to draw conclusions of the form ve +|- e ---> v, read the expression e evaluates to the value v in the value +environment ve. Therefore the relation _ |- _ ---> _ is defined in Isabelle +as the least fixpoint of the functor eval_fun below. From this definition +introduction rules and a strong elimination (induction) rule can be +derived. +*) + + eval_fun_def + " eval_fun(s) == \ +\ { pp. \ +\ (? ve c. pp=<,v_const(c)>) | \ +\ (? ve x. pp=<,ve_app ve x> & x:ve_dom(ve)) |\ +\ (? ve e x. pp=< e>,v_clos(<|x,e,ve|>)>)| \ +\ ( ? ve e x f cl. \ +\ pp=<,v_clos(cl)> & \ +\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \ +\ ) | \ +\ ( ? ve e1 e2 c1 c2. \ +\ pp=<,v_const(c_app c1 c2)> & \ +\ <,v_const(c1)>:s & <,v_const(c2)>:s \ +\ ) | \ +\ ( ? ve vem e1 e2 em xm v v2. \ +\ pp=<,v> & \ +\ <,v_clos(<|xm,em,vem|>)>:s & \ +\ <,v2>:s & \ +\ < v2},em>,v>:s \ +\ ) \ +\ }" + + eval_rel_def "eval_rel == lfp(eval_fun)" + eval_def "ve |- e ---> v == <,v>:eval_rel" + +(* The static semantics is defined in the same way as the dynamic +semantics. The relation te |- e ===> t express the expression e has the +type t in the type environment te. +*) + + elab_fun_def + "elab_fun(s) == \ +\ { pp. \ +\ (? te c t. pp=<,t> & c isof t) | \ +\ (? te x. pp=<,te_app te x> & x:te_dom(te)) | \ +\ (? te x e t1 t2. pp=< e>,t1->t2> & < t1},e>,t2>:s) | \ +\ (? te f x e t1 t2. \ +\ pp=<,t1->t2> & < t1->t2}+{x |=> t1},e>,t2>:s \ +\ ) | \ +\ (? te e1 e2 t1 t2. \ +\ pp=<,t2> & <,t1->t2>:s & <,t1>:s \ +\ ) \ +\ }" + + elab_rel_def "elab_rel == lfp(elab_fun)" + elab_def "te |- e ===> t == <,t>:elab_rel" + +(* The original correspondence relation *) + + isof_env_def + " ve isofenv te == \ +\ ve_dom(ve) = te_dom(te) & \ +\ ( ! x. \ +\ x:ve_dom(ve) --> \ +\ (? c.ve_app ve x = v_const(c) & c isof te_app te x) \ +\ ) \ +\ " + + isof_app "[| c1 isof t1->t2; c2 isof t1 |] ==> c_app c1 c2 isof t2" + +(* The extented correspondence relation *) + + hasty_fun_def + " hasty_fun(r) == \ +\ { p. \ +\ ( ? c t. p = & c isof t) | \ +\ ( ? ev e ve t te. \ +\ p = ),t> & \ +\ te |- fn ev => e ===> t & \ +\ ve_dom(ve) = te_dom(te) & \ +\ (! ev1.ev1:ve_dom(ve) --> : r) \ +\ ) \ +\ } \ +\ " + + hasty_rel_def "hasty_rel == gfp(hasty_fun)" + hasty_def "v hasty t == : hasty_rel" + hasty_env_def + " ve hastyenv te == \ +\ ve_dom(ve) = te_dom(te) & \ +\ (! x. x: ve_dom(ve) --> ve_app ve x hasty te_app te x)" + +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/NatSum.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/NatSum.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,43 @@ +(* Title: HOL/ex/natsum.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Summing natural numbers, squares and cubes. Could be continued... +*) + +val natsum_ss = arith_ss addsimps + ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac); + +(*The sum of the first n positive integers equals n(n+1)/2.*) +goal NatSum.thy "Suc(Suc(0))*sum (%i.i) (Suc n) = n*Suc(n)"; +by (simp_tac natsum_ss 1); +by (nat_ind_tac "n" 1); +by (simp_tac natsum_ss 1); +by (asm_simp_tac natsum_ss 1); +qed "sum_of_naturals"; + +goal NatSum.thy + "Suc(Suc(Suc(Suc(Suc(Suc(0))))))*sum (%i.i*i) (Suc n) = \ +\ n*Suc(n)*Suc(Suc(Suc(0))*n)"; +by (simp_tac natsum_ss 1); +by (nat_ind_tac "n" 1); +by (simp_tac natsum_ss 1); +by (asm_simp_tac natsum_ss 1); +qed "sum_of_squares"; + +goal NatSum.thy + "Suc(Suc(Suc(Suc(0))))*sum (%i.i*i*i) (Suc n) = n*n*Suc(n)*Suc(n)"; +by (simp_tac natsum_ss 1); +by (nat_ind_tac "n" 1); +by (simp_tac natsum_ss 1); +by (asm_simp_tac natsum_ss 1); +qed "sum_of_cubes"; + +(*The sum of the first n odd numbers equals n squared.*) +goal NatSum.thy "sum (%i.Suc(i+i)) n = n*n"; +by (nat_ind_tac "n" 1); +by (simp_tac natsum_ss 1); +by (asm_simp_tac natsum_ss 1); +qed "sum_of_odds"; + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/NatSum.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/NatSum.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,13 @@ +(* Title: HOL/ex/natsum.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n. +*) + +NatSum = Arith + +consts sum :: "[nat=>nat, nat] => nat" +rules sum_0 "sum f 0 = 0" + sum_Suc "sum f (Suc n) = f(n) + sum f n" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/PropLog.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/PropLog.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,234 @@ +(* Title: HOL/ex/pl.ML + ID: $Id$ + Author: Tobias Nipkow & Lawrence C Paulson + Copyright 1994 TU Muenchen & University of Cambridge + +Soundness and completeness of propositional logic w.r.t. truth-tables. + +Prove: If H|=p then G|=p where G:Fin(H) +*) + +open PropLog; + +(** Monotonicity **) +goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)"; +by (rtac lfp_mono 1); +by (REPEAT (ares_tac basic_monos 1)); +qed "thms_mono"; + +(*Rule is called I for Identity Combinator, not for Introduction*) +goal PropLog.thy "H |- p->p"; +by(best_tac (HOL_cs addIs [thms.K,thms.S,thms.MP]) 1); +qed "thms_I"; + +(** Weakening, left and right **) + +(* "[| G<=H; G |- p |] ==> H |- p" + This order of premises is convenient with RS +*) +bind_thm ("weaken_left", (thms_mono RS subsetD)); + +(* H |- p ==> insert(a,H) |- p *) +val weaken_left_insert = subset_insertI RS weaken_left; + +val weaken_left_Un1 = Un_upper1 RS weaken_left; +val weaken_left_Un2 = Un_upper2 RS weaken_left; + +goal PropLog.thy "!!H. H |- q ==> H |- p->q"; +by(fast_tac (HOL_cs addIs [thms.K,thms.MP]) 1); +qed "weaken_right"; + +(*The deduction theorem*) +goal PropLog.thy "!!H. insert p H |- q ==> H |- p->q"; +by (etac thms.induct 1); +by (fast_tac (set_cs addIs [thms_I, thms.H RS weaken_right]) 1); +by (fast_tac (set_cs addIs [thms.K RS weaken_right]) 1); +by (fast_tac (set_cs addIs [thms.S RS weaken_right]) 1); +by (fast_tac (set_cs addIs [thms.DN RS weaken_right]) 1); +by (fast_tac (set_cs addIs [thms.S RS thms.MP RS thms.MP]) 1); +qed "deduction"; + + +(* "[| insert p H |- q; H |- p |] ==> H |- q" + The cut rule - not used +*) +val cut = deduction RS thms.MP; + +(* H |- false ==> H |- p *) +val thms_falseE = weaken_right RS (thms.DN RS thms.MP); + +(* [| H |- p->false; H |- p; q: pl |] ==> H |- q *) +bind_thm ("thms_notE", (thms.MP RS thms_falseE)); + +(** The function eval **) + +val pl_ss = set_ss addsimps + (PropLog.pl.simps @ [eval2_false, eval2_var, eval2_imp] + @ [hyps_false, hyps_var, hyps_imp]); + +goalw PropLog.thy [eval_def] "tt[false] = False"; +by (simp_tac pl_ss 1); +qed "eval_false"; + +goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)"; +by (simp_tac pl_ss 1); +qed "eval_var"; + +goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])"; +by (simp_tac pl_ss 1); +qed "eval_imp"; + +val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp]; + +(*Soundness of the rules wrt truth-table semantics*) +goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p"; +by (etac thms.induct 1); +by (fast_tac (set_cs addSDs [eval_imp RS iffD1 RS mp]) 5); +by (ALLGOALS (asm_simp_tac pl_ss)); +qed "soundness"; + +(*** Towards the completeness proof ***) + +goal PropLog.thy "!!H. H |- p->false ==> H |- p->q"; +by (rtac deduction 1); +by (etac (weaken_left_insert RS thms_notE) 1); +by (rtac thms.H 1); +by (rtac insertI1 1); +qed "false_imp"; + +val [premp,premq] = goal PropLog.thy + "[| H |- p; H |- q->false |] ==> H |- (p->q)->false"; +by (rtac deduction 1); +by (rtac (premq RS weaken_left_insert RS thms.MP) 1); +by (rtac (thms.H RS thms.MP) 1); +by (rtac insertI1 1); +by (rtac (premp RS weaken_left_insert) 1); +qed "imp_false"; + +(*This formulation is required for strong induction hypotheses*) +goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)"; +by (rtac (expand_if RS iffD2) 1); +by(PropLog.pl.induct_tac "p" 1); +by (ALLGOALS (simp_tac (pl_ss addsimps [thms_I, thms.H]))); +by (fast_tac (set_cs addIs [weaken_left_Un1, weaken_left_Un2, + weaken_right, imp_false] + addSEs [false_imp]) 1); +qed "hyps_thms_if"; + +(*Key lemma for completeness; yields a set of assumptions satisfying p*) +val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p"; +by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN + rtac hyps_thms_if 2); +by (fast_tac set_cs 1); +qed "sat_thms_p"; + +(*For proving certain theorems in our new propositional logic*) +val thms_cs = + set_cs addSIs [deduction] addIs [thms.H, thms.H RS thms.MP]; + +(*The excluded middle in the form of an elimination rule*) +goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q"; +by (rtac (deduction RS deduction) 1); +by (rtac (thms.DN RS thms.MP) 1); +by (ALLGOALS (best_tac (thms_cs addSIs prems))); +qed "thms_excluded_middle"; + +(*Hard to prove directly because it requires cuts*) +val prems = goal PropLog.thy + "[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q"; +by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1); +by (REPEAT (resolve_tac (prems@[deduction]) 1)); +qed "thms_excluded_middle_rule"; + +(*** Completeness -- lemmas for reducing the set of assumptions ***) + +(*For the case hyps(p,t)-insert(#v,Y) |- p; + we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *) +goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"; +by (PropLog.pl.induct_tac "p" 1); +by (simp_tac pl_ss 1); +by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); +by (simp_tac pl_ss 1); +by (fast_tac set_cs 1); +qed "hyps_Diff"; + +(*For the case hyps(p,t)-insert(#v -> false,Y) |- p; + we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *) +goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"; +by (PropLog.pl.induct_tac "p" 1); +by (simp_tac pl_ss 1); +by (simp_tac (pl_ss setloop (split_tac [expand_if])) 1); +by (simp_tac pl_ss 1); +by (fast_tac set_cs 1); +qed "hyps_insert"; + +(** Two lemmas for use with weaken_left **) + +goal Set.thy "B-C <= insert a (B-insert a C)"; +by (fast_tac set_cs 1); +qed "insert_Diff_same"; + +goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)"; +by (fast_tac set_cs 1); +qed "insert_Diff_subset2"; + +(*The set hyps(p,t) is finite, and elements have the form #v or #v->false; + could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*) +goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})"; +by (PropLog.pl.induct_tac "p" 1); +by (ALLGOALS (simp_tac (pl_ss setloop (split_tac [expand_if])) THEN' + fast_tac (set_cs addSIs Fin.intrs@[Fin_UnI]))); +qed "hyps_finite"; + +val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; + +(*Induction on the finite set of assumptions hyps(p,t0). + We may repeatedly subtract assumptions until none are left!*) +val [sat] = goal PropLog.thy + "{} |= p ==> !t. hyps p t - hyps p t0 |- p"; +by (rtac (hyps_finite RS Fin_induct) 1); +by (simp_tac (pl_ss addsimps [sat RS sat_thms_p]) 1); +by (safe_tac set_cs); +(*Case hyps(p,t)-insert(#v,Y) |- p *) +by (rtac thms_excluded_middle_rule 1); +by (rtac (insert_Diff_same RS weaken_left) 1); +by (etac spec 1); +by (rtac (insert_Diff_subset2 RS weaken_left) 1); +by (rtac (hyps_Diff RS Diff_weaken_left) 1); +by (etac spec 1); +(*Case hyps(p,t)-insert(#v -> false,Y) |- p *) +by (rtac thms_excluded_middle_rule 1); +by (rtac (insert_Diff_same RS weaken_left) 2); +by (etac spec 2); +by (rtac (insert_Diff_subset2 RS weaken_left) 1); +by (rtac (hyps_insert RS Diff_weaken_left) 1); +by (etac spec 1); +qed "completeness_0_lemma"; + +(*The base case for completeness*) +val [sat] = goal PropLog.thy "{} |= p ==> {} |- p"; +by (rtac (Diff_cancel RS subst) 1); +by (rtac (sat RS (completeness_0_lemma RS spec)) 1); +qed "completeness_0"; + +(*A semantic analogue of the Deduction Theorem*) +val [sat] = goalw PropLog.thy [sat_def] "insert p H |= q ==> H |= p->q"; +by (simp_tac pl_ss 1); +by (cfast_tac [sat] 1); +qed "sat_imp"; + +val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p"; +by (rtac (finite RS Fin_induct) 1); +by (safe_tac (set_cs addSIs [completeness_0])); +by (rtac (weaken_left_insert RS thms.MP) 1); +by (fast_tac (set_cs addSIs [sat_imp]) 1); +by (fast_tac thms_cs 1); +qed "completeness_lemma"; + +val completeness = completeness_lemma RS spec RS mp; + +val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)"; +by (fast_tac (set_cs addSEs [soundness, finite RS completeness]) 1); +qed "thms_iff"; + +writeln"Reached end of file."; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/PropLog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/PropLog.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,45 @@ +(* Title: HOL/ex/PropLog.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Inductive definition of propositional logic. +*) + +PropLog = Finite + +datatype + 'a pl = false | var ('a) ("#_" [1000]) | "->" ('a pl,'a pl) (infixr 90) +consts + thms :: "'a pl set => 'a pl set" + "|-" :: "['a pl set, 'a pl] => bool" (infixl 50) + "|=" :: "['a pl set, 'a pl] => bool" (infixl 50) + eval2 :: "['a pl, 'a set] => bool" + eval :: "['a set, 'a pl] => bool" ("_[_]" [100,0] 100) + hyps :: "['a pl, 'a set] => 'a pl set" + +translations + "H |- p" == "p : thms(H)" + +inductive "thms(H)" + intrs + H "p:H ==> H |- p" + K "H |- p->q->p" + S "H |- (p->q->r) -> (p->q) -> p->r" + DN "H |- ((p->false) -> false) -> p" + MP "[| H |- p->q; H |- p |] ==> H |- q" + +defs + sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])" + eval_def "tt[p] == eval2 p tt" + +primrec eval2 pl + eval2_false "eval2(false) = (%x.False)" + eval2_var "eval2(#v) = (%tt.v:tt)" + eval2_imp "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)" + +primrec hyps pl + hyps_false "hyps(false) = (%tt.{})" + hyps_var "hyps(#v) = (%tt.{if v:tt then #v else #v->false})" + hyps_imp "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)" + +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Puzzle.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Puzzle.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,58 @@ +(* Title: HOL/ex/puzzle.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1993 TU Muenchen + +For puzzle.thy. A question from "Bundeswettbewerb Mathematik" + +Proof due to Herbert Ehler +*) + +(*specialized form of induction needed below*) +val prems = goal Nat.thy "[| P(0); !!n. P(Suc(n)) |] ==> !n.P(n)"; +by (EVERY1 [rtac (nat_induct RS allI), resolve_tac prems, resolve_tac prems]); +qed "nat_exh"; + +goal Puzzle.thy "! n. k=f(n) --> n <= f(n)"; +by (res_inst_tac [("n","k")] less_induct 1); +by (rtac nat_exh 1); +by (simp_tac nat_ss 1); +by (rtac impI 1); +by (rtac classical 1); +by (dtac not_leE 1); +by (subgoal_tac "f(na) <= f(f(na))" 1); +by (best_tac (HOL_cs addIs [lessD,Puzzle.f_ax,le_less_trans,le_trans]) 1); +by (fast_tac (HOL_cs addIs [Puzzle.f_ax]) 1); +bind_thm("lemma", result() RS spec RS mp); + +goal Puzzle.thy "n <= f(n)"; +by (fast_tac (HOL_cs addIs [lemma]) 1); +qed "lemma1"; + +goal Puzzle.thy "f(n) < f(Suc(n))"; +by (fast_tac (HOL_cs addIs [Puzzle.f_ax,le_less_trans,lemma1]) 1); +qed "lemma2"; + +val prems = goal Puzzle.thy "(!!n.f(n) <= f(Suc(n))) ==> m f(m) <= f(n)"; +by (res_inst_tac[("n","n")]nat_induct 1); +by (simp_tac nat_ss 1); +by (simp_tac nat_ss 1); +by (fast_tac (HOL_cs addIs (le_trans::prems)) 1); +bind_thm("mono_lemma1", result() RS mp); + +val [p1,p2] = goal Puzzle.thy + "[| !! n. f(n)<=f(Suc(n)); m<=n |] ==> f(m) <= f(n)"; +by (rtac (p2 RS le_imp_less_or_eq RS disjE) 1); +by (etac (p1 RS mono_lemma1) 1); +by (fast_tac (HOL_cs addIs [le_refl]) 1); +qed "mono_lemma"; + +val prems = goal Puzzle.thy "m <= n ==> f(m) <= f(n)"; +by (fast_tac (HOL_cs addIs ([mono_lemma,less_imp_le,lemma2]@prems)) 1); +qed "f_mono"; + +goal Puzzle.thy "f(n) = n"; +by (rtac le_anti_sym 1); +by (rtac lemma1 2); +by (fast_tac (HOL_cs addIs [Puzzle.f_ax,leI] addDs [leD,f_mono,lessD]) 1); +result(); diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Puzzle.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Puzzle.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,12 @@ +(* Title: HOL/ex/puzzle.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1993 TU Muenchen + +An question from "Bundeswettbewerb Mathematik" +*) + +Puzzle = Nat + +consts f :: "nat => nat" +rules f_ax "f(f(n)) < f(Suc(n))" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Qsort.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Qsort.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,84 @@ +(* Title: HOL/ex/qsort.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Two verifications of Quicksort +*) + +val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms); + +goal Qsort.thy "!x. mset (qsort le xs) x = mset xs x"; +by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +result(); + + +goal Qsort.thy "(Alls x:[x:xs.P(x)].Q(x)) = (Alls x:xs. P(x)-->Q(x))"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +val ss = ss addsimps [result()]; + +goal Qsort.thy + "((Alls x:xs.P(x)) & (Alls x:xs.Q(x))) = (Alls x:xs. P(x)&Q(x))"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac ss)); +val ss = ss addsimps [result()]; + +goal HOL.thy "((~P --> Q) & (P --> Q)) = Q"; +by(fast_tac HOL_cs 1); +qed "lemma"; + +goal Qsort.thy "(Alls x:qsort le xs.P(x)) = (Alls x:xs.P(x))"; +by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by(ALLGOALS(asm_simp_tac (ss addsimps [lemma]))); +val ss = ss addsimps [result()]; + +goal Qsort.thy + "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ +\ (Alls x:xs. Alls y:ys. le x y))"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac ss)); +val ss = ss addsimps [result()]; + +goal Qsort.thy + "!!le. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; +by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by(ALLGOALS(asm_full_simp_tac (ss addsimps [list_all_mem_conv]) )); +by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); +by(fast_tac HOL_cs 1); +result(); + + +(* A verification based on predicate calculus rather than combinators *) + +val sorted_Cons = + rewrite_rule [list_all_mem_conv RS eq_reflection] Sorting.sorted_Cons; + +val ss = list_ss addsimps + [Sorting.sorted_Nil,sorted_Cons, + Qsort.qsort_Nil,Qsort.qsort_Cons]; + + +goal Qsort.thy "x mem qsort le xs = x mem xs"; +by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +by(fast_tac HOL_cs 1); +val ss = ss addsimps [result()]; + +goal Qsort.thy + "sorted le (xs@ys) = (sorted le xs & sorted le ys & \ +\ (!x. x mem xs --> (!y. y mem ys --> le x y)))"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (ss setloop (split_tac [expand_if])))); +by(fast_tac HOL_cs 1); +val ss = ss addsimps [result()]; + +goal Qsort.thy + "!!xs. [| total(le); transf(le) |] ==> sorted le (qsort le xs)"; +by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1); +by(simp_tac ss 1); +by(asm_full_simp_tac (ss setloop (split_tac [expand_if])) 1); +by(rewrite_goals_tac [Sorting.total_def,Sorting.transf_def]); +by(fast_tac HOL_cs 1); +result(); diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Qsort.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Qsort.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,27 @@ +(* Title: HOL/ex/qsort.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Quicksort +*) + +Qsort = Sorting + +consts + qsort :: "[['a,'a] => bool, 'a list] => 'a list" + +rules + +qsort_Nil "qsort le [] = []" +qsort_Cons "qsort le (x#xs) = qsort le [y:xs . ~le x y] @ \ +\ (x# qsort le [y:xs . le x y])" + +(* computational induction. + The dependence of p on x but not xs is intentional. +*) +qsort_ind + "[| P([]); \ +\ !!x xs. [| P([y:xs . ~p x y]); P([y:xs . p x y]) |] ==> \ +\ P(x#xs) |] \ +\ ==> P(xs)" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/ROOT.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,32 @@ +(* Title: HOL/ex/ROOT + ID: $Id$ + Author: Tobias Nipkow, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + +Executes miscellaneous examples for Higher-Order Logic. +*) + +HOL_build_completed; (*Cause examples to fail if HOL did*) + +(writeln"Root file for HOL examples"; + proof_timing := true; + loadpath := ["ex"]; + time_use "ex/cla.ML"; + time_use "ex/meson.ML"; + time_use "ex/mesontest.ML"; + time_use_thy "String"; + time_use_thy "InSort"; + time_use_thy "Qsort"; + time_use_thy "LexProd"; + time_use_thy "Puzzle"; + time_use_thy "NatSum"; + time_use "ex/set.ML"; + time_use_thy "SList"; + time_use_thy "LList"; + time_use_thy "Acc"; + time_use_thy "PropLog"; + time_use_thy "Term"; + time_use_thy "Simult"; + time_use_thy "MT"; + writeln "END: Root file for HOL examples" +) handle _ => exit 1; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Rec.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Rec.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,5 @@ +open Rec; + +goalw thy [mono_def,Domf_def] "mono(Domf(F))"; +by (DEPTH_SOLVE (slow_step_tac set_cs 1)); +qed "mono_Domf"; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Rec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Rec.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,9 @@ +Rec = Fixedpt + +consts +fix :: "('a=>'a) => 'a" +Dom :: "(('a=>'b) => ('a=>'b)) => 'a set" +Domf :: "(('a=>'b) => ('a=>'b)) => 'a set => 'a set" +rules +Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}" +Dom_def "Dom(F) == lfp(Domf(F))" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/SList.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SList.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,397 @@ +(* Title: HOL/ex/SList.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Definition of type 'a list by a least fixed point +*) + +open SList; + +val list_con_defs = [NIL_def, CONS_def]; + +goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))"; +let val rew = rewrite_rule list_con_defs in +by (fast_tac (univ_cs addSIs (equalityI :: map rew list.intrs) + addEs [rew list.elim]) 1) +end; +qed "list_unfold"; + +(*This justifies using list in other recursive type definitions*) +goalw SList.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)"; +by (rtac lfp_mono 1); +by (REPEAT (ares_tac basic_monos 1)); +qed "list_mono"; + +(*Type checking -- list creates well-founded sets*) +goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1); +qed "list_sexp"; + +(* A <= sexp ==> list(A) <= sexp *) +bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans)); + +(*Induction for the type 'a list *) +val prems = goalw SList.thy [Nil_def,Cons_def] + "[| P(Nil); \ +\ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)"; +by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*) +by (rtac (Rep_list RS list.induct) 1); +by (REPEAT (ares_tac prems 1 + ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1)); +qed "list_induct"; + +(*Perform induction on xs. *) +fun list_ind_tac a M = + EVERY [res_inst_tac [("l",a)] list_induct M, + rename_last_tac a ["1"] (M+1)]; + +(*** Isomorphisms ***) + +goal SList.thy "inj(Rep_list)"; +by (rtac inj_inverseI 1); +by (rtac Rep_list_inverse 1); +qed "inj_Rep_list"; + +goal SList.thy "inj_onto Abs_list (list(range Leaf))"; +by (rtac inj_onto_inverseI 1); +by (etac Abs_list_inverse 1); +qed "inj_onto_Abs_list"; + +(** Distinctness of constructors **) + +goalw SList.thy list_con_defs "CONS M N ~= NIL"; +by (rtac In1_not_In0 1); +qed "CONS_not_NIL"; +bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym)); + +bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE)); +val NIL_neq_CONS = sym RS CONS_neq_NIL; + +goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil"; +by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1); +by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1)); +qed "Cons_not_Nil"; + +bind_thm ("Nil_not_Cons", (Cons_not_Nil RS not_sym)); + +bind_thm ("Cons_neq_Nil", (Cons_not_Nil RS notE)); +val Nil_neq_Cons = sym RS Cons_neq_Nil; + +(** Injectiveness of CONS and Cons **) + +goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)"; +by (fast_tac (HOL_cs addSEs [Scons_inject, make_elim In1_inject]) 1); +qed "CONS_CONS_eq"; + +bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE)); + +(*For reasoning about abstract list constructors*) +val list_cs = set_cs addIs [Rep_list] @ list.intrs + addSEs [CONS_neq_NIL,NIL_neq_CONS,CONS_inject] + addSDs [inj_onto_Abs_list RS inj_ontoD, + inj_Rep_list RS injD, Leaf_inject]; + +goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)"; +by (fast_tac list_cs 1); +qed "Cons_Cons_eq"; +bind_thm ("Cons_inject", (Cons_Cons_eq RS iffD1 RS conjE)); + +val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)"; +by (rtac (major RS setup_induction) 1); +by (etac list.induct 1); +by (ALLGOALS (fast_tac list_cs)); +qed "CONS_D"; + +val prems = goalw SList.thy [CONS_def,In1_def] + "CONS M N: sexp ==> M: sexp & N: sexp"; +by (cut_facts_tac prems 1); +by (fast_tac (set_cs addSDs [Scons_D]) 1); +qed "sexp_CONS_D"; + + +(*Basic ss with constructors and their freeness*) +val list_free_simps = [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, + CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq] + @ list.intrs; +val list_free_ss = HOL_ss addsimps list_free_simps; + +goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N"; +by (etac list.induct 1); +by (ALLGOALS (asm_simp_tac list_free_ss)); +qed "not_CONS_self"; + +goal SList.thy "!x. l ~= x#l"; +by (list_ind_tac "l" 1); +by (ALLGOALS (asm_simp_tac list_free_ss)); +qed "not_Cons_self"; + + +goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)"; +by(list_ind_tac "xs" 1); +by(simp_tac list_free_ss 1); +by(asm_simp_tac list_free_ss 1); +by(REPEAT(resolve_tac [exI,refl,conjI] 1)); +qed "neq_Nil_conv"; + +(** Conversion rules for List_case: case analysis operator **) + +goalw SList.thy [List_case_def,NIL_def] "List_case c h NIL = c"; +by (rtac Case_In0 1); +qed "List_case_NIL"; + +goalw SList.thy [List_case_def,CONS_def] "List_case c h (CONS M N) = h M N"; +by (simp_tac (HOL_ss addsimps [Split,Case_In1]) 1); +qed "List_case_CONS"; + +(*** List_rec -- by wf recursion on pred_sexp ***) + +(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not + hold if pred_sexp^+ were changed to pred_sexp. *) + +val List_rec_unfold = [List_rec_def, wf_pred_sexp RS wf_trancl] MRS def_wfrec + |> standard; + +(** pred_sexp lemmas **) + +goalw SList.thy [CONS_def,In1_def] + "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; +by (asm_simp_tac pred_sexp_ss 1); +qed "pred_sexp_CONS_I1"; + +goalw SList.thy [CONS_def,In1_def] + "!!M. [| M: sexp; N: sexp |] ==> : pred_sexp^+"; +by (asm_simp_tac pred_sexp_ss 1); +qed "pred_sexp_CONS_I2"; + +val [prem] = goal SList.thy + " : pred_sexp^+ ==> \ +\ : pred_sexp^+ & : pred_sexp^+"; +by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS + subsetD RS SigmaE2)) 1); +by (etac (sexp_CONS_D RS conjE) 1); +by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2, + prem RSN (2, trans_trancl RS transD)] 1)); +qed "pred_sexp_CONS_D"; + +(** Conversion rules for List_rec **) + +goal SList.thy "List_rec NIL c h = c"; +by (rtac (List_rec_unfold RS trans) 1); +by (simp_tac (HOL_ss addsimps [List_case_NIL]) 1); +qed "List_rec_NIL"; + +goal SList.thy "!!M. [| M: sexp; N: sexp |] ==> \ +\ List_rec (CONS M N) c h = h M N (List_rec N c h)"; +by (rtac (List_rec_unfold RS trans) 1); +by (asm_simp_tac + (HOL_ss addsimps [List_case_CONS, list.CONS_I, pred_sexp_CONS_I2, + cut_apply])1); +qed "List_rec_CONS"; + +(*** list_rec -- by List_rec ***) + +val Rep_list_in_sexp = + [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD; + +local + val list_rec_simps = list_free_simps @ + [List_rec_NIL, List_rec_CONS, + Abs_list_inverse, Rep_list_inverse, + Rep_list, rangeI, inj_Leaf, Inv_f_f, + sexp.LeafI, Rep_list_in_sexp] +in + val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def] + "list_rec Nil c h = c" + (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]); + + val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def] + "list_rec (a#l) c h = h a l (list_rec l c h)" + (fn _=> [simp_tac (HOL_ss addsimps list_rec_simps) 1]); +end; + +val list_simps = [List_rec_NIL, List_rec_CONS, + list_rec_Nil, list_rec_Cons]; +val list_ss = list_free_ss addsimps list_simps; + + +(*Type checking. Useful?*) +val major::A_subset_sexp::prems = goal SList.thy + "[| M: list(A); \ +\ A<=sexp; \ +\ c: C(NIL); \ +\ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) \ +\ |] ==> List_rec M c h : C(M :: 'a item)"; +val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD; +val sexp_A_I = A_subset_sexp RS subsetD; +by (rtac (major RS list.induct) 1); +by (ALLGOALS(asm_simp_tac (list_ss addsimps ([sexp_A_I,sexp_ListA_I]@prems)))); +qed "List_rec_type"; + +(** Generalized map functionals **) + +goalw SList.thy [Rep_map_def] "Rep_map f Nil = NIL"; +by (rtac list_rec_Nil 1); +qed "Rep_map_Nil"; + +goalw SList.thy [Rep_map_def] + "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)"; +by (rtac list_rec_Cons 1); +qed "Rep_map_Cons"; + +goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)"; +by (rtac list_induct 1); +by(ALLGOALS(asm_simp_tac list_ss)); +qed "Rep_map_type"; + +goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil"; +by (rtac List_rec_NIL 1); +qed "Abs_map_NIL"; + +val prems = goalw SList.thy [Abs_map_def] + "[| M: sexp; N: sexp |] ==> \ +\ Abs_map g (CONS M N) = g(M) # Abs_map g N"; +by (REPEAT (resolve_tac (List_rec_CONS::prems) 1)); +qed "Abs_map_CONS"; + +(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *) +val [rew] = goal SList.thy + "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c"; +by (rewtac rew); +by (rtac list_rec_Nil 1); +qed "def_list_rec_Nil"; + +val [rew] = goal SList.thy + "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)"; +by (rewtac rew); +by (rtac list_rec_Cons 1); +qed "def_list_rec_Cons"; + +fun list_recs def = + [standard (def RS def_list_rec_Nil), + standard (def RS def_list_rec_Cons)]; + +(*** Unfolding the basic combinators ***) + +val [null_Nil,null_Cons] = list_recs null_def; +val [_,hd_Cons] = list_recs hd_def; +val [_,tl_Cons] = list_recs tl_def; +val [ttl_Nil,ttl_Cons] = list_recs ttl_def; +val [append_Nil,append_Cons] = list_recs append_def; +val [mem_Nil, mem_Cons] = list_recs mem_def; +val [map_Nil,map_Cons] = list_recs map_def; +val [list_case_Nil,list_case_Cons] = list_recs list_case_def; +val [filter_Nil,filter_Cons] = list_recs filter_def; +val [list_all_Nil,list_all_Cons] = list_recs list_all_def; + +val list_ss = arith_ss addsimps + [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq, + list_rec_Nil, list_rec_Cons, + null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons, + mem_Nil, mem_Cons, + list_case_Nil, list_case_Cons, + append_Nil, append_Cons, + map_Nil, map_Cons, + list_all_Nil, list_all_Cons, + filter_Nil, filter_Cons]; + + +(** @ - append **) + +goal SList.thy "(xs@ys)@zs = xs@(ys@zs)"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac list_ss)); +qed "append_assoc"; + +goal SList.thy "xs @ [] = xs"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac list_ss)); +qed "append_Nil2"; + +(** mem **) + +goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +qed "mem_append"; + +goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +qed "mem_filter"; + +(** list_all **) + +goal SList.thy "(Alls x:xs.True) = True"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac list_ss)); +qed "list_all_True"; + +goal SList.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac list_ss)); +qed "list_all_conj"; + +goal SList.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (list_ss setloop (split_tac [expand_if])))); +by(fast_tac HOL_cs 1); +qed "list_all_mem_conv"; + + +(** The functional "map" **) + +val map_simps = [Abs_map_NIL, Abs_map_CONS, + Rep_map_Nil, Rep_map_Cons, + map_Nil, map_Cons]; +val map_ss = list_free_ss addsimps map_simps; + +val [major,A_subset_sexp,minor] = goal SList.thy + "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \ +\ ==> Rep_map f (Abs_map g M) = M"; +by (rtac (major RS list.induct) 1); +by (ALLGOALS (asm_simp_tac(map_ss addsimps [sexp_A_I,sexp_ListA_I,minor]))); +qed "Abs_map_inverse"; + +(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*) + +(** list_case **) + +goal SList.thy + "P(list_case a f xs) = ((xs=[] --> P(a)) & \ +\ (!y ys. xs=y#ys --> P(f y ys)))"; +by(list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac list_ss)); +by(fast_tac HOL_cs 1); +qed "expand_list_case"; + + +(** Additional mapping lemmas **) + +goal SList.thy "map (%x.x) xs = xs"; +by (list_ind_tac "xs" 1); +by (ALLGOALS (asm_simp_tac map_ss)); +qed "map_ident"; + +goal SList.thy "map f (xs@ys) = map f xs @ map f ys"; +by (list_ind_tac "xs" 1); +by (ALLGOALS (asm_simp_tac (map_ss addsimps [append_Nil,append_Cons]))); +qed "map_append"; + +goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)"; +by (list_ind_tac "xs" 1); +by (ALLGOALS (asm_simp_tac map_ss)); +qed "map_compose"; + +goal SList.thy "!!f. (!!x. f(x): sexp) ==> \ +\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"; +by (list_ind_tac "xs" 1); +by(ALLGOALS(asm_simp_tac(map_ss addsimps + [Rep_map_type,list_sexp RS subsetD]))); +qed "Abs_Rep_map"; + +val list_ss = list_ss addsimps + [mem_append, mem_filter, append_assoc, append_Nil2, map_ident, + list_all_True, list_all_conj]; + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/SList.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/SList.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,120 @@ +(* Title: HOL/ex/SList.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Definition of type 'a list (strict lists) by a least fixed point + +We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z) +and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z) +so that list can serve as a "functor" for defining other recursive types +*) + +SList = Sexp + + +types + 'a list + +arities + list :: (term) term + + +consts + + list :: "'a item set => 'a item set" + Rep_list :: "'a list => 'a item" + Abs_list :: "'a item => 'a list" + NIL :: "'a item" + CONS :: "['a item, 'a item] => 'a item" + Nil :: "'a list" + "#" :: "['a, 'a list] => 'a list" (infixr 65) + List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b" + List_rec :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b" + list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b" + list_rec :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b" + Rep_map :: "('b => 'a item) => ('b list => 'a item)" + Abs_map :: "('a item => 'b) => 'a item => 'b list" + null :: "'a list => bool" + hd :: "'a list => 'a" + tl,ttl :: "'a list => 'a list" + mem :: "['a, 'a list] => bool" (infixl 55) + list_all :: "('a => bool) => ('a list => bool)" + map :: "('a=>'b) => ('a list => 'b list)" + "@" :: "['a list, 'a list] => 'a list" (infixr 65) + filter :: "['a => bool, 'a list] => 'a list" + + (* list Enumeration *) + + "[]" :: "'a list" ("[]") + "@list" :: "args => 'a list" ("[(_)]") + + (* Special syntax for list_all and filter *) + "@Alls" :: "[idt, 'a list, bool] => bool" ("(2Alls _:_./ _)" 10) + "@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])") + +translations + "[x, xs]" == "x#[xs]" + "[x]" == "x#[]" + "[]" == "Nil" + + "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs" + + "[x:xs . P]" == "filter (%x.P) xs" + "Alls x:xs.P" == "list_all (%x.P) xs" + +defs + (* Defining the Concrete Constructors *) + NIL_def "NIL == In0(Numb(0))" + CONS_def "CONS M N == In1(M $ N)" + +inductive "list(A)" + intrs + NIL_I "NIL: list(A)" + CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)" + +rules + (* Faking a Type Definition ... *) + Rep_list "Rep_list(xs): list(range(Leaf))" + Rep_list_inverse "Abs_list(Rep_list(xs)) = xs" + Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M" + + +defs + (* Defining the Abstract Constructors *) + Nil_def "Nil == Abs_list(NIL)" + Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))" + + List_case_def "List_case c d == Case (%x.c) (Split d)" + + (* list Recursion -- the trancl is Essential; see list.ML *) + + List_rec_def + "List_rec M c d == wfrec (trancl pred_sexp) M \ +\ (List_case (%g.c) (%x y g. d x y (g y)))" + + list_rec_def + "list_rec l c d == \ +\ List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)" + + (* Generalized Map Functionals *) + + Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)" + Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)" + + null_def "null(xs) == list_rec xs True (%x xs r.False)" + hd_def "hd(xs) == list_rec xs (@x.True) (%x xs r.x)" + tl_def "tl(xs) == list_rec xs (@xs.True) (%x xs r.xs)" + (* a total version of tl: *) + ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)" + + mem_def "x mem xs == \ +\ list_rec xs False (%y ys r. if y=x then True else r)" + list_all_def "list_all P xs == list_rec xs True (%x l r. P(x) & r)" + map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)" + append_def "xs@ys == list_rec xs ys (%x l r. x#r)" + filter_def "filter P xs == \ +\ list_rec xs [] (%x xs r. if P(x) then x#r else r)" + + list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)" + +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Simult.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Simult.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,287 @@ +(* Title: HOL/ex/Simult.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Primitives for simultaneous recursive type definitions + includes worked example of trees & forests + +This is essentially the same data structure that on ex/term.ML, which is +simpler because it uses list as a new type former. The approach in this +file may be superior for other simultaneous recursions. +*) + +open Simult; + +(*** Monotonicity and unfolding of the function ***) + +goal Simult.thy "mono(%Z. A <*> Part Z In1 \ +\ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"; +by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono, + Part_mono] 1)); +qed "TF_fun_mono"; + +val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski); + +goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)"; +by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1)); +qed "TF_mono"; + +goalw Simult.thy [TF_def] "TF(sexp) <= sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I, sexp_In1I] + addSEs [PartE]) 1); +qed "TF_sexp"; + +(* A <= sexp ==> TF(A) <= sexp *) +val TF_subset_sexp = standard + (TF_mono RS (TF_sexp RSN (2,subset_trans))); + + +(** Elimination -- structural induction on the set TF **) + +val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def]; + +val major::prems = goalw Simult.thy TF_Rep_defs + "[| i: TF(A); \ +\ !!M N. [| M: A; N: Part (TF A) In1; R(N) |] ==> R(TCONS M N); \ +\ R(FNIL); \ +\ !!M N. [| M: Part (TF A) In0; N: Part (TF A) In1; R(M); R(N) \ +\ |] ==> R(FCONS M N) \ +\ |] ==> R(i)"; +by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1); +by (fast_tac (set_cs addIs (prems@[PartI]) + addEs [usumE, uprodE, PartE]) 1); +qed "TF_induct"; + +(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*) +val prems = goalw Simult.thy [Part_def] + "! M: TF(A). (M: Part (TF A) In0 --> P(M)) & (M: Part (TF A) In1 --> Q(M)) \ +\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))"; +by (cfast_tac prems 1); +qed "TF_induct_lemma"; + +val uplus_cs = set_cs addSIs [PartI] + addSDs [In0_inject, In1_inject] + addSEs [In0_neq_In1, In1_neq_In0, PartE]; + +(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *) + +(*Induction on TF with separate predicates P, Q*) +val prems = goalw Simult.thy TF_Rep_defs + "[| !!M N. [| M: A; N: Part (TF A) In1; Q(N) |] ==> P(TCONS M N); \ +\ Q(FNIL); \ +\ !!M N. [| M: Part (TF A) In0; N: Part (TF A) In1; P(M); Q(N) \ +\ |] ==> Q(FCONS M N) \ +\ |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))"; +by (rtac (ballI RS TF_induct_lemma) 1); +by (etac TF_induct 1); +by (rewrite_goals_tac TF_Rep_defs); +by (ALLGOALS (fast_tac (uplus_cs addIs prems))); +(*29 secs??*) +qed "Tree_Forest_induct"; + +(*Induction for the abstract types 'a tree, 'a forest*) +val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def] + "[| !!x ts. Q(ts) ==> P(Tcons x ts); \ +\ Q(Fnil); \ +\ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons t ts) \ +\ |] ==> (! t. P(t)) & (! ts. Q(ts))"; +by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"), + ("Q1","%z.Q(Abs_Forest(z))")] + (Tree_Forest_induct RS conjE) 1); +(*Instantiates ?A1 to range(Leaf). *) +by (fast_tac (set_cs addSEs [Rep_Tree_inverse RS subst, + Rep_Forest_inverse RS subst] + addSIs [Rep_Tree,Rep_Forest]) 4); +(*Cannot use simplifier: the rewrites work in the wrong direction!*) +by (ALLGOALS (fast_tac (set_cs addSEs [Abs_Tree_inverse RS subst, + Abs_Forest_inverse RS subst] + addSIs prems))); +qed "tree_forest_induct"; + + + +(*** Isomorphisms ***) + +goal Simult.thy "inj(Rep_Tree)"; +by (rtac inj_inverseI 1); +by (rtac Rep_Tree_inverse 1); +qed "inj_Rep_Tree"; + +goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)"; +by (rtac inj_onto_inverseI 1); +by (etac Abs_Tree_inverse 1); +qed "inj_onto_Abs_Tree"; + +goal Simult.thy "inj(Rep_Forest)"; +by (rtac inj_inverseI 1); +by (rtac Rep_Forest_inverse 1); +qed "inj_Rep_Forest"; + +goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)"; +by (rtac inj_onto_inverseI 1); +by (etac Abs_Forest_inverse 1); +qed "inj_onto_Abs_Forest"; + +(** Introduction rules for constructors **) + +(* c : A <*> Part (TF A) In1 + <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *) +val TF_I = TF_unfold RS equalityD2 RS subsetD; + +(*For reasoning about the representation*) +val TF_Rep_cs = uplus_cs addIs [TF_I, uprodI, usum_In0I, usum_In1I] + addSEs [Scons_inject]; + +val prems = goalw Simult.thy TF_Rep_defs + "[| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0"; +by (fast_tac (TF_Rep_cs addIs prems) 1); +qed "TCONS_I"; + +(* FNIL is a TF(A) -- this also justifies the type definition*) +goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1"; +by (fast_tac TF_Rep_cs 1); +qed "FNIL_I"; + +val prems = goalw Simult.thy TF_Rep_defs + "[| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \ +\ FCONS M N : Part (TF A) In1"; +by (fast_tac (TF_Rep_cs addIs prems) 1); +qed "FCONS_I"; + +(** Injectiveness of TCONS and FCONS **) + +goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)"; +by (fast_tac TF_Rep_cs 1); +qed "TCONS_TCONS_eq"; +bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE)); + +goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)"; +by (fast_tac TF_Rep_cs 1); +qed "FCONS_FCONS_eq"; +bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE)); + +(** Distinctness of TCONS, FNIL and FCONS **) + +goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL"; +by (fast_tac TF_Rep_cs 1); +qed "TCONS_not_FNIL"; +bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym)); + +bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE)); +val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL; + +goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL"; +by (fast_tac TF_Rep_cs 1); +qed "FCONS_not_FNIL"; +bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym)); + +bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE)); +val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL; + +goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L"; +by (fast_tac TF_Rep_cs 1); +qed "TCONS_not_FCONS"; +bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym)); + +bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE)); +val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS; + +(*???? Too many derived rules ???? + Automatically generate symmetric forms? Always expand TF_Rep_defs? *) + +(** Injectiveness of Tcons and Fcons **) + +(*For reasoning about abstract constructors*) +val TF_cs = set_cs addSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I] + addSEs [TCONS_inject, FCONS_inject, + TCONS_neq_FNIL, FNIL_neq_TCONS, + FCONS_neq_FNIL, FNIL_neq_FCONS, + TCONS_neq_FCONS, FCONS_neq_TCONS] + addSDs [inj_onto_Abs_Tree RS inj_ontoD, + inj_onto_Abs_Forest RS inj_ontoD, + inj_Rep_Tree RS injD, inj_Rep_Forest RS injD, + Leaf_inject]; + +goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)"; +by (fast_tac TF_cs 1); +qed "Tcons_Tcons_eq"; +bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE)); + +goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil"; +by (fast_tac TF_cs 1); +qed "Fcons_not_Fnil"; + +bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE); +val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil; + + +(** Injectiveness of Fcons **) + +goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)"; +by (fast_tac TF_cs 1); +qed "Fcons_Fcons_eq"; +bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE); + + +(*** TF_rec -- by wf recursion on pred_sexp ***) + +val TF_rec_unfold = + wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec); + +(** conversion rules for TF_rec **) + +goalw Simult.thy [TCONS_def] + "!!M N. [| M: sexp; N: sexp |] ==> \ +\ TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)"; +by (rtac (TF_rec_unfold RS trans) 1); +by (simp_tac (HOL_ss addsimps [Case_In0, Split]) 1); +by (asm_simp_tac (pred_sexp_ss addsimps [In0_def]) 1); +qed "TF_rec_TCONS"; + +goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c"; +by (rtac (TF_rec_unfold RS trans) 1); +by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1); +qed "TF_rec_FNIL"; + +goalw Simult.thy [FCONS_def] + "!!M N. [| M: sexp; N: sexp |] ==> \ +\ TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)"; +by (rtac (TF_rec_unfold RS trans) 1); +by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1); +by (asm_simp_tac (pred_sexp_ss addsimps [CONS_def,In1_def]) 1); +qed "TF_rec_FCONS"; + + +(*** tree_rec, forest_rec -- by TF_rec ***) + +val Rep_Tree_in_sexp = + [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans), + Rep_Tree] MRS subsetD; +val Rep_Forest_in_sexp = + [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans), + Rep_Forest] MRS subsetD; + +val tf_rec_simps = [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS, + TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest, + Rep_Tree_inverse, Rep_Forest_inverse, + Abs_Tree_inverse, Abs_Forest_inverse, + inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI, + Rep_Tree_in_sexp, Rep_Forest_in_sexp]; +val tf_rec_ss = HOL_ss addsimps tf_rec_simps; + +goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def] + "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)"; +by (simp_tac tf_rec_ss 1); +qed "tree_rec_Tcons"; + +goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c"; +by (simp_tac tf_rec_ss 1); +qed "forest_rec_Fnil"; + +goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def] + "forest_rec (Fcons t tf) b c d = \ +\ d t tf (tree_rec t b c d) (forest_rec tf b c d)"; +by (simp_tac tf_rec_ss 1); +qed "forest_rec_Cons"; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Simult.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Simult.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,82 @@ +(* Title: HOL/ex/Simult + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +A simultaneous recursive type definition: trees & forests + +This is essentially the same data structure that on ex/term.ML, which is +simpler because it uses list as a new type former. The approach in this +file may be superior for other simultaneous recursions. + +The inductive definition package does not help defining this sort of mutually +recursive data structure because it uses Inl, Inr instead of In0, In1. +*) + +Simult = SList + + +types 'a tree + 'a forest + +arities tree,forest :: (term)term + +consts + TF :: "'a item set => 'a item set" + FNIL :: "'a item" + TCONS,FCONS :: "['a item, 'a item] => 'a item" + Rep_Tree :: "'a tree => 'a item" + Abs_Tree :: "'a item => 'a tree" + Rep_Forest :: "'a forest => 'a item" + Abs_Forest :: "'a item => 'a forest" + Tcons :: "['a, 'a forest] => 'a tree" + Fcons :: "['a tree, 'a forest] => 'a forest" + Fnil :: "'a forest" + TF_rec :: "['a item, ['a item , 'a item, 'b]=>'b, \ +\ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b" + tree_rec :: "['a tree, ['a, 'a forest, 'b]=>'b, \ +\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b" + forest_rec :: "['a forest, ['a, 'a forest, 'b]=>'b, \ +\ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b" + +defs + (*the concrete constants*) + TCONS_def "TCONS M N == In0(M $ N)" + FNIL_def "FNIL == In1(NIL)" + FCONS_def "FCONS M N == In1(CONS M N)" + (*the abstract constants*) + Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))" + Fnil_def "Fnil == Abs_Forest(FNIL)" + Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))" + + TF_def "TF(A) == lfp(%Z. A <*> Part Z In1 \ +\ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))" + +rules + (*faking a type definition for tree...*) + Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0" + Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t" + Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z" + (*faking a type definition for forest...*) + Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1" + Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts" + Abs_Forest_inverse + "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z" + + +defs + (*recursion*) + TF_rec_def + "TF_rec M b c d == wfrec (trancl pred_sexp) M \ +\ (Case (Split(%x y g. b x y (g y))) \ +\ (List_case (%g.c) (%x y g. d x y (g x) (g y))))" + + tree_rec_def + "tree_rec t b c d == \ +\ TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \ +\ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" + + forest_rec_def + "forest_rec tf b c d == \ +\ TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) \ +\ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Sorting.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Sorting.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,26 @@ +(* Title: HOL/ex/sorting.ML + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Some general lemmas +*) + +val sorting_ss = list_ss addsimps + [Sorting.mset_Nil,Sorting.mset_Cons, + Sorting.sorted_Nil,Sorting.sorted_Cons, + Sorting.sorted1_Nil,Sorting.sorted1_One,Sorting.sorted1_Cons]; + +goal Sorting.thy "!x.mset (xs@ys) x = mset xs x + mset ys x"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if])))); +qed "mset_app_distr"; + +goal Sorting.thy "!x. mset [x:xs. ~p(x)] x + mset [x:xs.p(x)] x = \ +\ mset xs x"; +by(list.induct_tac "xs" 1); +by(ALLGOALS(asm_simp_tac (sorting_ss setloop (split_tac [expand_if])))); +qed "mset_compl_add"; + +val sorting_ss = sorting_ss addsimps + [mset_app_distr, mset_compl_add]; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Sorting.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Sorting.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,31 @@ +(* Title: HOL/ex/sorting.thy + ID: $Id$ + Author: Tobias Nipkow + Copyright 1994 TU Muenchen + +Specification of sorting +*) + +Sorting = List + +consts + sorted1:: "[['a,'a] => bool, 'a list] => bool" + sorted :: "[['a,'a] => bool, 'a list] => bool" + mset :: "'a list => ('a => nat)" + total :: "(['a,'a] => bool) => bool" + transf :: "(['a,'a] => bool) => bool" + +rules + +sorted1_Nil "sorted1 f []" +sorted1_One "sorted1 f [x]" +sorted1_Cons "sorted1 f (Cons x (y#zs)) = (f x y & sorted1 f (y#zs))" + +sorted_Nil "sorted le []" +sorted_Cons "sorted le (x#xs) = ((Alls y:xs. le x y) & sorted le xs)" + +mset_Nil "mset [] y = 0" +mset_Cons "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)" + +total_def "total r == (!x y. r x y | r y x)" +transf_def "transf f == (!x y z. f x y & f y z --> f x z)" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/String.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/String.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,22 @@ +val string_ss = list_ss addsimps (String.nibble.simps @ String.char.simps); + +goal String.thy "hd(''ABCD'') = CHR ''A''"; +by(simp_tac string_ss 1); +result(); + +goal String.thy "hd(''ABCD'') ~= CHR ''B''"; +by(simp_tac string_ss 1); +result(); + +goal String.thy "''ABCD'' ~= ''ABCX''"; +by(simp_tac string_ss 1); +result(); + +goal String.thy "''ABCD'' = ''ABCD''"; +by(simp_tac string_ss 1); +result(); + +goal String.thy + "''ABCDEFGHIJKLMNOPQRSTUVWXYZ'' ~= ''ABCDEFGHIJKLMNOPQRSTUVWXY''"; +by(simp_tac string_ss 1); +result(); diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/String.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/String.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,90 @@ +(* Title: HOL/String.thy + ID: $Id$ + +Hex chars. Strings. +*) + +String = List + + +datatype + nibble = H00 | H01 | H02 | H03 | H04 | H05 | H06 | H07 + | H08 | H09 | H0A | H0B | H0C | H0D | H0E | H0F + +datatype + char = Char (nibble, nibble) + +types + string = "char list" + +syntax + "_Char" :: "xstr => char" ("CHR _") + "_String" :: "xstr => string" ("_") + +end + + +ML + +local + open Syntax; + + val ssquote = enclose "''" "''"; + + + (* chars *) + + val zero = ord "0"; + val ten = ord "A" - 10; + + fun mk_nib n = + const ("H0" ^ chr (n + (if n <= 9 then zero else ten))); + + fun dest_nib (Const (c, _)) = + (case explode c of + ["H", "0", h] => ord h - (if h <= "9" then zero else ten) + | _ => raise Match) + | dest_nib _ = raise Match; + + fun dest_nibs t1 t2 = chr (dest_nib t1 * 16 + dest_nib t2); + + + fun mk_char c = + const "Char" $ mk_nib (ord c div 16) $ mk_nib (ord c mod 16); + + fun dest_char (Const ("Char", _) $ t1 $ t2) = dest_nibs t1 t2 + | dest_char _ = raise Match; + + + fun char_tr (*"_Char"*) [Free (c, _)] = + if size c = 1 then mk_char c + else error ("Bad character: " ^ quote c) + | char_tr (*"_Char"*) ts = raise_term "char_tr" ts; + + fun char_tr' (*"Char"*) [t1, t2] = + const "_Char" $ free (ssquote (dest_nibs t1 t2)) + | char_tr' (*"Char"*) _ = raise Match; + + + (* strings *) + + fun mk_string [] = const constrainC $ const "[]" $ const "string" + | mk_string (t :: ts) = const "op #" $ t $ mk_string ts; + + fun dest_string (Const ("[]", _)) = [] + | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs + | dest_string _ = raise Match; + + + fun string_tr (*"_String"*) [Free (txt, _)] = + mk_string (map mk_char (explode txt)) + | string_tr (*"_String"*) ts = raise_term "string_tr" ts; + + fun cons_tr' (*"op #"*) [c, cs] = + const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs))) + | cons_tr' (*"op #"*) ts = raise Match; + +in + val parse_translation = [("_Char", char_tr), ("_String", string_tr)]; + val print_translation = [("Char", char_tr'), ("op #", cons_tr')]; +end; + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Term.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Term.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,165 @@ +(* Title: HOL/ex/Term + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Terms over a given alphabet -- function applications; illustrates list functor + (essentially the same type as in Trees & Forests) +*) + +open Term; + +(*** Monotonicity and unfolding of the function ***) + +goal Term.thy "term(A) = A <*> list(term(A))"; +by (fast_tac (univ_cs addSIs (equalityI :: term.intrs) + addEs [term.elim]) 1); +qed "term_unfold"; + +(*This justifies using term in other recursive type definitions*) +goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)"; +by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1)); +qed "term_mono"; + +(** Type checking -- term creates well-founded sets **) + +goalw Term.thy term.defs "term(sexp) <= sexp"; +by (rtac lfp_lowerbound 1); +by (fast_tac (univ_cs addIs [sexp.SconsI, list_sexp RS subsetD]) 1); +qed "term_sexp"; + +(* A <= sexp ==> term(A) <= sexp *) +bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans)); + + +(** Elimination -- structural induction on the set term(A) **) + +(*Induction for the set term(A) *) +val [major,minor] = goal Term.thy + "[| M: term(A); \ +\ !!x zs. [| x: A; zs: list(term(A)); zs: list({x.R(x)}) \ +\ |] ==> R(x$zs) \ +\ |] ==> R(M)"; +by (rtac (major RS term.induct) 1); +by (REPEAT (eresolve_tac ([minor] @ + ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1)); +(*Proof could also use mono_Int RS subsetD RS IntE *) +qed "Term_induct"; + +(*Induction on term(A) followed by induction on list *) +val major::prems = goal Term.thy + "[| M: term(A); \ +\ !!x. [| x: A |] ==> R(x$NIL); \ +\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); R(x$zs) \ +\ |] ==> R(x $ CONS z zs) \ +\ |] ==> R(M)"; +by (rtac (major RS Term_induct) 1); +by (etac list.induct 1); +by (REPEAT (ares_tac prems 1)); +qed "Term_induct2"; + +(*** Structural Induction on the abstract type 'a term ***) + +val list_all_ss = map_ss addsimps [list_all_Nil, list_all_Cons]; + +val Rep_term_in_sexp = + Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD); + +(*Induction for the abstract type 'a term*) +val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def] + "[| !!x ts. list_all R ts ==> R(App x ts) \ +\ |] ==> R(t)"; +by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*) +by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1); +by (rtac (Rep_term RS Term_induct) 1); +by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS + list_subset_sexp, range_Leaf_subset_sexp] 1 + ORELSE etac rev_subsetD 1)); +by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")] + (Abs_map_inverse RS subst) 1); +by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1); +by (etac Abs_term_inverse 1); +by (etac rangeE 1); +by (hyp_subst_tac 1); +by (resolve_tac prems 1); +by (etac list.induct 1); +by (etac CollectE 2); +by (stac Abs_map_CONS 2); +by (etac conjunct1 2); +by (etac rev_subsetD 2); +by (rtac list_subset_sexp 2); +by (fast_tac set_cs 2); +by (ALLGOALS (asm_simp_tac list_all_ss)); +qed "term_induct"; + +(*Induction for the abstract type 'a term*) +val prems = goal Term.thy + "[| !!x. R(App x Nil); \ +\ !!x t ts. R(App x ts) ==> R(App x (t#ts)) \ +\ |] ==> R(t)"; +by (rtac term_induct 1); (*types force good instantiation*) +by (etac rev_mp 1); +by (rtac list_induct 1); (*types force good instantiation*) +by (ALLGOALS (asm_simp_tac (list_all_ss addsimps prems))); +qed "term_induct2"; + +(*Perform induction on xs. *) +fun term_ind2_tac a i = + EVERY [res_inst_tac [("t",a)] term_induct2 i, + rename_last_tac a ["1","s"] (i+1)]; + + + +(*** Term_rec -- by wf recursion on pred_sexp ***) + +val Term_rec_unfold = + wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec); + +(** conversion rules **) + +val [prem] = goal Term.thy + "N: list(term(A)) ==> \ +\ !M. : pred_sexp^+ --> \ +\ Abs_map (cut h (pred_sexp^+) M) N = \ +\ Abs_map h N"; +by (rtac (prem RS list.induct) 1); +by (simp_tac list_all_ss 1); +by (strip_tac 1); +by (etac (pred_sexp_CONS_D RS conjE) 1); +by (asm_simp_tac (list_all_ss addsimps [trancl_pred_sexpD1, cut_apply]) 1); +qed "Abs_map_lemma"; + +val [prem1,prem2,A_subset_sexp] = goal Term.thy + "[| M: sexp; N: list(term(A)); A<=sexp |] ==> \ +\ Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)"; +by (rtac (Term_rec_unfold RS trans) 1); +by (simp_tac (HOL_ss addsimps + [Split, + prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl, + prem1, prem2 RS rev_subsetD, list_subset_sexp, + term_subset_sexp, A_subset_sexp])1); +qed "Term_rec"; + +(*** term_rec -- by Term_rec ***) + +local + val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy) + [("f","Rep_term")] Rep_map_type; + val Rep_Tlist = Rep_term RS Rep_map_type1; + val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec)); + + (*Now avoids conditional rewriting with the premise N: list(term(A)), + since A will be uninstantiated and will cause rewriting to fail. *) + val term_rec_ss = HOL_ss + addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse), + Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, + inj_Leaf, Inv_f_f, + Abs_Rep_map, map_ident, sexp.LeafI] +in + +val term_rec = prove_goalw Term.thy + [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def] + "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)" + (fn _ => [simp_tac term_rec_ss 1]) + +end; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/Term.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Term.thy Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,55 @@ +(* Title: HOL/ex/Term + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Terms over a given alphabet -- function applications; illustrates list functor + (essentially the same type as in Trees & Forests) + +There is no constructor APP because it is simply cons ($) +*) + +Term = SList + + +types 'a term + +arities term :: (term)term + +consts + term :: "'a item set => 'a item set" + Rep_term :: "'a term => 'a item" + Abs_term :: "'a item => 'a term" + Rep_Tlist :: "'a term list => 'a item" + Abs_Tlist :: "'a item => 'a term list" + App :: "['a, ('a term)list] => 'a term" + Term_rec :: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b" + term_rec :: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b" + +inductive "term(A)" + intrs + APP_I "[| M: A; N : list(term(A)) |] ==> M$N : term(A)" + monos "[list_mono]" + +defs + (*defining abstraction/representation functions for term list...*) + Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)" + Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)" + + (*defining the abstract constants*) + App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))" + + (*list recursion*) + Term_rec_def + "Term_rec M d == wfrec (trancl pred_sexp) M \ +\ (Split(%x y g. d x y (Abs_map g y)))" + + term_rec_def + "term_rec t d == \ +\ Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)" + +rules + (*faking a type definition for term...*) + Rep_term "Rep_term(n): term(range(Leaf))" + Rep_term_inverse "Abs_term(Rep_term(t)) = t" + Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M" +end diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/cla.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/cla.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,455 @@ +(* Title: HOL/ex/cla + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Higher-Order Logic: predicate calculus problems + +Taken from FOL/cla.ML; beware of precedence of = vs <-> +*) + +writeln"File HOL/ex/cla."; + +goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)"; +by (fast_tac HOL_cs 1); +result(); + +(*If and only if*) + +goal HOL.thy "(P=Q) = (Q=P::bool)"; +by (fast_tac HOL_cs 1); +result(); + +goal HOL.thy "~ (P = (~P))"; +by (fast_tac HOL_cs 1); +result(); + + +(*Sample problems from + F. J. Pelletier, + Seventy-Five Problems for Testing Automatic Theorem Provers, + J. Automated Reasoning 2 (1986), 191-216. + Errata, JAR 4 (1988), 236-236. + +The hardest problems -- judging by experience with several theorem provers, +including matrix ones -- are 34 and 43. +*) + +writeln"Pelletier's examples"; +(*1*) +goal HOL.thy "(P-->Q) = (~Q --> ~P)"; +by (fast_tac HOL_cs 1); +result(); + +(*2*) +goal HOL.thy "(~ ~ P) = P"; +by (fast_tac HOL_cs 1); +result(); + +(*3*) +goal HOL.thy "~(P-->Q) --> (Q-->P)"; +by (fast_tac HOL_cs 1); +result(); + +(*4*) +goal HOL.thy "(~P-->Q) = (~Q --> P)"; +by (fast_tac HOL_cs 1); +result(); + +(*5*) +goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; +by (fast_tac HOL_cs 1); +result(); + +(*6*) +goal HOL.thy "P | ~ P"; +by (fast_tac HOL_cs 1); +result(); + +(*7*) +goal HOL.thy "P | ~ ~ ~ P"; +by (fast_tac HOL_cs 1); +result(); + +(*8. Peirce's law*) +goal HOL.thy "((P-->Q) --> P) --> P"; +by (fast_tac HOL_cs 1); +result(); + +(*9*) +goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; +by (fast_tac HOL_cs 1); +result(); + +(*10*) +goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"; +by (fast_tac HOL_cs 1); +result(); + +(*11. Proved in each direction (incorrectly, says Pelletier!!) *) +goal HOL.thy "P=P::bool"; +by (fast_tac HOL_cs 1); +result(); + +(*12. "Dijkstra's law"*) +goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; +by (fast_tac HOL_cs 1); +result(); + +(*13. Distributive law*) +goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))"; +by (fast_tac HOL_cs 1); +result(); + +(*14*) +goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))"; +by (fast_tac HOL_cs 1); +result(); + +(*15*) +goal HOL.thy "(P --> Q) = (~P | Q)"; +by (fast_tac HOL_cs 1); +result(); + +(*16*) +goal HOL.thy "(P-->Q) | (Q-->P)"; +by (fast_tac HOL_cs 1); +result(); + +(*17*) +goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Classical Logic: examples with quantifiers"; + +goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; +by (fast_tac HOL_cs 1); +result(); + +goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))"; +by (fast_tac HOL_cs 1); +result(); + +goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)"; +by (fast_tac HOL_cs 1); +result(); + +goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)"; +by (fast_tac HOL_cs 1); +result(); + +(*From Wishnu Prasetya*) +goal HOL.thy + "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \ +\ --> p(t) | r(t)"; +by (fast_tac HOL_cs 1); +result(); + + +writeln"Problems requiring quantifier duplication"; + +(*Needs multiple instantiation of the quantifier.*) +goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; +by (deepen_tac HOL_cs 1 1); +result(); + +(*Needs double instantiation of the quantifier*) +goal HOL.thy "? x. P(x) --> P(a) & P(b)"; +by (deepen_tac HOL_cs 1 1); +result(); + +goal HOL.thy "? z. P(z) --> (! x. P(x))"; +by (deepen_tac HOL_cs 1 1); +result(); + +goal HOL.thy "? x. (? y. P(y)) --> P(x)"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Hard examples with quantifiers"; + +writeln"Problem 18"; +goal HOL.thy "? y. ! x. P(y)-->P(x)"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 19"; +goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 20"; +goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \ +\ --> (? x y. P(x) & Q(y)) --> (? z. R(z))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 21"; +goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 22"; +goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 23"; +goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 24"; +goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \ +\ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \ +\ --> (? x. P(x)&R(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 25"; +goal HOL.thy "(? x. P(x)) & \ +\ (! x. L(x) --> ~ (M(x) & R(x))) & \ +\ (! x. P(x) --> (M(x) & L(x))) & \ +\ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ +\ --> (? x. Q(x)&P(x))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 26"; +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 27"; +goal HOL.thy "(? x. P(x) & ~Q(x)) & \ +\ (! x. P(x) --> R(x)) & \ +\ (! x. M(x) & L(x) --> P(x)) & \ +\ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \ +\ --> (! x. M(x) --> ~L(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 28. AMENDED"; +goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \ +\ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \ +\ ((? x.S(x)) --> (! x. L(x) --> M(x))) \ +\ --> (! x. P(x) & L(x) --> M(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; +goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ +\ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ +\ (! x y. F(x) & G(y) --> H(x) & J(y)))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 30"; +goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \ +\ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ +\ --> (! x. S(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 31"; +goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \ +\ (? x. L(x) & P(x)) & \ +\ (! x. ~ R(x) --> M(x)) \ +\ --> (? x. L(x) & M(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 32"; +goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \ +\ (! x. S(x) & R(x) --> L(x)) & \ +\ (! x. M(x) --> R(x)) \ +\ --> (! x. P(x) & M(x) --> L(x))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 33"; +goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ +\ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 34 AMENDED (TWICE!!) NOT PROVED AUTOMATICALLY"; +(*Andrews's challenge*) +goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ +\ ((? x. q(x)) = (! y. p(y)))) = \ +\ ((? x. ! y. q(x) = q(y)) = \ +\ ((? x. p(x)) = (! y. q(y))))"; +by (deepen_tac HOL_cs 3 1); +(*slower with smaller bounds*) +result(); + +writeln"Problem 35"; +goal HOL.thy "? x y. P x y --> (! u v. P u v)"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 36"; +goal HOL.thy "(! x. ? y. J x y) & \ +\ (! x. ? y. G x y) & \ +\ (! x y. J x y | G x y --> \ +\ (! z. J y z | G y z --> H x z)) \ +\ --> (! x. ? y. H x y)"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 37"; +goal HOL.thy "(! z. ? w. ! x. ? y. \ +\ (P x z -->P y w) & P y z & (P y w --> (? u.Q u w))) & \ +\ (! x z. ~(P x z) --> (? y. Q y z)) & \ +\ ((? x y. Q x y) --> (! x. R x x)) \ +\ --> (! x. ? y. R x y)"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 38"; +goal HOL.thy + "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ +\ (? z. ? w. p(z) & r x w & r w z)) = \ +\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ +\ (~p(a) | ~(? y. p(y) & r x y) | \ +\ (? z. ? w. p(z) & r x w & r w z)))"; + +writeln"Problem 39"; +goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 40. AMENDED"; +goal HOL.thy "(? y. ! x. F x y = F x x) \ +\ --> ~ (! x. ? y. ! z. F z y = (~ F z x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 41"; +goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x)) \ +\ --> ~ (? z. ! x. f x z)"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 42"; +goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; +by (deepen_tac HOL_cs 3 1); +result(); + +writeln"Problem 43 NOT PROVED AUTOMATICALLY"; +goal HOL.thy + "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool))) \ +\ --> (! x. (! y. q x y = (q y x::bool)))"; + + +writeln"Problem 44"; +goal HOL.thy "(! x. f(x) --> \ +\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ +\ (? x. j(x) & (! y. g(y) --> h x y)) \ +\ --> (? x. j(x) & ~f(x))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 45"; +goal HOL.thy + "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ +\ --> (! y. g(y) & h x y --> k(y))) & \ +\ ~ (? y. l(y) & k(y)) & \ +\ (? x. f(x) & (! y. h x y --> l(y)) \ +\ & (! y. g(y) & h x y --> j x y)) \ +\ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; +by (best_tac HOL_cs 1); +result(); + + +writeln"Problems (mainly) involving equality or functions"; + +writeln"Problem 48"; +goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 49 NOT PROVED AUTOMATICALLY"; +(*Hard because it involves substitution for Vars; + the type constraint ensures that x,y,z have the same type as a,b,u. *) +goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \ +\ --> (! u::'a.P(u))"; +by (Classical.safe_tac HOL_cs); +by (res_inst_tac [("x","a")] allE 1); +by (assume_tac 1); +by (res_inst_tac [("x","b")] allE 1); +by (assume_tac 1); +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 50"; +(*What has this to do with equality?*) +goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 51"; +goal HOL.thy + "(? z w. ! x y. P x y = (x=z & y=w)) --> \ +\ (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 52"; +(*Almost the same as 51. *) +goal HOL.thy + "(? z w. ! x y. P x y = (x=z & y=w)) --> \ +\ (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))"; +by (best_tac HOL_cs 1); +result(); + +writeln"Problem 55"; + +(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). + fast_tac DISCOVERS who killed Agatha. *) +goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \ +\ (killed agatha agatha | killed butler agatha | killed charles agatha) & \ +\ (!x y. killed x y --> hates x y & ~richer x y) & \ +\ (!x. hates agatha x --> ~hates charles x) & \ +\ (hates agatha agatha & hates agatha charles) & \ +\ (!x. lives(x) & ~richer x agatha --> hates butler x) & \ +\ (!x. hates agatha x --> hates butler x) & \ +\ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \ +\ killed ?who agatha"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 56"; +goal HOL.thy + "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 57"; +goal HOL.thy + "P (f a b) (f b c) & P (f b c) (f a c) & \ +\ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Problem 58 NOT PROVED AUTOMATICALLY"; +goal HOL.thy "(! x y. f(x)=g(y)) --> (! x y. f(f(x))=f(g(y)))"; +val f_cong = read_instantiate [("f","f")] arg_cong; +by (fast_tac (HOL_cs addIs [f_cong]) 1); +result(); + +writeln"Problem 59"; +goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))"; +by (deepen_tac HOL_cs 1 1); +result(); + +writeln"Problem 60"; +goal HOL.thy + "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; +by (fast_tac HOL_cs 1); +result(); + +writeln"Reached end of file."; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/meson.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/meson.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,417 @@ +(* Title: HOL/ex/meson + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +The MESON resolution proof procedure for HOL + +When making clauses, avoids using the rewriter -- instead uses RS recursively +*) + +writeln"File HOL/ex/meson."; + +(*Prove theorems using fast_tac*) +fun prove_fun s = + prove_goal HOL.thy s + (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]); + +(**** Negation Normal Form ****) + +(*** de Morgan laws ***) + +val not_conjD = prove_fun "~(P&Q) ==> ~P | ~Q"; +val not_disjD = prove_fun "~(P|Q) ==> ~P & ~Q"; +val not_notD = prove_fun "~~P ==> P"; +val not_allD = prove_fun "~(! x.P(x)) ==> ? x. ~P(x)"; +val not_exD = prove_fun "~(? x.P(x)) ==> ! x. ~P(x)"; + + +(*** Removal of --> and <-> (positive and negative occurrences) ***) + +val imp_to_disjD = prove_fun "P-->Q ==> ~P | Q"; +val not_impD = prove_fun "~(P-->Q) ==> P & ~Q"; + +val iff_to_disjD = prove_fun "P=Q ==> (~P | Q) & (~Q | P)"; + +(*Much more efficient than (P & ~Q) | (Q & ~P) for computing CNF*) +val not_iffD = prove_fun "~(P=Q) ==> (P | Q) & (~P | ~Q)"; + + +(**** Pulling out the existential quantifiers ****) + +(*** Conjunction ***) + +val conj_exD1 = prove_fun "(? x.P(x)) & Q ==> ? x. P(x) & Q"; +val conj_exD2 = prove_fun "P & (? x.Q(x)) ==> ? x. P & Q(x)"; + +(*** Disjunction ***) + +(*DO NOT USE with forall-Skolemization: makes fewer schematic variables!! + With ex-Skolemization, makes fewer Skolem constants*) +val disj_exD = prove_fun "(? x.P(x)) | (? x.Q(x)) ==> ? x. P(x) | Q(x)"; + +val disj_exD1 = prove_fun "(? x.P(x)) | Q ==> ? x. P(x) | Q"; +val disj_exD2 = prove_fun "P | (? x.Q(x)) ==> ? x. P | Q(x)"; + + +(**** Skolemization -- pulling "?" over "!" ****) + +(*"Axiom" of Choice, proved using the description operator*) +val [major] = goal HOL.thy + "! x. ? y. Q x y ==> ? f. ! x. Q x (f x)"; +by (cut_facts_tac [major] 1); +by (fast_tac (HOL_cs addEs [selectI]) 1); +qed "choice"; + + +(***** Generating clauses for the Meson Proof Procedure *****) + +(*** Disjunctions ***) + +val disj_assoc = prove_fun "(P|Q)|R ==> P|(Q|R)"; + +val disj_comm = prove_fun "P|Q ==> Q|P"; + +val disj_FalseD1 = prove_fun "False|P ==> P"; +val disj_FalseD2 = prove_fun "P|False ==> P"; + +(*** Generation of contrapositives ***) + +(*Inserts negated disjunct after removing the negation; P is a literal*) +val [major,minor] = goal HOL.thy "~P|Q ==> ((~P==>P) ==> Q)"; +by (rtac (major RS disjE) 1); +by (rtac notE 1); +by (etac minor 2); +by (ALLGOALS assume_tac); +qed "make_neg_rule"; + +(*For Plaisted's "Postive refinement" of the MESON procedure*) +val [major,minor] = goal HOL.thy "~P|Q ==> (P ==> Q)"; +by (rtac (major RS disjE) 1); +by (rtac notE 1); +by (rtac minor 2); +by (ALLGOALS assume_tac); +qed "make_refined_neg_rule"; + +(*P should be a literal*) +val [major,minor] = goal HOL.thy "P|Q ==> ((P==>~P) ==> Q)"; +by (rtac (major RS disjE) 1); +by (rtac notE 1); +by (etac minor 1); +by (ALLGOALS assume_tac); +qed "make_pos_rule"; + +(*** Generation of a goal clause -- put away the final literal ***) + +val [major,minor] = goal HOL.thy "~P ==> ((~P==>P) ==> False)"; +by (rtac notE 1); +by (rtac minor 2); +by (ALLGOALS (rtac major)); +qed "make_neg_goal"; + +val [major,minor] = goal HOL.thy "P ==> ((P==>~P) ==> False)"; +by (rtac notE 1); +by (rtac minor 1); +by (ALLGOALS (rtac major)); +qed "make_pos_goal"; + + +(**** Lemmas for forward proof (like congruence rules) ****) + +(*NOTE: could handle conjunctions (faster?) by + nf(th RS conjunct2) RS (nf(th RS conjunct1) RS conjI) *) +val major::prems = goal HOL.thy + "[| P'&Q'; P' ==> P; Q' ==> Q |] ==> P&Q"; +by (rtac (major RS conjE) 1); +by (rtac conjI 1); +by (ALLGOALS (eresolve_tac prems)); +qed "conj_forward"; + +val major::prems = goal HOL.thy + "[| P'|Q'; P' ==> P; Q' ==> Q |] ==> P|Q"; +by (rtac (major RS disjE) 1); +by (ALLGOALS (dresolve_tac prems)); +by (ALLGOALS (eresolve_tac [disjI1,disjI2])); +qed "disj_forward"; + +val major::prems = goal HOL.thy + "[| ! x. P'(x); !!x. P'(x) ==> P(x) |] ==> ! x. P(x)"; +by (rtac allI 1); +by (resolve_tac prems 1); +by (rtac (major RS spec) 1); +qed "all_forward"; + +val major::prems = goal HOL.thy + "[| ? x. P'(x); !!x. P'(x) ==> P(x) |] ==> ? x. P(x)"; +by (rtac (major RS exE) 1); +by (rtac exI 1); +by (eresolve_tac prems 1); +qed "ex_forward"; + + +(**** Operators for forward proof ****) + +(*raises exception if no rules apply -- unlike RL*) +fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) + | tryres (th, []) = raise THM("tryres", 0, [th]); + +val prop_of = #prop o rep_thm; + +(*Permits forward proof from rules that discharge assumptions*) +fun forward_res nf state = + case Sequence.pull + (tapply(ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)), + state)) + of Some(th,_) => th + | None => raise THM("forward_res", 0, [state]); + + +(*Negation Normal Form*) +val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD, + not_impD, not_iffD, not_allD, not_exD, not_notD]; +fun make_nnf th = make_nnf (tryres(th, nnf_rls)) + handle THM _ => + forward_res make_nnf + (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward])) + handle THM _ => th; + + +(*Are any of the constants in "bs" present in the term?*) +fun has_consts bs = + let fun has (Const(a,_)) = a mem bs + | has (f$u) = has f orelse has u + | has (Abs(_,_,t)) = has t + | has _ = false + in has end; + +(*Pull existential quantifiers (Skolemization)*) +fun skolemize th = + if not (has_consts ["Ex"] (prop_of th)) then th + else skolemize (tryres(th, [choice, conj_exD1, conj_exD2, + disj_exD, disj_exD1, disj_exD2])) + handle THM _ => + skolemize (forward_res skolemize + (tryres (th, [conj_forward, disj_forward, all_forward]))) + handle THM _ => forward_res skolemize (th RS ex_forward); + + +(**** Clause handling ****) + +fun literals (Const("Trueprop",_) $ P) = literals P + | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q + | literals (Const("not",_) $ P) = [(false,P)] + | literals P = [(true,P)]; + +(*number of literals in a term*) +val nliterals = length o literals; + +(*to delete tautologous clauses*) +fun taut_lits [] = false + | taut_lits ((flg,t)::ts) = (not flg,t) mem ts orelse taut_lits ts; + +val is_taut = taut_lits o literals o prop_of; + + +(*Generation of unique names -- maxidx cannot be relied upon to increase! + Cannot rely on "variant", since variables might coincide when literals + are joined to make a clause... + 19 chooses "U" as the first variable name*) +val name_ref = ref 19; + +(*Replaces universally quantified variables by FREE variables -- because + assumptions may not contain scheme variables. Later, call "generalize". *) +fun freeze_spec th = + let val sth = th RS spec + val newname = (name_ref := !name_ref + 1; + radixstring(26, "A", !name_ref)) + in read_instantiate [("x", newname)] sth end; + +fun resop nf [prem] = resolve_tac (nf prem) 1; + +(*Conjunctive normal form, detecting tautologies early. + Strips universal quantifiers and breaks up conjunctions. *) +fun cnf_aux seen (th,ths) = + if taut_lits (literals(prop_of th) @ seen) then ths + else if not (has_consts ["All","op &"] (prop_of th)) then th::ths + else (*conjunction?*) + cnf_aux seen (th RS conjunct1, + cnf_aux seen (th RS conjunct2, ths)) + handle THM _ => (*universal quant?*) + cnf_aux seen (freeze_spec th, ths) + handle THM _ => (*disjunction?*) + let val tac = + (METAHYPS (resop (cnf_nil seen)) 1) THEN + (STATE (fn st' => + METAHYPS (resop (cnf_nil (literals (concl_of st') @ seen))) 1)) + in Sequence.list_of_s (tapply(tac, th RS disj_forward)) @ ths + end +and cnf_nil seen th = cnf_aux seen (th,[]); + +(*Top-level call to cnf -- it's safe to reset name_ref*) +fun cnf (th,ths) = + (name_ref := 19; cnf (th RS conjunct1, cnf (th RS conjunct2, ths)) + handle THM _ => (*not a conjunction*) cnf_aux [] (th, ths)); + +(**** Removal of duplicate literals ****) + +(*Version for removal of duplicate literals*) +val major::prems = goal HOL.thy + "[| P'|Q'; P' ==> P; [| Q'; P==>False |] ==> Q |] ==> P|Q"; +by (rtac (major RS disjE) 1); +by (rtac disjI1 1); +by (rtac (disjCI RS disj_comm) 2); +by (ALLGOALS (eresolve_tac prems)); +by (etac notE 1); +by (assume_tac 1); +qed "disj_forward2"; + +(*Forward proof, passing extra assumptions as theorems to the tactic*) +fun forward_res2 nf hyps state = + case Sequence.pull + (tapply(REPEAT + (METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1), + state)) + of Some(th,_) => th + | None => raise THM("forward_res2", 0, [state]); + +(*Remove duplicates in P|Q by assuming ~P in Q + rls (initially []) accumulates assumptions of the form P==>False*) +fun nodups_aux rls th = nodups_aux rls (th RS disj_assoc) + handle THM _ => tryres(th,rls) + handle THM _ => tryres(forward_res2 nodups_aux rls (th RS disj_forward2), + [disj_FalseD1, disj_FalseD2, asm_rl]) + handle THM _ => th; + +(*Remove duplicate literals, if there are any*) +fun nodups th = + if null(findrep(literals(prop_of th))) then th + else nodups_aux [] th; + + +(**** Generation of contrapositives ****) + +(*Associate disjuctions to right -- make leftmost disjunct a LITERAL*) +fun assoc_right th = assoc_right (th RS disj_assoc) + handle THM _ => th; + +(*Must check for negative literal first!*) +val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule]; +val refined_clause_rules = [disj_assoc, make_refined_neg_rule, make_pos_rule]; + +(*Create a goal or support clause, conclusing False*) +fun make_goal th = (*Must check for negative literal first!*) + make_goal (tryres(th, clause_rules)) + handle THM _ => tryres(th, [make_neg_goal, make_pos_goal]); + +(*Sort clauses by number of literals*) +fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2); + +(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*) +fun sort_clauses ths = sort fewerlits (filter (not o is_taut) ths); + +(*Convert all suitable free variables to schematic variables*) +fun generalize th = forall_elim_vars 0 (forall_intr_frees th); + +(*make clauses from a list of theorems*) +fun make_clauses ths = + sort_clauses (map (generalize o nodups) (foldr cnf (ths,[]))); + +(*Create a Horn clause*) +fun make_horn crules th = make_horn crules (tryres(th,crules)) + handle THM _ => th; + +(*Generate Horn clauses for all contrapositives of a clause*) +fun add_contras crules (th,hcs) = + let fun rots (0,th) = hcs + | rots (k,th) = zero_var_indexes (make_horn crules th) :: + rots(k-1, assoc_right (th RS disj_comm)) + in case nliterals(prop_of th) of + 1 => th::hcs + | n => rots(n, assoc_right th) + end; + +(*Convert a list of clauses to (contrapositive) Horn clauses*) +fun make_horns ths = foldr (add_contras clause_rules) (ths,[]); + +(*Find an all-negative support clause*) +fun is_negative th = forall (not o #1) (literals (prop_of th)); + +val neg_clauses = filter is_negative; + + +(***** MESON PROOF PROCEDURE *****) + +fun rhyps (Const("==>",_) $ (Const("Trueprop",_) $ A) $ phi, + As) = rhyps(phi, A::As) + | rhyps (_, As) = As; + +(** Detecting repeated assumptions in a subgoal **) + +(*The stringtree detects repeated assumptions.*) +fun ins_term (net,t) = Net.insert_term((t,t), net, op aconv); + +(*detects repetitions in a list of terms*) +fun has_reps [] = false + | has_reps [_] = false + | has_reps [t,u] = (t aconv u) + | has_reps ts = (foldl ins_term (Net.empty, ts); false) + handle INSERT => true; + +(*Loop checking: FAIL if trying to prove the same thing twice + -- repeated literals*) +val check_tac = SUBGOAL (fn (prem,_) => + if has_reps (rhyps(prem,[])) then no_tac else all_tac); + +(* net_resolve_tac actually made it slower... *) +fun prolog_step_tac horns i = + (assume_tac i APPEND resolve_tac horns i) THEN + (ALLGOALS check_tac) THEN + (TRYALL eq_assume_tac); + + +(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*) +local fun addconcl(prem,sz) = size_of_term (Logic.strip_assums_concl prem) + sz +in +fun size_of_subgoals st = foldr addconcl (prems_of st, 0) +end; + +(*Could simply use nprems_of, which would count remaining subgoals -- no + discrimination as to their size! With BEST_FIRST, fails for problem 41.*) + +fun best_prolog_tac sizef horns = + BEST_FIRST (has_fewer_prems 1, sizef) (prolog_step_tac horns 1); + +fun depth_prolog_tac horns = + DEPTH_FIRST (has_fewer_prems 1) (prolog_step_tac horns 1); + +(*Return all negative clauses, as possible goal clauses*) +fun gocls cls = map make_goal (neg_clauses cls); + + +fun skolemize_tac prems = + cut_facts_tac (map (skolemize o make_nnf) prems) THEN' + REPEAT o (etac exE); + +fun MESON sko_tac = SELECT_GOAL + (EVERY1 [rtac ccontr, + METAHYPS (fn negs => + EVERY1 [skolemize_tac negs, + METAHYPS (sko_tac o make_clauses)])]); + +fun best_meson_tac sizef = + MESON (fn cls => + resolve_tac (gocls cls) 1 + THEN_BEST_FIRST + (has_fewer_prems 1, sizef, + prolog_step_tac (make_horns cls) 1)); + +(*First, breaks the goal into independent units*) +val safe_meson_tac = + SELECT_GOAL (TRY (safe_tac HOL_cs) THEN + TRYALL (best_meson_tac size_of_subgoals)); + +val depth_meson_tac = + MESON (fn cls => EVERY [resolve_tac (gocls cls) 1, + depth_prolog_tac (make_horns cls)]); + +writeln"Reached end of file."; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/mesontest.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/mesontest.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,496 @@ +(* Title: HOL/ex/meson + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Test data for the MESON proof procedure + (Excludes the equality problems 51, 52, 56, 58) + +show_hyps:=false; + +by (rtac ccontr 1); +val [prem] = gethyps 1; +val nnf = make_nnf prem; +val xsko = skolemize nnf; +by (cut_facts_tac [xsko] 1 THEN REPEAT (etac exE 1)); +val [_,sko] = gethyps 1; +val clauses = make_clauses [sko]; +val horns = make_horns clauses; +val go::_ = neg_clauses clauses; + +goal HOL.thy "False"; +by (rtac (make_goal go) 1); +by (prolog_step_tac horns 1); +by (depth_prolog_tac horns); +by (best_prolog_tac size_of_subgoals horns); +*) + +writeln"File HOL/ex/meson-test."; + +(**** Interactive examples ****) + +(*Generate nice names for Skolem functions*) +Logic.auto_rename := true; Logic.set_rename_prefix "a"; + + +writeln"Problem 25"; +goal HOL.thy "(? x. P(x)) & \ +\ (! x. L(x) --> ~ (M(x) & R(x))) & \ +\ (! x. P(x) --> (M(x) & L(x))) & \ +\ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ +\ --> (? x. Q(x)&P(x))"; +by (rtac ccontr 1); +val [prem25] = gethyps 1; +val nnf25 = make_nnf prem25; +val xsko25 = skolemize nnf25; +by (cut_facts_tac [xsko25] 1 THEN REPEAT (etac exE 1)); +val [_,sko25] = gethyps 1; +val clauses25 = make_clauses [sko25]; (*7 clauses*) +val horns25 = make_horns clauses25; (*16 Horn clauses*) +val go25::_ = neg_clauses clauses25; + +goal HOL.thy "False"; +by (rtac (make_goal go25) 1); +by (depth_prolog_tac horns25); + + +writeln"Problem 26"; +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; +by (rtac ccontr 1); +val [prem26] = gethyps 1; +val nnf26 = make_nnf prem26; +val xsko26 = skolemize nnf26; +by (cut_facts_tac [xsko26] 1 THEN REPEAT (etac exE 1)); +val [_,sko26] = gethyps 1; +val clauses26 = make_clauses [sko26]; (*9 clauses*) +val horns26 = make_horns clauses26; (*24 Horn clauses*) +val go26::_ = neg_clauses clauses26; + +goal HOL.thy "False"; +by (rtac (make_goal go26) 1); +by (depth_prolog_tac horns26); (*6 secs*) + + + +writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; +goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ +\ --> (! x. (! y. q x y = (q y x::bool)))"; +by (rtac ccontr 1); +val [prem43] = gethyps 1; +val nnf43 = make_nnf prem43; +val xsko43 = skolemize nnf43; +by (cut_facts_tac [xsko43] 1 THEN REPEAT (etac exE 1)); +val [_,sko43] = gethyps 1; +val clauses43 = make_clauses [sko43]; (*6*) +val horns43 = make_horns clauses43; (*16*) +val go43::_ = neg_clauses clauses43; + +goal HOL.thy "False"; +by (rtac (make_goal go43) 1); +by (best_prolog_tac size_of_subgoals horns43); +(*8.7 secs*) + + +(*Restore variable name preservation*) +Logic.auto_rename := false; + + +(**** Batch test data ****) + +(*Sample problems from + F. J. Pelletier, + Seventy-Five Problems for Testing Automatic Theorem Provers, + J. Automated Reasoning 2 (1986), 191-216. + Errata, JAR 4 (1988), 236-236. + +The hardest problems -- judging by experience with several theorem provers, +including matrix ones -- are 34 and 43. +*) + +writeln"Pelletier's examples"; +(*1*) +goal HOL.thy "(P-->Q) = (~Q --> ~P)"; +by (safe_meson_tac 1); +result(); + +(*2*) +goal HOL.thy "(~ ~ P) = P"; +by (safe_meson_tac 1); +result(); + +(*3*) +goal HOL.thy "~(P-->Q) --> (Q-->P)"; +by (safe_meson_tac 1); +result(); + +(*4*) +goal HOL.thy "(~P-->Q) = (~Q --> P)"; +by (safe_meson_tac 1); +result(); + +(*5*) +goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))"; +by (safe_meson_tac 1); +result(); + +(*6*) +goal HOL.thy "P | ~ P"; +by (safe_meson_tac 1); +result(); + +(*7*) +goal HOL.thy "P | ~ ~ ~ P"; +by (safe_meson_tac 1); +result(); + +(*8. Peirce's law*) +goal HOL.thy "((P-->Q) --> P) --> P"; +by (safe_meson_tac 1); +result(); + +(*9*) +goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"; +by (safe_meson_tac 1); +result(); + +(*10*) +goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)"; +by (safe_meson_tac 1); +result(); + +(*11. Proved in each direction (incorrectly, says Pelletier!!) *) +goal HOL.thy "P=(P::bool)"; +by (safe_meson_tac 1); +result(); + +(*12. "Dijkstra's law"*) +goal HOL.thy "((P = Q) = R) = (P = (Q = R))"; +by (best_meson_tac size_of_subgoals 1); +result(); + +(*13. Distributive law*) +goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))"; +by (safe_meson_tac 1); +result(); + +(*14*) +goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))"; +by (safe_meson_tac 1); +result(); + +(*15*) +goal HOL.thy "(P --> Q) = (~P | Q)"; +by (safe_meson_tac 1); +result(); + +(*16*) +goal HOL.thy "(P-->Q) | (Q-->P)"; +by (safe_meson_tac 1); +result(); + +(*17*) +goal HOL.thy "((P & (Q-->R))-->S) = ((~P | Q | S) & (~P | ~R | S))"; +by (safe_meson_tac 1); +result(); + +writeln"Classical Logic: examples with quantifiers"; + +goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))"; +by (safe_meson_tac 1); +result(); + +goal HOL.thy "(? x. P-->Q(x)) = (P --> (? x.Q(x)))"; +by (safe_meson_tac 1); +result(); + +goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)"; +by (safe_meson_tac 1); +result(); + +goal HOL.thy "((! x.P(x)) | Q) = (! x. P(x) | Q)"; +by (safe_meson_tac 1); +result(); + +writeln"Testing the complete tactic"; + +(*Not provable by pc_tac: needs multiple instantiation of !. + Could be proved trivially by a PROLOG interpreter*) +goal HOL.thy "(! x. P(x)-->P(f(x))) & P(d)-->P(f(f(f(d))))"; +by (safe_meson_tac 1); +result(); + +(*Not provable by pc_tac: needs double instantiation of EXISTS*) +goal HOL.thy "? x. P(x) --> P(a) & P(b)"; +by (safe_meson_tac 1); +result(); + +goal HOL.thy "? z. P(z) --> (! x. P(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Hard examples with quantifiers"; + +writeln"Problem 18"; +goal HOL.thy "? y. ! x. P(y)-->P(x)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 19"; +goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 20"; +goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w))) \ +\ --> (? x y. P(x) & Q(y)) --> (? z. R(z))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 21"; +goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 22"; +goal HOL.thy "(! x. P = Q(x)) --> (P = (! x. Q(x)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 23"; +goal HOL.thy "(! x. P | Q(x)) = (P | (! x. Q(x)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 24"; +goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) & \ +\ ~(? x.P(x)) --> (? x.Q(x)) & (! x. Q(x)|R(x) --> S(x)) \ +\ --> (? x. P(x)&R(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 25"; +goal HOL.thy "(? x. P(x)) & \ +\ (! x. L(x) --> ~ (M(x) & R(x))) & \ +\ (! x. P(x) --> (M(x) & L(x))) & \ +\ ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x))) \ +\ --> (? x. Q(x)&P(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 26"; +goal HOL.thy "((? x. p(x)) = (? x. q(x))) & \ +\ (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \ +\ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 27"; +goal HOL.thy "(? x. P(x) & ~Q(x)) & \ +\ (! x. P(x) --> R(x)) & \ +\ (! x. M(x) & L(x) --> P(x)) & \ +\ ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x))) \ +\ --> (! x. M(x) --> ~L(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 28. AMENDED"; +goal HOL.thy "(! x. P(x) --> (! x. Q(x))) & \ +\ ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) & \ +\ ((? x.S(x)) --> (! x. L(x) --> M(x))) \ +\ --> (! x. P(x) & L(x) --> M(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 29. Essentially the same as Principia Mathematica *11.71"; +goal HOL.thy "(? x. F(x)) & (? y. G(y)) \ +\ --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y))) = \ +\ (! x y. F(x) & G(y) --> H(x) & J(y)))"; +by (safe_meson_tac 1); (*5 secs*) +result(); + +writeln"Problem 30"; +goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \ +\ (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x)) \ +\ --> (! x. S(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 31"; +goal HOL.thy "~(? x.P(x) & (Q(x) | R(x))) & \ +\ (? x. L(x) & P(x)) & \ +\ (! x. ~ R(x) --> M(x)) \ +\ --> (? x. L(x) & M(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 32"; +goal HOL.thy "(! x. P(x) & (Q(x)|R(x))-->S(x)) & \ +\ (! x. S(x) & R(x) --> L(x)) & \ +\ (! x. M(x) --> R(x)) \ +\ --> (! x. P(x) & M(x) --> L(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 33"; +goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c)) = \ +\ (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"; +by (safe_meson_tac 1); (*5.6 secs*) +result(); + +writeln"Problem 34 AMENDED (TWICE!!)"; +(*Andrews's challenge*) +goal HOL.thy "((? x. ! y. p(x) = p(y)) = \ +\ ((? x. q(x)) = (! y. p(y)))) = \ +\ ((? x. ! y. q(x) = q(y)) = \ +\ ((? x. p(x)) = (! y. q(y))))"; +by (safe_meson_tac 1); (*90 secs*) +result(); + +writeln"Problem 35"; +goal HOL.thy "? x y. P x y --> (! u v. P u v)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 36"; +goal HOL.thy "(! x. ? y. J x y) & \ +\ (! x. ? y. G x y) & \ +\ (! x y. J x y | G x y --> \ +\ (! z. J y z | G y z --> H x z)) \ +\ --> (! x. ? y. H x y)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 37"; +goal HOL.thy "(! z. ? w. ! x. ? y. \ +\ (P x z-->P y w) & P y z & (P y w --> (? u.Q u w))) & \ +\ (! x z. ~P x z --> (? y. Q y z)) & \ +\ ((? x y. Q x y) --> (! x. R x x)) \ +\ --> (! x. ? y. R x y)"; +by (safe_meson_tac 1); (*causes unification tracing messages*) +result(); + +writeln"Problem 38"; +goal HOL.thy + "(! x. p(a) & (p(x) --> (? y. p(y) & r x y)) --> \ +\ (? z. ? w. p(z) & r x w & r w z)) = \ +\ (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) & \ +\ (~p(a) | ~(? y. p(y) & r x y) | \ +\ (? z. ? w. p(z) & r x w & r w z)))"; +by (safe_meson_tac 1); (*62 secs*) +result(); + +writeln"Problem 39"; +goal HOL.thy "~ (? x. ! y. F y x = (~F y y))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 40. AMENDED"; +goal HOL.thy "(? y. ! x. F x y = F x x) \ +\ --> ~ (! x. ? y. ! z. F z y = (~F z x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 41"; +goal HOL.thy "(! z. (? y. (! x. f x y = (f x z & ~ f x x)))) \ +\ --> ~ (? z. ! x. f x z)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 42"; +goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 43 NOW PROVED AUTOMATICALLY!!"; +goal HOL.thy "(! x. ! y. q x y = (! z. p z x = (p z y::bool))) \ +\ --> (! x. (! y. q x y = (q y x::bool)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 44"; +goal HOL.thy "(! x. f(x) --> \ +\ (? y. g(y) & h x y & (? y. g(y) & ~ h x y))) & \ +\ (? x. j(x) & (! y. g(y) --> h x y)) \ +\ --> (? x. j(x) & ~f(x))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 45"; +goal HOL.thy "(! x. f(x) & (! y. g(y) & h x y --> j x y) \ +\ --> (! y. g(y) & h x y --> k(y))) & \ +\ ~ (? y. l(y) & k(y)) & \ +\ (? x. f(x) & (! y. h x y --> l(y)) \ +\ & (! y. g(y) & h x y --> j x y)) \ +\ --> (? x. f(x) & ~ (? y. g(y) & h x y))"; +by (safe_meson_tac 1); (*11 secs*) +result(); + +writeln"Problem 46"; +goal HOL.thy + "(! x. f(x) & (! y. f(y) & h y x --> g(y)) --> g(x)) & \ +\ ((? x.f(x) & ~g(x)) --> \ +\ (? x. f(x) & ~g(x) & (! y. f(y) & ~g(y) --> j x y))) & \ +\ (! x y. f(x) & f(y) & h x y --> ~j y x) \ +\ --> (! x. f(x) --> g(x))"; +by (safe_meson_tac 1); (*11 secs*) +result(); + +(* Example suggested by Johannes Schumann and credited to Pelletier *) +goal HOL.thy "(!x y z. P x y --> P y z --> P x z) --> \ +\ (!x y z. Q x y --> Q y z --> Q x z) --> \ +\ (!x y.Q x y --> Q y x) --> (!x y. P x y | Q x y) --> \ +\ (!x y.P x y) | (!x y.Q x y)"; +by (safe_meson_tac 1); (*32 secs*) +result(); + +writeln"Problem 50"; +(*What has this to do with equality?*) +goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 55"; + +(*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988). + meson_tac cannot report who killed Agatha. *) +goal HOL.thy "lives(agatha) & lives(butler) & lives(charles) & \ +\ (killed agatha agatha | killed butler agatha | killed charles agatha) & \ +\ (!x y. killed x y --> hates x y & ~richer x y) & \ +\ (!x. hates agatha x --> ~hates charles x) & \ +\ (hates agatha agatha & hates agatha charles) & \ +\ (!x. lives(x) & ~richer x agatha --> hates butler x) & \ +\ (!x. hates agatha x --> hates butler x) & \ +\ (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \ +\ (? x. killed x agatha)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 57"; +goal HOL.thy + "P (f a b) (f b c) & P (f b c) (f a c) & \ +\ (! x y z. P x y & P y z --> P x z) --> P (f a b) (f a c)"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 58"; +(* Challenge found on info-hol *) +goal HOL.thy + "! P Q R x. ? v w. ! y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 59"; +goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))"; +by (safe_meson_tac 1); +result(); + +writeln"Problem 60"; +goal HOL.thy "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)"; +by (safe_meson_tac 1); +result(); + +writeln"Reached end of file."; + +(*26 August 1992: loaded in 277 secs. New Jersey v 75*) diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/rel.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/rel.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,109 @@ +(* Title: HOL/ex/rel + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + +Domain, range of a relation or function -- NOT YET WORKING +*) + +structure Rel = +struct +val thy = extend_theory Univ.thy "Rel" +([], [], [], [], + [ + (["domain"], "('a * 'b)set => 'a set"), + (["range2"], "('a * 'b)set => 'b set"), + (["field"], "('a * 'a)set => 'a set") + ], + None) + [ + ("domain_def", "domain(r) == {a. ? b. : r}" ), + ("range2_def", "range2(r) == {b. ? a. : r}" ), + ("field_def", "field(r) == domain(r) Un range2(r)" ) + ]; +end; + +local val ax = get_axiom Rel.thy +in +val domain_def = ax"domain_def"; +val range2_def = ax"range2_def"; +val field_def = ax"field_def"; +end; + + +(*** domain ***) + +val [prem] = goalw Rel.thy [domain_def,Pair_def] ": r ==> a : domain(r)"; +by (fast_tac (set_cs addIs [prem]) 1); +qed "domainI"; + +val major::prems = goalw Rel.thy [domain_def] + "[| a : domain(r); !!y. : r ==> P |] ==> P"; +by (rtac (major RS CollectE) 1); +by (etac exE 1); +by (REPEAT (ares_tac prems 1)); +qed "domainE"; + + +(*** range2 ***) + +val [prem] = goalw Rel.thy [range2_def,Pair_def] ": r ==> b : range2(r)"; +by (fast_tac (set_cs addIs [prem]) 1); +qed "range2I"; + +val major::prems = goalw Rel.thy [range2_def] + "[| b : range2(r); !!x. : r ==> P |] ==> P"; +by (rtac (major RS CollectE) 1); +by (etac exE 1); +by (REPEAT (ares_tac prems 1)); +qed "range2E"; + + +(*** field ***) + +val [prem] = goalw Rel.thy [field_def] ": r ==> a : field(r)"; +by (rtac (prem RS domainI RS UnI1) 1); +qed "fieldI1"; + +val [prem] = goalw Rel.thy [field_def] ": r ==> b : field(r)"; +by (rtac (prem RS range2I RS UnI2) 1); +qed "fieldI2"; + +val [prem] = goalw Rel.thy [field_def] + "(~ :r ==> : r) ==> a : field(r)"; +by (rtac (prem RS domainI RS UnCI) 1); +by (swap_res_tac [range2I] 1); +by (etac notnotD 1); +qed "fieldCI"; + +val major::prems = goalw Rel.thy [field_def] + "[| a : field(r); \ +\ !!x. : r ==> P; \ +\ !!x. : r ==> P |] ==> P"; +by (rtac (major RS UnE) 1); +by (REPEAT (eresolve_tac (prems@[domainE,range2E]) 1)); +qed "fieldE"; + +goalw Rel.thy [field_def] "domain(r) <= field(r)"; +by (rtac Un_upper1 1); +qed "domain_in_field"; + +goalw Rel.thy [field_def] "range2(r) <= field(r)"; +by (rtac Un_upper2 1); +qed "range2_in_field"; + + +????????????????????????????????????????????????????????????????; + +(*If r allows well-founded induction then wf(r)*) +val [prem1,prem2] = goalw Rel.thy [wf_def] + "[| field(r)<=A; \ +\ !!P u. ! x:A. (! y. : r --> P(y)) --> P(x) ==> P(u) |] \ +\ ==> wf(r)"; +by (rtac (prem1 RS wfI) 1); +by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1); +by (fast_tac ZF_cs 3); +by (fast_tac ZF_cs 2); +by (fast_tac ZF_cs 1); +qed "wfI2"; + diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/set.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/set.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,132 @@ +(* Title: HOL/ex/set.ML + ID: $Id$ + Author: Tobias Nipkow, Cambridge University Computer Laboratory + Copyright 1991 University of Cambridge + +Cantor's Theorem; the Schroeder-Berstein Theorem. +*) + + +writeln"File HOL/ex/set."; + +(*** A unique fixpoint theorem --- fast/best/meson all fail ***) + +val [prem] = goal HOL.thy "?!x.f(g(x))=x ==> ?!y.g(f(y))=y"; +by(EVERY1[rtac (prem RS ex1E), rtac ex1I, etac arg_cong, + rtac subst, atac, etac allE, rtac arg_cong, etac mp, etac arg_cong]); +result(); + +(*** Cantor's Theorem: There is no surjection from a set to its powerset. ***) + +goal Set.thy "~ (? f:: 'a=>'a set. ! S. ? x. f(x) = S)"; +(*requires best-first search because it is undirectional*) +by (best_tac (set_cs addSEs [equalityCE]) 1); +qed "cantor1"; + +(*This form displays the diagonal term*) +goal Set.thy "! f:: 'a=>'a set. ! x. f(x) ~= ?S(f)"; +by (best_tac (set_cs addSEs [equalityCE]) 1); +uresult(); + +(*This form exploits the set constructs*) +goal Set.thy "?S ~: range(f :: 'a=>'a set)"; +by (rtac notI 1); +by (etac rangeE 1); +by (etac equalityCE 1); +by (dtac CollectD 1); +by (contr_tac 1); +by (swap_res_tac [CollectI] 1); +by (assume_tac 1); + +choplev 0; +by (best_tac (set_cs addSEs [equalityCE]) 1); + +(*** The Schroder-Berstein Theorem ***) + +val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X"; +by (cut_facts_tac prems 1); +by (rtac equalityI 1); +by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1); +by (fast_tac (set_cs addEs [Inv_f_f RS ssubst]) 1); +qed "inv_image_comp"; + +val prems = goal Set.thy "f(a) ~: (f``X) ==> a~:X"; +by (cfast_tac prems 1); +qed "contra_imageI"; + +goal Lfp.thy "(a ~: Compl(X)) = (a:X)"; +by (fast_tac set_cs 1); +qed "not_Compl"; + +(*Lots of backtracking in this proof...*) +val [compl,fg,Xa] = goal Lfp.thy + "[| Compl(f``X) = g``Compl(X); f(a)=g(b); a:X |] ==> b:X"; +by (EVERY1 [rtac (not_Compl RS subst), rtac contra_imageI, + rtac (compl RS subst), rtac (fg RS subst), stac not_Compl, + rtac imageI, rtac Xa]); +qed "disj_lemma"; + +goal Lfp.thy "range(%z. if z:X then f(z) else g(z)) = f``X Un g``Compl(X)"; +by (rtac equalityI 1); +by (rewtac range_def); +by (fast_tac (set_cs addIs [if_P RS sym, if_not_P RS sym]) 2); +by (rtac subsetI 1); +by (etac CollectE 1); +by (etac exE 1); +by (etac ssubst 1); +by (rtac (excluded_middle RS disjE) 1); +by (EVERY' [rtac (if_P RS ssubst), atac, fast_tac set_cs] 2); +by (EVERY' [rtac (if_not_P RS ssubst), atac, fast_tac set_cs] 1); +qed "range_if_then_else"; + +goal Lfp.thy "a : X Un Compl(X)"; +by (fast_tac set_cs 1); +qed "X_Un_Compl"; + +goalw Lfp.thy [surj_def] "surj(f) = (!a. a : range(f))"; +by (fast_tac (set_cs addEs [ssubst]) 1); +qed "surj_iff_full_range"; + +val [compl] = goal Lfp.thy + "Compl(f``X) = g``Compl(X) ==> surj(%z. if z:X then f(z) else g(z))"; +by (sstac [surj_iff_full_range, range_if_then_else, compl RS sym] 1); +by (rtac (X_Un_Compl RS allI) 1); +qed "surj_if_then_else"; + +val [injf,injg,compl,bij] = goal Lfp.thy + "[| inj_onto f X; inj_onto g (Compl X); Compl(f``X) = g``Compl(X); \ +\ bij = (%z. if z:X then f(z) else g(z)) |] ==> \ +\ inj(bij) & surj(bij)"; +val f_eq_gE = make_elim (compl RS disj_lemma); +by (rtac (bij RS ssubst) 1); +by (rtac conjI 1); +by (rtac (compl RS surj_if_then_else) 2); +by (rewtac inj_def); +by (cut_facts_tac [injf,injg] 1); +by (EVERY1 [rtac allI, rtac allI, stac expand_if, rtac conjI, stac expand_if]); +by (fast_tac (set_cs addEs [inj_ontoD, sym RS f_eq_gE]) 1); +by (stac expand_if 1); +by (fast_tac (set_cs addEs [inj_ontoD, f_eq_gE]) 1); +qed "bij_if_then_else"; + +goal Lfp.thy "? X. X = Compl(g``Compl((f:: 'a=>'b)``X))"; +by (rtac exI 1); +by (rtac lfp_Tarski 1); +by (REPEAT (ares_tac [monoI, image_mono, Compl_anti_mono] 1)); +qed "decomposition"; + +val [injf,injg] = goal Lfp.thy + "[| inj(f:: 'a=>'b); inj(g:: 'b=>'a) |] ==> \ +\ ? h:: 'a=>'b. inj(h) & surj(h)"; +by (rtac (decomposition RS exE) 1); +by (rtac exI 1); +by (rtac bij_if_then_else 1); +by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1, + rtac (injg RS inj_onto_Inv) 1]); +by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI, + etac imageE, etac ssubst, rtac rangeI]); +by (EVERY1 [etac ssubst, stac double_complement, + rtac (injg RS inv_image_comp RS sym)]); +qed "schroeder_bernstein"; + +writeln"Reached end of file."; diff -r 3cdaa8724175 -r b051e2fc2e34 src/HOL/ex/unsolved.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/unsolved.ML Wed Mar 22 12:42:34 1995 +0100 @@ -0,0 +1,70 @@ +(* Title: HOL/ex/unsolved + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Problems that currently defeat the MESON procedure as well as best_tac +*) + +(*from Vladimir Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23*) +goal HOL.thy "? x x'. ! y. ? z z'. (~P(y,y) | P(x,x) | ~S(z,x)) & \ +\ (S(x,y) | ~S(y,z) | Q(z',z')) & \ +\ (Q(x',y) | ~Q(y,z') | S(x',x'))"; + + +writeln"Problem 47 Schubert's Steamroller"; +goal HOL.thy + "(! x. P1(x) --> P0(x)) & (? x.P1(x)) & \ +\ (! x. P2(x) --> P0(x)) & (? x.P2(x)) & \ +\ (! x. P3(x) --> P0(x)) & (? x.P3(x)) & \ +\ (! x. P4(x) --> P0(x)) & (? x.P4(x)) & \ +\ (! x. P5(x) --> P0(x)) & (? x.P5(x)) & \ +\ (! x. Q1(x) --> Q0(x)) & (? x.Q1(x)) & \ +\ (! x. P0(x) --> ((! y.Q0(y)-->R(x,y)) | \ +\ (! y.P0(y) & S(y,x) & \ +\ (? z.Q0(z)&R(y,z)) --> R(x,y)))) & \ +\ (! x y. P3(y) & (P5(x)|P4(x)) --> S(x,y)) & \ +\ (! x y. P3(x) & P2(y) --> S(x,y)) & \ +\ (! x y. P2(x) & P1(y) --> S(x,y)) & \ +\ (! x y. P1(x) & (P2(y)|Q1(y)) --> ~R(x,y)) & \ +\ (! x y. P3(x) & P4(y) --> R(x,y)) & \ +\ (! x y. P3(x) & P5(y) --> ~R(x,y)) & \ +\ (! x. (P4(x)|P5(x)) --> (? y.Q0(y) & R(x,y))) \ +\ --> (? x y. P0(x) & P0(y) & (? z. Q1(z) & R(y,z) & R(x,y)))"; + + +writeln"Problem 55"; + +(*Original, equational version by Len Schubert, via Pelletier *) +goal HOL.thy + "(? x. lives(x) & killed(x,agatha)) & \ +\ lives(agatha) & lives(butler) & lives(charles) & \ +\ (! x. lives(x) --> x=agatha | x=butler | x=charles) & \ +\ (! x y. killed(x,y) --> hates(x,y)) & \ +\ (! x y. killed(x,y) --> ~richer(x,y)) & \ +\ (! x. hates(agatha,x) --> ~hates(charles,x)) & \ +\ (! x. ~ x=butler --> hates(agatha,x)) & \ +\ (! x. ~richer(x,agatha) --> hates(butler,x)) & \ +\ (! x. hates(agatha,x) --> hates(butler,x)) & \ +\ (! x. ? y. ~hates(x,y)) & \ +\ ~ agatha=butler --> \ +\ killed(agatha,agatha)"; + +(** Charles Morgan's problems **) + +val axa = "! x y. T(i(x, i(y,x)))"; +val axb = "! x y z. T(i(i(x, i(y,z)), i(i(x,y), i(x,z))))"; +val axc = "! x y. T(i(i(n(x), n(y)), i(y,x)))"; +val axd = "! x y. T(i(x,y)) & T(x) --> T(y)"; + +fun axjoin ([], q) = q + | axjoin(p::ps, q) = "(" ^ p ^ ") --> (" ^ axjoin(ps,q) ^ ")"; + +goal HOL.thy (axjoin([axa,axb,axd], "! x. T(i(x,x))")); + +writeln"Problem 66"; +goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(x, n(n(x))))")); + +writeln"Problem 67"; +goal HOL.thy (axjoin([axa,axb,axc,axd], "! x. T(i(n(n(x)), x))")); +