--- /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. <b,a>: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); <a,b>: 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. <y,x>: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. <x,y>: r | <y,x>: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";
--- /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. <y,x>:r}"
+
+inductive "acc(r)"
+ intrs
+ pred "pred a r: Pow(acc(r)) ==> a: acc(r)"
+ monos "[Pow_mono]"
+
+end
--- /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();
--- /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
--- /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(<Leaf(v),w>))) (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. <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] "<NIL,NIL> : 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; <M,N>:s |] ==> <CONS x M, CONS x N> : 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) ==> <M,M> : 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. [| <M,N> : 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. <h1(u),h2(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(<x,x>))";
+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(<x,x>))";
+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) |] ==> \
+\ <f(CONS x l),g(CONS x l)> : \
+\ LListD_Fun (diag A) ((%u.<f(u),g(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. <x, 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]
+ "[| <l1,l2> : r; r <= llistD_Fun(r Un range(%x.<x,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] "<LNil,LNil> : 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]
+ "<l1,l2>:r ==> <LCons x l1, LCons x l2> : 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. <l,l> : llistD_Fun(r Un range(%x.<x,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. <f(LCons x l),g(LCons x l)> : \
+\ llistD_Fun(range(%u. <f(u),g(u)>) Un range(%v. <v,v>)) \
+\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
+by (res_inst_tac [("r", "range(%u. <f(u),g(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.<lmap f (iterates f u),iterates f (f 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 {<lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u))>}
+ 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. <nat_rec n (h u) (%m y.lmap f y), \
+\ nat_rec n (iterates f u) (%m y.lmap f y)>)")]
+ 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.<lappend (iterates f u) N,iterates f 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.<lmap f (lappend l n),lappend (lmap f l) (lmap f n)>)")]
+ 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";
--- /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) == \
+\ {<LNil,LNil>} Un \
+\ (UN x. (split(%l1 l2.<LCons(x,l1),LCons(x,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 "<NIL, NIL> : LListD(r)"
+ CONS_I "[| <a,b>: r; <M,N> : LListD(r) \
+\ |] ==> <CONS a M, CONS b N> : 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 = <NIL, NIL> | \
+\ (? M N a b. z = <CONS a M, CONS b N> & \
+\ <a, b> : r & <M, N> : 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(<Leaf(v), w>))) (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(<f(x), M'>)))"
+
+ lmap_def
+ "lmap f l == llist_corec l (llist_case (Inl Unity) (%y z. Inr(<f(y), z>)))"
+
+ iterates_def "iterates f a == llist_corec a (%x. Inr(<x, f(x)>))"
+
+(*Append generates its result by applying f, where
+ f(<NIL,NIL>) = Inl(Unity)
+ f(<NIL, CONS N1 N2>) = Inr(<N1, <NIL,N2>)
+ f(<CONS M1 M2, N>) = Inr(<M1, <M2,N>)
+*)
+
+ Lappend_def
+ "Lappend M N == LList_corec <M,N> \
+\ (split(List_case (List_case (Inl Unity) (%N1 N2. Inr(<N1, <NIL,N2>>))) \
+\ (%M1 M2 N. Inr(<M1, <M2,N>>))))"
+
+ lappend_def
+ "lappend l n == llist_corec <l,n> \
+\ (split(llist_case (llist_case (Inl Unity) (%n1 n2. Inr(<n1, <LNil,n2>>))) \
+\ (%l1 l2 n. Inr(<l1, <l2,n>>))))"
+
+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
--- /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(<a,b>) ==> !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";
--- /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 = <<a,b>,<a',b'>> & (<a,a'> : ra | a=a' & <b,b'> : rb)}"
+end
+
--- /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 <a,b>) (snd <a,b>)";
+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 <a,b>) (snd <a,b>) ==> 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 <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,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 <<a,b>,c>)) (snd(fst <<a,b>,c>)) (snd <<a,b>,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(<<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 xm e1 e2 em v v2. \
+\ [| P(<<ve,e1>,v_clos(<|xm,em,vem|>)>); \
+\ P(<<ve,e2>,v2>); \
+\ P(<<vem + {xm |-> v2},em>,v>) \
+\ |] ==> \
+\ P(<<ve,e1 @ e2>,v>) \
+\ |] ==> \
+\ P(<<ve,e>,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(<<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 (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(<<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 (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 ==> <v_const(c),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) --> \
+\ <ve_app ve ev1,te_app te ev1> : {<v_clos(<|ev,e,ve|>),t>} Un hasty_rel \
+\ |] ==> \
+\ <v_clos(<|ev,e,ve|>),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(<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) --> <ve_app ve ev1,te_app te ev1> : hasty_rel \
+\ |] ==> P(<v_clos(<|ev,e,ve|>),t>); \
+\ <v,t> : hasty_rel \
+\ |] ==> P(<v,t>)";
+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
+ " [| <v,t> : 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) --> <ve_app ve ev1,te_app te ev1> : 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";
+
+
--- /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=<<ve,e_const(c)>,v_const(c)>) | \
+\ (? ve x. pp=<<ve,e_var(x)>,ve_app ve x> & x:ve_dom(ve)) |\
+\ (? ve e x. pp=<<ve,fn x => e>,v_clos(<|x,e,ve|>)>)| \
+\ ( ? ve e x f cl. \
+\ pp=<<ve,fix f(x) = e>,v_clos(cl)> & \
+\ cl=<|x, e, ve+{f |-> v_clos(cl)} |> \
+\ ) | \
+\ ( ? ve e1 e2 c1 c2. \
+\ pp=<<ve,e1 @ e2>,v_const(c_app c1 c2)> & \
+\ <<ve,e1>,v_const(c1)>:s & <<ve,e2>,v_const(c2)>:s \
+\ ) | \
+\ ( ? ve vem e1 e2 em xm v v2. \
+\ pp=<<ve,e1 @ e2>,v> & \
+\ <<ve,e1>,v_clos(<|xm,em,vem|>)>:s & \
+\ <<ve,e2>,v2>:s & \
+\ <<vem+{xm |-> v2},em>,v>:s \
+\ ) \
+\ }"
+
+ eval_rel_def "eval_rel == lfp(eval_fun)"
+ eval_def "ve |- e ---> v == <<ve,e>,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=<<te,e_const(c)>,t> & c isof t) | \
+\ (? te x. pp=<<te,e_var(x)>,te_app te x> & x:te_dom(te)) | \
+\ (? te x e t1 t2. pp=<<te,fn x => e>,t1->t2> & <<te+{x |=> t1},e>,t2>:s) | \
+\ (? te f x e t1 t2. \
+\ pp=<<te,fix f(x)=e>,t1->t2> & <<te+{f |=> t1->t2}+{x |=> t1},e>,t2>:s \
+\ ) | \
+\ (? te e1 e2 t1 t2. \
+\ pp=<<te,e1 @ e2>,t2> & <<te,e1>,t1->t2>:s & <<te,e2>,t1>:s \
+\ ) \
+\ }"
+
+ elab_rel_def "elab_rel == lfp(elab_fun)"
+ elab_def "te |- e ===> t == <<te,e>,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 = <v_const(c),t> & c isof t) | \
+\ ( ? ev e ve t te. \
+\ p = <v_clos(<|ev,e,ve|>),t> & \
+\ te |- fn ev => e ===> t & \
+\ ve_dom(ve) = te_dom(te) & \
+\ (! ev1.ev1:ve_dom(ve) --> <ve_app ve ev1,te_app te ev1> : r) \
+\ ) \
+\ } \
+\ "
+
+ hasty_rel_def "hasty_rel == gfp(hasty_fun)"
+ hasty_def "v hasty t == <v,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
--- /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";
+
--- /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
--- /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.";
--- /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
--- /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<n --> 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();
--- /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
--- /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();
--- /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
--- /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;
--- /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";
--- /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
--- /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 |] ==> <M, CONS M N> : 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 |] ==> <N, CONS M N> : pred_sexp^+";
+by (asm_simp_tac pred_sexp_ss 1);
+qed "pred_sexp_CONS_I2";
+
+val [prem] = goal SList.thy
+ "<CONS M1 M2, N> : pred_sexp^+ ==> \
+\ <M1,N> : pred_sexp^+ & <M2,N> : 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];
+
--- /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
--- /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";
--- /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
--- /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];
--- /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
--- /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();
--- /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;
+
--- /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. <N,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;
--- /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
--- /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.";
--- /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.";
--- /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*)
--- /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. <a,b> : r}" ),
+ ("range2_def", "range2(r) == {b. ? a. <a,b> : 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] "<a,b>: 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. <a,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] "<a,b>: 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. <x,b>: 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] "<a,b>: r ==> a : field(r)";
+by (rtac (prem RS domainI RS UnI1) 1);
+qed "fieldI1";
+
+val [prem] = goalw Rel.thy [field_def] "<a,b>: r ==> b : field(r)";
+by (rtac (prem RS range2I RS UnI2) 1);
+qed "fieldI2";
+
+val [prem] = goalw Rel.thy [field_def]
+ "(~ <c,a>:r ==> <a,b>: 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. <a,x>: r ==> P; \
+\ !!x. <x,a>: 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. <y,x>: 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";
+
--- /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.";
--- /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))"));
+