Moved induction examples to directory Induct
authorpaulson
Wed May 07 13:51:22 1997 +0200 (1997-05-07)
changeset 31253f0ab2c306f7
parent 3124 1c0dfa7ebb72
child 3126 feb7a5d01c1e
Moved induction examples to directory Induct
src/HOL/IsaMakefile
src/HOL/Makefile
src/HOL/README.html
src/HOL/ex/Acc.ML
src/HOL/ex/Acc.thy
src/HOL/ex/Comb.ML
src/HOL/ex/Comb.thy
src/HOL/ex/LFilter.ML
src/HOL/ex/LFilter.thy
src/HOL/ex/LList.ML
src/HOL/ex/LList.thy
src/HOL/ex/Mutil.ML
src/HOL/ex/Mutil.thy
src/HOL/ex/Perm.ML
src/HOL/ex/Perm.thy
src/HOL/ex/PropLog.ML
src/HOL/ex/PropLog.thy
src/HOL/ex/ROOT.ML
src/HOL/ex/SList.ML
src/HOL/ex/SList.thy
src/HOL/ex/Simult.ML
src/HOL/ex/Simult.thy
src/HOL/ex/Term.ML
src/HOL/ex/Term.thy
     1.1 --- a/src/HOL/IsaMakefile	Wed May 07 13:50:52 1997 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Wed May 07 13:51:22 1997 +0200
     1.3 @@ -41,6 +41,17 @@
     1.4  
     1.5  #### Tests and examples
     1.6  
     1.7 +## Inductive definitions: simple examples
     1.8 +
     1.9 +INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
    1.10 +
    1.11 +INDUCT_FILES = Induct/ROOT.ML \
    1.12 +	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
    1.13 +
    1.14 +Induct:	$(OUT)/HOL $(INDUCT_FILES)
    1.15 +	@$(ISATOOL) usedir $(OUT)/HOL Induct
    1.16 +
    1.17 +
    1.18  ## IMP-semantics example
    1.19  
    1.20  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    1.21 @@ -185,8 +196,7 @@
    1.22  
    1.23  ## Miscellaneous examples
    1.24  
    1.25 -EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
    1.26 -	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
    1.27 +EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
    1.28  
    1.29  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    1.30  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    1.31 @@ -198,7 +208,8 @@
    1.32  ## Full test
    1.33  
    1.34  test:	$(OUT)/HOL \
    1.35 -	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
    1.36 +		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
    1.37 +		W0 MiniML IOA AxClasses Quot ex
    1.38  	echo 'Test examples ran successfully' > test
    1.39  
    1.40  
     2.1 --- a/src/HOL/Makefile	Wed May 07 13:50:52 1997 +0200
     2.2 +++ b/src/HOL/Makefile	Wed May 07 13:51:22 1997 +0200
     2.3 @@ -88,6 +88,21 @@
     2.4  	else echo 'exit_use_dir"../TFL";quit();' | $(LOGIC); \
     2.5  	fi
     2.6  
     2.7 +
     2.8 +## Inductive definitions: simple examples
     2.9 +
    2.10 +INDUCT_FILES =  Perm Comb Mutil SList LList LFilter Acc PropLog Term Simult
    2.11 +
    2.12 +INDUCT_FILES = Induct/ROOT.ML \
    2.13 +	    $(INDUCT_NAMES:%=Induct/%.thy) $(INDUCT_NAMES:%=Induct/%.ML)
    2.14 +
    2.15 +Induct:	$(BIN)/HOL $(INDUCT_FILES)
    2.16 +	@if [ "$${MAKE_HTML-undefined}" != "undefined" ]; \
    2.17 +	then echo 'make_html := true; exit_use_dir"Induct";quit();' | $(LOGIC); \
    2.18 +	else echo 'exit_use_dir"Induct";quit();' | $(LOGIC); \
    2.19 +	fi
    2.20 +
    2.21 +
    2.22  ##IMP-semantics example
    2.23  IMP_NAMES = Expr Com Natural Transition Denotation Hoare VC
    2.24  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
    2.25 @@ -201,8 +216,7 @@
    2.26  	fi
    2.27  
    2.28  ##Miscellaneous examples
    2.29 -EX_NAMES = String BT Perm Comb InSort Qsort LexProd Puzzle Mutil \
    2.30 -	   Primes NatSum SList LList LFilter Acc PropLog Term Simult MT
    2.31 +EX_NAMES = String BT InSort Qsort LexProd Puzzle Primes NatSum MT
    2.32  
    2.33  EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \
    2.34  	   ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    2.35 @@ -214,7 +228,9 @@
    2.36  	fi
    2.37  
    2.38  #Full test.
    2.39 -test:	$(BIN)/HOL TFL IMP Hoare Lex Integ Auth Subst Lambda MiniML ex
    2.40 +test:	$(BIN)/HOL \
    2.41 +		TFL Induct IMP Hoare Lex Integ Auth Subst Lambda  \
    2.42 +		W0 MiniML IOA AxClasses Quot ex
    2.43  	echo 'Test examples ran successfully' > test
    2.44  
    2.45  .PRECIOUS:  $(BIN)/Pure $(BIN)/HOL 
     3.1 --- a/src/HOL/README.html	Wed May 07 13:50:52 1997 +0200
     3.2 +++ b/src/HOL/README.html	Wed May 07 13:51:22 1997 +0200
     3.3 @@ -31,11 +31,14 @@
     3.4  <DT>IMP
     3.5  <DD>mechanization of a large part of a semantics text by Glynn Winskel
     3.6  
     3.7 +<DT>Induct
     3.8 +<DD>examples of (co)inductive definitions
     3.9 +
    3.10  <DT>Integ
    3.11  <DD>a theory of the integers including efficient integer calculations
    3.12  
    3.13  <DT>IOA
    3.14 -<DD>extended example of Input/Output Automata (takes a long time to run!)
    3.15 +<DD>extended example of Input/Output Automata
    3.16  
    3.17  <DT>Lambda
    3.18  <DD>a proof of the Church-Rosser theorem for lambda-calculus
     4.1 --- a/src/HOL/ex/Acc.ML	Wed May 07 13:50:52 1997 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,63 +0,0 @@
     4.4 -(*  Title:      HOL/ex/Acc
     4.5 -    ID:         $Id$
     4.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 -    Copyright   1994  University of Cambridge
     4.8 -
     4.9 -Inductive definition of acc(r)
    4.10 -
    4.11 -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    4.12 -Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    4.13 -*)
    4.14 -
    4.15 -open Acc;
    4.16 -
    4.17 -(*The intended introduction rule*)
    4.18 -val prems = goal Acc.thy
    4.19 -    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
    4.20 -by (fast_tac (!claset addIs (prems @ 
    4.21 -                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
    4.22 -qed "accI";
    4.23 -
    4.24 -goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
    4.25 -by (etac acc.elim 1);
    4.26 -by (rewtac pred_def);
    4.27 -by (Fast_tac 1);
    4.28 -qed "acc_downward";
    4.29 -
    4.30 -val [major,indhyp] = goal Acc.thy
    4.31 -    "[| a : acc(r);                                             \
    4.32 -\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
    4.33 -\    |] ==> P(a)";
    4.34 -by (rtac (major RS acc.induct) 1);
    4.35 -by (rtac indhyp 1);
    4.36 -by (resolve_tac acc.intrs 1);
    4.37 -by (rewtac pred_def);
    4.38 -by (Fast_tac 2);
    4.39 -by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
    4.40 -qed "acc_induct";
    4.41 -
    4.42 -
    4.43 -val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
    4.44 -by (rtac (major RS wfI) 1);
    4.45 -by (etac acc.induct 1);
    4.46 -by (rewtac pred_def);
    4.47 -by (Fast_tac 1);
    4.48 -qed "acc_wfI";
    4.49 -
    4.50 -val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
    4.51 -by (rtac (major RS wf_induct) 1);
    4.52 -by (rtac (impI RS allI) 1);
    4.53 -by (rtac accI 1);
    4.54 -by (Fast_tac 1);
    4.55 -qed "acc_wfD_lemma";
    4.56 -
    4.57 -val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
    4.58 -by (rtac subsetI 1);
    4.59 -by (res_inst_tac [("p", "x")] PairE 1);
    4.60 -by (fast_tac (!claset addSIs [SigmaI,
    4.61 -                             major RS acc_wfD_lemma RS spec RS mp]) 1);
    4.62 -qed "acc_wfD";
    4.63 -
    4.64 -goal Acc.thy "wf(r)  =  (r <= (acc r) Times (acc r))";
    4.65 -by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
    4.66 -qed "wf_acc_iff";
     5.1 --- a/src/HOL/ex/Acc.thy	Wed May 07 13:50:52 1997 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,26 +0,0 @@
     5.4 -(*  Title:      HOL/ex/Acc.thy
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1994  University of Cambridge
     5.8 -
     5.9 -Inductive definition of acc(r)
    5.10 -
    5.11 -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    5.12 -Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    5.13 -*)
    5.14 -
    5.15 -Acc = WF + 
    5.16 -
    5.17 -constdefs
    5.18 -  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
    5.19 -  "pred x r == {y. (y,x):r}"
    5.20 -
    5.21 -consts
    5.22 -  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
    5.23 -
    5.24 -inductive "acc(r)"
    5.25 -  intrs
    5.26 -    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
    5.27 -  monos     "[Pow_mono]"
    5.28 -
    5.29 -end
     6.1 --- a/src/HOL/ex/Comb.ML	Wed May 07 13:50:52 1997 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,179 +0,0 @@
     6.4 -(*  Title:      HOL/ex/comb.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson
     6.7 -    Copyright   1996  University of Cambridge
     6.8 -
     6.9 -Combinatory Logic example: the Church-Rosser Theorem
    6.10 -Curiously, combinators do not include free variables.
    6.11 -
    6.12 -Example taken from
    6.13 -    J. Camilleri and T. F. Melham.
    6.14 -    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    6.15 -    Report 265, University of Cambridge Computer Laboratory, 1992.
    6.16 -
    6.17 -HOL system proofs may be found in
    6.18 -/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    6.19 -*)
    6.20 -
    6.21 -open Comb;
    6.22 -
    6.23 -(*** Reflexive/Transitive closure preserves the Church-Rosser property 
    6.24 -     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
    6.25 -***)
    6.26 -
    6.27 -val [_, spec_mp] = [spec] RL [mp];
    6.28 -
    6.29 -(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
    6.30 -goalw Comb.thy [diamond_def]
    6.31 -    "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
    6.32 -\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
    6.33 -by (etac rtrancl_induct 1);
    6.34 -by (Blast_tac 1);
    6.35 -by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    6.36 -                           addSDs [spec_mp]) 1);
    6.37 -val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
    6.38 -
    6.39 -val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
    6.40 -by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
    6.41 -by (rtac (impI RS allI RS allI) 1);
    6.42 -by (etac rtrancl_induct 1);
    6.43 -by (Blast_tac 1);
    6.44 -by (slow_best_tac  (*Seems to be a brittle, undirected search*)
    6.45 -    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    6.46 -            addEs [major RS diamond_strip_lemmaE]) 1);
    6.47 -qed "diamond_rtrancl";
    6.48 -
    6.49 -
    6.50 -(*** Results about Contraction ***)
    6.51 -
    6.52 -(*Derive a case for each combinator constructor*)
    6.53 -val K_contractE = contract.mk_cases comb.simps "K -1-> z";
    6.54 -val S_contractE = contract.mk_cases comb.simps "S -1-> z";
    6.55 -val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
    6.56 -
    6.57 -AddSIs [contract.K, contract.S];
    6.58 -AddIs  [contract.Ap1, contract.Ap2];
    6.59 -AddSEs [K_contractE, S_contractE, Ap_contractE];
    6.60 -Unsafe_Addss  (!simpset);
    6.61 -
    6.62 -goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
    6.63 -by (Blast_tac 1);
    6.64 -qed "I_contract_E";
    6.65 -AddSEs [I_contract_E];
    6.66 -
    6.67 -goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
    6.68 -by (Blast_tac 1);
    6.69 -qed "K1_contractD";
    6.70 -AddSEs [K1_contractD];
    6.71 -
    6.72 -goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
    6.73 -by (etac rtrancl_induct 1);
    6.74 -by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
    6.75 -qed "Ap_reduce1";
    6.76 -
    6.77 -goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
    6.78 -by (etac rtrancl_induct 1);
    6.79 -by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
    6.80 -qed "Ap_reduce2";
    6.81 -
    6.82 -(** Counterexample to the diamond property for -1-> **)
    6.83 -
    6.84 -goal Comb.thy "K#I#(I#I) -1-> I";
    6.85 -by (rtac contract.K 1);
    6.86 -qed "KIII_contract1";
    6.87 -
    6.88 -goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
    6.89 -by (Blast_tac 1);
    6.90 -qed "KIII_contract2";
    6.91 -
    6.92 -goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
    6.93 -by (Blast_tac 1);
    6.94 -qed "KIII_contract3";
    6.95 -
    6.96 -goalw Comb.thy [diamond_def] "~ diamond(contract)";
    6.97 -by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
    6.98 -qed "not_diamond_contract";
    6.99 -
   6.100 -
   6.101 -
   6.102 -(*** Results about Parallel Contraction ***)
   6.103 -
   6.104 -(*Derive a case for each combinator constructor*)
   6.105 -val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
   6.106 -val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
   6.107 -val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
   6.108 -
   6.109 -AddIs  parcontract.intrs;
   6.110 -AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
   6.111 -Unsafe_Addss  (!simpset);
   6.112 -
   6.113 -(*** Basic properties of parallel contraction ***)
   6.114 -
   6.115 -goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
   6.116 -by (Blast_tac 1);
   6.117 -qed "K1_parcontractD";
   6.118 -AddSDs [K1_parcontractD];
   6.119 -
   6.120 -goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
   6.121 -by (Blast_tac 1);
   6.122 -qed "S1_parcontractD";
   6.123 -AddSDs [S1_parcontractD];
   6.124 -
   6.125 -goal Comb.thy
   6.126 - "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
   6.127 -by (Blast_tac 1);
   6.128 -qed "S2_parcontractD";
   6.129 -AddSDs [S2_parcontractD];
   6.130 -
   6.131 -(*The rules above are not essential but make proofs much faster*)
   6.132 -
   6.133 -
   6.134 -(*Church-Rosser property for parallel contraction*)
   6.135 -goalw Comb.thy [diamond_def] "diamond parcontract";
   6.136 -by (rtac (impI RS allI RS allI) 1);
   6.137 -by (etac parcontract.induct 1 THEN prune_params_tac);
   6.138 -by (Step_tac 1);
   6.139 -by (ALLGOALS Blast_tac);
   6.140 -qed "diamond_parcontract";
   6.141 -
   6.142 -
   6.143 -(*** Equivalence of x--->y and x===>y ***)
   6.144 -
   6.145 -goal Comb.thy "contract <= parcontract";
   6.146 -by (rtac subsetI 1);
   6.147 -by (split_all_tac 1);
   6.148 -by (etac contract.induct 1);
   6.149 -by (ALLGOALS Blast_tac);
   6.150 -qed "contract_subset_parcontract";
   6.151 -
   6.152 -(*Reductions: simply throw together reflexivity, transitivity and
   6.153 -  the one-step reductions*)
   6.154 -
   6.155 -AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
   6.156 -
   6.157 -(*Example only: not used*)
   6.158 -goalw Comb.thy [I_def] "I#x ---> x";
   6.159 -by (Blast_tac 1);
   6.160 -qed "reduce_I";
   6.161 -
   6.162 -goal Comb.thy "parcontract <= contract^*";
   6.163 -by (rtac subsetI 1);
   6.164 -by (split_all_tac 1);
   6.165 -by (etac parcontract.induct 1 THEN prune_params_tac);
   6.166 -by (ALLGOALS Blast_tac);
   6.167 -qed "parcontract_subset_reduce";
   6.168 -
   6.169 -goal Comb.thy "contract^* = parcontract^*";
   6.170 -by (REPEAT 
   6.171 -    (resolve_tac [equalityI, 
   6.172 -                  contract_subset_parcontract RS rtrancl_mono, 
   6.173 -                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
   6.174 -qed "reduce_eq_parreduce";
   6.175 -
   6.176 -goal Comb.thy "diamond(contract^*)";
   6.177 -by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, 
   6.178 -                                 diamond_parcontract]) 1);
   6.179 -qed "diamond_reduce";
   6.180 -
   6.181 -
   6.182 -writeln"Reached end of file.";
     7.1 --- a/src/HOL/ex/Comb.thy	Wed May 07 13:50:52 1997 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,74 +0,0 @@
     7.4 -(*  Title:      HOL/ex/Comb.thy
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson
     7.7 -    Copyright   1996  University of Cambridge
     7.8 -
     7.9 -Combinatory Logic example: the Church-Rosser Theorem
    7.10 -Curiously, combinators do not include free variables.
    7.11 -
    7.12 -Example taken from
    7.13 -    J. Camilleri and T. F. Melham.
    7.14 -    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    7.15 -    Report 265, University of Cambridge Computer Laboratory, 1992.
    7.16 -*)
    7.17 -
    7.18 -
    7.19 -Comb = Trancl +
    7.20 -
    7.21 -(** Datatype definition of combinators S and K, with infixed application **)
    7.22 -datatype comb = K
    7.23 -              | S
    7.24 -              | "#" comb comb (infixl 90)
    7.25 -
    7.26 -(** Inductive definition of contractions, -1->
    7.27 -             and (multi-step) reductions, --->
    7.28 -**)
    7.29 -consts
    7.30 -  contract  :: "(comb*comb) set"
    7.31 -  "-1->"    :: [comb,comb] => bool   (infixl 50)
    7.32 -  "--->"    :: [comb,comb] => bool   (infixl 50)
    7.33 -
    7.34 -translations
    7.35 -  "x -1-> y" == "(x,y) : contract"
    7.36 -  "x ---> y" == "(x,y) : contract^*"
    7.37 -
    7.38 -inductive contract
    7.39 -  intrs
    7.40 -    K     "K#x#y -1-> x"
    7.41 -    S     "S#x#y#z -1-> (x#z)#(y#z)"
    7.42 -    Ap1   "x-1->y ==> x#z -1-> y#z"
    7.43 -    Ap2   "x-1->y ==> z#x -1-> z#y"
    7.44 -
    7.45 -
    7.46 -(** Inductive definition of parallel contractions, =1=>
    7.47 -             and (multi-step) parallel reductions, ===>
    7.48 -**)
    7.49 -consts
    7.50 -  parcontract :: "(comb*comb) set"
    7.51 -  "=1=>"    :: [comb,comb] => bool   (infixl 50)
    7.52 -  "===>"    :: [comb,comb] => bool   (infixl 50)
    7.53 -
    7.54 -translations
    7.55 -  "x =1=> y" == "(x,y) : parcontract"
    7.56 -  "x ===> y" == "(x,y) : parcontract^*"
    7.57 -
    7.58 -inductive parcontract
    7.59 -  intrs
    7.60 -    refl  "x =1=> x"
    7.61 -    K     "K#x#y =1=> x"
    7.62 -    S     "S#x#y#z =1=> (x#z)#(y#z)"
    7.63 -    Ap    "[| x=1=>y;  z=1=>w |] ==> x#z =1=> y#w"
    7.64 -
    7.65 -
    7.66 -(*Misc definitions*)
    7.67 -constdefs
    7.68 -  I :: comb
    7.69 -  "I == S#K#K"
    7.70 -
    7.71 -  (*confluence; Lambda/Commutation treats this more abstractly*)
    7.72 -  diamond   :: "('a * 'a)set => bool"	
    7.73 -  "diamond(r) == ALL x y. (x,y):r --> 
    7.74 -                  (ALL y'. (x,y'):r --> 
    7.75 -                    (EX z. (y,z):r & (y',z) : r))"
    7.76 -
    7.77 -end
     8.1 --- a/src/HOL/ex/LFilter.ML	Wed May 07 13:50:52 1997 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,341 +0,0 @@
     8.4 -(*  Title:      HOL/ex/LFilter
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1997  University of Cambridge
     8.8 -
     8.9 -The "filter" functional for coinductive lists
    8.10 -  --defined by a combination of induction and coinduction
    8.11 -*)
    8.12 -
    8.13 -open LFilter;
    8.14 -
    8.15 -
    8.16 -(*** findRel: basic laws ****)
    8.17 -
    8.18 -val findRel_LConsE = 
    8.19 -    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
    8.20 -
    8.21 -AddSEs [findRel_LConsE];
    8.22 -
    8.23 -
    8.24 -goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    8.25 -by (etac findRel.induct 1);
    8.26 -by (Blast_tac 1);
    8.27 -by (Blast_tac 1);
    8.28 -qed_spec_mp "findRel_functional";
    8.29 -
    8.30 -goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
    8.31 -by (etac findRel.induct 1);
    8.32 -by (Blast_tac 1);
    8.33 -by (Blast_tac 1);
    8.34 -qed_spec_mp "findRel_imp_LCons";
    8.35 -
    8.36 -goal thy "!!p. (LNil,l): findRel p ==> R";
    8.37 -by (blast_tac (!claset addEs [findRel.elim]) 1);
    8.38 -qed "findRel_LNil";
    8.39 -
    8.40 -AddSEs [findRel_LNil];
    8.41 -
    8.42 -
    8.43 -(*** Properties of Domain (findRel p) ***)
    8.44 -
    8.45 -goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
    8.46 -by (case_tac "p x" 1);
    8.47 -by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
    8.48 -qed "LCons_Domain_findRel";
    8.49 -
    8.50 -Addsimps [LCons_Domain_findRel];
    8.51 -
    8.52 -val major::prems = 
    8.53 -goal thy "[| l: Domain (findRel p);                                   \
    8.54 -\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
    8.55 -\         |] ==> Q";
    8.56 -by (rtac (major RS DomainE) 1);
    8.57 -by (forward_tac [findRel_imp_LCons] 1);
    8.58 -by (REPEAT (eresolve_tac [exE,conjE] 1));
    8.59 -by (hyp_subst_tac 1);
    8.60 -by (REPEAT (ares_tac prems 1));
    8.61 -qed "Domain_findRelE";
    8.62 -
    8.63 -val prems = goal thy
    8.64 -    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
    8.65 -by (Step_tac 1);
    8.66 -by (etac findRel.induct 1);
    8.67 -by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
    8.68 -by (blast_tac (!claset addIs findRel.intrs) 1);
    8.69 -qed "Domain_findRel_mono";
    8.70 -
    8.71 -
    8.72 -(*** find: basic equations ***)
    8.73 -
    8.74 -goalw thy [find_def] "find p LNil = LNil";
    8.75 -by (blast_tac (!claset addIs [select_equality]) 1);
    8.76 -qed "find_LNil";
    8.77 -
    8.78 -goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
    8.79 -by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
    8.80 -qed "findRel_imp_find";
    8.81 -
    8.82 -goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
    8.83 -by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
    8.84 -qed "find_LCons_found";
    8.85 -
    8.86 -goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
    8.87 -by (blast_tac (!claset addIs [select_equality]) 1);
    8.88 -qed "diverge_find_LNil";
    8.89 -
    8.90 -Addsimps [diverge_find_LNil];
    8.91 -
    8.92 -goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
    8.93 -by (case_tac "LCons x l : Domain(findRel p)" 1);
    8.94 -by (Asm_full_simp_tac 2);
    8.95 -by (Step_tac 1);
    8.96 -by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
    8.97 -by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
    8.98 -qed "find_LCons_seek";
    8.99 -
   8.100 -goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
   8.101 -by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
   8.102 -                           setloop split_tac[expand_if]) 1);
   8.103 -qed "find_LCons";
   8.104 -
   8.105 -
   8.106 -
   8.107 -(*** lfilter: basic equations ***)
   8.108 -
   8.109 -goal thy "lfilter p LNil = LNil";
   8.110 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   8.111 -by (simp_tac (!simpset addsimps [find_LNil]) 1);
   8.112 -qed "lfilter_LNil";
   8.113 -
   8.114 -goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
   8.115 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   8.116 -by (Asm_simp_tac 1);
   8.117 -qed "diverge_lfilter_LNil";
   8.118 -
   8.119 -
   8.120 -goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
   8.121 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   8.122 -by (asm_simp_tac (!simpset addsimps [find_LCons_found]) 1);
   8.123 -qed "lfilter_LCons_found";
   8.124 -
   8.125 -
   8.126 -goal thy "!!p. (l, LCons x l') : findRel p \
   8.127 -\              ==> lfilter p l = LCons x (lfilter p l')";
   8.128 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   8.129 -by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
   8.130 -qed "findRel_imp_lfilter";
   8.131 -
   8.132 -goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
   8.133 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   8.134 -by (case_tac "LCons x l : Domain(findRel p)" 1);
   8.135 -by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   8.136 -by (etac Domain_findRelE 1);
   8.137 -by (safe_tac (!claset delrules [conjI]));
   8.138 -by (asm_full_simp_tac 
   8.139 -    (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
   8.140 -                        find_LCons_seek]) 1);
   8.141 -qed "lfilter_LCons_seek";
   8.142 -
   8.143 -
   8.144 -goal thy "lfilter p (LCons x l) = \
   8.145 -\         (if p x then LCons x (lfilter p l) else lfilter p l)";
   8.146 -by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
   8.147 -                           setloop split_tac[expand_if]) 1);
   8.148 -qed "lfilter_LCons";
   8.149 -
   8.150 -AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   8.151 -Addsimps [lfilter_LNil, lfilter_LCons];
   8.152 -
   8.153 -
   8.154 -goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
   8.155 -by (rtac notI 1);
   8.156 -by (etac Domain_findRelE 1);
   8.157 -by (etac rev_mp 1);
   8.158 -by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   8.159 -qed "lfilter_eq_LNil";
   8.160 -
   8.161 -
   8.162 -goal thy "!!p. lfilter p l = LCons x l' -->     \
   8.163 -\              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
   8.164 -by (stac (lfilter_def RS def_llist_corec) 1);
   8.165 -by (case_tac "l : Domain(findRel p)" 1);
   8.166 -by (etac Domain_findRelE 1);
   8.167 -by (Asm_simp_tac 2);
   8.168 -by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
   8.169 -by (Blast_tac 1);
   8.170 -qed_spec_mp "lfilter_eq_LCons";
   8.171 -
   8.172 -
   8.173 -goal thy "lfilter p l = LNil  |  \
   8.174 -\         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
   8.175 -by (case_tac "l : Domain(findRel p)" 1);
   8.176 -by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   8.177 -by (blast_tac (!claset addSEs [Domain_findRelE] 
   8.178 -                       addIs [findRel_imp_lfilter]) 1);
   8.179 -qed "lfilter_cases";
   8.180 -
   8.181 -
   8.182 -(*** lfilter: simple facts by coinduction ***)
   8.183 -
   8.184 -goal thy "lfilter (%x.True) l = l";
   8.185 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   8.186 -by (ALLGOALS Simp_tac);
   8.187 -by (Blast_tac 1);
   8.188 -qed "lfilter_K_True";
   8.189 -
   8.190 -goal thy "lfilter p (lfilter p l) = lfilter p l";
   8.191 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   8.192 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   8.193 -by (Step_tac 1);
   8.194 -(*Cases: p x is true or false*)
   8.195 -by (Blast_tac 1);
   8.196 -by (rtac (lfilter_cases RS disjE) 1);
   8.197 -by (etac ssubst 1);
   8.198 -by (Auto_tac());
   8.199 -qed "lfilter_idem";
   8.200 -
   8.201 -
   8.202 -(*** Numerous lemmas required to prove lfilter_conj:
   8.203 -     lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
   8.204 - ***)
   8.205 -
   8.206 -goal thy "!!p. (l,l') : findRel q \
   8.207 -\           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
   8.208 -by (etac findRel.induct 1);
   8.209 -by (blast_tac (!claset addIs findRel.intrs) 1);
   8.210 -by (blast_tac (!claset addIs findRel.intrs) 1);
   8.211 -qed_spec_mp "findRel_conj_lemma";
   8.212 -
   8.213 -val findRel_conj = refl RSN (2, findRel_conj_lemma);
   8.214 -
   8.215 -goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
   8.216 -\              ==> (l, LCons x l') : findRel q --> ~ p x     \
   8.217 -\                  --> l' : Domain (findRel (%x. p x & q x))";
   8.218 -by (etac findRel.induct 1);
   8.219 -by (Auto_tac());
   8.220 -qed_spec_mp "findRel_not_conj_Domain";
   8.221 -
   8.222 -
   8.223 -goal thy "!!p. (l,lxx) : findRel q ==> \
   8.224 -\            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
   8.225 -\            --> (l,lz) : findRel (%x. p x & q x)";
   8.226 -by (etac findRel.induct 1);
   8.227 -by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
   8.228 -qed_spec_mp "findRel_conj2";
   8.229 -
   8.230 -
   8.231 -goal thy "!!p. (lx,ly) : findRel p \
   8.232 -\              ==> ALL l. lx = lfilter q l \
   8.233 -\                  --> l : Domain (findRel(%x. p x & q x))";
   8.234 -by (etac findRel.induct 1);
   8.235 -by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
   8.236 -                       addIs  [findRel_conj]) 1);
   8.237 -by (Auto_tac());
   8.238 -by (dtac (sym RS lfilter_eq_LCons) 1);
   8.239 -by (Auto_tac());
   8.240 -by (dtac spec 1);
   8.241 -by (dtac (refl RS rev_mp) 1);
   8.242 -by (blast_tac (!claset addIs [findRel_conj2]) 1);
   8.243 -qed_spec_mp "findRel_lfilter_Domain_conj";
   8.244 -
   8.245 -
   8.246 -goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
   8.247 -\              ==> l'' = LCons y l' --> \
   8.248 -\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
   8.249 -by (etac findRel.induct 1);
   8.250 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
   8.251 -by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
   8.252 -qed_spec_mp "findRel_conj_lfilter";
   8.253 -
   8.254 -
   8.255 -
   8.256 -goal thy "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)  \
   8.257 -\         : llistD_Fun (range                                   \
   8.258 -\                       (%u. (lfilter p (lfilter q u),          \
   8.259 -\                             lfilter (%x. p x & q x) u)))";
   8.260 -by (case_tac "l : Domain(findRel q)" 1);
   8.261 -by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   8.262 -by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
   8.263 -(*There are no qs in l: both lists are LNil*)
   8.264 -by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   8.265 -by (etac Domain_findRelE 1);
   8.266 -(*case q x*)
   8.267 -by (case_tac "p x" 1);
   8.268 -by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
   8.269 -                                     findRel_conj RS findRel_imp_lfilter]) 1);
   8.270 -by (Blast_tac 1);
   8.271 -(*case q x and ~(p x) *)
   8.272 -by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   8.273 -by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
   8.274 -(*subcase: there is no p&q in l' and therefore none in l*)
   8.275 -by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   8.276 -by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
   8.277 -by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
   8.278 -by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
   8.279 -(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
   8.280 -by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   8.281 -(*subcase: there is a p&q in l' and therefore also one in l*)
   8.282 -by (etac Domain_findRelE 1);
   8.283 -by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
   8.284 -by (blast_tac (!claset addIs [findRel_conj2]) 2);
   8.285 -by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
   8.286 -by (blast_tac (!claset addIs [findRel_conj_lfilter]) 2);
   8.287 -by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   8.288 -by (Blast_tac 1);
   8.289 -val lemma = result();
   8.290 -
   8.291 -
   8.292 -goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
   8.293 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   8.294 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   8.295 -by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
   8.296 -qed "lfilter_conj";
   8.297 -
   8.298 -
   8.299 -(*** Numerous lemmas required to prove ??:
   8.300 -     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
   8.301 - ***)
   8.302 -
   8.303 -goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
   8.304 -by (etac findRel.induct 1);
   8.305 -by (ALLGOALS Asm_full_simp_tac);
   8.306 -qed "findRel_lmap_Domain";
   8.307 -
   8.308 -
   8.309 -goal thy "!!p. lmap f l = LCons x l' -->     \
   8.310 -\              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
   8.311 -by (stac (lmap_def RS def_llist_corec) 1);
   8.312 -by (res_inst_tac [("l", "l")] llistE 1);
   8.313 -by (Auto_tac());
   8.314 -qed_spec_mp "lmap_eq_LCons";
   8.315 -
   8.316 -
   8.317 -goal thy "!!p. (lx,ly) : findRel p ==>  \
   8.318 -\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
   8.319 -\    (EX y l''. x = f y & l' = lmap f l'' &       \
   8.320 -\    (l, LCons y l'') : findRel(%x. p(f x)))";
   8.321 -by (etac findRel.induct 1);
   8.322 -by (ALLGOALS Asm_simp_tac);
   8.323 -by (safe_tac (!claset addSDs [lmap_eq_LCons]));
   8.324 -by (blast_tac (!claset addIs findRel.intrs) 1);
   8.325 -by (blast_tac (!claset addIs findRel.intrs) 1);
   8.326 -qed_spec_mp "lmap_LCons_findRel_lemma";
   8.327 -
   8.328 -val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
   8.329 -
   8.330 -goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
   8.331 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   8.332 -by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   8.333 -by (Step_tac 1);
   8.334 -by (Blast_tac 1);
   8.335 -by (case_tac "lmap f l : Domain (findRel p)" 1);
   8.336 -by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
   8.337 -by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
   8.338 -by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   8.339 -by (etac Domain_findRelE 1);
   8.340 -by (forward_tac [lmap_LCons_findRel] 1);
   8.341 -by (Step_tac 1);
   8.342 -by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   8.343 -by (Blast_tac 1);
   8.344 -qed "lfilter_lmap";
     9.1 --- a/src/HOL/ex/LFilter.thy	Wed May 07 13:50:52 1997 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,29 +0,0 @@
     9.4 -(*  Title:      HOL/LList.thy
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1997  University of Cambridge
     9.8 -
     9.9 -The "filter" functional for coinductive lists
    9.10 -  --defined by a combination of induction and coinduction
    9.11 -*)
    9.12 -
    9.13 -LFilter = LList + Relation +
    9.14 -
    9.15 -consts
    9.16 -  findRel	:: "('a => bool) => ('a llist * 'a llist)set"
    9.17 -
    9.18 -inductive "findRel p"
    9.19 -  intrs
    9.20 -    found  "p x ==> (LCons x l, LCons x l) : findRel p"
    9.21 -    seek   "[| ~p x;  (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
    9.22 -
    9.23 -constdefs
    9.24 -  find		:: ['a => bool, 'a llist] => 'a llist
    9.25 -    "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
    9.26 -
    9.27 -  lfilter	:: ['a => bool, 'a llist] => 'a llist
    9.28 -    "lfilter p l == llist_corec l (%l. case find p l of
    9.29 -                                            LNil => Inl ()
    9.30 -                                          | LCons y z => Inr(y,z))"
    9.31 -
    9.32 -end
    10.1 --- a/src/HOL/ex/LList.ML	Wed May 07 13:50:52 1997 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,886 +0,0 @@
    10.4 -(*  Title:      HOL/ex/LList
    10.5 -    ID:         $Id$
    10.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 -    Copyright   1993  University of Cambridge
    10.8 -
    10.9 -SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
   10.10 -*)
   10.11 -
   10.12 -open LList;
   10.13 -
   10.14 -(** Simplification **)
   10.15 -
   10.16 -simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
   10.17 -
   10.18 -(*For adding _eqI rules to a simpset; we must remove Pair_eq because
   10.19 -  it may turn an instance of reflexivity into a conjunction!*)
   10.20 -fun add_eqI ss = ss addsimps [range_eqI, image_eqI] 
   10.21 -                    delsimps [Pair_eq];
   10.22 -
   10.23 -
   10.24 -(*This justifies using llist in other recursive type definitions*)
   10.25 -goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
   10.26 -by (rtac gfp_mono 1);
   10.27 -by (REPEAT (ares_tac basic_monos 1));
   10.28 -qed "llist_mono";
   10.29 -
   10.30 -
   10.31 -goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
   10.32 -let val rew = rewrite_rule [NIL_def, CONS_def] in  
   10.33 -by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
   10.34 -                      addEs [rew llist.elim]) 1)
   10.35 -end;
   10.36 -qed "llist_unfold";
   10.37 -
   10.38 -
   10.39 -(*** Type checking by coinduction, using list_Fun 
   10.40 -     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
   10.41 -***)
   10.42 -
   10.43 -goalw LList.thy [list_Fun_def]
   10.44 -    "!!M. [| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
   10.45 -by (etac llist.coinduct 1);
   10.46 -by (etac (subsetD RS CollectD) 1);
   10.47 -by (assume_tac 1);
   10.48 -qed "llist_coinduct";
   10.49 -
   10.50 -goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
   10.51 -by (Fast_tac 1);
   10.52 -qed "list_Fun_NIL_I";
   10.53 -
   10.54 -goalw LList.thy [list_Fun_def,CONS_def]
   10.55 -    "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
   10.56 -by (Fast_tac 1);
   10.57 -qed "list_Fun_CONS_I";
   10.58 -
   10.59 -(*Utilise the "strong" part, i.e. gfp(f)*)
   10.60 -goalw LList.thy (llist.defs @ [list_Fun_def])
   10.61 -    "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
   10.62 -by (etac (llist.mono RS gfp_fun_UnI2) 1);
   10.63 -qed "list_Fun_llist_I";
   10.64 -
   10.65 -(*** LList_corec satisfies the desired recurion equation ***)
   10.66 -
   10.67 -(*A continuity result?*)
   10.68 -goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))";
   10.69 -by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
   10.70 -qed "CONS_UN1";
   10.71 -
   10.72 -(*UNUSED; obsolete?
   10.73 -goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
   10.74 -by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
   10.75 -qed "split_UN1";
   10.76 -
   10.77 -goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
   10.78 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
   10.79 -qed "sum_case2_UN1";
   10.80 -*)
   10.81 -
   10.82 -val prems = goalw LList.thy [CONS_def]
   10.83 -    "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
   10.84 -by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
   10.85 -qed "CONS_mono";
   10.86 -
   10.87 -Addsimps [LList_corec_fun_def RS def_nat_rec_0,
   10.88 -          LList_corec_fun_def RS def_nat_rec_Suc];
   10.89 -
   10.90 -(** The directions of the equality are proved separately **)
   10.91 -
   10.92 -goalw LList.thy [LList_corec_def]
   10.93 -    "LList_corec a f <= sum_case (%u.NIL) \
   10.94 -\                          (split(%z w. CONS z (LList_corec w f))) (f a)";
   10.95 -by (rtac UN1_least 1);
   10.96 -by (res_inst_tac [("n","k")] natE 1);
   10.97 -by (ALLGOALS (Asm_simp_tac));
   10.98 -by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
   10.99 -qed "LList_corec_subset1";
  10.100 -
  10.101 -goalw LList.thy [LList_corec_def]
  10.102 -    "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
  10.103 -\    LList_corec a f";
  10.104 -by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
  10.105 -by (safe_tac (!claset));
  10.106 -by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
  10.107 -qed "LList_corec_subset2";
  10.108 -
  10.109 -(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
  10.110 -goal LList.thy
  10.111 -    "LList_corec a f = sum_case (%u. NIL) \
  10.112 -\                           (split(%z w. CONS z (LList_corec w f))) (f a)";
  10.113 -by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
  10.114 -                         LList_corec_subset2] 1));
  10.115 -qed "LList_corec";
  10.116 -
  10.117 -(*definitional version of same*)
  10.118 -val [rew] = goal LList.thy
  10.119 -    "[| !!x. h(x) == LList_corec x f |] ==>     \
  10.120 -\    h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
  10.121 -by (rewtac rew);
  10.122 -by (rtac LList_corec 1);
  10.123 -qed "def_LList_corec";
  10.124 -
  10.125 -(*A typical use of co-induction to show membership in the gfp. 
  10.126 -  Bisimulation is  range(%x. LList_corec x f) *)
  10.127 -goal LList.thy "LList_corec a f : llist({u.True})";
  10.128 -by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
  10.129 -by (rtac rangeI 1);
  10.130 -by (safe_tac (!claset));
  10.131 -by (stac LList_corec 1);
  10.132 -by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
  10.133 -                       |> add_eqI) 1);
  10.134 -qed "LList_corec_type";
  10.135 -
  10.136 -(*Lemma for the proof of llist_corec*)
  10.137 -goal LList.thy
  10.138 -   "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
  10.139 -\   llist(range Leaf)";
  10.140 -by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
  10.141 -by (rtac rangeI 1);
  10.142 -by (safe_tac (!claset));
  10.143 -by (stac LList_corec 1);
  10.144 -by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
  10.145 -by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
  10.146 -qed "LList_corec_type2";
  10.147 -
  10.148 -
  10.149 -(**** llist equality as a gfp; the bisimulation principle ****)
  10.150 -
  10.151 -(*This theorem is actually used, unlike the many similar ones in ZF*)
  10.152 -goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
  10.153 -let val rew = rewrite_rule [NIL_def, CONS_def] in  
  10.154 -by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
  10.155 -                      addEs [rew LListD.elim]) 1)
  10.156 -end;
  10.157 -qed "LListD_unfold";
  10.158 -
  10.159 -goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
  10.160 -by (res_inst_tac [("n", "k")] less_induct 1);
  10.161 -by (safe_tac ((claset_of "Fun") delrules [equalityI]));
  10.162 -by (etac LListD.elim 1);
  10.163 -by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
  10.164 -by (res_inst_tac [("n", "n")] natE 1);
  10.165 -by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
  10.166 -by (rename_tac "n'" 1);
  10.167 -by (res_inst_tac [("n", "n'")] natE 1);
  10.168 -by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
  10.169 -by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
  10.170 -qed "LListD_implies_ntrunc_equality";
  10.171 -
  10.172 -(*The domain of the LListD relation*)
  10.173 -goalw LList.thy (llist.defs @ [NIL_def, CONS_def])
  10.174 -    "fst``LListD(diag(A)) <= llist(A)";
  10.175 -by (rtac gfp_upperbound 1);
  10.176 -(*avoids unfolding LListD on the rhs*)
  10.177 -by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
  10.178 -by (Simp_tac 1);
  10.179 -by (Fast_tac 1);
  10.180 -qed "fst_image_LListD";
  10.181 -
  10.182 -(*This inclusion justifies the use of coinduction to show M=N*)
  10.183 -goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
  10.184 -by (rtac subsetI 1);
  10.185 -by (res_inst_tac [("p","x")] PairE 1);
  10.186 -by (safe_tac (!claset));
  10.187 -by (rtac diag_eqI 1);
  10.188 -by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
  10.189 -          ntrunc_equality) 1);
  10.190 -by (assume_tac 1);
  10.191 -by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
  10.192 -qed "LListD_subset_diag";
  10.193 -
  10.194 -
  10.195 -(** Coinduction, using LListD_Fun
  10.196 -    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  10.197 - **)
  10.198 -
  10.199 -goalw thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
  10.200 -by (REPEAT (ares_tac basic_monos 1));
  10.201 -qed "LListD_Fun_mono";
  10.202 -
  10.203 -goalw LList.thy [LListD_Fun_def]
  10.204 -    "!!M. [| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
  10.205 -by (etac LListD.coinduct 1);
  10.206 -by (etac (subsetD RS CollectD) 1);
  10.207 -by (assume_tac 1);
  10.208 -qed "LListD_coinduct";
  10.209 -
  10.210 -goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
  10.211 -by (Fast_tac 1);
  10.212 -qed "LListD_Fun_NIL_I";
  10.213 -
  10.214 -goalw LList.thy [LListD_Fun_def,CONS_def]
  10.215 - "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
  10.216 -by (Fast_tac 1);
  10.217 -qed "LListD_Fun_CONS_I";
  10.218 -
  10.219 -(*Utilise the "strong" part, i.e. gfp(f)*)
  10.220 -goalw LList.thy (LListD.defs @ [LListD_Fun_def])
  10.221 -    "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
  10.222 -by (etac (LListD.mono RS gfp_fun_UnI2) 1);
  10.223 -qed "LListD_Fun_LListD_I";
  10.224 -
  10.225 -
  10.226 -(*This converse inclusion helps to strengthen LList_equalityI*)
  10.227 -goal LList.thy "diag(llist(A)) <= LListD(diag(A))";
  10.228 -by (rtac subsetI 1);
  10.229 -by (etac LListD_coinduct 1);
  10.230 -by (rtac subsetI 1);
  10.231 -by (etac diagE 1);
  10.232 -by (etac ssubst 1);
  10.233 -by (eresolve_tac [llist.elim] 1);
  10.234 -by (ALLGOALS
  10.235 -    (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I,
  10.236 -                                      LListD_Fun_CONS_I])));
  10.237 -qed "diag_subset_LListD";
  10.238 -
  10.239 -goal LList.thy "LListD(diag(A)) = diag(llist(A))";
  10.240 -by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
  10.241 -                         diag_subset_LListD] 1));
  10.242 -qed "LListD_eq_diag";
  10.243 -
  10.244 -goal LList.thy 
  10.245 -    "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
  10.246 -by (rtac (LListD_eq_diag RS subst) 1);
  10.247 -by (rtac LListD_Fun_LListD_I 1);
  10.248 -by (asm_simp_tac (!simpset addsimps [LListD_eq_diag, diagI]) 1);
  10.249 -qed "LListD_Fun_diag_I";
  10.250 -
  10.251 -
  10.252 -(** To show two LLists are equal, exhibit a bisimulation! 
  10.253 -      [also admits true equality]
  10.254 -   Replace "A" by some particular set, like {x.True}??? *)
  10.255 -goal LList.thy 
  10.256 -    "!!r. [| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
  10.257 -\         |] ==>  M=N";
  10.258 -by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
  10.259 -by (etac LListD_coinduct 1);
  10.260 -by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
  10.261 -by (safe_tac (!claset));
  10.262 -qed "LList_equalityI";
  10.263 -
  10.264 -
  10.265 -(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
  10.266 -
  10.267 -(*abstract proof using a bisimulation*)
  10.268 -val [prem1,prem2] = goal LList.thy
  10.269 - "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
  10.270 -\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
  10.271 -\ ==> h1=h2";
  10.272 -by (rtac ext 1);
  10.273 -(*next step avoids an unknown (and flexflex pair) in simplification*)
  10.274 -by (res_inst_tac [("A", "{u.True}"),
  10.275 -                  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
  10.276 -by (rtac rangeI 1);
  10.277 -by (safe_tac (!claset));
  10.278 -by (stac prem1 1);
  10.279 -by (stac prem2 1);
  10.280 -by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
  10.281 -                                 CollectI RS LListD_Fun_CONS_I]
  10.282 -                       |> add_eqI) 1);
  10.283 -qed "LList_corec_unique";
  10.284 -
  10.285 -val [prem] = goal LList.thy
  10.286 - "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
  10.287 -\ ==> h = (%x.LList_corec x f)";
  10.288 -by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
  10.289 -qed "equals_LList_corec";
  10.290 -
  10.291 -
  10.292 -(** Obsolete LList_corec_unique proof: complete induction, not coinduction **)
  10.293 -
  10.294 -goalw LList.thy [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
  10.295 -by (rtac ntrunc_one_In1 1);
  10.296 -qed "ntrunc_one_CONS";
  10.297 -
  10.298 -goalw LList.thy [CONS_def]
  10.299 -    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
  10.300 -by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1);
  10.301 -qed "ntrunc_CONS";
  10.302 -
  10.303 -val [prem1,prem2] = goal LList.thy
  10.304 - "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
  10.305 -\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
  10.306 -\ ==> h1=h2";
  10.307 -by (rtac (ntrunc_equality RS ext) 1);
  10.308 -by (rename_tac "x k" 1);
  10.309 -by (res_inst_tac [("x", "x")] spec 1);
  10.310 -by (res_inst_tac [("n", "k")] less_induct 1);
  10.311 -by (rename_tac "n" 1);
  10.312 -by (rtac allI 1);
  10.313 -by (rename_tac "y" 1);
  10.314 -by (stac prem1 1);
  10.315 -by (stac prem2 1);
  10.316 -by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
  10.317 -by (strip_tac 1);
  10.318 -by (res_inst_tac [("n", "n")] natE 1);
  10.319 -by (rename_tac "m" 2);
  10.320 -by (res_inst_tac [("n", "m")] natE 2);
  10.321 -by (ALLGOALS(asm_simp_tac(!simpset addsimps
  10.322 -            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
  10.323 -result();
  10.324 -
  10.325 -
  10.326 -(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
  10.327 -
  10.328 -goal LList.thy "mono(CONS(M))";
  10.329 -by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1));
  10.330 -qed "Lconst_fun_mono";
  10.331 -
  10.332 -(* Lconst(M) = CONS M (Lconst M) *)
  10.333 -bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski)));
  10.334 -
  10.335 -(*A typical use of co-induction to show membership in the gfp.
  10.336 -  The containing set is simply the singleton {Lconst(M)}. *)
  10.337 -goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
  10.338 -by (rtac (singletonI RS llist_coinduct) 1);
  10.339 -by (safe_tac (!claset));
  10.340 -by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
  10.341 -by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
  10.342 -qed "Lconst_type";
  10.343 -
  10.344 -goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
  10.345 -by (rtac (equals_LList_corec RS fun_cong) 1);
  10.346 -by (Simp_tac 1);
  10.347 -by (rtac Lconst 1);
  10.348 -qed "Lconst_eq_LList_corec";
  10.349 -
  10.350 -(*Thus we could have used gfp in the definition of Lconst*)
  10.351 -goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
  10.352 -by (rtac (equals_LList_corec RS fun_cong) 1);
  10.353 -by (Simp_tac 1);
  10.354 -by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
  10.355 -qed "gfp_Lconst_eq_LList_corec";
  10.356 -
  10.357 -
  10.358 -(*** Isomorphisms ***)
  10.359 -
  10.360 -goal LList.thy "inj(Rep_llist)";
  10.361 -by (rtac inj_inverseI 1);
  10.362 -by (rtac Rep_llist_inverse 1);
  10.363 -qed "inj_Rep_llist";
  10.364 -
  10.365 -goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
  10.366 -by (rtac inj_onto_inverseI 1);
  10.367 -by (etac Abs_llist_inverse 1);
  10.368 -qed "inj_onto_Abs_llist";
  10.369 -
  10.370 -(** Distinctness of constructors **)
  10.371 -
  10.372 -goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
  10.373 -by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
  10.374 -by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
  10.375 -qed "LCons_not_LNil";
  10.376 -
  10.377 -bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
  10.378 -
  10.379 -AddIffs [LCons_not_LNil, LNil_not_LCons];
  10.380 -
  10.381 -
  10.382 -(** llist constructors **)
  10.383 -
  10.384 -goalw LList.thy [LNil_def]
  10.385 -    "Rep_llist(LNil) = NIL";
  10.386 -by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
  10.387 -qed "Rep_llist_LNil";
  10.388 -
  10.389 -goalw LList.thy [LCons_def]
  10.390 -    "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
  10.391 -by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
  10.392 -                         rangeI, Rep_llist] 1));
  10.393 -qed "Rep_llist_LCons";
  10.394 -
  10.395 -(** Injectiveness of CONS and LCons **)
  10.396 -
  10.397 -goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
  10.398 -by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
  10.399 -qed "CONS_CONS_eq2";
  10.400 -
  10.401 -bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
  10.402 -
  10.403 -
  10.404 -(*For reasoning about abstract llist constructors*)
  10.405 -
  10.406 -AddIs ([Rep_llist]@llist.intrs);
  10.407 -AddSDs [inj_onto_Abs_llist RS inj_ontoD,
  10.408 -        inj_Rep_llist RS injD, Leaf_inject];
  10.409 -
  10.410 -goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
  10.411 -by (Fast_tac 1);
  10.412 -qed "LCons_LCons_eq";
  10.413 -
  10.414 -AddIffs [LCons_LCons_eq];
  10.415 -
  10.416 -val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
  10.417 -by (rtac (major RS llist.elim) 1);
  10.418 -by (etac CONS_neq_NIL 1);
  10.419 -by (Fast_tac 1);
  10.420 -qed "CONS_D2";
  10.421 -
  10.422 -
  10.423 -(****** Reasoning about llist(A) ******)
  10.424 -
  10.425 -Addsimps [List_case_NIL, List_case_CONS];
  10.426 -
  10.427 -(*A special case of list_equality for functions over lazy lists*)
  10.428 -val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
  10.429 - "[| M: llist(A); g(NIL): llist(A);                             \
  10.430 -\    f(NIL)=g(NIL);                                             \
  10.431 -\    !!x l. [| x:A;  l: llist(A) |] ==>                         \
  10.432 -\           (f(CONS x l),g(CONS x l)) :                         \
  10.433 -\               LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un  \
  10.434 -\                                   diag(llist(A)))             \
  10.435 -\ |] ==> f(M) = g(M)";
  10.436 -by (rtac LList_equalityI 1);
  10.437 -by (rtac (Mlist RS imageI) 1);
  10.438 -by (rtac subsetI 1);
  10.439 -by (etac imageE 1);
  10.440 -by (etac ssubst 1);
  10.441 -by (etac llist.elim 1);
  10.442 -by (etac ssubst 1);
  10.443 -by (stac NILcase 1);
  10.444 -by (rtac (gMlist RS LListD_Fun_diag_I) 1);
  10.445 -by (etac ssubst 1);
  10.446 -by (REPEAT (ares_tac [CONScase] 1));
  10.447 -qed "LList_fun_equalityI";
  10.448 -
  10.449 -
  10.450 -(*** The functional "Lmap" ***)
  10.451 -
  10.452 -goal LList.thy "Lmap f NIL = NIL";
  10.453 -by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
  10.454 -by (Simp_tac 1);
  10.455 -qed "Lmap_NIL";
  10.456 -
  10.457 -goal LList.thy "Lmap f (CONS M N) = CONS (f M) (Lmap f N)";
  10.458 -by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
  10.459 -by (Simp_tac 1);
  10.460 -qed "Lmap_CONS";
  10.461 -
  10.462 -(*Another type-checking proof by coinduction*)
  10.463 -val [major,minor] = goal LList.thy
  10.464 -    "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
  10.465 -by (rtac (major RS imageI RS llist_coinduct) 1);
  10.466 -by (safe_tac (!claset));
  10.467 -by (etac llist.elim 1);
  10.468 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  10.469 -by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
  10.470 -                      minor, imageI, UnI1] 1));
  10.471 -qed "Lmap_type";
  10.472 -
  10.473 -(*This type checking rule synthesises a sufficiently large set for f*)
  10.474 -val [major] = goal LList.thy  "M: llist(A) ==> Lmap f M: llist(f``A)";
  10.475 -by (rtac (major RS Lmap_type) 1);
  10.476 -by (etac imageI 1);
  10.477 -qed "Lmap_type2";
  10.478 -
  10.479 -(** Two easy results about Lmap **)
  10.480 -
  10.481 -val [prem] = goalw LList.thy [o_def]
  10.482 -    "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
  10.483 -by (rtac (prem RS imageI RS LList_equalityI) 1);
  10.484 -by (safe_tac (!claset));
  10.485 -by (etac llist.elim 1);
  10.486 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  10.487 -by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
  10.488 -                      rangeI RS LListD_Fun_CONS_I] 1));
  10.489 -qed "Lmap_compose";
  10.490 -
  10.491 -val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
  10.492 -by (rtac (prem RS imageI RS LList_equalityI) 1);
  10.493 -by (safe_tac (!claset));
  10.494 -by (etac llist.elim 1);
  10.495 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  10.496 -by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
  10.497 -                      rangeI RS LListD_Fun_CONS_I] 1));
  10.498 -qed "Lmap_ident";
  10.499 -
  10.500 -
  10.501 -(*** Lappend -- its two arguments cause some complications! ***)
  10.502 -
  10.503 -goalw LList.thy [Lappend_def] "Lappend NIL NIL = NIL";
  10.504 -by (rtac (LList_corec RS trans) 1);
  10.505 -by (Simp_tac 1);
  10.506 -qed "Lappend_NIL_NIL";
  10.507 -
  10.508 -goalw LList.thy [Lappend_def]
  10.509 -    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')";
  10.510 -by (rtac (LList_corec RS trans) 1);
  10.511 -by (Simp_tac 1);
  10.512 -qed "Lappend_NIL_CONS";
  10.513 -
  10.514 -goalw LList.thy [Lappend_def]
  10.515 -    "Lappend (CONS M M') N = CONS M (Lappend M' N)";
  10.516 -by (rtac (LList_corec RS trans) 1);
  10.517 -by (Simp_tac 1);
  10.518 -qed "Lappend_CONS";
  10.519 -
  10.520 -Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
  10.521 -          Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
  10.522 -Delsimps [Pair_eq];
  10.523 -
  10.524 -goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
  10.525 -by (etac LList_fun_equalityI 1);
  10.526 -by (ALLGOALS Asm_simp_tac);
  10.527 -qed "Lappend_NIL";
  10.528 -
  10.529 -goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M";
  10.530 -by (etac LList_fun_equalityI 1);
  10.531 -by (ALLGOALS Asm_simp_tac);
  10.532 -qed "Lappend_NIL2";
  10.533 -
  10.534 -(** Alternative type-checking proofs for Lappend **)
  10.535 -
  10.536 -(*weak co-induction: bisimulation and case analysis on both variables*)
  10.537 -goal LList.thy
  10.538 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
  10.539 -by (res_inst_tac
  10.540 -    [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
  10.541 -by (Fast_tac 1);
  10.542 -by (safe_tac (!claset));
  10.543 -by (eres_inst_tac [("a", "u")] llist.elim 1);
  10.544 -by (eres_inst_tac [("a", "v")] llist.elim 1);
  10.545 -by (ALLGOALS
  10.546 -    (Asm_simp_tac THEN'
  10.547 -     fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
  10.548 -qed "Lappend_type";
  10.549 -
  10.550 -(*strong co-induction: bisimulation and case analysis on one variable*)
  10.551 -goal LList.thy
  10.552 -    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
  10.553 -by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1);
  10.554 -by (etac imageI 1);
  10.555 -by (rtac subsetI 1);
  10.556 -by (etac imageE 1);
  10.557 -by (eres_inst_tac [("a", "u")] llist.elim 1);
  10.558 -by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
  10.559 -by (Asm_simp_tac 1);
  10.560 -by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
  10.561 -qed "Lappend_type";
  10.562 -
  10.563 -(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
  10.564 -
  10.565 -(** llist_case: case analysis for 'a llist **)
  10.566 -
  10.567 -Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
  10.568 -           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
  10.569 -
  10.570 -goalw LList.thy [llist_case_def,LNil_def]  "llist_case c d LNil = c";
  10.571 -by (Simp_tac 1);
  10.572 -qed "llist_case_LNil";
  10.573 -
  10.574 -goalw LList.thy [llist_case_def,LCons_def]
  10.575 -    "llist_case c d (LCons M N) = d M N";
  10.576 -by (Simp_tac 1);
  10.577 -qed "llist_case_LCons";
  10.578 -
  10.579 -(*Elimination is case analysis, not induction.*)
  10.580 -val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
  10.581 -    "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P \
  10.582 -\    |] ==> P";
  10.583 -by (rtac (Rep_llist RS llist.elim) 1);
  10.584 -by (rtac (inj_Rep_llist RS injD RS prem1) 1);
  10.585 -by (stac Rep_llist_LNil 1);
  10.586 -by (assume_tac 1);
  10.587 -by (etac rangeE 1);
  10.588 -by (rtac (inj_Rep_llist RS injD RS prem2) 1);
  10.589 -by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
  10.590 -by (etac (Abs_llist_inverse RS ssubst) 1);
  10.591 -by (rtac refl 1);
  10.592 -qed "llistE";
  10.593 -
  10.594 -(** llist_corec: corecursion for 'a llist **)
  10.595 -
  10.596 -goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
  10.597 -    "llist_corec a f = sum_case (%u. LNil) \
  10.598 -\                           (split(%z w. LCons z (llist_corec w f))) (f a)";
  10.599 -by (stac LList_corec 1);
  10.600 -by (res_inst_tac [("s","f(a)")] sumE 1);
  10.601 -by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
  10.602 -by (res_inst_tac [("p","y")] PairE 1);
  10.603 -by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
  10.604 -(*FIXME: correct case splits usd to be found automatically:
  10.605 -by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*)
  10.606 -qed "llist_corec";
  10.607 -
  10.608 -(*definitional version of same*)
  10.609 -val [rew] = goal LList.thy
  10.610 -    "[| !!x. h(x) == llist_corec x f |] ==>     \
  10.611 -\    h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
  10.612 -by (rewtac rew);
  10.613 -by (rtac llist_corec 1);
  10.614 -qed "def_llist_corec";
  10.615 -
  10.616 -(**** Proofs about type 'a llist functions ****)
  10.617 -
  10.618 -(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
  10.619 -
  10.620 -goalw LList.thy [LListD_Fun_def]
  10.621 -    "!!r A. r <= (llist A) Times (llist A) ==> \
  10.622 -\           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
  10.623 -by (stac llist_unfold 1);
  10.624 -by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
  10.625 -by (Fast_tac 1);
  10.626 -qed "LListD_Fun_subset_Sigma_llist";
  10.627 -
  10.628 -goal LList.thy
  10.629 -    "prod_fun Rep_llist Rep_llist `` r <= \
  10.630 -\    (llist(range Leaf)) Times (llist(range Leaf))";
  10.631 -by (fast_tac (!claset addIs [Rep_llist]) 1);
  10.632 -qed "subset_Sigma_llist";
  10.633 -
  10.634 -val [prem] = goal LList.thy
  10.635 -    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
  10.636 -\    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
  10.637 -by (safe_tac (!claset));
  10.638 -by (rtac (prem RS subsetD RS SigmaE2) 1);
  10.639 -by (assume_tac 1);
  10.640 -by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
  10.641 -qed "prod_fun_lemma";
  10.642 -
  10.643 -goal LList.thy
  10.644 -    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
  10.645 -\    diag(llist(range Leaf))";
  10.646 -by (rtac equalityI 1);
  10.647 -by (fast_tac (!claset addIs [Rep_llist]) 1);
  10.648 -by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
  10.649 -qed "prod_fun_range_eq_diag";
  10.650 -
  10.651 -(*Surprisingly hard to prove.  Used with lfilter*)
  10.652 -goalw thy [llistD_Fun_def, prod_fun_def]
  10.653 -    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
  10.654 -by (Auto_tac());
  10.655 -by (rtac image_eqI 1);
  10.656 -by (fast_tac (!claset addss (!simpset)) 1);
  10.657 -by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
  10.658 -qed "llistD_Fun_mono";
  10.659 -
  10.660 -(** To show two llists are equal, exhibit a bisimulation! 
  10.661 -      [also admits true equality] **)
  10.662 -val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
  10.663 -    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
  10.664 -by (rtac (inj_Rep_llist RS injD) 1);
  10.665 -by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
  10.666 -                  ("A", "range(Leaf)")] 
  10.667 -        LList_equalityI 1);
  10.668 -by (rtac (prem1 RS prod_fun_imageI) 1);
  10.669 -by (rtac (prem2 RS image_mono RS subset_trans) 1);
  10.670 -by (rtac (image_compose RS subst) 1);
  10.671 -by (rtac (prod_fun_compose RS subst) 1);
  10.672 -by (stac image_Un 1);
  10.673 -by (stac prod_fun_range_eq_diag 1);
  10.674 -by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
  10.675 -by (rtac (subset_Sigma_llist RS Un_least) 1);
  10.676 -by (rtac diag_subset_Sigma 1);
  10.677 -qed "llist_equalityI";
  10.678 -
  10.679 -(** Rules to prove the 2nd premise of llist_equalityI **)
  10.680 -goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
  10.681 -by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
  10.682 -qed "llistD_Fun_LNil_I";
  10.683 -
  10.684 -val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
  10.685 -    "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
  10.686 -by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
  10.687 -by (rtac (prem RS prod_fun_imageI) 1);
  10.688 -qed "llistD_Fun_LCons_I";
  10.689 -
  10.690 -(*Utilise the "strong" part, i.e. gfp(f)*)
  10.691 -goalw LList.thy [llistD_Fun_def]
  10.692 -     "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
  10.693 -by (rtac (Rep_llist_inverse RS subst) 1);
  10.694 -by (rtac prod_fun_imageI 1);
  10.695 -by (stac image_Un 1);
  10.696 -by (stac prod_fun_range_eq_diag 1);
  10.697 -by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
  10.698 -qed "llistD_Fun_range_I";
  10.699 -
  10.700 -(*A special case of list_equality for functions over lazy lists*)
  10.701 -val [prem1,prem2] = goal LList.thy
  10.702 -    "[| f(LNil)=g(LNil);                                                \
  10.703 -\       !!x l. (f(LCons x l),g(LCons x l)) :                            \
  10.704 -\              llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
  10.705 -\    |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
  10.706 -by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
  10.707 -by (rtac rangeI 1);
  10.708 -by (rtac subsetI 1);
  10.709 -by (etac rangeE 1);
  10.710 -by (etac ssubst 1);
  10.711 -by (res_inst_tac [("l", "u")] llistE 1);
  10.712 -by (etac ssubst 1);
  10.713 -by (stac prem1 1);
  10.714 -by (rtac llistD_Fun_range_I 1);
  10.715 -by (etac ssubst 1);
  10.716 -by (rtac prem2 1);
  10.717 -qed "llist_fun_equalityI";
  10.718 -
  10.719 -(*simpset for llist bisimulations*)
  10.720 -Addsimps [llist_case_LNil, llist_case_LCons, 
  10.721 -          llistD_Fun_LNil_I, llistD_Fun_LCons_I];
  10.722 -
  10.723 -
  10.724 -(*** The functional "lmap" ***)
  10.725 -
  10.726 -goal LList.thy "lmap f LNil = LNil";
  10.727 -by (rtac (lmap_def RS def_llist_corec RS trans) 1);
  10.728 -by (Simp_tac 1);
  10.729 -qed "lmap_LNil";
  10.730 -
  10.731 -goal LList.thy "lmap f (LCons M N) = LCons (f M) (lmap f N)";
  10.732 -by (rtac (lmap_def RS def_llist_corec RS trans) 1);
  10.733 -by (Simp_tac 1);
  10.734 -qed "lmap_LCons";
  10.735 -
  10.736 -Addsimps [lmap_LNil, lmap_LCons];
  10.737 -
  10.738 -
  10.739 -(** Two easy results about lmap **)
  10.740 -
  10.741 -goal LList.thy "lmap (f o g) l = lmap f (lmap g l)";
  10.742 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  10.743 -by (ALLGOALS Simp_tac);
  10.744 -qed "lmap_compose";
  10.745 -
  10.746 -goal LList.thy "lmap (%x.x) l = l";
  10.747 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  10.748 -by (ALLGOALS Simp_tac);
  10.749 -qed "lmap_ident";
  10.750 -
  10.751 -
  10.752 -(*** iterates -- llist_fun_equalityI cannot be used! ***)
  10.753 -
  10.754 -goal LList.thy "iterates f x = LCons x (iterates f (f x))";
  10.755 -by (rtac (iterates_def RS def_llist_corec RS trans) 1);
  10.756 -by (Simp_tac 1);
  10.757 -qed "iterates";
  10.758 -
  10.759 -goal LList.thy "lmap f (iterates f x) = iterates f (f x)";
  10.760 -by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
  10.761 -    llist_equalityI 1);
  10.762 -by (rtac rangeI 1);
  10.763 -by (safe_tac (!claset));
  10.764 -by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
  10.765 -by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
  10.766 -by (Simp_tac 1);
  10.767 -qed "lmap_iterates";
  10.768 -
  10.769 -goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))";
  10.770 -by (stac lmap_iterates 1);
  10.771 -by (rtac iterates 1);
  10.772 -qed "iterates_lmap";
  10.773 -
  10.774 -(*** A rather complex proof about iterates -- cf Andy Pitts ***)
  10.775 -
  10.776 -(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
  10.777 -
  10.778 -goal LList.thy
  10.779 -    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
  10.780 -\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
  10.781 -by (nat_ind_tac "n" 1);
  10.782 -by (ALLGOALS Asm_simp_tac);
  10.783 -qed "fun_power_lmap";
  10.784 -
  10.785 -goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
  10.786 -by (nat_ind_tac "n" 1);
  10.787 -by (ALLGOALS Asm_simp_tac);
  10.788 -qed "fun_power_Suc";
  10.789 -
  10.790 -val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
  10.791 - [("f","Pair")] (standard(refl RS cong RS cong));
  10.792 -
  10.793 -(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
  10.794 -  for all u and all n::nat.*)
  10.795 -val [prem] = goal LList.thy
  10.796 -    "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
  10.797 -by (rtac ext 1);
  10.798 -by (res_inst_tac [("r", 
  10.799 -   "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
  10.800 -\                    nat_rec (iterates f u) (%m y.lmap f y) n))")] 
  10.801 -    llist_equalityI 1);
  10.802 -by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
  10.803 -by (safe_tac (!claset));
  10.804 -by (stac iterates 1);
  10.805 -by (stac prem 1);
  10.806 -by (stac fun_power_lmap 1);
  10.807 -by (stac fun_power_lmap 1);
  10.808 -by (rtac llistD_Fun_LCons_I 1);
  10.809 -by (rtac (lmap_iterates RS subst) 1);
  10.810 -by (stac fun_power_Suc 1);
  10.811 -by (stac fun_power_Suc 1);
  10.812 -by (rtac (UN1_I RS UnI1) 1);
  10.813 -by (rtac rangeI 1);
  10.814 -qed "iterates_equality";
  10.815 -
  10.816 -
  10.817 -(*** lappend -- its two arguments cause some complications! ***)
  10.818 -
  10.819 -goalw LList.thy [lappend_def] "lappend LNil LNil = LNil";
  10.820 -by (rtac (llist_corec RS trans) 1);
  10.821 -by (Simp_tac 1);
  10.822 -qed "lappend_LNil_LNil";
  10.823 -
  10.824 -goalw LList.thy [lappend_def]
  10.825 -    "lappend LNil (LCons l l') = LCons l (lappend LNil l')";
  10.826 -by (rtac (llist_corec RS trans) 1);
  10.827 -by (Simp_tac 1);
  10.828 -qed "lappend_LNil_LCons";
  10.829 -
  10.830 -goalw LList.thy [lappend_def]
  10.831 -    "lappend (LCons l l') N = LCons l (lappend l' N)";
  10.832 -by (rtac (llist_corec RS trans) 1);
  10.833 -by (Simp_tac 1);
  10.834 -qed "lappend_LCons";
  10.835 -
  10.836 -Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
  10.837 -
  10.838 -goal LList.thy "lappend LNil l = l";
  10.839 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  10.840 -by (ALLGOALS Simp_tac);
  10.841 -qed "lappend_LNil";
  10.842 -
  10.843 -goal LList.thy "lappend l LNil = l";
  10.844 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  10.845 -by (ALLGOALS Simp_tac);
  10.846 -qed "lappend_LNil2";
  10.847 -
  10.848 -Addsimps [lappend_LNil, lappend_LNil2];
  10.849 -
  10.850 -(*The infinite first argument blocks the second*)
  10.851 -goal LList.thy "lappend (iterates f x) N = iterates f x";
  10.852 -by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
  10.853 -    llist_equalityI 1);
  10.854 -by (rtac rangeI 1);
  10.855 -by (safe_tac (!claset));
  10.856 -by (stac iterates 1);
  10.857 -by (Simp_tac 1);
  10.858 -qed "lappend_iterates";
  10.859 -
  10.860 -(** Two proofs that lmap distributes over lappend **)
  10.861 -
  10.862 -(*Long proof requiring case analysis on both both arguments*)
  10.863 -goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
  10.864 -by (res_inst_tac 
  10.865 -    [("r",  
  10.866 -      "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
  10.867 -    llist_equalityI 1);
  10.868 -by (rtac UN1_I 1);
  10.869 -by (rtac rangeI 1);
  10.870 -by (safe_tac (!claset));
  10.871 -by (res_inst_tac [("l", "l")] llistE 1);
  10.872 -by (res_inst_tac [("l", "n")] llistE 1);
  10.873 -by (ALLGOALS Asm_simp_tac);
  10.874 -by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
  10.875 -qed "lmap_lappend_distrib";
  10.876 -
  10.877 -(*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
  10.878 -goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
  10.879 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  10.880 -by (Simp_tac 1);
  10.881 -by (Simp_tac 1);
  10.882 -qed "lmap_lappend_distrib";
  10.883 -
  10.884 -(*Without strong coinduction, three case analyses might be needed*)
  10.885 -goal LList.thy "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
  10.886 -by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
  10.887 -by (Simp_tac 1);
  10.888 -by (Simp_tac 1);
  10.889 -qed "lappend_assoc";
    11.1 --- a/src/HOL/ex/LList.thy	Wed May 07 13:50:52 1997 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,153 +0,0 @@
    11.4 -(*  Title:      HOL/LList.thy
    11.5 -    ID:         $Id$
    11.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 -    Copyright   1994  University of Cambridge
    11.8 -
    11.9 -Definition of type 'a llist by a greatest fixed point
   11.10 -
   11.11 -Shares NIL, CONS, List_case with List.thy
   11.12 -
   11.13 -Still needs filter and flatten functions -- hard because they need
   11.14 -bounds on the amount of lookahead required.
   11.15 -
   11.16 -Could try (but would it work for the gfp analogue of term?)
   11.17 -  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
   11.18 -
   11.19 -A nice but complex example would be [ML for the Working Programmer, page 176]
   11.20 -  from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
   11.21 -
   11.22 -Previous definition of llistD_Fun was explicit:
   11.23 -  llistD_Fun_def
   11.24 -   "llistD_Fun(r) ==    
   11.25 -       {(LNil,LNil)}  Un        
   11.26 -       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   11.27 -*)
   11.28 -
   11.29 -LList = Gfp + SList +
   11.30 -
   11.31 -types
   11.32 -  'a llist
   11.33 -
   11.34 -arities
   11.35 -   llist :: (term)term
   11.36 -
   11.37 -consts
   11.38 -  list_Fun   :: ['a item set, 'a item set] => 'a item set
   11.39 -  LListD_Fun :: 
   11.40 -      "[('a item * 'a item)set, ('a item * 'a item)set] => 
   11.41 -      ('a item * 'a item)set"
   11.42 -
   11.43 -  llist      :: 'a item set => 'a item set
   11.44 -  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   11.45 -  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
   11.46 -
   11.47 -  Rep_llist  :: 'a llist => 'a item
   11.48 -  Abs_llist  :: 'a item => 'a llist
   11.49 -  LNil       :: 'a llist
   11.50 -  LCons      :: ['a, 'a llist] => 'a llist
   11.51 -  
   11.52 -  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
   11.53 -
   11.54 -  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
   11.55 -  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   11.56 -  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
   11.57 -
   11.58 -  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
   11.59 -  lmap       :: ('a=>'b) => ('a llist => 'b llist)
   11.60 -
   11.61 -  iterates   :: ['a => 'a, 'a] => 'a llist
   11.62 -
   11.63 -  Lconst     :: 'a item => 'a item
   11.64 -  Lappend    :: ['a item, 'a item] => 'a item
   11.65 -  lappend    :: ['a llist, 'a llist] => 'a llist
   11.66 -
   11.67 -
   11.68 -coinductive "llist(A)"
   11.69 -  intrs
   11.70 -    NIL_I  "NIL: llist(A)"
   11.71 -    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : llist(A)"
   11.72 -
   11.73 -coinductive "LListD(r)"
   11.74 -  intrs
   11.75 -    NIL_I  "(NIL, NIL) : LListD(r)"
   11.76 -    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
   11.77 -            |] ==> (CONS a M, CONS b N) : LListD(r)"
   11.78 -
   11.79 -translations
   11.80 -  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
   11.81 -
   11.82 -
   11.83 -defs
   11.84 -  (*Now used exclusively for abbreviating the coinduction rule*)
   11.85 -  list_Fun_def   "list_Fun A X ==   
   11.86 -                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   11.87 -
   11.88 -  LListD_Fun_def "LListD_Fun r X ==   
   11.89 -                  {z. z = (NIL, NIL) |   
   11.90 -                      (? M N a b. z = (CONS a M, CONS b N) &   
   11.91 -                                  (a, b) : r & (M, N) : X)}"
   11.92 -
   11.93 -  (*defining the abstract constructors*)
   11.94 -  LNil_def      "LNil == Abs_llist(NIL)"
   11.95 -  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   11.96 -
   11.97 -  llist_case_def
   11.98 -   "llist_case c d l == 
   11.99 -       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
  11.100 -
  11.101 -  LList_corec_fun_def
  11.102 -    "LList_corec_fun k f == 
  11.103 -     nat_rec (%x. {})                         
  11.104 -             (%j r x. case f x of Inl u    => NIL
  11.105 -                                | Inr(z,w) => CONS z (r w)) 
  11.106 -             k"
  11.107 -
  11.108 -  LList_corec_def
  11.109 -    "LList_corec a f == UN k. LList_corec_fun k f a"
  11.110 -
  11.111 -  llist_corec_def
  11.112 -   "llist_corec a f == 
  11.113 -       Abs_llist(LList_corec a 
  11.114 -                 (%z.case f z of Inl x    => Inl(x)
  11.115 -                               | Inr(v,w) => Inr(Leaf(v), w)))"
  11.116 -
  11.117 -  llistD_Fun_def
  11.118 -   "llistD_Fun(r) ==    
  11.119 -        prod_fun Abs_llist Abs_llist ``         
  11.120 -                LListD_Fun (diag(range Leaf))   
  11.121 -                            (prod_fun Rep_llist Rep_llist `` r)"
  11.122 -
  11.123 -  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
  11.124 -
  11.125 -  Lmap_def
  11.126 -   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
  11.127 -
  11.128 -  lmap_def
  11.129 -   "lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
  11.130 -                                           | LCons y z => Inr(f(y), z))"
  11.131 -
  11.132 -  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
  11.133 -
  11.134 -(*Append generates its result by applying f, where
  11.135 -    f((NIL,NIL))          = Inl(())
  11.136 -    f((NIL, CONS N1 N2))  = Inr((N1, (NIL,N2))
  11.137 -    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
  11.138 -*)
  11.139 -
  11.140 -  Lappend_def
  11.141 -   "Lappend M N == LList_corec (M,N)                                         
  11.142 -     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
  11.143 -                      (%M1 M2 N. Inr((M1, (M2,N))))))"
  11.144 -
  11.145 -  lappend_def
  11.146 -   "lappend l n == llist_corec (l,n)                                         
  11.147 -   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
  11.148 -                     (%l1 l2 n. Inr((l1, (l2,n))))))"
  11.149 -
  11.150 -rules
  11.151 -    (*faking a type definition...*)
  11.152 -  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
  11.153 -  Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
  11.154 -  Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
  11.155 -
  11.156 -end
    12.1 --- a/src/HOL/ex/Mutil.ML	Wed May 07 13:50:52 1997 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,172 +0,0 @@
    12.4 -(*  Title:      HOL/ex/Mutil
    12.5 -    ID:         $Id$
    12.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 -    Copyright   1996  University of Cambridge
    12.8 -
    12.9 -The Mutilated Chess Board Problem, formalized inductively
   12.10 -*)
   12.11 -
   12.12 -open Mutil;
   12.13 -
   12.14 -Addsimps tiling.intrs;
   12.15 -
   12.16 -(** The union of two disjoint tilings is a tiling **)
   12.17 -
   12.18 -goal thy "!!t. t: tiling A ==> \
   12.19 -\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
   12.20 -by (etac tiling.induct 1);
   12.21 -by (Simp_tac 1);
   12.22 -by (simp_tac (!simpset addsimps [Un_assoc]) 1);
   12.23 -by (blast_tac (!claset addIs tiling.intrs) 1);
   12.24 -qed_spec_mp "tiling_UnI";
   12.25 -
   12.26 -
   12.27 -(*** Chess boards ***)
   12.28 -
   12.29 -val [below_0, below_Suc] = nat_recs below_def;
   12.30 -Addsimps [below_0, below_Suc];
   12.31 -
   12.32 -goal thy "ALL i. (i: below k) = (i<k)";
   12.33 -by (nat_ind_tac "k" 1);
   12.34 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
   12.35 -by (Blast_tac 1);
   12.36 -qed_spec_mp "below_less_iff";
   12.37 -
   12.38 -Addsimps [below_less_iff];
   12.39 -
   12.40 -goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
   12.41 -by (Simp_tac 1);
   12.42 -by (Blast_tac 1);
   12.43 -qed "Sigma_Suc1";
   12.44 -
   12.45 -goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
   12.46 -by (Simp_tac 1);
   12.47 -by (Blast_tac 1);
   12.48 -qed "Sigma_Suc2";
   12.49 -
   12.50 -(*Deletion is essential to allow use of Sigma_Suc1,2*)
   12.51 -Delsimps [below_Suc];
   12.52 -
   12.53 -goal thy "{i} Times below(n + n) : tiling domino";
   12.54 -by (nat_ind_tac "n" 1);
   12.55 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
   12.56 -by (resolve_tac tiling.intrs 1);
   12.57 -by (assume_tac 2);
   12.58 -by (subgoal_tac    (*seems the easiest way of turning one to the other*)
   12.59 -    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
   12.60 -\    {(i, n+n), (i, Suc(n+n))}" 1);
   12.61 -by (Blast_tac 2);
   12.62 -by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
   12.63 -by (blast_tac (!claset addEs  [less_irrefl, less_asym]
   12.64 -                       addSDs [below_less_iff RS iffD1]) 1);
   12.65 -qed "dominoes_tile_row";
   12.66 -
   12.67 -goal thy "(below m) Times below(n + n) : tiling domino";
   12.68 -by (nat_ind_tac "m" 1);
   12.69 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
   12.70 -by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
   12.71 -                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
   12.72 -qed "dominoes_tile_matrix";
   12.73 -
   12.74 -
   12.75 -(*** Basic properties of evnodd ***)
   12.76 -
   12.77 -goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
   12.78 -by (Simp_tac 1);
   12.79 -qed "evnodd_iff";
   12.80 -
   12.81 -goalw thy [evnodd_def] "evnodd A b <= A";
   12.82 -by (rtac Int_lower1 1);
   12.83 -qed "evnodd_subset";
   12.84 -
   12.85 -(* finite X ==> finite(evnodd X b) *)
   12.86 -bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
   12.87 -
   12.88 -goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
   12.89 -by (Blast_tac 1);
   12.90 -qed "evnodd_Un";
   12.91 -
   12.92 -goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
   12.93 -by (Blast_tac 1);
   12.94 -qed "evnodd_Diff";
   12.95 -
   12.96 -goalw thy [evnodd_def] "evnodd {} b = {}";
   12.97 -by (Simp_tac 1);
   12.98 -qed "evnodd_empty";
   12.99 -
  12.100 -goalw thy [evnodd_def]
  12.101 -    "evnodd (insert (i,j) C) b = \
  12.102 -\    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
  12.103 -by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
  12.104 -             setloop (split_tac [expand_if] THEN' Step_tac)) 1);
  12.105 -qed "evnodd_insert";
  12.106 -
  12.107 -
  12.108 -(*** Dominoes ***)
  12.109 -
  12.110 -goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
  12.111 -by (eresolve_tac [domino.elim] 1);
  12.112 -by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
  12.113 -by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
  12.114 -by (REPEAT_FIRST assume_tac);
  12.115 -(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
  12.116 -by (REPEAT (asm_full_simp_tac (!simpset addsimps
  12.117 -                          [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
  12.118 -                          setloop split_tac [expand_if]) 1
  12.119 -           THEN Blast_tac 1));
  12.120 -qed "domino_singleton";
  12.121 -
  12.122 -goal thy "!!d. d:domino ==> finite d";
  12.123 -by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
  12.124 -                      addSEs [domino.elim]) 1);
  12.125 -qed "domino_finite";
  12.126 -
  12.127 -
  12.128 -(*** Tilings of dominoes ***)
  12.129 -
  12.130 -goal thy "!!t. t:tiling domino ==> finite t";
  12.131 -by (eresolve_tac [tiling.induct] 1);
  12.132 -by (rtac finite_emptyI 1);
  12.133 -by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
  12.134 -qed "tiling_domino_finite";
  12.135 -
  12.136 -goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
  12.137 -by (eresolve_tac [tiling.induct] 1);
  12.138 -by (simp_tac (!simpset addsimps [evnodd_def]) 1);
  12.139 -by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
  12.140 -by (Simp_tac 2 THEN assume_tac 1);
  12.141 -by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
  12.142 -by (Simp_tac 2 THEN assume_tac 1);
  12.143 -by (Step_tac 1);
  12.144 -by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
  12.145 -by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
  12.146 -                                     tiling_domino_finite,
  12.147 -                                     evnodd_subset RS finite_subset,
  12.148 -                                     card_insert_disjoint]) 1);
  12.149 -by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
  12.150 -qed "tiling_domino_0_1";
  12.151 -
  12.152 -goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
  12.153 -\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
  12.154 -\                |] ==> t' ~: tiling domino";
  12.155 -by (rtac notI 1);
  12.156 -by (dtac tiling_domino_0_1 1);
  12.157 -by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
  12.158 -by (Asm_full_simp_tac 1);
  12.159 -by (subgoal_tac "t : tiling domino" 1);
  12.160 -(*Requires a small simpset that won't move the Suc applications*)
  12.161 -by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
  12.162 -by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
  12.163 -by (asm_simp_tac (!simpset addsimps add_ac) 2);
  12.164 -by (asm_full_simp_tac 
  12.165 -    (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty, 
  12.166 -                        mod_less, tiling_domino_0_1 RS sym]) 1);
  12.167 -by (rtac less_trans 1);
  12.168 -by (REPEAT
  12.169 -    (rtac card_Diff 1 
  12.170 -     THEN
  12.171 -     asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
  12.172 -     THEN
  12.173 -     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
  12.174 -qed "mutil_not_tiling";
  12.175 -
    13.1 --- a/src/HOL/ex/Mutil.thy	Wed May 07 13:50:52 1997 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,32 +0,0 @@
    13.4 -(*  Title:      HOL/ex/Mutil
    13.5 -    ID:         $Id$
    13.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 -    Copyright   1996  University of Cambridge
    13.8 -
    13.9 -The Mutilated Chess Board Problem, formalized inductively
   13.10 -  Originator is Max Black, according to J A Robinson.
   13.11 -  Popularized as the Mutilated Checkerboard Problem by J McCarthy
   13.12 -*)
   13.13 -
   13.14 -Mutil = Finite +
   13.15 -consts
   13.16 -  domino  :: "(nat*nat)set set"
   13.17 -  tiling  :: 'a set set => 'a set set
   13.18 -  below   :: nat => nat set
   13.19 -  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
   13.20 -
   13.21 -inductive domino
   13.22 -  intrs
   13.23 -    horiz  "{(i, j), (i, Suc j)} : domino"
   13.24 -    vertl  "{(i, j), (Suc i, j)} : domino"
   13.25 -
   13.26 -inductive "tiling A"
   13.27 -  intrs
   13.28 -    empty  "{} : tiling A"
   13.29 -    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
   13.30 -
   13.31 -defs
   13.32 -  below_def  "below n    == nat_rec {} insert n"
   13.33 -  evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
   13.34 -
   13.35 -end
    14.1 --- a/src/HOL/ex/Perm.ML	Wed May 07 13:50:52 1997 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,98 +0,0 @@
    14.4 -(*  Title:      HOL/ex/Perm.ML
    14.5 -    ID:         $Id$
    14.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 -    Copyright   1995  University of Cambridge
    14.8 -
    14.9 -Permutations: example of an inductive definition
   14.10 -*)
   14.11 -
   14.12 -(*It would be nice to prove
   14.13 -    xs <~~> ys = (!x. count xs x = count ys x)
   14.14 -See mset on HOL/ex/Sorting.thy
   14.15 -*)
   14.16 -
   14.17 -open Perm;
   14.18 -
   14.19 -goal Perm.thy "l <~~> l";
   14.20 -by (list.induct_tac "l" 1);
   14.21 -by (REPEAT (ares_tac perm.intrs 1));
   14.22 -qed "perm_refl";
   14.23 -
   14.24 -
   14.25 -(** Some examples of rule induction on permutations **)
   14.26 -
   14.27 -(*The form of the premise lets the induction bind xs and ys.*)
   14.28 -goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
   14.29 -by (etac perm.induct 1);
   14.30 -by (ALLGOALS Asm_simp_tac);
   14.31 -qed "perm_Nil_lemma";
   14.32 -
   14.33 -(*A more general version is actually easier to understand!*)
   14.34 -goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
   14.35 -by (etac perm.induct 1);
   14.36 -by (ALLGOALS Asm_simp_tac);
   14.37 -qed "perm_length";
   14.38 -
   14.39 -goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
   14.40 -by (etac perm.induct 1);
   14.41 -by (REPEAT (ares_tac perm.intrs 1));
   14.42 -qed "perm_sym";
   14.43 -
   14.44 -goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
   14.45 -by (etac perm.induct 1);
   14.46 -by (Fast_tac 4);
   14.47 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   14.48 -val perm_mem_lemma = result();
   14.49 -
   14.50 -bind_thm ("perm_mem", perm_mem_lemma RS mp);
   14.51 -
   14.52 -(** Ways of making new permutations **)
   14.53 -
   14.54 -(*We can insert the head anywhere in the list*)
   14.55 -goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
   14.56 -by (list.induct_tac "xs" 1);
   14.57 -by (simp_tac (!simpset addsimps [perm_refl]) 1);
   14.58 -by (Simp_tac 1);
   14.59 -by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
   14.60 -qed "perm_append_Cons";
   14.61 -
   14.62 -(*single steps
   14.63 -by (rtac perm.trans 1);
   14.64 -by (rtac perm.swap 1);
   14.65 -by (rtac perm.Cons 1);
   14.66 -*)
   14.67 -
   14.68 -goal Perm.thy "xs@ys <~~> ys@xs";
   14.69 -by (list.induct_tac "xs" 1);
   14.70 -by (simp_tac (!simpset addsimps [perm_refl]) 1);
   14.71 -by (Simp_tac 1);
   14.72 -by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
   14.73 -qed "perm_append_swap";
   14.74 -
   14.75 -
   14.76 -goal Perm.thy "a # xs <~~> xs @ [a]";
   14.77 -by (rtac perm.trans 1);
   14.78 -by (rtac perm_append_swap 2);
   14.79 -by (simp_tac (!simpset addsimps [perm_refl]) 1);
   14.80 -qed "perm_append_single";
   14.81 -
   14.82 -goal Perm.thy "rev xs <~~> xs";
   14.83 -by (list.induct_tac "xs" 1);
   14.84 -by (simp_tac (!simpset addsimps [perm_refl]) 1);
   14.85 -by (Simp_tac 1);
   14.86 -by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
   14.87 -by (etac perm.Cons 1);
   14.88 -qed "perm_rev";
   14.89 -
   14.90 -goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
   14.91 -by (list.induct_tac "l" 1);
   14.92 -by (Simp_tac 1);
   14.93 -by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
   14.94 -qed "perm_append1";
   14.95 -
   14.96 -goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
   14.97 -by (rtac (perm_append_swap RS perm.trans) 1);
   14.98 -by (etac (perm_append1 RS perm.trans) 1);
   14.99 -by (rtac perm_append_swap 1);
  14.100 -qed "perm_append2";
  14.101 -
    15.1 --- a/src/HOL/ex/Perm.thy	Wed May 07 13:50:52 1997 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,24 +0,0 @@
    15.4 -(*  Title:      HOL/ex/Perm.thy
    15.5 -    ID:         $Id$
    15.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 -    Copyright   1995  University of Cambridge
    15.8 -
    15.9 -Permutations: example of an inductive definition
   15.10 -*)
   15.11 -
   15.12 -Perm = List +
   15.13 -
   15.14 -consts  perm    :: "('a list * 'a list) set"   
   15.15 -syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
   15.16 -
   15.17 -translations
   15.18 -    "x <~~> y" == "(x,y) : perm"
   15.19 -
   15.20 -inductive perm
   15.21 -  intrs
   15.22 -    Nil   "[] <~~> []"
   15.23 -    swap  "y#x#l <~~> x#y#l"
   15.24 -    Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
   15.25 -    trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
   15.26 -
   15.27 -end
    16.1 --- a/src/HOL/ex/PropLog.ML	Wed May 07 13:50:52 1997 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,229 +0,0 @@
    16.4 -(*  Title:      HOL/ex/pl.ML
    16.5 -    ID:         $Id$
    16.6 -    Author:     Tobias Nipkow & Lawrence C Paulson
    16.7 -    Copyright   1994  TU Muenchen & University of Cambridge
    16.8 -
    16.9 -Soundness and completeness of propositional logic w.r.t. truth-tables.
   16.10 -
   16.11 -Prove: If H|=p then G|=p where G:Fin(H)
   16.12 -*)
   16.13 -
   16.14 -open PropLog;
   16.15 -
   16.16 -(** Monotonicity **)
   16.17 -goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
   16.18 -by (rtac lfp_mono 1);
   16.19 -by (REPEAT (ares_tac basic_monos 1));
   16.20 -qed "thms_mono";
   16.21 -
   16.22 -(*Rule is called I for Identity Combinator, not for Introduction*)
   16.23 -goal PropLog.thy "H |- p->p";
   16.24 -by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
   16.25 -qed "thms_I";
   16.26 -
   16.27 -(** Weakening, left and right **)
   16.28 -
   16.29 -(* "[| G<=H;  G |- p |] ==> H |- p"
   16.30 -   This order of premises is convenient with RS
   16.31 -*)
   16.32 -bind_thm ("weaken_left", (thms_mono RS subsetD));
   16.33 -
   16.34 -(* H |- p ==> insert(a,H) |- p *)
   16.35 -val weaken_left_insert = subset_insertI RS weaken_left;
   16.36 -
   16.37 -val weaken_left_Un1  =    Un_upper1 RS weaken_left;
   16.38 -val weaken_left_Un2  =    Un_upper2 RS weaken_left;
   16.39 -
   16.40 -goal PropLog.thy "!!H. H |- q ==> H |- p->q";
   16.41 -by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
   16.42 -qed "weaken_right";
   16.43 -
   16.44 -(*The deduction theorem*)
   16.45 -goal PropLog.thy "!!H. insert p H |- q  ==>  H |- p->q";
   16.46 -by (etac thms.induct 1);
   16.47 -by (ALLGOALS 
   16.48 -    (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
   16.49 -                             thms.S RS thms.MP RS thms.MP, weaken_right])));
   16.50 -qed "deduction";
   16.51 -
   16.52 -
   16.53 -(* "[| insert p H |- q; H |- p |] ==> H |- q"
   16.54 -    The cut rule - not used
   16.55 -*)
   16.56 -val cut = deduction RS thms.MP;
   16.57 -
   16.58 -(* H |- false ==> H |- p *)
   16.59 -val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
   16.60 -
   16.61 -(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
   16.62 -bind_thm ("thms_notE", (thms.MP RS thms_falseE));
   16.63 -
   16.64 -(** The function eval **)
   16.65 -
   16.66 -goalw PropLog.thy [eval_def] "tt[false] = False";
   16.67 -by (Simp_tac 1);
   16.68 -qed "eval_false";
   16.69 -
   16.70 -goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
   16.71 -by (Simp_tac 1);
   16.72 -qed "eval_var";
   16.73 -
   16.74 -goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
   16.75 -by (Simp_tac 1);
   16.76 -qed "eval_imp";
   16.77 -
   16.78 -Addsimps [eval_false, eval_var, eval_imp];
   16.79 -
   16.80 -(*Soundness of the rules wrt truth-table semantics*)
   16.81 -goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
   16.82 -by (etac thms.induct 1);
   16.83 -by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
   16.84 -by (ALLGOALS Asm_simp_tac);
   16.85 -qed "soundness";
   16.86 -
   16.87 -(*** Towards the completeness proof ***)
   16.88 -
   16.89 -goal PropLog.thy "!!H. H |- p->false ==> H |- p->q";
   16.90 -by (rtac deduction 1);
   16.91 -by (etac (weaken_left_insert RS thms_notE) 1);
   16.92 -by (rtac thms.H 1);
   16.93 -by (rtac insertI1 1);
   16.94 -qed "false_imp";
   16.95 -
   16.96 -val [premp,premq] = goal PropLog.thy
   16.97 -    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
   16.98 -by (rtac deduction 1);
   16.99 -by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
  16.100 -by (rtac (thms.H RS thms.MP) 1);
  16.101 -by (rtac insertI1 1);
  16.102 -by (rtac (premp RS weaken_left_insert) 1);
  16.103 -qed "imp_false";
  16.104 -
  16.105 -(*This formulation is required for strong induction hypotheses*)
  16.106 -goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
  16.107 -by (rtac (expand_if RS iffD2) 1);
  16.108 -by (PropLog.pl.induct_tac "p" 1);
  16.109 -by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
  16.110 -by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, 
  16.111 -                           weaken_right, imp_false]
  16.112 -                    addSEs [false_imp]) 1);
  16.113 -qed "hyps_thms_if";
  16.114 -
  16.115 -(*Key lemma for completeness; yields a set of assumptions satisfying p*)
  16.116 -val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
  16.117 -by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
  16.118 -    rtac hyps_thms_if 2);
  16.119 -by (Fast_tac 1);
  16.120 -qed "sat_thms_p";
  16.121 -
  16.122 -(*For proving certain theorems in our new propositional logic*)
  16.123 -
  16.124 -AddSIs [deduction];
  16.125 -AddIs [thms.H, thms.H RS thms.MP];
  16.126 -
  16.127 -(*The excluded middle in the form of an elimination rule*)
  16.128 -goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
  16.129 -by (rtac (deduction RS deduction) 1);
  16.130 -by (rtac (thms.DN RS thms.MP) 1);
  16.131 -by (ALLGOALS (best_tac (!claset addSIs prems)));
  16.132 -qed "thms_excluded_middle";
  16.133 -
  16.134 -(*Hard to prove directly because it requires cuts*)
  16.135 -val prems = goal PropLog.thy
  16.136 -    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q";
  16.137 -by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
  16.138 -by (REPEAT (resolve_tac (prems@[deduction]) 1));
  16.139 -qed "thms_excluded_middle_rule";
  16.140 -
  16.141 -(*** Completeness -- lemmas for reducing the set of assumptions ***)
  16.142 -
  16.143 -(*For the case hyps(p,t)-insert(#v,Y) |- p;
  16.144 -  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
  16.145 -goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
  16.146 -by (PropLog.pl.induct_tac "p" 1);
  16.147 -by (Simp_tac 1);
  16.148 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  16.149 -by (Simp_tac 1);
  16.150 -by (Fast_tac 1);
  16.151 -qed "hyps_Diff";
  16.152 -
  16.153 -(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
  16.154 -  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
  16.155 -goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
  16.156 -by (PropLog.pl.induct_tac "p" 1);
  16.157 -by (Simp_tac 1);
  16.158 -by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  16.159 -by (Simp_tac 1);
  16.160 -by (Fast_tac 1);
  16.161 -qed "hyps_insert";
  16.162 -
  16.163 -(** Two lemmas for use with weaken_left **)
  16.164 -
  16.165 -goal Set.thy "B-C <= insert a (B-insert a C)";
  16.166 -by (Fast_tac 1);
  16.167 -qed "insert_Diff_same";
  16.168 -
  16.169 -goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
  16.170 -by (Fast_tac 1);
  16.171 -qed "insert_Diff_subset2";
  16.172 -
  16.173 -(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
  16.174 - could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
  16.175 -goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
  16.176 -by (PropLog.pl.induct_tac "p" 1);
  16.177 -by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
  16.178 -by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
  16.179 -qed "hyps_finite";
  16.180 -
  16.181 -val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
  16.182 -
  16.183 -(*Induction on the finite set of assumptions hyps(p,t0).
  16.184 -  We may repeatedly subtract assumptions until none are left!*)
  16.185 -val [sat] = goal PropLog.thy
  16.186 -    "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
  16.187 -by (rtac (hyps_finite RS Fin_induct) 1);
  16.188 -by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
  16.189 -by (safe_tac (!claset));
  16.190 -(*Case hyps(p,t)-insert(#v,Y) |- p *)
  16.191 -by (rtac thms_excluded_middle_rule 1);
  16.192 -by (rtac (insert_Diff_same RS weaken_left) 1);
  16.193 -by (etac spec 1);
  16.194 -by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  16.195 -by (rtac (hyps_Diff RS Diff_weaken_left) 1);
  16.196 -by (etac spec 1);
  16.197 -(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
  16.198 -by (rtac thms_excluded_middle_rule 1);
  16.199 -by (rtac (insert_Diff_same RS weaken_left) 2);
  16.200 -by (etac spec 2);
  16.201 -by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  16.202 -by (rtac (hyps_insert RS Diff_weaken_left) 1);
  16.203 -by (etac spec 1);
  16.204 -qed "completeness_0_lemma";
  16.205 -
  16.206 -(*The base case for completeness*)
  16.207 -val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
  16.208 -by (rtac (Diff_cancel RS subst) 1);
  16.209 -by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
  16.210 -qed "completeness_0";
  16.211 -
  16.212 -(*A semantic analogue of the Deduction Theorem*)
  16.213 -goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
  16.214 -by (Simp_tac 1);
  16.215 -by (Fast_tac 1);
  16.216 -qed "sat_imp";
  16.217 -
  16.218 -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
  16.219 -by (rtac (finite RS Fin_induct) 1);
  16.220 -by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
  16.221 -by (rtac (weaken_left_insert RS thms.MP) 1);
  16.222 -by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
  16.223 -by (Fast_tac 1);
  16.224 -qed "completeness_lemma";
  16.225 -
  16.226 -val completeness = completeness_lemma RS spec RS mp;
  16.227 -
  16.228 -val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
  16.229 -by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
  16.230 -qed "thms_iff";
  16.231 -
  16.232 -writeln"Reached end of file.";
    17.1 --- a/src/HOL/ex/PropLog.thy	Wed May 07 13:50:52 1997 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,46 +0,0 @@
    17.4 -(*  Title:      HOL/ex/PropLog.thy
    17.5 -    ID:         $Id$
    17.6 -    Author:     Tobias Nipkow
    17.7 -    Copyright   1994  TU Muenchen
    17.8 -
    17.9 -Inductive definition of propositional logic.
   17.10 -*)
   17.11 -
   17.12 -PropLog = Finite +
   17.13 -datatype
   17.14 -    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
   17.15 -consts
   17.16 -  thms :: 'a pl set => 'a pl set
   17.17 -  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   17.18 -  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
   17.19 -  eval2 :: ['a pl, 'a set] => bool
   17.20 -  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
   17.21 -  hyps  :: ['a pl, 'a set] => 'a pl set
   17.22 -
   17.23 -translations
   17.24 -  "H |- p" == "p : thms(H)"
   17.25 -
   17.26 -inductive "thms(H)"
   17.27 -  intrs
   17.28 -  H   "p:H ==> H |- p"
   17.29 -  K   "H |- p->q->p"
   17.30 -  S   "H |- (p->q->r) -> (p->q) -> p->r"
   17.31 -  DN  "H |- ((p->false) -> false) -> p"
   17.32 -  MP  "[| H |- p->q; H |- p |] ==> H |- q"
   17.33 -
   17.34 -defs
   17.35 -  sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
   17.36 -  eval_def "tt[p] == eval2 p tt"
   17.37 -
   17.38 -primrec eval2 pl
   17.39 -  "eval2(false) = (%x.False)"
   17.40 -  "eval2(#v) = (%tt.v:tt)"
   17.41 -  "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
   17.42 -
   17.43 -primrec hyps pl
   17.44 -  "hyps(false) = (%tt.{})"
   17.45 -  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
   17.46 -  "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
   17.47 -
   17.48 -end
   17.49 -
    18.1 --- a/src/HOL/ex/ROOT.ML	Wed May 07 13:50:52 1997 +0200
    18.2 +++ b/src/HOL/ex/ROOT.ML	Wed May 07 13:51:22 1997 +0200
    18.3 @@ -16,22 +16,13 @@
    18.4  (** time_use "mesontest2.ML";  ULTRA SLOW **)
    18.5  time_use_thy "String";
    18.6  time_use_thy "BT";
    18.7 -time_use_thy "Perm";
    18.8 -time_use_thy "Comb";
    18.9  time_use_thy "InSort";
   18.10  time_use_thy "Qsort";
   18.11  time_use_thy "LexProd";
   18.12  time_use_thy "Puzzle";
   18.13 -time_use_thy "Mutil";
   18.14  time_use_thy "Primes";
   18.15  time_use_thy "NatSum";
   18.16  time_use     "set.ML";
   18.17 -time_use_thy "SList";
   18.18 -time_use_thy "LFilter";
   18.19 -time_use_thy "Acc";
   18.20 -time_use_thy "PropLog";
   18.21 -time_use_thy "Term";
   18.22 -time_use_thy "Simult";
   18.23  time_use_thy "MT";
   18.24  
   18.25  writeln "END: Root file for HOL examples";
    19.1 --- a/src/HOL/ex/SList.ML	Wed May 07 13:50:52 1997 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,372 +0,0 @@
    19.4 -(*  Title:      HOL/ex/SList.ML
    19.5 -    ID:         $Id$
    19.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7 -    Copyright   1993  University of Cambridge
    19.8 -
    19.9 -Definition of type 'a list by a least fixed point
   19.10 -*)
   19.11 -
   19.12 -open SList;
   19.13 -
   19.14 -val list_con_defs = [NIL_def, CONS_def];
   19.15 -
   19.16 -goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
   19.17 -let val rew = rewrite_rule list_con_defs in  
   19.18 -by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
   19.19 -                      addEs [rew list.elim]) 1)
   19.20 -end;
   19.21 -qed "list_unfold";
   19.22 -
   19.23 -(*This justifies using list in other recursive type definitions*)
   19.24 -goalw SList.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
   19.25 -by (rtac lfp_mono 1);
   19.26 -by (REPEAT (ares_tac basic_monos 1));
   19.27 -qed "list_mono";
   19.28 -
   19.29 -(*Type checking -- list creates well-founded sets*)
   19.30 -goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
   19.31 -by (rtac lfp_lowerbound 1);
   19.32 -by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
   19.33 -qed "list_sexp";
   19.34 -
   19.35 -(* A <= sexp ==> list(A) <= sexp *)
   19.36 -bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
   19.37 -
   19.38 -(*Induction for the type 'a list *)
   19.39 -val prems = goalw SList.thy [Nil_def,Cons_def]
   19.40 -    "[| P(Nil);   \
   19.41 -\       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
   19.42 -by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
   19.43 -by (rtac (Rep_list RS list.induct) 1);
   19.44 -by (REPEAT (ares_tac prems 1
   19.45 -     ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
   19.46 -qed "list_induct2";
   19.47 -
   19.48 -(*Perform induction on xs. *)
   19.49 -fun list_ind_tac a M = 
   19.50 -    EVERY [res_inst_tac [("l",a)] list_induct2 M,
   19.51 -           rename_last_tac a ["1"] (M+1)];
   19.52 -
   19.53 -(*** Isomorphisms ***)
   19.54 -
   19.55 -goal SList.thy "inj(Rep_list)";
   19.56 -by (rtac inj_inverseI 1);
   19.57 -by (rtac Rep_list_inverse 1);
   19.58 -qed "inj_Rep_list";
   19.59 -
   19.60 -goal SList.thy "inj_onto Abs_list (list(range Leaf))";
   19.61 -by (rtac inj_onto_inverseI 1);
   19.62 -by (etac Abs_list_inverse 1);
   19.63 -qed "inj_onto_Abs_list";
   19.64 -
   19.65 -(** Distinctness of constructors **)
   19.66 -
   19.67 -goalw SList.thy list_con_defs "CONS M N ~= NIL";
   19.68 -by (rtac In1_not_In0 1);
   19.69 -qed "CONS_not_NIL";
   19.70 -bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
   19.71 -
   19.72 -bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
   19.73 -val NIL_neq_CONS = sym RS CONS_neq_NIL;
   19.74 -
   19.75 -goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
   19.76 -by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
   19.77 -by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
   19.78 -qed "Cons_not_Nil";
   19.79 -
   19.80 -bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
   19.81 -
   19.82 -(** Injectiveness of CONS and Cons **)
   19.83 -
   19.84 -goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
   19.85 -by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
   19.86 -qed "CONS_CONS_eq";
   19.87 -
   19.88 -(*For reasoning about abstract list constructors*)
   19.89 -AddIs ([Rep_list] @ list.intrs);
   19.90 -
   19.91 -AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
   19.92 -
   19.93 -AddSDs [inj_onto_Abs_list RS inj_ontoD,
   19.94 -        inj_Rep_list RS injD, Leaf_inject];
   19.95 -
   19.96 -goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
   19.97 -by (Fast_tac 1);
   19.98 -qed "Cons_Cons_eq";
   19.99 -bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
  19.100 -
  19.101 -val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
  19.102 -by (rtac (major RS setup_induction) 1);
  19.103 -by (etac list.induct 1);
  19.104 -by (ALLGOALS (Fast_tac));
  19.105 -qed "CONS_D";
  19.106 -
  19.107 -val prems = goalw SList.thy [CONS_def,In1_def]
  19.108 -    "CONS M N: sexp ==> M: sexp & N: sexp";
  19.109 -by (cut_facts_tac prems 1);
  19.110 -by (fast_tac (!claset addSDs [Scons_D]) 1);
  19.111 -qed "sexp_CONS_D";
  19.112 -
  19.113 -
  19.114 -(*Reasoning about constructors and their freeness*)
  19.115 -Addsimps list.intrs;
  19.116 -
  19.117 -AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
  19.118 -
  19.119 -goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
  19.120 -by (etac list.induct 1);
  19.121 -by (ALLGOALS Asm_simp_tac);
  19.122 -qed "not_CONS_self";
  19.123 -
  19.124 -goal SList.thy "!x. l ~= x#l";
  19.125 -by (list_ind_tac "l" 1);
  19.126 -by (ALLGOALS Asm_simp_tac);
  19.127 -qed "not_Cons_self2";
  19.128 -
  19.129 -
  19.130 -goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
  19.131 -by (list_ind_tac "xs" 1);
  19.132 -by (Simp_tac 1);
  19.133 -by (Asm_simp_tac 1);
  19.134 -by (REPEAT(resolve_tac [exI,refl,conjI] 1));
  19.135 -qed "neq_Nil_conv2";
  19.136 -
  19.137 -(** Conversion rules for List_case: case analysis operator **)
  19.138 -
  19.139 -goalw SList.thy [List_case_def,NIL_def] "List_case c h NIL = c";
  19.140 -by (rtac Case_In0 1);
  19.141 -qed "List_case_NIL";
  19.142 -
  19.143 -goalw SList.thy [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
  19.144 -by (simp_tac (!simpset addsimps [Split,Case_In1]) 1);
  19.145 -qed "List_case_CONS";
  19.146 -
  19.147 -(*** List_rec -- by wf recursion on pred_sexp ***)
  19.148 -
  19.149 -(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
  19.150 -   hold if pred_sexp^+ were changed to pred_sexp. *)
  19.151 -
  19.152 -goal SList.thy
  19.153 -   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
  19.154 -                           \     (%g. List_case c (%x y. d x y (g y)))";
  19.155 -by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
  19.156 -val List_rec_unfold = standard 
  19.157 -  ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
  19.158 -
  19.159 -(*---------------------------------------------------------------------------
  19.160 - * Old:
  19.161 - * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
  19.162 - *                     |> standard;
  19.163 - *---------------------------------------------------------------------------*)
  19.164 -
  19.165 -(** pred_sexp lemmas **)
  19.166 -
  19.167 -goalw SList.thy [CONS_def,In1_def]
  19.168 -    "!!M. [| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
  19.169 -by (Asm_simp_tac 1);
  19.170 -qed "pred_sexp_CONS_I1";
  19.171 -
  19.172 -goalw SList.thy [CONS_def,In1_def]
  19.173 -    "!!M. [| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
  19.174 -by (Asm_simp_tac 1);
  19.175 -qed "pred_sexp_CONS_I2";
  19.176 -
  19.177 -val [prem] = goal SList.thy
  19.178 -    "(CONS M1 M2, N) : pred_sexp^+ ==> \
  19.179 -\    (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
  19.180 -by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
  19.181 -                   subsetD RS SigmaE2)) 1);
  19.182 -by (etac (sexp_CONS_D RS conjE) 1);
  19.183 -by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
  19.184 -                      prem RSN (2, trans_trancl RS transD)] 1));
  19.185 -qed "pred_sexp_CONS_D";
  19.186 -
  19.187 -(** Conversion rules for List_rec **)
  19.188 -
  19.189 -goal SList.thy "List_rec NIL c h = c";
  19.190 -by (rtac (List_rec_unfold RS trans) 1);
  19.191 -by (simp_tac (!simpset addsimps [List_case_NIL]) 1);
  19.192 -qed "List_rec_NIL";
  19.193 -
  19.194 -goal SList.thy "!!M. [| M: sexp;  N: sexp |] ==> \
  19.195 -\    List_rec (CONS M N) c h = h M N (List_rec N c h)";
  19.196 -by (rtac (List_rec_unfold RS trans) 1);
  19.197 -by (asm_simp_tac (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
  19.198 -qed "List_rec_CONS";
  19.199 -
  19.200 -(*** list_rec -- by List_rec ***)
  19.201 -
  19.202 -val Rep_list_in_sexp =
  19.203 -    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
  19.204 -
  19.205 -local
  19.206 -  val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
  19.207 -                        Abs_list_inverse, Rep_list_inverse,
  19.208 -                        Rep_list, rangeI, inj_Leaf, inv_f_f,
  19.209 -                        sexp.LeafI, Rep_list_in_sexp]
  19.210 -in
  19.211 -  val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
  19.212 -      "list_rec Nil c h = c"
  19.213 -   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
  19.214 -
  19.215 -  val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def]
  19.216 -      "list_rec (a#l) c h = h a l (list_rec l c h)"
  19.217 -   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
  19.218 -end;
  19.219 -
  19.220 -Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
  19.221 -
  19.222 -
  19.223 -(*Type checking.  Useful?*)
  19.224 -val major::A_subset_sexp::prems = goal SList.thy
  19.225 -    "[| M: list(A);     \
  19.226 -\       A<=sexp;        \
  19.227 -\       c: C(NIL);      \
  19.228 -\       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
  19.229 -\    |] ==> List_rec M c h : C(M :: 'a item)";
  19.230 -val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
  19.231 -val sexp_A_I = A_subset_sexp RS subsetD;
  19.232 -by (rtac (major RS list.induct) 1);
  19.233 -by (ALLGOALS(asm_simp_tac (!simpset addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
  19.234 -qed "List_rec_type";
  19.235 -
  19.236 -(** Generalized map functionals **)
  19.237 -
  19.238 -goalw SList.thy [Rep_map_def] "Rep_map f Nil = NIL";
  19.239 -by (rtac list_rec_Nil 1);
  19.240 -qed "Rep_map_Nil";
  19.241 -
  19.242 -goalw SList.thy [Rep_map_def]
  19.243 -    "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
  19.244 -by (rtac list_rec_Cons 1);
  19.245 -qed "Rep_map_Cons";
  19.246 -
  19.247 -goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
  19.248 -by (rtac list_induct2 1);
  19.249 -by (ALLGOALS Asm_simp_tac);
  19.250 -qed "Rep_map_type";
  19.251 -
  19.252 -goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil";
  19.253 -by (rtac List_rec_NIL 1);
  19.254 -qed "Abs_map_NIL";
  19.255 -
  19.256 -val prems = goalw SList.thy [Abs_map_def]
  19.257 -    "[| M: sexp;  N: sexp |] ==> \
  19.258 -\    Abs_map g (CONS M N) = g(M) # Abs_map g N";
  19.259 -by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
  19.260 -qed "Abs_map_CONS";
  19.261 -
  19.262 -(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
  19.263 -val [rew] = goal SList.thy
  19.264 -    "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
  19.265 -by (rewtac rew);
  19.266 -by (rtac list_rec_Nil 1);
  19.267 -qed "def_list_rec_Nil";
  19.268 -
  19.269 -val [rew] = goal SList.thy
  19.270 -    "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
  19.271 -by (rewtac rew);
  19.272 -by (rtac list_rec_Cons 1);
  19.273 -qed "def_list_rec_Cons";
  19.274 -
  19.275 -fun list_recs def =
  19.276 -      [standard (def RS def_list_rec_Nil),
  19.277 -       standard (def RS def_list_rec_Cons)];
  19.278 -
  19.279 -(*** Unfolding the basic combinators ***)
  19.280 -
  19.281 -val [null_Nil, null_Cons]               = list_recs null_def;
  19.282 -val [_, hd_Cons]                        = list_recs hd_def;
  19.283 -val [_, tl_Cons]                        = list_recs tl_def;
  19.284 -val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
  19.285 -val [append_Nil3, append_Cons]          = list_recs append_def;
  19.286 -val [mem_Nil, mem_Cons]                 = list_recs mem_def;
  19.287 -val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
  19.288 -val [map_Nil, map_Cons]                 = list_recs map_def;
  19.289 -val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
  19.290 -val [filter_Nil, filter_Cons]           = list_recs filter_def;
  19.291 -
  19.292 -Addsimps
  19.293 -  [null_Nil, ttl_Nil,
  19.294 -   mem_Nil, mem_Cons,
  19.295 -   list_case_Nil, list_case_Cons,
  19.296 -   append_Nil3, append_Cons,
  19.297 -   set_of_list_Nil, set_of_list_Cons, 
  19.298 -   map_Nil, map_Cons,
  19.299 -   filter_Nil, filter_Cons];
  19.300 -
  19.301 -
  19.302 -(** @ - append **)
  19.303 -
  19.304 -goal SList.thy "(xs@ys)@zs = xs@(ys@zs)";
  19.305 -by (list_ind_tac "xs" 1);
  19.306 -by (ALLGOALS Asm_simp_tac);
  19.307 -qed "append_assoc2";
  19.308 -
  19.309 -goal SList.thy "xs @ [] = xs";
  19.310 -by (list_ind_tac "xs" 1);
  19.311 -by (ALLGOALS Asm_simp_tac);
  19.312 -qed "append_Nil4";
  19.313 -
  19.314 -(** mem **)
  19.315 -
  19.316 -goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
  19.317 -by (list_ind_tac "xs" 1);
  19.318 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
  19.319 -qed "mem_append2";
  19.320 -
  19.321 -goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
  19.322 -by (list_ind_tac "xs" 1);
  19.323 -by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
  19.324 -qed "mem_filter2";
  19.325 -
  19.326 -
  19.327 -(** The functional "map" **)
  19.328 -
  19.329 -Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
  19.330 -
  19.331 -val [major,A_subset_sexp,minor] = goal SList.thy 
  19.332 -    "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
  19.333 -\    ==> Rep_map f (Abs_map g M) = M";
  19.334 -by (rtac (major RS list.induct) 1);
  19.335 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sexp_A_I,sexp_ListA_I,minor])));
  19.336 -qed "Abs_map_inverse";
  19.337 -
  19.338 -(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
  19.339 -
  19.340 -(** list_case **)
  19.341 -
  19.342 -goal SList.thy
  19.343 - "P(list_case a f xs) = ((xs=[] --> P(a)) & \
  19.344 -\                        (!y ys. xs=y#ys --> P(f y ys)))";
  19.345 -by (list_ind_tac "xs" 1);
  19.346 -by (ALLGOALS Asm_simp_tac);
  19.347 -by (Fast_tac 1);
  19.348 -qed "expand_list_case2";
  19.349 -
  19.350 -
  19.351 -(** Additional mapping lemmas **)
  19.352 -
  19.353 -goal SList.thy "map (%x.x) xs = xs";
  19.354 -by (list_ind_tac "xs" 1);
  19.355 -by (ALLGOALS Asm_simp_tac);
  19.356 -qed "map_ident2";
  19.357 -
  19.358 -goal SList.thy "map f (xs@ys) = map f xs @ map f ys";
  19.359 -by (list_ind_tac "xs" 1);
  19.360 -by (ALLGOALS Asm_simp_tac);
  19.361 -qed "map_append2";
  19.362 -
  19.363 -goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)";
  19.364 -by (list_ind_tac "xs" 1);
  19.365 -by (ALLGOALS Asm_simp_tac);
  19.366 -qed "map_compose2";
  19.367 -
  19.368 -goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
  19.369 -\       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
  19.370 -by (list_ind_tac "xs" 1);
  19.371 -by (ALLGOALS(asm_simp_tac(!simpset addsimps
  19.372 -       [Rep_map_type,list_sexp RS subsetD])));
  19.373 -qed "Abs_Rep_map";
  19.374 -
  19.375 -Addsimps [append_Nil4, map_ident2];
    20.1 --- a/src/HOL/ex/SList.thy	Wed May 07 13:50:52 1997 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,119 +0,0 @@
    20.4 -(*  Title:      HOL/ex/SList.thy
    20.5 -    ID:         $Id$
    20.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7 -    Copyright   1993  University of Cambridge
    20.8 -
    20.9 -Definition of type 'a list (strict lists) by a least fixed point
   20.10 -
   20.11 -We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
   20.12 -and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
   20.13 -so that list can serve as a "functor" for defining other recursive types
   20.14 -*)
   20.15 -
   20.16 -SList = Sexp +
   20.17 -
   20.18 -types
   20.19 -  'a list
   20.20 -
   20.21 -arities
   20.22 -  list :: (term) term
   20.23 -
   20.24 -
   20.25 -consts
   20.26 -
   20.27 -  list        :: 'a item set => 'a item set
   20.28 -  Rep_list    :: 'a list => 'a item
   20.29 -  Abs_list    :: 'a item => 'a list
   20.30 -  NIL         :: 'a item
   20.31 -  CONS        :: ['a item, 'a item] => 'a item
   20.32 -  Nil         :: 'a list
   20.33 -  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
   20.34 -  List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   20.35 -  List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
   20.36 -  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
   20.37 -  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
   20.38 -  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
   20.39 -  Abs_map     :: ('a item => 'b) => 'a item => 'b list
   20.40 -  null        :: 'a list => bool
   20.41 -  hd          :: 'a list => 'a
   20.42 -  tl,ttl      :: 'a list => 'a list
   20.43 -  set_of_list :: ('a list => 'a set)
   20.44 -  mem         :: ['a, 'a list] => bool                            (infixl 55)
   20.45 -  map         :: ('a=>'b) => ('a list => 'b list)
   20.46 -  "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
   20.47 -  filter      :: ['a => bool, 'a list] => 'a list
   20.48 -
   20.49 -  (* list Enumeration *)
   20.50 -
   20.51 -  "[]"        :: 'a list                              ("[]")
   20.52 -  "@list"     :: args => 'a list                      ("[(_)]")
   20.53 -
   20.54 -  (* Special syntax for filter *)
   20.55 -  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
   20.56 -
   20.57 -translations
   20.58 -  "[x, xs]"     == "x#[xs]"
   20.59 -  "[x]"         == "x#[]"
   20.60 -  "[]"          == "Nil"
   20.61 -
   20.62 -  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
   20.63 -
   20.64 -  "[x:xs . P]"  == "filter (%x.P) xs"
   20.65 -
   20.66 -defs
   20.67 -  (* Defining the Concrete Constructors *)
   20.68 -  NIL_def       "NIL == In0(Numb(0))"
   20.69 -  CONS_def      "CONS M N == In1(M $ N)"
   20.70 -
   20.71 -inductive "list(A)"
   20.72 -  intrs
   20.73 -    NIL_I  "NIL: list(A)"
   20.74 -    CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
   20.75 -
   20.76 -rules
   20.77 -  (* Faking a Type Definition ... *)
   20.78 -  Rep_list          "Rep_list(xs): list(range(Leaf))"
   20.79 -  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
   20.80 -  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
   20.81 -
   20.82 -
   20.83 -defs
   20.84 -  (* Defining the Abstract Constructors *)
   20.85 -  Nil_def       "Nil == Abs_list(NIL)"
   20.86 -  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
   20.87 -
   20.88 -  List_case_def "List_case c d == Case (%x.c) (Split d)"
   20.89 -
   20.90 -  (* list Recursion -- the trancl is Essential; see list.ML *)
   20.91 -
   20.92 -  List_rec_def
   20.93 -   "List_rec M c d == wfrec (trancl pred_sexp)
   20.94 -                            (%g. List_case c (%x y. d x y (g y))) M"
   20.95 -
   20.96 -  list_rec_def
   20.97 -   "list_rec l c d == 
   20.98 -   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
   20.99 -
  20.100 -  (* Generalized Map Functionals *)
  20.101 -
  20.102 -  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
  20.103 -  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
  20.104 -
  20.105 -  null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
  20.106 -  hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
  20.107 -  tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
  20.108 -  (* a total version of tl: *)
  20.109 -  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
  20.110 -
  20.111 -  set_of_list_def "set_of_list xs    == list_rec xs {} (%x l r. insert x r)"
  20.112 -
  20.113 -  mem_def       "x mem xs            == 
  20.114 -                   list_rec xs False (%y ys r. if y=x then True else r)"
  20.115 -  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
  20.116 -  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
  20.117 -  filter_def    "filter P xs         == 
  20.118 -                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
  20.119 -
  20.120 -  list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
  20.121 -
  20.122 -end
    21.1 --- a/src/HOL/ex/Simult.ML	Wed May 07 13:50:52 1997 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,298 +0,0 @@
    21.4 -(*  Title:      HOL/ex/Simult.ML
    21.5 -    ID:         $Id$
    21.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 -    Copyright   1993  University of Cambridge
    21.8 -
    21.9 -Primitives for simultaneous recursive type definitions
   21.10 -  includes worked example of trees & forests
   21.11 -
   21.12 -This is essentially the same data structure that on ex/term.ML, which is
   21.13 -simpler because it uses list as a new type former.  The approach in this
   21.14 -file may be superior for other simultaneous recursions.
   21.15 -*)
   21.16 -
   21.17 -open Simult;
   21.18 -
   21.19 -(*** Monotonicity and unfolding of the function ***)
   21.20 -
   21.21 -goal Simult.thy "mono(%Z.  A <*> Part Z In1 \
   21.22 -\                      <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))";
   21.23 -by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
   21.24 -                      Part_mono] 1));
   21.25 -qed "TF_fun_mono";
   21.26 -
   21.27 -val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
   21.28 -
   21.29 -goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
   21.30 -by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
   21.31 -qed "TF_mono";
   21.32 -
   21.33 -goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
   21.34 -by (rtac lfp_lowerbound 1);
   21.35 -by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
   21.36 -                      addSEs [PartE]) 1);
   21.37 -qed "TF_sexp";
   21.38 -
   21.39 -(* A <= sexp ==> TF(A) <= sexp *)
   21.40 -val TF_subset_sexp = standard
   21.41 -    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
   21.42 -
   21.43 -
   21.44 -(** Elimination -- structural induction on the set TF **)
   21.45 -
   21.46 -val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
   21.47 -
   21.48 -val major::prems = goalw Simult.thy TF_Rep_defs
   21.49 - "[| i: TF(A);  \
   21.50 -\    !!M N. [| M: A;  N: Part (TF A) In1;  R(N) |] ==> R(TCONS M N);    \
   21.51 -\    R(FNIL);                   \
   21.52 -\    !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  R(M);  R(N) \
   21.53 -\            |] ==> R(FCONS M N)    \
   21.54 -\    |] ==> R(i)";
   21.55 -by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
   21.56 -by (blast_tac (!claset addIs (prems@[PartI])
   21.57 -                       addEs [usumE, uprodE, PartE]) 1);
   21.58 -qed "TF_induct";
   21.59 -
   21.60 -(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
   21.61 -goalw Simult.thy [Part_def]
   21.62 - "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
   21.63 -\                   (M: Part (TF A) In1 --> Q(M)) \
   21.64 -\  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
   21.65 -by (Blast_tac 1);
   21.66 -qed "TF_induct_lemma";
   21.67 -
   21.68 -(*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
   21.69 -
   21.70 -(*Induction on TF with separate predicates P, Q*)
   21.71 -val prems = goalw Simult.thy TF_Rep_defs
   21.72 -    "[| !!M N. [| M: A;  N: Part (TF A) In1;  Q(N) |] ==> P(TCONS M N); \
   21.73 -\       Q(FNIL);        \
   21.74 -\       !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  P(M);  Q(N) \
   21.75 -\               |] ==> Q(FCONS M N)     \
   21.76 -\    |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))";
   21.77 -by (rtac (ballI RS TF_induct_lemma) 1);
   21.78 -by (etac TF_induct 1);
   21.79 -by (rewrite_goals_tac TF_Rep_defs);
   21.80 -	(*Blast_tac needs this type instantiation in order to preserve the
   21.81 -          right overloading of equality.  The injectiveness properties for
   21.82 -          type 'a item hold only for set types.*)
   21.83 -val PartE' = read_instantiate [("'a", "?'c set")] PartE;
   21.84 -by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
   21.85 -qed "Tree_Forest_induct";
   21.86 -
   21.87 -(*Induction for the abstract types 'a tree, 'a forest*)
   21.88 -val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
   21.89 -    "[| !!x ts. Q(ts) ==> P(Tcons x ts);     \
   21.90 -\       Q(Fnil);        \
   21.91 -\       !!t ts. [| P(t);  Q(ts) |] ==> Q(Fcons t ts)    \
   21.92 -\    |] ==> (! t. P(t)) & (! ts. Q(ts))";
   21.93 -by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
   21.94 -                  ("Q1","%z.Q(Abs_Forest(z))")] 
   21.95 -    (Tree_Forest_induct RS conjE) 1);
   21.96 -(*Instantiates ?A1 to range(Leaf). *)
   21.97 -by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
   21.98 -			      Rep_Forest_inverse RS subst] 
   21.99 -                       addSIs [Rep_Tree,Rep_Forest]) 4);
  21.100 -(*Cannot use simplifier: the rewrites work in the wrong direction!*)
  21.101 -by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
  21.102 -					Abs_Forest_inverse RS subst] 
  21.103 -                                addSIs prems)));
  21.104 -qed "tree_forest_induct";
  21.105 -
  21.106 -
  21.107 -
  21.108 -(*** Isomorphisms ***)
  21.109 -
  21.110 -goal Simult.thy "inj(Rep_Tree)";
  21.111 -by (rtac inj_inverseI 1);
  21.112 -by (rtac Rep_Tree_inverse 1);
  21.113 -qed "inj_Rep_Tree";
  21.114 -
  21.115 -goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
  21.116 -by (rtac inj_onto_inverseI 1);
  21.117 -by (etac Abs_Tree_inverse 1);
  21.118 -qed "inj_onto_Abs_Tree";
  21.119 -
  21.120 -goal Simult.thy "inj(Rep_Forest)";
  21.121 -by (rtac inj_inverseI 1);
  21.122 -by (rtac Rep_Forest_inverse 1);
  21.123 -qed "inj_Rep_Forest";
  21.124 -
  21.125 -goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
  21.126 -by (rtac inj_onto_inverseI 1);
  21.127 -by (etac Abs_Forest_inverse 1);
  21.128 -qed "inj_onto_Abs_Forest";
  21.129 -
  21.130 -(** Introduction rules for constructors **)
  21.131 -
  21.132 -(* c : A <*> Part (TF A) In1 
  21.133 -        <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *)
  21.134 -val TF_I = TF_unfold RS equalityD2 RS subsetD;
  21.135 -
  21.136 -(*For reasoning about the representation*)
  21.137 -AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
  21.138 -AddSEs [Scons_inject];
  21.139 -
  21.140 -goalw Simult.thy TF_Rep_defs
  21.141 -    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
  21.142 -by (Blast_tac 1);
  21.143 -qed "TCONS_I";
  21.144 -
  21.145 -(* FNIL is a TF(A) -- this also justifies the type definition*)
  21.146 -goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
  21.147 -by (Blast_tac 1);
  21.148 -qed "FNIL_I";
  21.149 -
  21.150 -goalw Simult.thy TF_Rep_defs
  21.151 -    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
  21.152 -\         FCONS M N : Part (TF A) In1";
  21.153 -by (Blast_tac 1);
  21.154 -qed "FCONS_I";
  21.155 -
  21.156 -(** Injectiveness of TCONS and FCONS **)
  21.157 -
  21.158 -goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
  21.159 -by (Blast_tac 1);
  21.160 -qed "TCONS_TCONS_eq";
  21.161 -bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
  21.162 -
  21.163 -goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
  21.164 -by (Blast_tac 1);
  21.165 -qed "FCONS_FCONS_eq";
  21.166 -bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
  21.167 -
  21.168 -(** Distinctness of TCONS, FNIL and FCONS **)
  21.169 -
  21.170 -goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
  21.171 -by (Blast_tac 1);
  21.172 -qed "TCONS_not_FNIL";
  21.173 -bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
  21.174 -
  21.175 -bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
  21.176 -val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
  21.177 -
  21.178 -goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
  21.179 -by (Blast_tac 1);
  21.180 -qed "FCONS_not_FNIL";
  21.181 -bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
  21.182 -
  21.183 -bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
  21.184 -val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
  21.185 -
  21.186 -goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
  21.187 -by (Blast_tac 1);
  21.188 -qed "TCONS_not_FCONS";
  21.189 -bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
  21.190 -
  21.191 -bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
  21.192 -val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
  21.193 -
  21.194 -(*???? Too many derived rules ????
  21.195 -  Automatically generate symmetric forms?  Always expand TF_Rep_defs? *)
  21.196 -
  21.197 -(** Injectiveness of Tcons and Fcons **)
  21.198 -
  21.199 -(*For reasoning about abstract constructors*)
  21.200 -AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
  21.201 -AddSEs [TCONS_inject, FCONS_inject,
  21.202 -                           TCONS_neq_FNIL, FNIL_neq_TCONS,
  21.203 -                           FCONS_neq_FNIL, FNIL_neq_FCONS,
  21.204 -                           TCONS_neq_FCONS, FCONS_neq_TCONS];
  21.205 -AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
  21.206 -                           inj_onto_Abs_Forest RS inj_ontoD,
  21.207 -                           inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
  21.208 -                           Leaf_inject];
  21.209 -
  21.210 -goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
  21.211 -by (Blast_tac 1);
  21.212 -qed "Tcons_Tcons_eq";
  21.213 -bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
  21.214 -
  21.215 -goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
  21.216 -by (Blast_tac 1);
  21.217 -qed "Fcons_not_Fnil";
  21.218 -
  21.219 -bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
  21.220 -val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
  21.221 -
  21.222 -
  21.223 -(** Injectiveness of Fcons **)
  21.224 -
  21.225 -goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
  21.226 -by (Blast_tac 1);
  21.227 -qed "Fcons_Fcons_eq";
  21.228 -bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
  21.229 -
  21.230 -
  21.231 -(*** TF_rec -- by wf recursion on pred_sexp ***)
  21.232 -
  21.233 -goal Simult.thy
  21.234 -   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
  21.235 -                         \       (%g. Case (Split(%x y. b x y (g y))) \
  21.236 -                         \           (List_case c (%x y. d x y (g x) (g y))))";
  21.237 -by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
  21.238 -val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
  21.239 -                    ((result() RS eq_reflection) RS def_wfrec);
  21.240 -
  21.241 -(*---------------------------------------------------------------------------
  21.242 - * Old: 
  21.243 - * val TF_rec_unfold =
  21.244 - *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
  21.245 - *---------------------------------------------------------------------------*)
  21.246 -
  21.247 -(** conversion rules for TF_rec **)
  21.248 -
  21.249 -goalw Simult.thy [TCONS_def]
  21.250 -    "!!M N. [| M: sexp;  N: sexp |] ==>         \
  21.251 -\           TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
  21.252 -by (rtac (TF_rec_unfold RS trans) 1);
  21.253 -by (simp_tac (!simpset addsimps [Case_In0, Split]) 1);
  21.254 -by (asm_simp_tac (!simpset addsimps [In0_def]) 1);
  21.255 -qed "TF_rec_TCONS";
  21.256 -
  21.257 -goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c";
  21.258 -by (rtac (TF_rec_unfold RS trans) 1);
  21.259 -by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
  21.260 -qed "TF_rec_FNIL";
  21.261 -
  21.262 -goalw Simult.thy [FCONS_def]
  21.263 - "!!M N. [| M: sexp;  N: sexp |] ==>    \
  21.264 -\        TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
  21.265 -by (rtac (TF_rec_unfold RS trans) 1);
  21.266 -by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
  21.267 -by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1);
  21.268 -qed "TF_rec_FCONS";
  21.269 -
  21.270 -
  21.271 -(*** tree_rec, forest_rec -- by TF_rec ***)
  21.272 -
  21.273 -val Rep_Tree_in_sexp =
  21.274 -    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
  21.275 -     Rep_Tree] MRS subsetD;
  21.276 -val Rep_Forest_in_sexp =
  21.277 -    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
  21.278 -     Rep_Forest] MRS subsetD;
  21.279 -
  21.280 -val tf_rec_ss = HOL_ss addsimps
  21.281 -  [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
  21.282 -   TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
  21.283 -   Rep_Tree_inverse, Rep_Forest_inverse,
  21.284 -   Abs_Tree_inverse, Abs_Forest_inverse,
  21.285 -   inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
  21.286 -   Rep_Tree_in_sexp, Rep_Forest_in_sexp];
  21.287 -
  21.288 -goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
  21.289 -    "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)";
  21.290 -by (simp_tac tf_rec_ss 1);
  21.291 -qed "tree_rec_Tcons";
  21.292 -
  21.293 -goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c";
  21.294 -by (simp_tac tf_rec_ss 1);
  21.295 -qed "forest_rec_Fnil";
  21.296 -
  21.297 -goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
  21.298 -    "forest_rec (Fcons t tf) b c d = \
  21.299 -\    d t tf (tree_rec t b c d) (forest_rec tf b c d)";
  21.300 -by (simp_tac tf_rec_ss 1);
  21.301 -qed "forest_rec_Cons";
    22.1 --- a/src/HOL/ex/Simult.thy	Wed May 07 13:50:52 1997 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,82 +0,0 @@
    22.4 -(*  Title:      HOL/ex/Simult
    22.5 -    ID:         $Id$
    22.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 -    Copyright   1993  University of Cambridge
    22.8 -
    22.9 -A simultaneous recursive type definition: trees & forests
   22.10 -
   22.11 -This is essentially the same data structure that on ex/term.ML, which is
   22.12 -simpler because it uses list as a new type former.  The approach in this
   22.13 -file may be superior for other simultaneous recursions.
   22.14 -
   22.15 -The inductive definition package does not help defining this sort of mutually
   22.16 -recursive data structure because it uses Inl, Inr instead of In0, In1.
   22.17 -*)
   22.18 -
   22.19 -Simult = SList +
   22.20 -
   22.21 -types    'a tree
   22.22 -         'a forest
   22.23 -
   22.24 -arities  tree,forest :: (term)term
   22.25 -
   22.26 -consts
   22.27 -  TF          :: 'a item set => 'a item set
   22.28 -  FNIL        :: 'a item
   22.29 -  TCONS,FCONS :: ['a item, 'a item] => 'a item
   22.30 -  Rep_Tree    :: 'a tree => 'a item
   22.31 -  Abs_Tree    :: 'a item => 'a tree
   22.32 -  Rep_Forest  :: 'a forest => 'a item
   22.33 -  Abs_Forest  :: 'a item => 'a forest
   22.34 -  Tcons       :: ['a, 'a forest] => 'a tree
   22.35 -  Fcons       :: ['a tree, 'a forest] => 'a forest
   22.36 -  Fnil        :: 'a forest
   22.37 -  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
   22.38 -                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
   22.39 -  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
   22.40 -                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
   22.41 -  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
   22.42 -                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
   22.43 -
   22.44 -defs
   22.45 -     (*the concrete constants*)
   22.46 -  TCONS_def     "TCONS M N == In0(M $ N)"
   22.47 -  FNIL_def      "FNIL      == In1(NIL)"
   22.48 -  FCONS_def     "FCONS M N == In1(CONS M N)"
   22.49 -     (*the abstract constants*)
   22.50 -  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
   22.51 -  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
   22.52 -  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
   22.53 -
   22.54 -  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
   22.55 -                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
   22.56 -
   22.57 -rules
   22.58 -  (*faking a type definition for tree...*)
   22.59 -  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
   22.60 -  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
   22.61 -  Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
   22.62 -    (*faking a type definition for forest...*)
   22.63 -  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
   22.64 -  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
   22.65 -  Abs_Forest_inverse 
   22.66 -        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
   22.67 -
   22.68 -
   22.69 -defs
   22.70 -     (*recursion*)
   22.71 -  TF_rec_def    
   22.72 -   "TF_rec M b c d == wfrec (trancl pred_sexp)
   22.73 -               (%g. Case (Split(%x y. b x y (g y))) 
   22.74 -                      (List_case c (%x y. d x y (g x) (g y)))) M"
   22.75 -
   22.76 -  tree_rec_def
   22.77 -   "tree_rec t b c d == 
   22.78 -   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
   22.79 -          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   22.80 -
   22.81 -  forest_rec_def
   22.82 -   "forest_rec tf b c d == 
   22.83 -   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
   22.84 -          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   22.85 -end
    23.1 --- a/src/HOL/ex/Term.ML	Wed May 07 13:50:52 1997 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,172 +0,0 @@
    23.4 -(*  Title:      HOL/ex/Term
    23.5 -    ID:         $Id$
    23.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 -    Copyright   1992  University of Cambridge
    23.8 -
    23.9 -Terms over a given alphabet -- function applications; illustrates list functor
   23.10 -  (essentially the same type as in Trees & Forests)
   23.11 -*)
   23.12 -
   23.13 -open Term;
   23.14 -
   23.15 -(*** Monotonicity and unfolding of the function ***)
   23.16 -
   23.17 -goal Term.thy "term(A) = A <*> list(term(A))";
   23.18 -by (fast_tac (!claset addSIs (equalityI :: term.intrs)
   23.19 -                      addEs [term.elim]) 1);
   23.20 -qed "term_unfold";
   23.21 -
   23.22 -(*This justifies using term in other recursive type definitions*)
   23.23 -goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
   23.24 -by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
   23.25 -qed "term_mono";
   23.26 -
   23.27 -(** Type checking -- term creates well-founded sets **)
   23.28 -
   23.29 -goalw Term.thy term.defs "term(sexp) <= sexp";
   23.30 -by (rtac lfp_lowerbound 1);
   23.31 -by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
   23.32 -qed "term_sexp";
   23.33 -
   23.34 -(* A <= sexp ==> term(A) <= sexp *)
   23.35 -bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
   23.36 -
   23.37 -
   23.38 -(** Elimination -- structural induction on the set term(A) **)
   23.39 -
   23.40 -(*Induction for the set term(A) *)
   23.41 -val [major,minor] = goal Term.thy 
   23.42 -    "[| M: term(A);  \
   23.43 -\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
   23.44 -\               |] ==> R(x$zs)  \
   23.45 -\    |] ==> R(M)";
   23.46 -by (rtac (major RS term.induct) 1);
   23.47 -by (REPEAT (eresolve_tac ([minor] @
   23.48 -                ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
   23.49 -(*Proof could also use  mono_Int RS subsetD RS IntE *)
   23.50 -qed "Term_induct";
   23.51 -
   23.52 -(*Induction on term(A) followed by induction on list *)
   23.53 -val major::prems = goal Term.thy
   23.54 -    "[| M: term(A);  \
   23.55 -\       !!x.      [| x: A |] ==> R(x$NIL);  \
   23.56 -\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
   23.57 -\                 |] ==> R(x $ CONS z zs)  \
   23.58 -\    |] ==> R(M)";
   23.59 -by (rtac (major RS Term_induct) 1);
   23.60 -by (etac list.induct 1);
   23.61 -by (REPEAT (ares_tac prems 1));
   23.62 -qed "Term_induct2";
   23.63 -
   23.64 -(*** Structural Induction on the abstract type 'a term ***)
   23.65 -
   23.66 -val Rep_term_in_sexp =
   23.67 -    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
   23.68 -
   23.69 -(*Induction for the abstract type 'a term*)
   23.70 -val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
   23.71 -    "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts)  \
   23.72 -\    |] ==> R(t)";
   23.73 -by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
   23.74 -by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
   23.75 -by (rtac (Rep_term RS Term_induct) 1);
   23.76 -by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
   23.77 -    list_subset_sexp, range_Leaf_subset_sexp] 1
   23.78 -     ORELSE etac rev_subsetD 1));
   23.79 -by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
   23.80 -        (Abs_map_inverse RS subst) 1);
   23.81 -by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
   23.82 -by (etac Abs_term_inverse 1);
   23.83 -by (etac rangeE 1);
   23.84 -by (hyp_subst_tac 1);
   23.85 -by (resolve_tac prems 1);
   23.86 -by (etac list.induct 1);
   23.87 -by (etac CollectE 2);
   23.88 -by (stac Abs_map_CONS 2);
   23.89 -by (etac conjunct1 2);
   23.90 -by (etac rev_subsetD 2);
   23.91 -by (rtac list_subset_sexp 2);
   23.92 -by (ALLGOALS Asm_simp_tac);
   23.93 -by (ALLGOALS Fast_tac);
   23.94 -qed "term_induct";
   23.95 -
   23.96 -(*Induction for the abstract type 'a term*)
   23.97 -val prems = goal Term.thy 
   23.98 -    "[| !!x. R(App x Nil);  \
   23.99 -\       !!x t ts. R(App x ts) ==> R(App x (t#ts))  \
  23.100 -\    |] ==> R(t)";
  23.101 -by (rtac term_induct 1);  (*types force good instantiation*)
  23.102 -by (etac rev_mp 1);
  23.103 -by (rtac list_induct2 1);  (*types force good instantiation*)
  23.104 -by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
  23.105 -qed "term_induct2";
  23.106 -
  23.107 -(*Perform induction on xs. *)
  23.108 -fun term_ind2_tac a i = 
  23.109 -    EVERY [res_inst_tac [("t",a)] term_induct2 i,
  23.110 -           rename_last_tac a ["1","s"] (i+1)];
  23.111 -
  23.112 -
  23.113 -
  23.114 -(*** Term_rec -- by wf recursion on pred_sexp ***)
  23.115 -
  23.116 -goal Term.thy
  23.117 -   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
  23.118 -                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
  23.119 -by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
  23.120 -bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
  23.121 -                            ((result() RS eq_reflection) RS def_wfrec));
  23.122 -
  23.123 -(*---------------------------------------------------------------------------
  23.124 - * Old:
  23.125 - * val Term_rec_unfold =
  23.126 - *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
  23.127 - *---------------------------------------------------------------------------*)
  23.128 -
  23.129 -(** conversion rules **)
  23.130 -
  23.131 -val [prem] = goal Term.thy
  23.132 -    "N: list(term(A)) ==>  \
  23.133 -\    !M. (N,M): pred_sexp^+ --> \
  23.134 -\        Abs_map (cut h (pred_sexp^+) M) N = \
  23.135 -\        Abs_map h N";
  23.136 -by (rtac (prem RS list.induct) 1);
  23.137 -by (Simp_tac 1);
  23.138 -by (strip_tac 1);
  23.139 -by (etac (pred_sexp_CONS_D RS conjE) 1);
  23.140 -by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1);
  23.141 -qed "Abs_map_lemma";
  23.142 -
  23.143 -val [prem1,prem2,A_subset_sexp] = goal Term.thy
  23.144 -    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
  23.145 -\    Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
  23.146 -by (rtac (Term_rec_unfold RS trans) 1);
  23.147 -by (simp_tac (HOL_ss addsimps
  23.148 -      [Split,
  23.149 -       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
  23.150 -       prem1, prem2 RS rev_subsetD, list_subset_sexp,
  23.151 -       term_subset_sexp, A_subset_sexp]) 1);
  23.152 -qed "Term_rec";
  23.153 -
  23.154 -(*** term_rec -- by Term_rec ***)
  23.155 -
  23.156 -local
  23.157 -  val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
  23.158 -                        [("f","Rep_term")] Rep_map_type;
  23.159 -  val Rep_Tlist = Rep_term RS Rep_map_type1;
  23.160 -  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
  23.161 -
  23.162 -  (*Now avoids conditional rewriting with the premise N: list(term(A)),
  23.163 -    since A will be uninstantiated and will cause rewriting to fail. *)
  23.164 -  val term_rec_ss = HOL_ss
  23.165 -      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
  23.166 -                Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
  23.167 -                inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
  23.168 -in
  23.169 -
  23.170 -val term_rec = prove_goalw Term.thy
  23.171 -         [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
  23.172 -    "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"
  23.173 - (fn _ => [simp_tac term_rec_ss 1])
  23.174 -
  23.175 -end;
    24.1 --- a/src/HOL/ex/Term.thy	Wed May 07 13:50:52 1997 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,55 +0,0 @@
    24.4 -(*  Title:      HOL/ex/Term
    24.5 -    ID:         $Id$
    24.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7 -    Copyright   1992  University of Cambridge
    24.8 -
    24.9 -Terms over a given alphabet -- function applications; illustrates list functor
   24.10 -  (essentially the same type as in Trees & Forests)
   24.11 -
   24.12 -There is no constructor APP because it is simply cons ($) 
   24.13 -*)
   24.14 -
   24.15 -Term = SList +
   24.16 -
   24.17 -types   'a term
   24.18 -
   24.19 -arities term :: (term)term
   24.20 -
   24.21 -consts
   24.22 -  term          :: 'a item set => 'a item set
   24.23 -  Rep_term      :: 'a term => 'a item
   24.24 -  Abs_term      :: 'a item => 'a term
   24.25 -  Rep_Tlist     :: 'a term list => 'a item
   24.26 -  Abs_Tlist     :: 'a item => 'a term list
   24.27 -  App           :: ['a, ('a term)list] => 'a term
   24.28 -  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
   24.29 -  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
   24.30 -
   24.31 -inductive "term(A)"
   24.32 -  intrs
   24.33 -    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
   24.34 -  monos   "[list_mono]"
   24.35 -
   24.36 -defs
   24.37 -  (*defining abstraction/representation functions for term list...*)
   24.38 -  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
   24.39 -  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
   24.40 -
   24.41 -  (*defining the abstract constants*)
   24.42 -  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
   24.43 -
   24.44 -  (*list recursion*)
   24.45 -  Term_rec_def  
   24.46 -   "Term_rec M d == wfrec (trancl pred_sexp)
   24.47 -           (%g. Split(%x y. d x y (Abs_map g y))) M"
   24.48 -
   24.49 -  term_rec_def
   24.50 -   "term_rec t d == 
   24.51 -   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
   24.52 -
   24.53 -rules
   24.54 -    (*faking a type definition for term...*)
   24.55 -  Rep_term              "Rep_term(n): term(range(Leaf))"
   24.56 -  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
   24.57 -  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
   24.58 -end