--- a/src/HOL/IsaMakefile Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/IsaMakefile Wed May 07 13:51:22 1997 +0200
@@ -41,6 +41,17 @@
#### Tests and examples
+## Inductive definitions: simple examples
+
+INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
+
+INDUCT_FILES = Induct/ROOT.ML \
+ $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
+
+Induct: $(OUT)/HOL $(INDUCT_FILES)
+ @$(ISATOOL) usedir $(OUT)/HOL Induct
+
+
## IMP-semantics example
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
@@ -185,8 +196,7 @@
## Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
- Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
+EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
@@ -198,7 +208,8 @@
## Full test
test: $(OUT)/HOL \
- TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
+ TFL Induct IMP Hoare Lex Integ Auth Subst Lambda \
+ W0 MiniML IOA AxClasses Quot ex
echo 'Test examples ran successfully' > test
--- a/src/HOL/Makefile Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/Makefile Wed May 07 13:51:22 1997 +0200
@@ -88,6 +88,21 @@
else echo 'exit_use_dir"../TFL";quit();' | $(LOGIC); \
fi
+
+## Inductive definitions: simple examples
+
+INDUCT_FILES = Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
+
+INDUCT_FILES = Induct/ROOT.ML \
+ $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
+
+Induct: $(BIN)/HOL $(INDUCT_FILES)
+ @if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
+ then echo 'make_html := true; exit_use_dir"Induct";quit();' | $(LOGIC); \
+ else echo 'exit_use_dir"Induct";quit();' | $(LOGIC); \
+ fi
+
+
##IMP-semantics example
IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
@@ -201,8 +216,7 @@
fi
##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
- Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
+EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
@@ -214,7 +228,9 @@
fi
#Full test.
-test: $(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML ex
+test: $(BIN)/HOL \
+ TFL Induct IMP Hoare Lex Integ Auth Subst Lambda \
+ W0 MiniML IOA AxClasses Quot ex
echo 'Test examples ran successfully' > test
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
--- a/src/HOL/README.html Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/README.html Wed May 07 13:51:22 1997 +0200
@@ -31,11 +31,14 @@
<DT>IMP
<DD>mechanization of a large part of a semantics text by Glynn Winskel
+<DT>Induct
+<DD>examples of (co)inductive definitions
+
<DT>Integ
<DD>a theory of the integers including efficient integer calculations
<DT>IOA
-<DD>extended example of Input/Output Automata (takes a long time to run!)
+<DD>extended example of Input/Output Automata
<DT>Lambda
<DD>a proof of the Church-Rosser theorem for lambda-calculus
--- a/src/HOL/ex/Acc.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(* 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 (!claset 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 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 2);
-by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
-qed "acc_induct";
-
-
-val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
-by (rtac (major RS wfI) 1);
-by (etac acc.induct 1);
-by (rewtac pred_def);
-by (Fast_tac 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);
-by (rtac (impI RS allI) 1);
-by (rtac accI 1);
-by (Fast_tac 1);
-qed "acc_wfD_lemma";
-
-val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
-by (rtac subsetI 1);
-by (res_inst_tac [("p", "x")] PairE 1);
-by (fast_tac (!claset addSIs [SigmaI,
- major RS acc_wfD_lemma RS spec RS mp]) 1);
-qed "acc_wfD";
-
-goal Acc.thy "wf(r) = (r <= (acc r) Times (acc r))";
-by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-qed "wf_acc_iff";
--- a/src/HOL/ex/Acc.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* 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 +
-
-constdefs
- pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
- "pred x r == {y. (y,x):r}"
-
-consts
- acc :: "('a * 'a)set => 'a set" (*Accessible part*)
-
-inductive "acc(r)"
- intrs
- pred "pred a r: Pow(acc(r)) ==> a: acc(r)"
- monos "[Pow_mono]"
-
-end
--- a/src/HOL/ex/Comb.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,179 +0,0 @@
-(* Title: HOL/ex/comb.ML
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
- J. Camilleri and T. F. Melham.
- Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
- Report 265, University of Cambridge Computer Laboratory, 1992.
-
-HOL system proofs may be found in
-/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
-*)
-
-open Comb;
-
-(*** Reflexive/Transitive closure preserves the Church-Rosser property
- So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
-***)
-
-val [_, spec_mp] = [spec] RL [mp];
-
-(*Strip lemma. The induction hyp is all but the last diamond of the strip.*)
-goalw Comb.thy [diamond_def]
- "!!r. [| diamond(r); (x,y):r^* |] ==> \
-\ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
-by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
- addSDs [spec_mp]) 1);
-val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
-
-val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
-by (rewtac diamond_def); (*unfold only in goal, not in premise!*)
-by (rtac (impI RS allI RS allI) 1);
-by (etac rtrancl_induct 1);
-by (Blast_tac 1);
-by (slow_best_tac (*Seems to be a brittle, undirected search*)
- (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
- addEs [major RS diamond_strip_lemmaE]) 1);
-qed "diamond_rtrancl";
-
-
-(*** Results about Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases comb.simps "K -1-> z";
-val S_contractE = contract.mk_cases comb.simps "S -1-> z";
-val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
-
-AddSIs [contract.K, contract.S];
-AddIs [contract.Ap1, contract.Ap2];
-AddSEs [K_contractE, S_contractE, Ap_contractE];
-Unsafe_Addss (!simpset);
-
-goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
-by (Blast_tac 1);
-qed "I_contract_E";
-AddSEs [I_contract_E];
-
-goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
-by (Blast_tac 1);
-qed "K1_contractD";
-AddSEs [K1_contractD];
-
-goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
-qed "Ap_reduce1";
-
-goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
-qed "Ap_reduce2";
-
-(** Counterexample to the diamond property for -1-> **)
-
-goal Comb.thy "K#I#(I#I) -1-> I";
-by (rtac contract.K 1);
-qed "KIII_contract1";
-
-goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
-by (Blast_tac 1);
-qed "KIII_contract2";
-
-goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
-by (Blast_tac 1);
-qed "KIII_contract3";
-
-goalw Comb.thy [diamond_def] "~ diamond(contract)";
-by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
-qed "not_diamond_contract";
-
-
-
-(*** Results about Parallel Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
-val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
-
-AddIs parcontract.intrs;
-AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-Unsafe_Addss (!simpset);
-
-(*** Basic properties of parallel contraction ***)
-
-goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
-by (Blast_tac 1);
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
-by (Blast_tac 1);
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-goal Comb.thy
- "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
-by (Blast_tac 1);
-qed "S2_parcontractD";
-AddSDs [S2_parcontractD];
-
-(*The rules above are not essential but make proofs much faster*)
-
-
-(*Church-Rosser property for parallel contraction*)
-goalw Comb.thy [diamond_def] "diamond parcontract";
-by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by (Step_tac 1);
-by (ALLGOALS Blast_tac);
-qed "diamond_parcontract";
-
-
-(*** Equivalence of x--->y and x===>y ***)
-
-goal Comb.thy "contract <= parcontract";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac contract.induct 1);
-by (ALLGOALS Blast_tac);
-qed "contract_subset_parcontract";
-
-(*Reductions: simply throw together reflexivity, transitivity and
- the one-step reductions*)
-
-AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
-
-(*Example only: not used*)
-goalw Comb.thy [I_def] "I#x ---> x";
-by (Blast_tac 1);
-qed "reduce_I";
-
-goal Comb.thy "parcontract <= contract^*";
-by (rtac subsetI 1);
-by (split_all_tac 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by (ALLGOALS Blast_tac);
-qed "parcontract_subset_reduce";
-
-goal Comb.thy "contract^* = parcontract^*";
-by (REPEAT
- (resolve_tac [equalityI,
- contract_subset_parcontract RS rtrancl_mono,
- parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
-qed "reduce_eq_parreduce";
-
-goal Comb.thy "diamond(contract^*)";
-by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl,
- diamond_parcontract]) 1);
-qed "diamond_reduce";
-
-
-writeln"Reached end of file.";
--- a/src/HOL/ex/Comb.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-(* Title: HOL/ex/Comb.thy
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
- J. Camilleri and T. F. Melham.
- Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
- Report 265, University of Cambridge Computer Laboratory, 1992.
-*)
-
-
-Comb = Trancl +
-
-(** Datatype definition of combinators S and K, with infixed application **)
-datatype comb = K
- | S
- | "#" comb comb (infixl 90)
-
-(** Inductive definition of contractions, -1->
- and (multi-step) reductions, --->
-**)
-consts
- contract :: "(comb*comb) set"
- "-1->" :: [comb,comb] => bool (infixl 50)
- "--->" :: [comb,comb] => bool (infixl 50)
-
-translations
- "x -1-> y" == "(x,y) : contract"
- "x ---> y" == "(x,y) : contract^*"
-
-inductive contract
- intrs
- K "K#x#y -1-> x"
- S "S#x#y#z -1-> (x#z)#(y#z)"
- Ap1 "x-1->y ==> x#z -1-> y#z"
- Ap2 "x-1->y ==> z#x -1-> z#y"
-
-
-(** Inductive definition of parallel contractions, =1=>
- and (multi-step) parallel reductions, ===>
-**)
-consts
- parcontract :: "(comb*comb) set"
- "=1=>" :: [comb,comb] => bool (infixl 50)
- "===>" :: [comb,comb] => bool (infixl 50)
-
-translations
- "x =1=> y" == "(x,y) : parcontract"
- "x ===> y" == "(x,y) : parcontract^*"
-
-inductive parcontract
- intrs
- refl "x =1=> x"
- K "K#x#y =1=> x"
- S "S#x#y#z =1=> (x#z)#(y#z)"
- Ap "[| x=1=>y; z=1=>w |] ==> x#z =1=> y#w"
-
-
-(*Misc definitions*)
-constdefs
- I :: comb
- "I == S#K#K"
-
- (*confluence; Lambda/Commutation treats this more abstractly*)
- diamond :: "('a * 'a)set => bool"
- "diamond(r) == ALL x y. (x,y):r -->
- (ALL y'. (x,y'):r -->
- (EX z. (y,z):r & (y',z) : r))"
-
-end
--- a/src/HOL/ex/LFilter.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,341 +0,0 @@
-(* Title: HOL/ex/LFilter
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The "filter" functional for coinductive lists
- --defined by a combination of induction and coinduction
-*)
-
-open LFilter;
-
-
-(*** findRel: basic laws ****)
-
-val findRel_LConsE =
- findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
-
-AddSEs [findRel_LConsE];
-
-
-goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
-by (etac findRel.induct 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "findRel_functional";
-
-goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
-by (etac findRel.induct 1);
-by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "findRel_imp_LCons";
-
-goal thy "!!p. (LNil,l): findRel p ==> R";
-by (blast_tac (!claset addEs [findRel.elim]) 1);
-qed "findRel_LNil";
-
-AddSEs [findRel_LNil];
-
-
-(*** Properties of Domain (findRel p) ***)
-
-goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
-by (case_tac "p x" 1);
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
-qed "LCons_Domain_findRel";
-
-Addsimps [LCons_Domain_findRel];
-
-val major::prems =
-goal thy "[| l: Domain (findRel p); \
-\ !!x l'. [| (l, LCons x l') : findRel p; p x |] ==> Q \
-\ |] ==> Q";
-by (rtac (major RS DomainE) 1);
-by (forward_tac [findRel_imp_LCons] 1);
-by (REPEAT (eresolve_tac [exE,conjE] 1));
-by (hyp_subst_tac 1);
-by (REPEAT (ares_tac prems 1));
-qed "Domain_findRelE";
-
-val prems = goal thy
- "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
-by (Step_tac 1);
-by (etac findRel.induct 1);
-by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
-qed "Domain_findRel_mono";
-
-
-(*** find: basic equations ***)
-
-goalw thy [find_def] "find p LNil = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
-qed "find_LNil";
-
-goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
-by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
-qed "findRel_imp_find";
-
-goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
-by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_found";
-
-goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
-qed "diverge_find_LNil";
-
-Addsimps [diverge_find_LNil];
-
-goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
-by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (Asm_full_simp_tac 2);
-by (Step_tac 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
-by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_seek";
-
-goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
- setloop split_tac[expand_if]) 1);
-qed "find_LCons";
-
-
-
-(*** lfilter: basic equations ***)
-
-goal thy "lfilter p LNil = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (simp_tac (!simpset addsimps [find_LNil]) 1);
-qed "lfilter_LNil";
-
-goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "diverge_lfilter_LNil";
-
-
-goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (!simpset addsimps [find_LCons_found]) 1);
-qed "lfilter_LCons_found";
-
-
-goal thy "!!p. (l, LCons x l') : findRel p \
-\ ==> lfilter p l = LCons x (lfilter p l')";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
-qed "findRel_imp_lfilter";
-
-goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-by (safe_tac (!claset delrules [conjI]));
-by (asm_full_simp_tac
- (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
- find_LCons_seek]) 1);
-qed "lfilter_LCons_seek";
-
-
-goal thy "lfilter p (LCons x l) = \
-\ (if p x then LCons x (lfilter p l) else lfilter p l)";
-by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
- setloop split_tac[expand_if]) 1);
-qed "lfilter_LCons";
-
-AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LNil, lfilter_LCons];
-
-
-goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
-by (rtac notI 1);
-by (etac Domain_findRelE 1);
-by (etac rev_mp 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
-qed "lfilter_eq_LNil";
-
-
-goal thy "!!p. lfilter p l = LCons x l' --> \
-\ (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
-by (stac (lfilter_def RS def_llist_corec) 1);
-by (case_tac "l : Domain(findRel p)" 1);
-by (etac Domain_findRelE 1);
-by (Asm_simp_tac 2);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
-by (Blast_tac 1);
-qed_spec_mp "lfilter_eq_LCons";
-
-
-goal thy "lfilter p l = LNil | \
-\ (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
-by (case_tac "l : Domain(findRel p)" 1);
-by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (blast_tac (!claset addSEs [Domain_findRelE]
- addIs [findRel_imp_lfilter]) 1);
-qed "lfilter_cases";
-
-
-(*** lfilter: simple facts by coinduction ***)
-
-goal thy "lfilter (%x.True) l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed "lfilter_K_True";
-
-goal thy "lfilter p (lfilter p l) = lfilter p l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
-(*Cases: p x is true or false*)
-by (Blast_tac 1);
-by (rtac (lfilter_cases RS disjE) 1);
-by (etac ssubst 1);
-by (Auto_tac());
-qed "lfilter_idem";
-
-
-(*** Numerous lemmas required to prove lfilter_conj:
- lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
- ***)
-
-goal thy "!!p. (l,l') : findRel q \
-\ ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
-by (etac findRel.induct 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
-qed_spec_mp "findRel_conj_lemma";
-
-val findRel_conj = refl RSN (2, findRel_conj_lemma);
-
-goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
-\ ==> (l, LCons x l') : findRel q --> ~ p x \
-\ --> l' : Domain (findRel (%x. p x & q x))";
-by (etac findRel.induct 1);
-by (Auto_tac());
-qed_spec_mp "findRel_not_conj_Domain";
-
-
-goal thy "!!p. (l,lxx) : findRel q ==> \
-\ lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
-\ --> (l,lz) : findRel (%x. p x & q x)";
-by (etac findRel.induct 1);
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
-qed_spec_mp "findRel_conj2";
-
-
-goal thy "!!p. (lx,ly) : findRel p \
-\ ==> ALL l. lx = lfilter q l \
-\ --> l : Domain (findRel(%x. p x & q x))";
-by (etac findRel.induct 1);
-by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
- addIs [findRel_conj]) 1);
-by (Auto_tac());
-by (dtac (sym RS lfilter_eq_LCons) 1);
-by (Auto_tac());
-by (dtac spec 1);
-by (dtac (refl RS rev_mp) 1);
-by (blast_tac (!claset addIs [findRel_conj2]) 1);
-qed_spec_mp "findRel_lfilter_Domain_conj";
-
-
-goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
-\ ==> l'' = LCons y l' --> \
-\ (lfilter q l, LCons y (lfilter q l')) : findRel p";
-by (etac findRel.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
-qed_spec_mp "findRel_conj_lfilter";
-
-
-
-goal thy "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) \
-\ : llistD_Fun (range \
-\ (%u. (lfilter p (lfilter q u), \
-\ lfilter (%x. p x & q x) u)))";
-by (case_tac "l : Domain(findRel q)" 1);
-by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
-by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
-(*There are no qs in l: both lists are LNil*)
-by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-(*case q x*)
-by (case_tac "p x" 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
- findRel_conj RS findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-(*case q x and ~(p x) *)
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
-by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
-(*subcase: there is no p&q in l' and therefore none in l*)
-by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
-by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
-by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
-by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
-(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*)
-by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-(*subcase: there is a p&q in l' and therefore also one in l*)
-by (etac Domain_findRelE 1);
-by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
-by (blast_tac (!claset addIs [findRel_conj2]) 2);
-by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
-by (blast_tac (!claset addIs [findRel_conj_lfilter]) 2);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-val lemma = result();
-
-
-goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
-qed "lfilter_conj";
-
-
-(*** Numerous lemmas required to prove ??:
- lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
- ***)
-
-goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
-by (etac findRel.induct 1);
-by (ALLGOALS Asm_full_simp_tac);
-qed "findRel_lmap_Domain";
-
-
-goal thy "!!p. lmap f l = LCons x l' --> \
-\ (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
-by (stac (lmap_def RS def_llist_corec) 1);
-by (res_inst_tac [("l", "l")] llistE 1);
-by (Auto_tac());
-qed_spec_mp "lmap_eq_LCons";
-
-
-goal thy "!!p. (lx,ly) : findRel p ==> \
-\ ALL l. lmap f l = lx --> ly = LCons x l' --> \
-\ (EX y l''. x = f y & l' = lmap f l'' & \
-\ (l, LCons y l'') : findRel(%x. p(f x)))";
-by (etac findRel.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (safe_tac (!claset addSDs [lmap_eq_LCons]));
-by (blast_tac (!claset addIs findRel.intrs) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
-qed_spec_mp "lmap_LCons_findRel_lemma";
-
-val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
-
-goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
-by (Step_tac 1);
-by (Blast_tac 1);
-by (case_tac "lmap f l : Domain (findRel p)" 1);
-by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
-by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
-by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
-by (etac Domain_findRelE 1);
-by (forward_tac [lmap_LCons_findRel] 1);
-by (Step_tac 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
-qed "lfilter_lmap";
--- a/src/HOL/ex/LFilter.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-(* Title: HOL/LList.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The "filter" functional for coinductive lists
- --defined by a combination of induction and coinduction
-*)
-
-LFilter = LList + Relation +
-
-consts
- findRel :: "('a => bool) => ('a llist * 'a llist)set"
-
-inductive "findRel p"
- intrs
- found "p x ==> (LCons x l, LCons x l) : findRel p"
- seek "[| ~p x; (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
-
-constdefs
- find :: ['a => bool, 'a llist] => 'a llist
- "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
-
- lfilter :: ['a => bool, 'a llist] => 'a llist
- "lfilter p l == llist_corec l (%l. case find p l of
- LNil => Inl ()
- | LCons y z => Inr(y,z))"
-
-end
--- a/src/HOL/ex/LList.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,886 +0,0 @@
-(* Title: HOL/ex/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 **)
-
-simpset := !simpset 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 (!claset 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)";
-by (etac llist.coinduct 1);
-by (etac (subsetD RS CollectD) 1);
-by (assume_tac 1);
-qed "llist_coinduct";
-
-goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (Fast_tac 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 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 (!simpset 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 (!simpset 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 (!simpset 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";
-
-Addsimps [LList_corec_fun_def RS def_nat_rec_0,
- LList_corec_fun_def RS def_nat_rec_Suc];
-
-(** 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));
-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 (!simpset addsimps [CONS_UN1]) 1);
-by (safe_tac (!claset));
-by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
-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 (!claset));
-by (stac LList_corec 1);
-by (simp_tac (!simpset 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 (!claset));
-by (stac LList_corec 1);
-by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (!claset 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 (!claset 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 ((claset_of "Fun") delrules [equalityI]));
-by (etac LListD.elim 1);
-by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
-by (res_inst_tac [("n", "n")] natE 1);
-by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
-by (rename_tac "n'" 1);
-by (res_inst_tac [("n", "n'")] natE 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
-by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 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 1);
-by (Fast_tac 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 (!claset));
-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 thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
-by (REPEAT (ares_tac basic_monos 1));
-qed "LListD_Fun_mono";
-
-goalw LList.thy [LListD_Fun_def]
- "!!M. [| M : X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M : LListD(r)";
-by (etac LListD.coinduct 1);
-by (etac (subsetD RS CollectD) 1);
-by (assume_tac 1);
-qed "LListD_coinduct";
-
-goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (Fast_tac 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 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 (etac diagE 1);
-by (etac ssubst 1);
-by (eresolve_tac [llist.elim] 1);
-by (ALLGOALS
- (asm_simp_tac (!simpset 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);
-by (rtac LListD_Fun_LListD_I 1);
-by (asm_simp_tac (!simpset 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 (!simpset addsimps [LListD_eq_diag]) 1);
-by (safe_tac (!claset));
-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 (!claset));
-by (stac prem1 1);
-by (stac prem2 1);
-by (simp_tac (!simpset 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 (!simpset 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 (rename_tac "x k" 1);
-by (res_inst_tac [("x", "x")] spec 1);
-by (res_inst_tac [("n", "k")] less_induct 1);
-by (rename_tac "n" 1);
-by (rtac allI 1);
-by (rename_tac "y" 1);
-by (stac prem1 1);
-by (stac prem2 1);
-by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
-by (strip_tac 1);
-by (res_inst_tac [("n", "n")] natE 1);
-by (rename_tac "m" 2);
-by (res_inst_tac [("n", "m")] natE 2);
-by (ALLGOALS(asm_simp_tac(!simpset addsimps
- [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
-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 (!claset));
-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 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 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);
-
-AddIffs [LCons_not_LNil, LNil_not_LCons];
-
-
-(** 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 (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
-qed "CONS_CONS_eq2";
-
-bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
-
-
-(*For reasoning about abstract llist constructors*)
-
-AddIs ([Rep_llist]@llist.intrs);
-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 1);
-qed "LCons_LCons_eq";
-
-AddIffs [LCons_LCons_eq];
-
-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 1);
-qed "CONS_D2";
-
-
-(****** Reasoning about llist(A) ******)
-
-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);
-by (rtac (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);
-by (rtac (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 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 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 (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset 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 (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset 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 (!claset));
-by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (!simpset 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 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 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 1);
-qed "Lappend_CONS";
-
-Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
- Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
-Delsimps [Pair_eq];
-
-goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-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);
-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 1);
-by (safe_tac (!claset));
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (eres_inst_tac [("a", "v")] llist.elim 1);
-by (ALLGOALS
- (Asm_simp_tac THEN'
- fast_tac (!claset 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);
-by (etac imageI 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
-by (Asm_simp_tac 1);
-by (fast_tac (!claset 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 **)
-
-Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
- Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
-
-goalw LList.thy [llist_case_def,LNil_def] "llist_case c d LNil = c";
-by (Simp_tac 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 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 (!simpset delsimps [CONS_CONS_eq] 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 (!simpset addsimps [LList_corec_type2]) 1);
-by (res_inst_tac [("p","y")] PairE 1);
-by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
-(*FIXME: correct case splits usd to be found automatically:
-by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 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 <= (llist A) Times (llist A) ==> \
-\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
-by (stac llist_unfold 1);
-by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
-by (Fast_tac 1);
-qed "LListD_Fun_subset_Sigma_llist";
-
-goal LList.thy
- "prod_fun Rep_llist Rep_llist `` r <= \
-\ (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (!claset addIs [Rep_llist]) 1);
-qed "subset_Sigma_llist";
-
-val [prem] = goal LList.thy
- "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
-\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
-by (safe_tac (!claset));
-by (rtac (prem RS subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (!simpset 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))";
-by (rtac equalityI 1);
-by (fast_tac (!claset addIs [Rep_llist]) 1);
-by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
-qed "prod_fun_range_eq_diag";
-
-(*Surprisingly hard to prove. Used with lfilter*)
-goalw thy [llistD_Fun_def, prod_fun_def]
- "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
-by (Auto_tac());
-by (rtac image_eqI 1);
-by (fast_tac (!claset addss (!simpset)) 1);
-by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
-qed "llistD_Fun_mono";
-
-(** 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 (stac image_Un 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)))";
-by (rtac (Rep_llist_inverse RS subst) 1);
-by (rtac prod_fun_imageI 1);
-by (stac image_Un 1);
-by (stac prod_fun_range_eq_diag 1);
-by (rtac (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*)
-Addsimps [llist_case_LNil, llist_case_LCons,
- llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-
-
-(*** The functional "lmap" ***)
-
-goal LList.thy "lmap f LNil = LNil";
-by (rtac (lmap_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 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 1);
-qed "lmap_LCons";
-
-Addsimps [lmap_LNil, 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);
-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);
-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 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 (!claset));
-by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
-by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
-by (Simp_tac 1);
-qed "lmap_iterates";
-
-goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))";
-by (stac lmap_iterates 1);
-by (rtac 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 (LCons b l) (%m. lmap(f)) n = \
-\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "fun_power_lmap";
-
-goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-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)";
-by (rtac ext 1);
-by (res_inst_tac [("r",
- "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
-\ nat_rec (iterates f u) (%m y.lmap f y) n))")]
- llist_equalityI 1);
-by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
-by (safe_tac (!claset));
-by (stac iterates 1);
-by (stac prem 1);
-by (stac fun_power_lmap 1);
-by (stac fun_power_lmap 1);
-by (rtac llistD_Fun_LCons_I 1);
-by (rtac (lmap_iterates RS subst) 1);
-by (stac fun_power_Suc 1);
-by (stac fun_power_Suc 1);
-by (rtac (UN1_I RS UnI1) 1);
-by (rtac 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 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 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 1);
-qed "lappend_LCons";
-
-Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
-
-goal LList.thy "lappend LNil l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil";
-
-goal LList.thy "lappend l LNil = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil2";
-
-Addsimps [lappend_LNil, 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 (!claset));
-by (stac iterates 1);
-by (Simp_tac 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 (!claset));
-by (res_inst_tac [("l", "l")] llistE 1);
-by (res_inst_tac [("l", "n")] llistE 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
-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 1);
-by (Simp_tac 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 1);
-by (Simp_tac 1);
-qed "lappend_assoc";
--- a/src/HOL/ex/LList.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,153 +0,0 @@
-(* 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)"
-
-translations
- "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
-
-
-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 (%x. {})
- (%j r x. case f x of Inl u => NIL
- | Inr(z,w) => CONS z (r w))
- k"
-
- 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.case f z of Inl x => Inl(x)
- | Inr(v,w) => Inr(Leaf(v), w)))"
-
- 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 ()) (%x M'. Inr((f(x), M'))))"
-
- lmap_def
- "lmap f l == llist_corec l (%z. case z of LNil => (Inl ())
- | LCons 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(())
- 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 ()) (%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 ()) (%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
--- a/src/HOL/ex/Mutil.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* Title: HOL/ex/Mutil
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
-*)
-
-open Mutil;
-
-Addsimps tiling.intrs;
-
-(** The union of two disjoint tilings is a tiling **)
-
-goal thy "!!t. t: tiling A ==> \
-\ u: tiling A --> t <= Compl u --> t Un u : tiling A";
-by (etac tiling.induct 1);
-by (Simp_tac 1);
-by (simp_tac (!simpset addsimps [Un_assoc]) 1);
-by (blast_tac (!claset addIs tiling.intrs) 1);
-qed_spec_mp "tiling_UnI";
-
-
-(*** Chess boards ***)
-
-val [below_0, below_Suc] = nat_recs below_def;
-Addsimps [below_0, below_Suc];
-
-goal thy "ALL i. (i: below k) = (i<k)";
-by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
-by (Blast_tac 1);
-qed_spec_mp "below_less_iff";
-
-Addsimps [below_less_iff];
-
-goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Sigma_Suc1";
-
-goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "Sigma_Suc2";
-
-(*Deletion is essential to allow use of Sigma_Suc1,2*)
-Delsimps [below_Suc];
-
-goal thy "{i} Times below(n + n) : tiling domino";
-by (nat_ind_tac "n" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
-by (resolve_tac tiling.intrs 1);
-by (assume_tac 2);
-by (subgoal_tac (*seems the easiest way of turning one to the other*)
- "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
-\ {(i, n+n), (i, Suc(n+n))}" 1);
-by (Blast_tac 2);
-by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (blast_tac (!claset addEs [less_irrefl, less_asym]
- addSDs [below_less_iff RS iffD1]) 1);
-qed "dominoes_tile_row";
-
-goal thy "(below m) Times below(n + n) : tiling domino";
-by (nat_ind_tac "m" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
-by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
- addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
-qed "dominoes_tile_matrix";
-
-
-(*** Basic properties of evnodd ***)
-
-goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A & (i+j) mod 2 = b)";
-by (Simp_tac 1);
-qed "evnodd_iff";
-
-goalw thy [evnodd_def] "evnodd A b <= A";
-by (rtac Int_lower1 1);
-qed "evnodd_subset";
-
-(* finite X ==> finite(evnodd X b) *)
-bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
-
-goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Un";
-
-goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
-by (Blast_tac 1);
-qed "evnodd_Diff";
-
-goalw thy [evnodd_def] "evnodd {} b = {}";
-by (Simp_tac 1);
-qed "evnodd_empty";
-
-goalw thy [evnodd_def]
- "evnodd (insert (i,j) C) b = \
-\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
-by (asm_full_simp_tac (!simpset addsimps [evnodd_def]
- setloop (split_tac [expand_if] THEN' Step_tac)) 1);
-qed "evnodd_insert";
-
-
-(*** Dominoes ***)
-
-goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
-by (eresolve_tac [domino.elim] 1);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
-by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
-by (REPEAT_FIRST assume_tac);
-(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
-by (REPEAT (asm_full_simp_tac (!simpset addsimps
- [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc]
- setloop split_tac [expand_if]) 1
- THEN Blast_tac 1));
-qed "domino_singleton";
-
-goal thy "!!d. d:domino ==> finite d";
-by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI]
- addSEs [domino.elim]) 1);
-qed "domino_finite";
-
-
-(*** Tilings of dominoes ***)
-
-goal thy "!!t. t:tiling domino ==> finite t";
-by (eresolve_tac [tiling.induct] 1);
-by (rtac finite_emptyI 1);
-by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
-qed "tiling_domino_finite";
-
-goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
-by (eresolve_tac [tiling.induct] 1);
-by (simp_tac (!simpset addsimps [evnodd_def]) 1);
-by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
-by (Simp_tac 2 THEN assume_tac 1);
-by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
-by (Simp_tac 2 THEN assume_tac 1);
-by (Step_tac 1);
-by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
-by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left,
- tiling_domino_finite,
- evnodd_subset RS finite_subset,
- card_insert_disjoint]) 1);
-by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
-qed "tiling_domino_0_1";
-
-goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
-\ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \
-\ |] ==> t' ~: tiling domino";
-by (rtac notI 1);
-by (dtac tiling_domino_0_1 1);
-by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
-by (Asm_full_simp_tac 1);
-by (subgoal_tac "t : tiling domino" 1);
-(*Requires a small simpset that won't move the Suc applications*)
-by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
-by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
-by (asm_simp_tac (!simpset addsimps add_ac) 2);
-by (asm_full_simp_tac
- (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty,
- mod_less, tiling_domino_0_1 RS sym]) 1);
-by (rtac less_trans 1);
-by (REPEAT
- (rtac card_Diff 1
- THEN
- asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1
- THEN
- asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
-qed "mutil_not_tiling";
-
--- a/src/HOL/ex/Mutil.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: HOL/ex/Mutil
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1996 University of Cambridge
-
-The Mutilated Chess Board Problem, formalized inductively
- Originator is Max Black, according to J A Robinson.
- Popularized as the Mutilated Checkerboard Problem by J McCarthy
-*)
-
-Mutil = Finite +
-consts
- domino :: "(nat*nat)set set"
- tiling :: 'a set set => 'a set set
- below :: nat => nat set
- evnodd :: "[(nat*nat)set, nat] => (nat*nat)set"
-
-inductive domino
- intrs
- horiz "{(i, j), (i, Suc j)} : domino"
- vertl "{(i, j), (Suc i, j)} : domino"
-
-inductive "tiling A"
- intrs
- empty "{} : tiling A"
- Un "[| a: A; t: tiling A; a <= Compl t |] ==> a Un t : tiling A"
-
-defs
- below_def "below n == nat_rec {} insert n"
- evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
-
-end
--- a/src/HOL/ex/Perm.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,98 +0,0 @@
-(* Title: HOL/ex/Perm.ML
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-
-Permutations: example of an inductive definition
-*)
-
-(*It would be nice to prove
- xs <~~> ys = (!x. count xs x = count ys x)
-See mset on HOL/ex/Sorting.thy
-*)
-
-open Perm;
-
-goal Perm.thy "l <~~> l";
-by (list.induct_tac "l" 1);
-by (REPEAT (ares_tac perm.intrs 1));
-qed "perm_refl";
-
-
-(** Some examples of rule induction on permutations **)
-
-(*The form of the premise lets the induction bind xs and ys.*)
-goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
-by (etac perm.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "perm_Nil_lemma";
-
-(*A more general version is actually easier to understand!*)
-goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
-by (etac perm.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "perm_length";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
-by (etac perm.induct 1);
-by (REPEAT (ares_tac perm.intrs 1));
-qed "perm_sym";
-
-goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
-by (etac perm.induct 1);
-by (Fast_tac 4);
-by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
-val perm_mem_lemma = result();
-
-bind_thm ("perm_mem", perm_mem_lemma RS mp);
-
-(** Ways of making new permutations **)
-
-(*We can insert the head anywhere in the list*)
-goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
-qed "perm_append_Cons";
-
-(*single steps
-by (rtac perm.trans 1);
-by (rtac perm.swap 1);
-by (rtac perm.Cons 1);
-*)
-
-goal Perm.thy "xs@ys <~~> ys@xs";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
-qed "perm_append_swap";
-
-
-goal Perm.thy "a # xs <~~> xs @ [a]";
-by (rtac perm.trans 1);
-by (rtac perm_append_swap 2);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-qed "perm_append_single";
-
-goal Perm.thy "rev xs <~~> xs";
-by (list.induct_tac "xs" 1);
-by (simp_tac (!simpset addsimps [perm_refl]) 1);
-by (Simp_tac 1);
-by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
-by (etac perm.Cons 1);
-qed "perm_rev";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
-by (list.induct_tac "l" 1);
-by (Simp_tac 1);
-by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
-qed "perm_append1";
-
-goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
-by (rtac (perm_append_swap RS perm.trans) 1);
-by (etac (perm_append1 RS perm.trans) 1);
-by (rtac perm_append_swap 1);
-qed "perm_append2";
-
--- a/src/HOL/ex/Perm.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(* Title: HOL/ex/Perm.thy
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1995 University of Cambridge
-
-Permutations: example of an inductive definition
-*)
-
-Perm = List +
-
-consts perm :: "('a list * 'a list) set"
-syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50)
-
-translations
- "x <~~> y" == "(x,y) : perm"
-
-inductive perm
- intrs
- Nil "[] <~~> []"
- swap "y#x#l <~~> x#y#l"
- Cons "xs <~~> ys ==> z#xs <~~> z#ys"
- trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs"
-
-end
--- a/src/HOL/ex/PropLog.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,229 +0,0 @@
-(* 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 (!claset 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 (!claset 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 (ALLGOALS
- (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN,
- thms.S RS thms.MP RS thms.MP, weaken_right])));
-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 **)
-
-goalw PropLog.thy [eval_def] "tt[false] = False";
-by (Simp_tac 1);
-qed "eval_false";
-
-goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
-by (Simp_tac 1);
-qed "eval_var";
-
-goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
-by (Simp_tac 1);
-qed "eval_imp";
-
-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 (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
-by (ALLGOALS Asm_simp_tac);
-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 (!simpset addsimps [thms_I, thms.H])));
-by (fast_tac (!claset 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 1);
-qed "sat_thms_p";
-
-(*For proving certain theorems in our new propositional logic*)
-
-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 (!claset 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 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Simp_tac 1);
-by (Fast_tac 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 1);
-by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
-by (Simp_tac 1);
-by (Fast_tac 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 1);
-qed "insert_Diff_same";
-
-goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
-by (Fast_tac 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 (!simpset setloop (split_tac [expand_if]))));
-by (ALLGOALS (fast_tac (!claset 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 (!simpset addsimps [sat RS sat_thms_p]) 1);
-by (safe_tac (!claset));
-(*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*)
-goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
-by (Simp_tac 1);
-by (Fast_tac 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 ((claset_of "Fun") addSIs [completeness_0]));
-by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
-by (Fast_tac 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 (!claset addSEs [soundness, finite RS completeness]) 1);
-qed "thms_iff";
-
-writeln"Reached end of file.";
--- a/src/HOL/ex/PropLog.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* 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) = (%x.False)"
- "eval2(#v) = (%tt.v:tt)"
- "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
-
-primrec hyps pl
- "hyps(false) = (%tt.{})"
- "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
- "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
-
-end
-
--- a/src/HOL/ex/ROOT.ML Wed May 07 13:50:52 1997 +0200
+++ b/src/HOL/ex/ROOT.ML Wed May 07 13:51:22 1997 +0200
@@ -16,22 +16,13 @@
(** time_use "mesontest2.ML"; ULTRA SLOW **)
time_use_thy "String";
time_use_thy "BT";
-time_use_thy "Perm";
-time_use_thy "Comb";
time_use_thy "InSort";
time_use_thy "Qsort";
time_use_thy "LexProd";
time_use_thy "Puzzle";
-time_use_thy "Mutil";
time_use_thy "Primes";
time_use_thy "NatSum";
time_use "set.ML";
-time_use_thy "SList";
-time_use_thy "LFilter";
-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";
--- a/src/HOL/ex/SList.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,372 +0,0 @@
-(* 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 (!claset 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 (!claset 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_induct2";
-
-(*Perform induction on xs. *)
-fun list_ind_tac a M =
- EVERY [res_inst_tac [("l",a)] list_induct2 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);
-
-(** Injectiveness of CONS and Cons **)
-
-goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
-by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
-qed "CONS_CONS_eq";
-
-(*For reasoning about abstract list constructors*)
-AddIs ([Rep_list] @ list.intrs);
-
-AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
-
-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 1);
-qed "Cons_Cons_eq";
-bind_thm ("Cons_inject2", (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));
-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 (!claset addSDs [Scons_D]) 1);
-qed "sexp_CONS_D";
-
-
-(*Reasoning about constructors and their freeness*)
-Addsimps list.intrs;
-
-AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
-
-goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "not_CONS_self";
-
-goal SList.thy "!x. l ~= x#l";
-by (list_ind_tac "l" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "not_Cons_self2";
-
-
-goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
-by (list_ind_tac "xs" 1);
-by (Simp_tac 1);
-by (Asm_simp_tac 1);
-by (REPEAT(resolve_tac [exI,refl,conjI] 1));
-qed "neq_Nil_conv2";
-
-(** 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 (!simpset 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. *)
-
-goal SList.thy
- "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
- \ (%g. List_case c (%x y. d x y (g y)))";
-by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
-val List_rec_unfold = standard
- ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
-
-(*---------------------------------------------------------------------------
- * Old:
- * 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 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 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 (!simpset 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 (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 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_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 (!simpset 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 (!simpset addsimps list_rec_simps) 1]);
-end;
-
-Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
-
-
-(*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 (!simpset 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_induct2 1);
-by (ALLGOALS Asm_simp_tac);
-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_Nil3, append_Cons] = list_recs append_def;
-val [mem_Nil, mem_Cons] = list_recs mem_def;
-val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_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;
-
-Addsimps
- [null_Nil, ttl_Nil,
- mem_Nil, mem_Cons,
- list_case_Nil, list_case_Cons,
- append_Nil3, append_Cons,
- set_of_list_Nil, set_of_list_Cons,
- map_Nil, map_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);
-qed "append_assoc2";
-
-goal SList.thy "xs @ [] = xs";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "append_Nil4";
-
-(** 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 (!simpset setloop (split_tac [expand_if]))));
-qed "mem_append2";
-
-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 (!simpset setloop (split_tac [expand_if]))));
-qed "mem_filter2";
-
-
-(** The functional "map" **)
-
-Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
-
-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 (!simpset 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);
-by (Fast_tac 1);
-qed "expand_list_case2";
-
-
-(** Additional mapping lemmas **)
-
-goal SList.thy "map (%x.x) xs = xs";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_ident2";
-
-goal SList.thy "map f (xs@ys) = map f xs @ map f ys";
-by (list_ind_tac "xs" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "map_append2";
-
-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);
-qed "map_compose2";
-
-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(!simpset addsimps
- [Rep_map_type,list_sexp RS subsetD])));
-qed "Abs_Rep_map";
-
-Addsimps [append_Nil4, map_ident2];
--- a/src/HOL/ex/SList.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,119 +0,0 @@
-(* 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
- set_of_list :: ('a list => 'a set)
- mem :: ['a, 'a list] => bool (infixl 55)
- 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 filter *)
- "@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"
-
-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)
- (%g. List_case c (%x y. d x y (g y))) M"
-
- 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)"
-
- set_of_list_def "set_of_list xs == list_rec xs {} (%x l r. insert x r)"
-
- mem_def "x mem xs ==
- list_rec xs False (%y ys r. if y=x then True else 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
--- a/src/HOL/ex/Simult.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,298 +0,0 @@
-(* 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 (blast_tac (!claset 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 (blast_tac (!claset addIs (prems@[PartI])
- addEs [usumE, uprodE, PartE]) 1);
-qed "TF_induct";
-
-(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
-goalw Simult.thy [Part_def]
- "!!A. ! 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 (Blast_tac 1);
-qed "TF_induct_lemma";
-
-(*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);
- (*Blast_tac needs this type instantiation in order to preserve the
- right overloading of equality. The injectiveness properties for
- type 'a item hold only for set types.*)
-val PartE' = read_instantiate [("'a", "?'c set")] PartE;
-by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
-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 (!claset 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 (!claset 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*)
-AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
-AddSEs [Scons_inject];
-
-goalw Simult.thy TF_Rep_defs
- "!!A. [| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
-by (Blast_tac 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 (Blast_tac 1);
-qed "FNIL_I";
-
-goalw Simult.thy TF_Rep_defs
- "!!A. [| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
-\ FCONS M N : Part (TF A) In1";
-by (Blast_tac 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 (Blast_tac 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 (Blast_tac 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 (Blast_tac 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 (Blast_tac 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 (Blast_tac 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*)
-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 (Blast_tac 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 (Blast_tac 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 (Blast_tac 1);
-qed "Fcons_Fcons_eq";
-bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
-
-
-(*** TF_rec -- by wf recursion on pred_sexp ***)
-
-goal Simult.thy
- "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
- \ (%g. Case (Split(%x y. b x y (g y))) \
- \ (List_case c (%x y. d x y (g x) (g y))))";
-by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
-val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS
- ((result() RS eq_reflection) RS def_wfrec);
-
-(*---------------------------------------------------------------------------
- * Old:
- * 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 (!simpset addsimps [Case_In0, Split]) 1);
-by (asm_simp_tac (!simpset 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 (!simpset 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_ss = HOL_ss addsimps
- [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];
-
-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";
--- a/src/HOL/ex/Simult.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-(* 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)
- (%g. Case (Split(%x y. b x y (g y)))
- (List_case c (%x y. d x y (g x) (g y)))) M"
-
- 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
--- a/src/HOL/ex/Term.ML Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-(* 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 (!claset 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 (!claset 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 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. (ALL t: set_of_list ts. R t) ==> 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 (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Fast_tac);
-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_induct2 1); (*types force good instantiation*)
-by (ALLGOALS (asm_simp_tac (!simpset 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 ***)
-
-goal Term.thy
- "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
- \ (%g. Split(%x y. d x y (Abs_map g y)))";
-by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
-bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS
- ((result() RS eq_reflection) RS def_wfrec));
-
-(*---------------------------------------------------------------------------
- * Old:
- * 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 1);
-by (strip_tac 1);
-by (etac (pred_sexp_CONS_D RS conjE) 1);
-by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 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_ident2, 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;
--- a/src/HOL/ex/Term.thy Wed May 07 13:50:52 1997 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-(* 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)
- (%g. Split(%x y. d x y (Abs_map g y))) M"
-
- 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