--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Acc.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,63 @@
+(* Title: HOL/ex/Acc
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Inductive definition of acc(r)
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon. Dec 1992.
+*)
+
+open Acc;
+
+(*The intended introduction rule*)
+val prems = goal Acc.thy
+ "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
+by (fast_tac (!claset addIs (prems @
+ map (rewrite_rule [pred_def]) acc.intrs)) 1);
+qed "accI";
+
+goal Acc.thy "!!a b r. [| b: acc(r); (a,b): r |] ==> a: acc(r)";
+by (etac acc.elim 1);
+by (rewtac pred_def);
+by (Fast_tac 1);
+qed "acc_downward";
+
+val [major,indhyp] = goal Acc.thy
+ "[| a : acc(r); \
+\ !!x. [| x: acc(r); ALL y. (y,x):r --> P(y) |] ==> P(x) \
+\ |] ==> P(a)";
+by (rtac (major RS acc.induct) 1);
+by (rtac indhyp 1);
+by (resolve_tac acc.intrs 1);
+by (rewtac pred_def);
+by (Fast_tac 2);
+by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
+qed "acc_induct";
+
+
+val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
+by (rtac (major RS wfI) 1);
+by (etac acc.induct 1);
+by (rewtac pred_def);
+by (Fast_tac 1);
+qed "acc_wfI";
+
+val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
+by (rtac (major RS wf_induct) 1);
+by (rtac (impI RS allI) 1);
+by (rtac accI 1);
+by (Fast_tac 1);
+qed "acc_wfD_lemma";
+
+val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
+by (rtac subsetI 1);
+by (res_inst_tac [("p", "x")] PairE 1);
+by (fast_tac (!claset addSIs [SigmaI,
+ major RS acc_wfD_lemma RS spec RS mp]) 1);
+qed "acc_wfD";
+
+goal Acc.thy "wf(r) = (r <= (acc r) Times (acc r))";
+by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
+qed "wf_acc_iff";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Acc.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,26 @@
+(* Title: HOL/ex/Acc.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Inductive definition of acc(r)
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon. Dec 1992.
+*)
+
+Acc = WF +
+
+constdefs
+ pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
+ "pred x r == {y. (y,x):r}"
+
+consts
+ acc :: "('a * 'a)set => 'a set" (*Accessible part*)
+
+inductive "acc(r)"
+ intrs
+ pred "pred a r: Pow(acc(r)) ==> a: acc(r)"
+ monos "[Pow_mono]"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Com.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,43 @@
+(* Title: HOL/Induct/Com
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Commands
+*)
+
+open Com;
+
+AddIs exec.intrs;
+
+val exec_elim_cases = map (exec.mk_cases exp.simps)
+ ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
+ "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
+
+val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
+
+AddSEs exec_elim_cases;
+
+(*This theorem justifies using "exec" in the inductive definition of "eval"*)
+goalw thy exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "exec_mono";
+
+
+Unify.trace_bound := 30;
+Unify.search_bound := 60;
+
+(*Command execution is functional (deterministic) provided evaluation is*)
+goal thy "!!x. Function ev ==> Function(exec ev)";
+by (simp_tac (!simpset addsimps [Function_def, Unique_def]) 1);
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (etac exec.induct 1);
+by (Blast_tac 3);
+by (Blast_tac 1);
+by (rewrite_goals_tac [Function_def, Unique_def]);
+(*Takes ONE MINUTE due to slow proof reconstruction*)
+by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case])));
+qed "Function_exec";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Com.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,69 @@
+(* Title: HOL/Induct/Com
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Commands
+*)
+
+Com = Arith +
+
+types loc
+ state = "loc => nat"
+ n2n2n = "nat => nat => nat"
+
+arities loc :: term
+
+(*To avoid a mutually recursive datatype declaration, expressions and commands
+ are combined to form a single datatype.*)
+datatype
+ exp = N nat
+ | X loc
+ | Op n2n2n exp exp
+ | valOf exp exp ("VALOF _ RESULTIS _" 60)
+ | SKIP
+ | ":=" loc exp (infixl 60)
+ | Semi exp exp ("_;;_" [60, 60] 10)
+ | Cond exp exp exp ("IF _ THEN _ ELSE _" 60)
+ | While exp exp ("WHILE _ DO _" 60)
+
+(** Execution of commands **)
+consts exec :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
+ "@exec" :: "((exp*state) * (nat*state)) set =>
+ [exp*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
+
+translations "csig -[eval]-> s" == "(csig,s) : exec eval"
+
+constdefs assign :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95)
+ "s[m/x] == (%y. if y=x then m else s y)"
+
+
+(*Command execution. Natural numbers represent Booleans: 0=True, 1=False*)
+inductive "exec eval"
+ intrs
+ Skip "(SKIP,s) -[eval]-> s"
+
+ Assign "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
+
+ Semi "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
+ ==> (c0 ;; c1, s) -[eval]-> s1"
+
+ IfTrue "[| ((e,s), (0,s')) : eval; (c0,s') -[eval]-> s1 |]
+ ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+ IfFalse "[| ((e,s), (1,s')) : eval; (c1,s') -[eval]-> s1 |]
+ ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+ WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
+
+ WhileTrue "[| ((e,s), (0,s1)) : eval;
+ (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
+ ==> (WHILE e DO c, s) -[eval]-> s3"
+
+constdefs
+ Unique :: "['a, 'b, ('a*'b) set] => bool"
+ "Unique x y r == ALL y'. (x,y'): r --> y = y'"
+
+ Function :: "('a*'b) set => bool"
+ "Function r == ALL x y. (x,y): r --> Unique x y r"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Comb.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,179 @@
+(* Title: HOL/ex/comb.ML
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1996 University of Cambridge
+
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+ J. Camilleri and T. F. Melham.
+ Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+ Report 265, University of Cambridge Computer Laboratory, 1992.
+
+HOL system proofs may be found in
+/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
+*)
+
+open Comb;
+
+(*** Reflexive/Transitive closure preserves the Church-Rosser property
+ So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
+***)
+
+val [_, spec_mp] = [spec] RL [mp];
+
+(*Strip lemma. The induction hyp is all but the last diamond of the strip.*)
+goalw Comb.thy [diamond_def]
+ "!!r. [| diamond(r); (x,y):r^* |] ==> \
+\ ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
+by (etac rtrancl_induct 1);
+by (Blast_tac 1);
+by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
+ addSDs [spec_mp]) 1);
+val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
+
+val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
+by (rewtac diamond_def); (*unfold only in goal, not in premise!*)
+by (rtac (impI RS allI RS allI) 1);
+by (etac rtrancl_induct 1);
+by (Blast_tac 1);
+by (slow_best_tac (*Seems to be a brittle, undirected search*)
+ (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
+ addEs [major RS diamond_strip_lemmaE]) 1);
+qed "diamond_rtrancl";
+
+
+(*** Results about Contraction ***)
+
+(*Derive a case for each combinator constructor*)
+val K_contractE = contract.mk_cases comb.simps "K -1-> z";
+val S_contractE = contract.mk_cases comb.simps "S -1-> z";
+val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
+
+AddSIs [contract.K, contract.S];
+AddIs [contract.Ap1, contract.Ap2];
+AddSEs [K_contractE, S_contractE, Ap_contractE];
+Unsafe_Addss (!simpset);
+
+goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
+by (Blast_tac 1);
+qed "I_contract_E";
+AddSEs [I_contract_E];
+
+goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
+by (Blast_tac 1);
+qed "K1_contractD";
+AddSEs [K1_contractD];
+
+goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
+by (etac rtrancl_induct 1);
+by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
+qed "Ap_reduce1";
+
+goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
+by (etac rtrancl_induct 1);
+by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
+qed "Ap_reduce2";
+
+(** Counterexample to the diamond property for -1-> **)
+
+goal Comb.thy "K#I#(I#I) -1-> I";
+by (rtac contract.K 1);
+qed "KIII_contract1";
+
+goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
+by (Blast_tac 1);
+qed "KIII_contract2";
+
+goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
+by (Blast_tac 1);
+qed "KIII_contract3";
+
+goalw Comb.thy [diamond_def] "~ diamond(contract)";
+by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
+qed "not_diamond_contract";
+
+
+
+(*** Results about Parallel Contraction ***)
+
+(*Derive a case for each combinator constructor*)
+val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
+val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
+val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
+
+AddIs parcontract.intrs;
+AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
+Unsafe_Addss (!simpset);
+
+(*** Basic properties of parallel contraction ***)
+
+goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
+by (Blast_tac 1);
+qed "K1_parcontractD";
+AddSDs [K1_parcontractD];
+
+goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
+by (Blast_tac 1);
+qed "S1_parcontractD";
+AddSDs [S1_parcontractD];
+
+goal Comb.thy
+ "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
+by (Blast_tac 1);
+qed "S2_parcontractD";
+AddSDs [S2_parcontractD];
+
+(*The rules above are not essential but make proofs much faster*)
+
+
+(*Church-Rosser property for parallel contraction*)
+goalw Comb.thy [diamond_def] "diamond parcontract";
+by (rtac (impI RS allI RS allI) 1);
+by (etac parcontract.induct 1 THEN prune_params_tac);
+by (Step_tac 1);
+by (ALLGOALS Blast_tac);
+qed "diamond_parcontract";
+
+
+(*** Equivalence of x--->y and x===>y ***)
+
+goal Comb.thy "contract <= parcontract";
+by (rtac subsetI 1);
+by (split_all_tac 1);
+by (etac contract.induct 1);
+by (ALLGOALS Blast_tac);
+qed "contract_subset_parcontract";
+
+(*Reductions: simply throw together reflexivity, transitivity and
+ the one-step reductions*)
+
+AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
+
+(*Example only: not used*)
+goalw Comb.thy [I_def] "I#x ---> x";
+by (Blast_tac 1);
+qed "reduce_I";
+
+goal Comb.thy "parcontract <= contract^*";
+by (rtac subsetI 1);
+by (split_all_tac 1);
+by (etac parcontract.induct 1 THEN prune_params_tac);
+by (ALLGOALS Blast_tac);
+qed "parcontract_subset_reduce";
+
+goal Comb.thy "contract^* = parcontract^*";
+by (REPEAT
+ (resolve_tac [equalityI,
+ contract_subset_parcontract RS rtrancl_mono,
+ parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
+qed "reduce_eq_parreduce";
+
+goal Comb.thy "diamond(contract^*)";
+by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl,
+ diamond_parcontract]) 1);
+qed "diamond_reduce";
+
+
+writeln"Reached end of file.";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Comb.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,74 @@
+(* Title: HOL/ex/Comb.thy
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1996 University of Cambridge
+
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+ J. Camilleri and T. F. Melham.
+ Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+ Report 265, University of Cambridge Computer Laboratory, 1992.
+*)
+
+
+Comb = Trancl +
+
+(** Datatype definition of combinators S and K, with infixed application **)
+datatype comb = K
+ | S
+ | "#" comb comb (infixl 90)
+
+(** Inductive definition of contractions, -1->
+ and (multi-step) reductions, --->
+**)
+consts
+ contract :: "(comb*comb) set"
+ "-1->" :: [comb,comb] => bool (infixl 50)
+ "--->" :: [comb,comb] => bool (infixl 50)
+
+translations
+ "x -1-> y" == "(x,y) : contract"
+ "x ---> y" == "(x,y) : contract^*"
+
+inductive contract
+ intrs
+ K "K#x#y -1-> x"
+ S "S#x#y#z -1-> (x#z)#(y#z)"
+ Ap1 "x-1->y ==> x#z -1-> y#z"
+ Ap2 "x-1->y ==> z#x -1-> z#y"
+
+
+(** Inductive definition of parallel contractions, =1=>
+ and (multi-step) parallel reductions, ===>
+**)
+consts
+ parcontract :: "(comb*comb) set"
+ "=1=>" :: [comb,comb] => bool (infixl 50)
+ "===>" :: [comb,comb] => bool (infixl 50)
+
+translations
+ "x =1=> y" == "(x,y) : parcontract"
+ "x ===> y" == "(x,y) : parcontract^*"
+
+inductive parcontract
+ intrs
+ refl "x =1=> x"
+ K "K#x#y =1=> x"
+ S "S#x#y#z =1=> (x#z)#(y#z)"
+ Ap "[| x=1=>y; z=1=>w |] ==> x#z =1=> y#w"
+
+
+(*Misc definitions*)
+constdefs
+ I :: comb
+ "I == S#K#K"
+
+ (*confluence; Lambda/Commutation treats this more abstractly*)
+ diamond :: "('a * 'a)set => bool"
+ "diamond(r) == ALL x y. (x,y):r -->
+ (ALL y'. (x,y'):r -->
+ (EX z. (y,z):r & (y',z) : r))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Exp.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,86 @@
+(* Title: HOL/Induct/Exp
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
+*)
+
+open Exp;
+
+val eval_elim_cases = map (eval.mk_cases exp.simps)
+ ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
+ "(Op f a1 a2,sigma) -|-> (n,s')",
+ "(VALOF c RESULTIS e, s) -|-> (n, s1)"
+ ];
+
+AddSEs eval_elim_cases;
+
+
+(** Make the induction rule look nicer -- though eta_contract makes the new
+ version look worse than it is...**)
+
+goal thy "{((e,s),(n,s')). P e s n s'} = \
+\ Collect (split (%v. split (split P v)))";
+by (rtac Collect_cong 1);
+by (split_all_tac 1);
+by (Simp_tac 1);
+val split_lemma = result();
+
+(*New induction rule. Note the form of the VALOF induction hypothesis*)
+val major::prems = goal thy
+ "[| (e,s) -|-> (n,s'); \
+\ !!n s. P (N n) s n s; \
+\ !!s x. P (X x) s (s x) s; \
+\ !!e0 e1 f n0 n1 s s0 s1. \
+\ [| (e0,s) -|-> (n0,s0); P e0 s n0 s0; \
+\ (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1 \
+\ |] ==> P (Op f e0 e1) s (f n0 n1) s1; \
+\ !!c e n s s0 s1. \
+\ [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
+\ (e,s0) -|-> (n,s1); P e s0 n s1 |] \
+\ ==> P (VALOF c RESULTIS e) s n s1 \
+\ |] ==> P e s n s'";
+by (rtac (major RS eval.induct) 1);
+by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
+by (blast_tac (!claset addIs prems) 1);
+by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1);
+qed "eval_induct";
+
+
+(*Lemma for Function_eval. The major premise is that (c,s) executes to s1
+ using eval restricted to its functional part. Note that the execution
+ (c,s) -[eval]-> s2 can use unrestricted eval! The reason is that
+ the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
+ functional on the argument (c,s).
+*)
+goal thy
+ "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
+\ ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
+by (etac exec.induct 1);
+by (ALLGOALS Full_simp_tac);
+by (Blast_tac 3);
+by (Blast_tac 1);
+by (rewtac Unique_def);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
+by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
+by (Step_tac 1);
+by (etac exec_WHILE_case 1);
+by (ALLGOALS Fast_tac); (*Blast_tac: proof fails*)
+qed "com_Unique";
+
+
+(*Expression evaluation is functional, or deterministic*)
+goal thy "Function eval";
+by (simp_tac (!simpset addsimps [Function_def]) 1);
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (etac eval_induct 1);
+by (dtac com_Unique 4);
+by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def])));
+by (ALLGOALS Blast_tac);
+qed "Function_eval";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Exp.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,33 @@
+(* Title: HOL/Induct/Exp
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
+*)
+
+Exp = Com +
+
+(** Evaluation of arithmetic expressions **)
+consts eval :: "((exp*state) * (nat*state)) set"
+ "-|->" :: "[exp*state,nat*state] => bool" (infixl 50)
+translations
+ "esig -|-> (n,s)" <= "(esig,n,s) : eval"
+ "esig -|-> ns" == "(esig,ns) : eval"
+
+inductive eval
+ intrs
+ N "(N(n),s) -|-> (n,s)"
+
+ X "(X(x),s) -|-> (s(x),s)"
+
+ Op "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |]
+ ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
+
+ valOf "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |]
+ ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
+
+ monos "[exec_mono]"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/LFilter.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,341 @@
+(* Title: HOL/ex/LFilter
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+The "filter" functional for coinductive lists
+ --defined by a combination of induction and coinduction
+*)
+
+open LFilter;
+
+
+(*** findRel: basic laws ****)
+
+val findRel_LConsE =
+ findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
+
+AddSEs [findRel_LConsE];
+
+
+goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
+by (etac findRel.induct 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "findRel_functional";
+
+goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
+by (etac findRel.induct 1);
+by (Blast_tac 1);
+by (Blast_tac 1);
+qed_spec_mp "findRel_imp_LCons";
+
+goal thy "!!p. (LNil,l): findRel p ==> R";
+by (blast_tac (!claset addEs [findRel.elim]) 1);
+qed "findRel_LNil";
+
+AddSEs [findRel_LNil];
+
+
+(*** Properties of Domain (findRel p) ***)
+
+goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
+by (case_tac "p x" 1);
+by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+qed "LCons_Domain_findRel";
+
+Addsimps [LCons_Domain_findRel];
+
+val major::prems =
+goal thy "[| l: Domain (findRel p); \
+\ !!x l'. [| (l, LCons x l') : findRel p; p x |] ==> Q \
+\ |] ==> Q";
+by (rtac (major RS DomainE) 1);
+by (forward_tac [findRel_imp_LCons] 1);
+by (REPEAT (eresolve_tac [exE,conjE] 1));
+by (hyp_subst_tac 1);
+by (REPEAT (ares_tac prems 1));
+qed "Domain_findRelE";
+
+val prems = goal thy
+ "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
+by (Step_tac 1);
+by (etac findRel.induct 1);
+by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
+by (blast_tac (!claset addIs findRel.intrs) 1);
+qed "Domain_findRel_mono";
+
+
+(*** find: basic equations ***)
+
+goalw thy [find_def] "find p LNil = LNil";
+by (blast_tac (!claset addIs [select_equality]) 1);
+qed "find_LNil";
+
+goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
+by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
+qed "findRel_imp_find";
+
+goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
+by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
+qed "find_LCons_found";
+
+goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
+by (blast_tac (!claset addIs [select_equality]) 1);
+qed "diverge_find_LNil";
+
+Addsimps [diverge_find_LNil];
+
+goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
+by (case_tac "LCons x l : Domain(findRel p)" 1);
+by (Asm_full_simp_tac 2);
+by (Step_tac 1);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
+by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
+qed "find_LCons_seek";
+
+goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
+by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
+ setloop split_tac[expand_if]) 1);
+qed "find_LCons";
+
+
+
+(*** lfilter: basic equations ***)
+
+goal thy "lfilter p LNil = LNil";
+by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
+by (simp_tac (!simpset addsimps [find_LNil]) 1);
+qed "lfilter_LNil";
+
+goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
+by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
+by (Asm_simp_tac 1);
+qed "diverge_lfilter_LNil";
+
+
+goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
+by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
+by (asm_simp_tac (!simpset addsimps [find_LCons_found]) 1);
+qed "lfilter_LCons_found";
+
+
+goal thy "!!p. (l, LCons x l') : findRel p \
+\ ==> lfilter p l = LCons x (lfilter p l')";
+by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
+qed "findRel_imp_lfilter";
+
+goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
+by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
+by (case_tac "LCons x l : Domain(findRel p)" 1);
+by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
+by (etac Domain_findRelE 1);
+by (safe_tac (!claset delrules [conjI]));
+by (asm_full_simp_tac
+ (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
+ find_LCons_seek]) 1);
+qed "lfilter_LCons_seek";
+
+
+goal thy "lfilter p (LCons x l) = \
+\ (if p x then LCons x (lfilter p l) else lfilter p l)";
+by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
+ setloop split_tac[expand_if]) 1);
+qed "lfilter_LCons";
+
+AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
+Addsimps [lfilter_LNil, lfilter_LCons];
+
+
+goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
+by (rtac notI 1);
+by (etac Domain_findRelE 1);
+by (etac rev_mp 1);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
+qed "lfilter_eq_LNil";
+
+
+goal thy "!!p. lfilter p l = LCons x l' --> \
+\ (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
+by (stac (lfilter_def RS def_llist_corec) 1);
+by (case_tac "l : Domain(findRel p)" 1);
+by (etac Domain_findRelE 1);
+by (Asm_simp_tac 2);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
+by (Blast_tac 1);
+qed_spec_mp "lfilter_eq_LCons";
+
+
+goal thy "lfilter p l = LNil | \
+\ (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
+by (case_tac "l : Domain(findRel p)" 1);
+by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
+by (blast_tac (!claset addSEs [Domain_findRelE]
+ addIs [findRel_imp_lfilter]) 1);
+qed "lfilter_cases";
+
+
+(*** lfilter: simple facts by coinduction ***)
+
+goal thy "lfilter (%x.True) l = l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS Simp_tac);
+by (Blast_tac 1);
+qed "lfilter_K_True";
+
+goal thy "lfilter p (lfilter p l) = lfilter p l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (Step_tac 1);
+(*Cases: p x is true or false*)
+by (Blast_tac 1);
+by (rtac (lfilter_cases RS disjE) 1);
+by (etac ssubst 1);
+by (Auto_tac());
+qed "lfilter_idem";
+
+
+(*** Numerous lemmas required to prove lfilter_conj:
+ lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
+ ***)
+
+goal thy "!!p. (l,l') : findRel q \
+\ ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
+by (etac findRel.induct 1);
+by (blast_tac (!claset addIs findRel.intrs) 1);
+by (blast_tac (!claset addIs findRel.intrs) 1);
+qed_spec_mp "findRel_conj_lemma";
+
+val findRel_conj = refl RSN (2, findRel_conj_lemma);
+
+goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
+\ ==> (l, LCons x l') : findRel q --> ~ p x \
+\ --> l' : Domain (findRel (%x. p x & q x))";
+by (etac findRel.induct 1);
+by (Auto_tac());
+qed_spec_mp "findRel_not_conj_Domain";
+
+
+goal thy "!!p. (l,lxx) : findRel q ==> \
+\ lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
+\ --> (l,lz) : findRel (%x. p x & q x)";
+by (etac findRel.induct 1);
+by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+qed_spec_mp "findRel_conj2";
+
+
+goal thy "!!p. (lx,ly) : findRel p \
+\ ==> ALL l. lx = lfilter q l \
+\ --> l : Domain (findRel(%x. p x & q x))";
+by (etac findRel.induct 1);
+by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
+ addIs [findRel_conj]) 1);
+by (Auto_tac());
+by (dtac (sym RS lfilter_eq_LCons) 1);
+by (Auto_tac());
+by (dtac spec 1);
+by (dtac (refl RS rev_mp) 1);
+by (blast_tac (!claset addIs [findRel_conj2]) 1);
+qed_spec_mp "findRel_lfilter_Domain_conj";
+
+
+goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
+\ ==> l'' = LCons y l' --> \
+\ (lfilter q l, LCons y (lfilter q l')) : findRel p";
+by (etac findRel.induct 1);
+by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
+by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+qed_spec_mp "findRel_conj_lfilter";
+
+
+
+goal thy "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l) \
+\ : llistD_Fun (range \
+\ (%u. (lfilter p (lfilter q u), \
+\ lfilter (%x. p x & q x) u)))";
+by (case_tac "l : Domain(findRel q)" 1);
+by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
+by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
+(*There are no qs in l: both lists are LNil*)
+by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
+by (etac Domain_findRelE 1);
+(*case q x*)
+by (case_tac "p x" 1);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
+ findRel_conj RS findRel_imp_lfilter]) 1);
+by (Blast_tac 1);
+(*case q x and ~(p x) *)
+by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
+by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
+(*subcase: there is no p&q in l' and therefore none in l*)
+by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
+by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
+by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
+by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
+(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*)
+by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
+(*subcase: there is a p&q in l' and therefore also one in l*)
+by (etac Domain_findRelE 1);
+by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
+by (blast_tac (!claset addIs [findRel_conj2]) 2);
+by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
+by (blast_tac (!claset addIs [findRel_conj_lfilter]) 2);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
+by (Blast_tac 1);
+val lemma = result();
+
+
+goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
+qed "lfilter_conj";
+
+
+(*** Numerous lemmas required to prove ??:
+ lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
+ ***)
+
+goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
+by (etac findRel.induct 1);
+by (ALLGOALS Asm_full_simp_tac);
+qed "findRel_lmap_Domain";
+
+
+goal thy "!!p. lmap f l = LCons x l' --> \
+\ (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
+by (stac (lmap_def RS def_llist_corec) 1);
+by (res_inst_tac [("l", "l")] llistE 1);
+by (Auto_tac());
+qed_spec_mp "lmap_eq_LCons";
+
+
+goal thy "!!p. (lx,ly) : findRel p ==> \
+\ ALL l. lmap f l = lx --> ly = LCons x l' --> \
+\ (EX y l''. x = f y & l' = lmap f l'' & \
+\ (l, LCons y l'') : findRel(%x. p(f x)))";
+by (etac findRel.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (safe_tac (!claset addSDs [lmap_eq_LCons]));
+by (blast_tac (!claset addIs findRel.intrs) 1);
+by (blast_tac (!claset addIs findRel.intrs) 1);
+qed_spec_mp "lmap_LCons_findRel_lemma";
+
+val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
+
+goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
+by (Step_tac 1);
+by (Blast_tac 1);
+by (case_tac "lmap f l : Domain (findRel p)" 1);
+by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
+by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
+by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
+by (etac Domain_findRelE 1);
+by (forward_tac [lmap_LCons_findRel] 1);
+by (Step_tac 1);
+by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
+by (Blast_tac 1);
+qed "lfilter_lmap";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/LFilter.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,29 @@
+(* Title: HOL/LList.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+The "filter" functional for coinductive lists
+ --defined by a combination of induction and coinduction
+*)
+
+LFilter = LList + Relation +
+
+consts
+ findRel :: "('a => bool) => ('a llist * 'a llist)set"
+
+inductive "findRel p"
+ intrs
+ found "p x ==> (LCons x l, LCons x l) : findRel p"
+ seek "[| ~p x; (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
+
+constdefs
+ find :: ['a => bool, 'a llist] => 'a llist
+ "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
+
+ lfilter :: ['a => bool, 'a llist] => 'a llist
+ "lfilter p l == llist_corec l (%l. case find p l of
+ LNil => Inl ()
+ | LCons y z => Inr(y,z))"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/LList.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,886 @@
+(* Title: HOL/ex/LList
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
+*)
+
+open LList;
+
+(** Simplification **)
+
+simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
+
+(*For adding _eqI rules to a simpset; we must remove Pair_eq because
+ it may turn an instance of reflexivity into a conjunction!*)
+fun add_eqI ss = ss addsimps [range_eqI, image_eqI]
+ delsimps [Pair_eq];
+
+
+(*This justifies using llist in other recursive type definitions*)
+goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+by (rtac gfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "llist_mono";
+
+
+goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
+let val rew = rewrite_rule [NIL_def, CONS_def] in
+by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
+ addEs [rew llist.elim]) 1)
+end;
+qed "llist_unfold";
+
+
+(*** Type checking by coinduction, using list_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+***)
+
+goalw LList.thy [list_Fun_def]
+ "!!M. [| M : X; X <= list_Fun A (X Un llist(A)) |] ==> M : llist(A)";
+by (etac llist.coinduct 1);
+by (etac (subsetD RS CollectD) 1);
+by (assume_tac 1);
+qed "llist_coinduct";
+
+goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
+by (Fast_tac 1);
+qed "list_Fun_NIL_I";
+
+goalw LList.thy [list_Fun_def,CONS_def]
+ "!!M N. [| M: A; N: X |] ==> CONS M N : list_Fun A X";
+by (Fast_tac 1);
+qed "list_Fun_CONS_I";
+
+(*Utilise the "strong" part, i.e. gfp(f)*)
+goalw LList.thy (llist.defs @ [list_Fun_def])
+ "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
+by (etac (llist.mono RS gfp_fun_UnI2) 1);
+qed "list_Fun_llist_I";
+
+(*** LList_corec satisfies the desired recurion equation ***)
+
+(*A continuity result?*)
+goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))";
+by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
+qed "CONS_UN1";
+
+(*UNUSED; obsolete?
+goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
+by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
+qed "split_UN1";
+
+goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
+by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
+qed "sum_case2_UN1";
+*)
+
+val prems = goalw LList.thy [CONS_def]
+ "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'";
+by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
+qed "CONS_mono";
+
+Addsimps [LList_corec_fun_def RS def_nat_rec_0,
+ LList_corec_fun_def RS def_nat_rec_Suc];
+
+(** The directions of the equality are proved separately **)
+
+goalw LList.thy [LList_corec_def]
+ "LList_corec a f <= sum_case (%u.NIL) \
+\ (split(%z w. CONS z (LList_corec w f))) (f a)";
+by (rtac UN1_least 1);
+by (res_inst_tac [("n","k")] natE 1);
+by (ALLGOALS (Asm_simp_tac));
+by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
+qed "LList_corec_subset1";
+
+goalw LList.thy [LList_corec_def]
+ "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
+\ LList_corec a f";
+by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
+by (safe_tac (!claset));
+by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
+qed "LList_corec_subset2";
+
+(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
+goal LList.thy
+ "LList_corec a f = sum_case (%u. NIL) \
+\ (split(%z w. CONS z (LList_corec w f))) (f a)";
+by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
+ LList_corec_subset2] 1));
+qed "LList_corec";
+
+(*definitional version of same*)
+val [rew] = goal LList.thy
+ "[| !!x. h(x) == LList_corec x f |] ==> \
+\ h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
+by (rewtac rew);
+by (rtac LList_corec 1);
+qed "def_LList_corec";
+
+(*A typical use of co-induction to show membership in the gfp.
+ Bisimulation is range(%x. LList_corec x f) *)
+goal LList.thy "LList_corec a f : llist({u.True})";
+by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (stac LList_corec 1);
+by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
+ |> add_eqI) 1);
+qed "LList_corec_type";
+
+(*Lemma for the proof of llist_corec*)
+goal LList.thy
+ "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
+\ llist(range Leaf)";
+by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (stac LList_corec 1);
+by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
+qed "LList_corec_type2";
+
+
+(**** llist equality as a gfp; the bisimulation principle ****)
+
+(*This theorem is actually used, unlike the many similar ones in ZF*)
+goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
+let val rew = rewrite_rule [NIL_def, CONS_def] in
+by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
+ addEs [rew LListD.elim]) 1)
+end;
+qed "LListD_unfold";
+
+goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
+by (res_inst_tac [("n", "k")] less_induct 1);
+by (safe_tac ((claset_of "Fun") delrules [equalityI]));
+by (etac LListD.elim 1);
+by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
+by (res_inst_tac [("n", "n")] natE 1);
+by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
+by (rename_tac "n'" 1);
+by (res_inst_tac [("n", "n'")] natE 1);
+by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
+by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
+qed "LListD_implies_ntrunc_equality";
+
+(*The domain of the LListD relation*)
+goalw LList.thy (llist.defs @ [NIL_def, CONS_def])
+ "fst``LListD(diag(A)) <= llist(A)";
+by (rtac gfp_upperbound 1);
+(*avoids unfolding LListD on the rhs*)
+by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "fst_image_LListD";
+
+(*This inclusion justifies the use of coinduction to show M=N*)
+goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
+by (rtac subsetI 1);
+by (res_inst_tac [("p","x")] PairE 1);
+by (safe_tac (!claset));
+by (rtac diag_eqI 1);
+by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS
+ ntrunc_equality) 1);
+by (assume_tac 1);
+by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
+qed "LListD_subset_diag";
+
+
+(** Coinduction, using LListD_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+ **)
+
+goalw thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
+by (REPEAT (ares_tac basic_monos 1));
+qed "LListD_Fun_mono";
+
+goalw LList.thy [LListD_Fun_def]
+ "!!M. [| M : X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M : LListD(r)";
+by (etac LListD.coinduct 1);
+by (etac (subsetD RS CollectD) 1);
+by (assume_tac 1);
+qed "LListD_coinduct";
+
+goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
+by (Fast_tac 1);
+qed "LListD_Fun_NIL_I";
+
+goalw LList.thy [LListD_Fun_def,CONS_def]
+ "!!x. [| x:A; (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
+by (Fast_tac 1);
+qed "LListD_Fun_CONS_I";
+
+(*Utilise the "strong" part, i.e. gfp(f)*)
+goalw LList.thy (LListD.defs @ [LListD_Fun_def])
+ "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
+by (etac (LListD.mono RS gfp_fun_UnI2) 1);
+qed "LListD_Fun_LListD_I";
+
+
+(*This converse inclusion helps to strengthen LList_equalityI*)
+goal LList.thy "diag(llist(A)) <= LListD(diag(A))";
+by (rtac subsetI 1);
+by (etac LListD_coinduct 1);
+by (rtac subsetI 1);
+by (etac diagE 1);
+by (etac ssubst 1);
+by (eresolve_tac [llist.elim] 1);
+by (ALLGOALS
+ (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I,
+ LListD_Fun_CONS_I])));
+qed "diag_subset_LListD";
+
+goal LList.thy "LListD(diag(A)) = diag(llist(A))";
+by (REPEAT (resolve_tac [equalityI, LListD_subset_diag,
+ diag_subset_LListD] 1));
+qed "LListD_eq_diag";
+
+goal LList.thy
+ "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
+by (rtac (LListD_eq_diag RS subst) 1);
+by (rtac LListD_Fun_LListD_I 1);
+by (asm_simp_tac (!simpset addsimps [LListD_eq_diag, diagI]) 1);
+qed "LListD_Fun_diag_I";
+
+
+(** To show two LLists are equal, exhibit a bisimulation!
+ [also admits true equality]
+ Replace "A" by some particular set, like {x.True}??? *)
+goal LList.thy
+ "!!r. [| (M,N) : r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
+\ |] ==> M=N";
+by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
+by (etac LListD_coinduct 1);
+by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
+by (safe_tac (!claset));
+qed "LList_equalityI";
+
+
+(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
+
+(*abstract proof using a bisimulation*)
+val [prem1,prem2] = goal LList.thy
+ "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \
+\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+\ ==> h1=h2";
+by (rtac ext 1);
+(*next step avoids an unknown (and flexflex pair) in simplification*)
+by (res_inst_tac [("A", "{u.True}"),
+ ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (stac prem1 1);
+by (stac prem2 1);
+by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
+ CollectI RS LListD_Fun_CONS_I]
+ |> add_eqI) 1);
+qed "LList_corec_unique";
+
+val [prem] = goal LList.thy
+ "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
+\ ==> h = (%x.LList_corec x f)";
+by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
+qed "equals_LList_corec";
+
+
+(** Obsolete LList_corec_unique proof: complete induction, not coinduction **)
+
+goalw LList.thy [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
+by (rtac ntrunc_one_In1 1);
+qed "ntrunc_one_CONS";
+
+goalw LList.thy [CONS_def]
+ "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
+by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1);
+qed "ntrunc_CONS";
+
+val [prem1,prem2] = goal LList.thy
+ "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x); \
+\ !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+\ ==> h1=h2";
+by (rtac (ntrunc_equality RS ext) 1);
+by (rename_tac "x k" 1);
+by (res_inst_tac [("x", "x")] spec 1);
+by (res_inst_tac [("n", "k")] less_induct 1);
+by (rename_tac "n" 1);
+by (rtac allI 1);
+by (rename_tac "y" 1);
+by (stac prem1 1);
+by (stac prem2 1);
+by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
+by (strip_tac 1);
+by (res_inst_tac [("n", "n")] natE 1);
+by (rename_tac "m" 2);
+by (res_inst_tac [("n", "m")] natE 2);
+by (ALLGOALS(asm_simp_tac(!simpset addsimps
+ [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
+result();
+
+
+(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
+
+goal LList.thy "mono(CONS(M))";
+by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1));
+qed "Lconst_fun_mono";
+
+(* Lconst(M) = CONS M (Lconst M) *)
+bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski)));
+
+(*A typical use of co-induction to show membership in the gfp.
+ The containing set is simply the singleton {Lconst(M)}. *)
+goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
+by (rtac (singletonI RS llist_coinduct) 1);
+by (safe_tac (!claset));
+by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
+by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
+qed "Lconst_type";
+
+goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
+by (rtac (equals_LList_corec RS fun_cong) 1);
+by (Simp_tac 1);
+by (rtac Lconst 1);
+qed "Lconst_eq_LList_corec";
+
+(*Thus we could have used gfp in the definition of Lconst*)
+goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
+by (rtac (equals_LList_corec RS fun_cong) 1);
+by (Simp_tac 1);
+by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
+qed "gfp_Lconst_eq_LList_corec";
+
+
+(*** Isomorphisms ***)
+
+goal LList.thy "inj(Rep_llist)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_llist_inverse 1);
+qed "inj_Rep_llist";
+
+goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_llist_inverse 1);
+qed "inj_onto_Abs_llist";
+
+(** Distinctness of constructors **)
+
+goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
+by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
+qed "LCons_not_LNil";
+
+bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
+
+AddIffs [LCons_not_LNil, LNil_not_LCons];
+
+
+(** llist constructors **)
+
+goalw LList.thy [LNil_def]
+ "Rep_llist(LNil) = NIL";
+by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
+qed "Rep_llist_LNil";
+
+goalw LList.thy [LCons_def]
+ "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
+by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
+ rangeI, Rep_llist] 1));
+qed "Rep_llist_LCons";
+
+(** Injectiveness of CONS and LCons **)
+
+goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
+qed "CONS_CONS_eq2";
+
+bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
+
+
+(*For reasoning about abstract llist constructors*)
+
+AddIs ([Rep_llist]@llist.intrs);
+AddSDs [inj_onto_Abs_llist RS inj_ontoD,
+ inj_Rep_llist RS injD, Leaf_inject];
+
+goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
+by (Fast_tac 1);
+qed "LCons_LCons_eq";
+
+AddIffs [LCons_LCons_eq];
+
+val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
+by (rtac (major RS llist.elim) 1);
+by (etac CONS_neq_NIL 1);
+by (Fast_tac 1);
+qed "CONS_D2";
+
+
+(****** Reasoning about llist(A) ******)
+
+Addsimps [List_case_NIL, List_case_CONS];
+
+(*A special case of list_equality for functions over lazy lists*)
+val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
+ "[| M: llist(A); g(NIL): llist(A); \
+\ f(NIL)=g(NIL); \
+\ !!x l. [| x:A; l: llist(A) |] ==> \
+\ (f(CONS x l),g(CONS x l)) : \
+\ LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un \
+\ diag(llist(A))) \
+\ |] ==> f(M) = g(M)";
+by (rtac LList_equalityI 1);
+by (rtac (Mlist RS imageI) 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
+by (etac ssubst 1);
+by (etac llist.elim 1);
+by (etac ssubst 1);
+by (stac NILcase 1);
+by (rtac (gMlist RS LListD_Fun_diag_I) 1);
+by (etac ssubst 1);
+by (REPEAT (ares_tac [CONScase] 1));
+qed "LList_fun_equalityI";
+
+
+(*** The functional "Lmap" ***)
+
+goal LList.thy "Lmap f NIL = NIL";
+by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
+by (Simp_tac 1);
+qed "Lmap_NIL";
+
+goal LList.thy "Lmap f (CONS M N) = CONS (f M) (Lmap f N)";
+by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
+by (Simp_tac 1);
+qed "Lmap_CONS";
+
+(*Another type-checking proof by coinduction*)
+val [major,minor] = goal LList.thy
+ "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
+by (rtac (major RS imageI RS llist_coinduct) 1);
+by (safe_tac (!claset));
+by (etac llist.elim 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
+by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I,
+ minor, imageI, UnI1] 1));
+qed "Lmap_type";
+
+(*This type checking rule synthesises a sufficiently large set for f*)
+val [major] = goal LList.thy "M: llist(A) ==> Lmap f M: llist(f``A)";
+by (rtac (major RS Lmap_type) 1);
+by (etac imageI 1);
+qed "Lmap_type2";
+
+(** Two easy results about Lmap **)
+
+val [prem] = goalw LList.thy [o_def]
+ "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
+by (rtac (prem RS imageI RS LList_equalityI) 1);
+by (safe_tac (!claset));
+by (etac llist.elim 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
+by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
+ rangeI RS LListD_Fun_CONS_I] 1));
+qed "Lmap_compose";
+
+val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
+by (rtac (prem RS imageI RS LList_equalityI) 1);
+by (safe_tac (!claset));
+by (etac llist.elim 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
+by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
+ rangeI RS LListD_Fun_CONS_I] 1));
+qed "Lmap_ident";
+
+
+(*** Lappend -- its two arguments cause some complications! ***)
+
+goalw LList.thy [Lappend_def] "Lappend NIL NIL = NIL";
+by (rtac (LList_corec RS trans) 1);
+by (Simp_tac 1);
+qed "Lappend_NIL_NIL";
+
+goalw LList.thy [Lappend_def]
+ "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')";
+by (rtac (LList_corec RS trans) 1);
+by (Simp_tac 1);
+qed "Lappend_NIL_CONS";
+
+goalw LList.thy [Lappend_def]
+ "Lappend (CONS M M') N = CONS M (Lappend M' N)";
+by (rtac (LList_corec RS trans) 1);
+by (Simp_tac 1);
+qed "Lappend_CONS";
+
+Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
+ Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
+Delsimps [Pair_eq];
+
+goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
+by (etac LList_fun_equalityI 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Lappend_NIL";
+
+goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M";
+by (etac LList_fun_equalityI 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Lappend_NIL2";
+
+(** Alternative type-checking proofs for Lappend **)
+
+(*weak co-induction: bisimulation and case analysis on both variables*)
+goal LList.thy
+ "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+by (res_inst_tac
+ [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
+by (Fast_tac 1);
+by (safe_tac (!claset));
+by (eres_inst_tac [("a", "u")] llist.elim 1);
+by (eres_inst_tac [("a", "v")] llist.elim 1);
+by (ALLGOALS
+ (Asm_simp_tac THEN'
+ fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
+qed "Lappend_type";
+
+(*strong co-induction: bisimulation and case analysis on one variable*)
+goal LList.thy
+ "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
+by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1);
+by (etac imageI 1);
+by (rtac subsetI 1);
+by (etac imageE 1);
+by (eres_inst_tac [("a", "u")] llist.elim 1);
+by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
+by (Asm_simp_tac 1);
+by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
+qed "Lappend_type";
+
+(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
+
+(** llist_case: case analysis for 'a llist **)
+
+Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
+ Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
+
+goalw LList.thy [llist_case_def,LNil_def] "llist_case c d LNil = c";
+by (Simp_tac 1);
+qed "llist_case_LNil";
+
+goalw LList.thy [llist_case_def,LCons_def]
+ "llist_case c d (LCons M N) = d M N";
+by (Simp_tac 1);
+qed "llist_case_LCons";
+
+(*Elimination is case analysis, not induction.*)
+val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
+ "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P \
+\ |] ==> P";
+by (rtac (Rep_llist RS llist.elim) 1);
+by (rtac (inj_Rep_llist RS injD RS prem1) 1);
+by (stac Rep_llist_LNil 1);
+by (assume_tac 1);
+by (etac rangeE 1);
+by (rtac (inj_Rep_llist RS injD RS prem2) 1);
+by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
+by (etac (Abs_llist_inverse RS ssubst) 1);
+by (rtac refl 1);
+qed "llistE";
+
+(** llist_corec: corecursion for 'a llist **)
+
+goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
+ "llist_corec a f = sum_case (%u. LNil) \
+\ (split(%z w. LCons z (llist_corec w f))) (f a)";
+by (stac LList_corec 1);
+by (res_inst_tac [("s","f(a)")] sumE 1);
+by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
+by (res_inst_tac [("p","y")] PairE 1);
+by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
+(*FIXME: correct case splits usd to be found automatically:
+by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*)
+qed "llist_corec";
+
+(*definitional version of same*)
+val [rew] = goal LList.thy
+ "[| !!x. h(x) == llist_corec x f |] ==> \
+\ h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
+by (rewtac rew);
+by (rtac llist_corec 1);
+qed "def_llist_corec";
+
+(**** Proofs about type 'a llist functions ****)
+
+(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
+
+goalw LList.thy [LListD_Fun_def]
+ "!!r A. r <= (llist A) Times (llist A) ==> \
+\ LListD_Fun (diag A) r <= (llist A) Times (llist A)";
+by (stac llist_unfold 1);
+by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
+by (Fast_tac 1);
+qed "LListD_Fun_subset_Sigma_llist";
+
+goal LList.thy
+ "prod_fun Rep_llist Rep_llist `` r <= \
+\ (llist(range Leaf)) Times (llist(range Leaf))";
+by (fast_tac (!claset addIs [Rep_llist]) 1);
+qed "subset_Sigma_llist";
+
+val [prem] = goal LList.thy
+ "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
+\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
+by (safe_tac (!claset));
+by (rtac (prem RS subsetD RS SigmaE2) 1);
+by (assume_tac 1);
+by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
+qed "prod_fun_lemma";
+
+goal LList.thy
+ "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
+\ diag(llist(range Leaf))";
+by (rtac equalityI 1);
+by (fast_tac (!claset addIs [Rep_llist]) 1);
+by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
+qed "prod_fun_range_eq_diag";
+
+(*Surprisingly hard to prove. Used with lfilter*)
+goalw thy [llistD_Fun_def, prod_fun_def]
+ "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
+by (Auto_tac());
+by (rtac image_eqI 1);
+by (fast_tac (!claset addss (!simpset)) 1);
+by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
+qed "llistD_Fun_mono";
+
+(** To show two llists are equal, exhibit a bisimulation!
+ [also admits true equality] **)
+val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
+ "[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
+by (rtac (inj_Rep_llist RS injD) 1);
+by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
+ ("A", "range(Leaf)")]
+ LList_equalityI 1);
+by (rtac (prem1 RS prod_fun_imageI) 1);
+by (rtac (prem2 RS image_mono RS subset_trans) 1);
+by (rtac (image_compose RS subst) 1);
+by (rtac (prod_fun_compose RS subst) 1);
+by (stac image_Un 1);
+by (stac prod_fun_range_eq_diag 1);
+by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
+by (rtac (subset_Sigma_llist RS Un_least) 1);
+by (rtac diag_subset_Sigma 1);
+qed "llist_equalityI";
+
+(** Rules to prove the 2nd premise of llist_equalityI **)
+goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
+by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
+qed "llistD_Fun_LNil_I";
+
+val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
+ "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
+by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
+by (rtac (prem RS prod_fun_imageI) 1);
+qed "llistD_Fun_LCons_I";
+
+(*Utilise the "strong" part, i.e. gfp(f)*)
+goalw LList.thy [llistD_Fun_def]
+ "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
+by (rtac (Rep_llist_inverse RS subst) 1);
+by (rtac prod_fun_imageI 1);
+by (stac image_Un 1);
+by (stac prod_fun_range_eq_diag 1);
+by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
+qed "llistD_Fun_range_I";
+
+(*A special case of list_equality for functions over lazy lists*)
+val [prem1,prem2] = goal LList.thy
+ "[| f(LNil)=g(LNil); \
+\ !!x l. (f(LCons x l),g(LCons x l)) : \
+\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \
+\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
+by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
+by (rtac rangeI 1);
+by (rtac subsetI 1);
+by (etac rangeE 1);
+by (etac ssubst 1);
+by (res_inst_tac [("l", "u")] llistE 1);
+by (etac ssubst 1);
+by (stac prem1 1);
+by (rtac llistD_Fun_range_I 1);
+by (etac ssubst 1);
+by (rtac prem2 1);
+qed "llist_fun_equalityI";
+
+(*simpset for llist bisimulations*)
+Addsimps [llist_case_LNil, llist_case_LCons,
+ llistD_Fun_LNil_I, llistD_Fun_LCons_I];
+
+
+(*** The functional "lmap" ***)
+
+goal LList.thy "lmap f LNil = LNil";
+by (rtac (lmap_def RS def_llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "lmap_LNil";
+
+goal LList.thy "lmap f (LCons M N) = LCons (f M) (lmap f N)";
+by (rtac (lmap_def RS def_llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "lmap_LCons";
+
+Addsimps [lmap_LNil, lmap_LCons];
+
+
+(** Two easy results about lmap **)
+
+goal LList.thy "lmap (f o g) l = lmap f (lmap g l)";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS Simp_tac);
+qed "lmap_compose";
+
+goal LList.thy "lmap (%x.x) l = l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS Simp_tac);
+qed "lmap_ident";
+
+
+(*** iterates -- llist_fun_equalityI cannot be used! ***)
+
+goal LList.thy "iterates f x = LCons x (iterates f (f x))";
+by (rtac (iterates_def RS def_llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "iterates";
+
+goal LList.thy "lmap f (iterates f x) = iterates f (f x)";
+by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")]
+ llist_equalityI 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
+by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
+by (Simp_tac 1);
+qed "lmap_iterates";
+
+goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))";
+by (stac lmap_iterates 1);
+by (rtac iterates 1);
+qed "iterates_lmap";
+
+(*** A rather complex proof about iterates -- cf Andy Pitts ***)
+
+(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
+
+goal LList.thy
+ "nat_rec (LCons b l) (%m. lmap(f)) n = \
+\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "fun_power_lmap";
+
+goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "fun_power_Suc";
+
+val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
+ [("f","Pair")] (standard(refl RS cong RS cong));
+
+(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
+ for all u and all n::nat.*)
+val [prem] = goal LList.thy
+ "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
+by (rtac ext 1);
+by (res_inst_tac [("r",
+ "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
+\ nat_rec (iterates f u) (%m y.lmap f y) n))")]
+ llist_equalityI 1);
+by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
+by (safe_tac (!claset));
+by (stac iterates 1);
+by (stac prem 1);
+by (stac fun_power_lmap 1);
+by (stac fun_power_lmap 1);
+by (rtac llistD_Fun_LCons_I 1);
+by (rtac (lmap_iterates RS subst) 1);
+by (stac fun_power_Suc 1);
+by (stac fun_power_Suc 1);
+by (rtac (UN1_I RS UnI1) 1);
+by (rtac rangeI 1);
+qed "iterates_equality";
+
+
+(*** lappend -- its two arguments cause some complications! ***)
+
+goalw LList.thy [lappend_def] "lappend LNil LNil = LNil";
+by (rtac (llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "lappend_LNil_LNil";
+
+goalw LList.thy [lappend_def]
+ "lappend LNil (LCons l l') = LCons l (lappend LNil l')";
+by (rtac (llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "lappend_LNil_LCons";
+
+goalw LList.thy [lappend_def]
+ "lappend (LCons l l') N = LCons l (lappend l' N)";
+by (rtac (llist_corec RS trans) 1);
+by (Simp_tac 1);
+qed "lappend_LCons";
+
+Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
+
+goal LList.thy "lappend LNil l = l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS Simp_tac);
+qed "lappend_LNil";
+
+goal LList.thy "lappend l LNil = l";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (ALLGOALS Simp_tac);
+qed "lappend_LNil2";
+
+Addsimps [lappend_LNil, lappend_LNil2];
+
+(*The infinite first argument blocks the second*)
+goal LList.thy "lappend (iterates f x) N = iterates f x";
+by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")]
+ llist_equalityI 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (stac iterates 1);
+by (Simp_tac 1);
+qed "lappend_iterates";
+
+(** Two proofs that lmap distributes over lappend **)
+
+(*Long proof requiring case analysis on both both arguments*)
+goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
+by (res_inst_tac
+ [("r",
+ "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")]
+ llist_equalityI 1);
+by (rtac UN1_I 1);
+by (rtac rangeI 1);
+by (safe_tac (!claset));
+by (res_inst_tac [("l", "l")] llistE 1);
+by (res_inst_tac [("l", "n")] llistE 1);
+by (ALLGOALS Asm_simp_tac);
+by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
+qed "lmap_lappend_distrib";
+
+(*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
+goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
+by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+qed "lmap_lappend_distrib";
+
+(*Without strong coinduction, three case analyses might be needed*)
+goal LList.thy "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
+by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+qed "lappend_assoc";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/LList.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,153 @@
+(* Title: HOL/LList.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Definition of type 'a llist by a greatest fixed point
+
+Shares NIL, CONS, List_case with List.thy
+
+Still needs filter and flatten functions -- hard because they need
+bounds on the amount of lookahead required.
+
+Could try (but would it work for the gfp analogue of term?)
+ LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
+
+A nice but complex example would be [ML for the Working Programmer, page 176]
+ from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
+
+Previous definition of llistD_Fun was explicit:
+ llistD_Fun_def
+ "llistD_Fun(r) ==
+ {(LNil,LNil)} Un
+ (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
+*)
+
+LList = Gfp + SList +
+
+types
+ 'a llist
+
+arities
+ llist :: (term)term
+
+consts
+ list_Fun :: ['a item set, 'a item set] => 'a item set
+ LListD_Fun ::
+ "[('a item * 'a item)set, ('a item * 'a item)set] =>
+ ('a item * 'a item)set"
+
+ llist :: 'a item set => 'a item set
+ LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
+ llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
+
+ Rep_llist :: 'a llist => 'a item
+ Abs_llist :: 'a item => 'a llist
+ LNil :: 'a llist
+ LCons :: ['a, 'a llist] => 'a llist
+
+ llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
+
+ LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
+ LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
+ llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
+
+ Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ lmap :: ('a=>'b) => ('a llist => 'b llist)
+
+ iterates :: ['a => 'a, 'a] => 'a llist
+
+ Lconst :: 'a item => 'a item
+ Lappend :: ['a item, 'a item] => 'a item
+ lappend :: ['a llist, 'a llist] => 'a llist
+
+
+coinductive "llist(A)"
+ intrs
+ NIL_I "NIL: llist(A)"
+ CONS_I "[| a: A; M: llist(A) |] ==> CONS a M : llist(A)"
+
+coinductive "LListD(r)"
+ intrs
+ NIL_I "(NIL, NIL) : LListD(r)"
+ CONS_I "[| (a,b): r; (M,N) : LListD(r)
+ |] ==> (CONS a M, CONS b N) : LListD(r)"
+
+translations
+ "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
+
+
+defs
+ (*Now used exclusively for abbreviating the coinduction rule*)
+ list_Fun_def "list_Fun A X ==
+ {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+
+ LListD_Fun_def "LListD_Fun r X ==
+ {z. z = (NIL, NIL) |
+ (? M N a b. z = (CONS a M, CONS b N) &
+ (a, b) : r & (M, N) : X)}"
+
+ (*defining the abstract constructors*)
+ LNil_def "LNil == Abs_llist(NIL)"
+ LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
+
+ llist_case_def
+ "llist_case c d l ==
+ List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
+
+ LList_corec_fun_def
+ "LList_corec_fun k f ==
+ nat_rec (%x. {})
+ (%j r x. case f x of Inl u => NIL
+ | Inr(z,w) => CONS z (r w))
+ k"
+
+ LList_corec_def
+ "LList_corec a f == UN k. LList_corec_fun k f a"
+
+ llist_corec_def
+ "llist_corec a f ==
+ Abs_llist(LList_corec a
+ (%z.case f z of Inl x => Inl(x)
+ | Inr(v,w) => Inr(Leaf(v), w)))"
+
+ llistD_Fun_def
+ "llistD_Fun(r) ==
+ prod_fun Abs_llist Abs_llist ``
+ LListD_Fun (diag(range Leaf))
+ (prod_fun Rep_llist Rep_llist `` r)"
+
+ Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
+
+ Lmap_def
+ "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
+
+ lmap_def
+ "lmap f l == llist_corec l (%z. case z of LNil => (Inl ())
+ | LCons y z => Inr(f(y), z))"
+
+ iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
+
+(*Append generates its result by applying f, where
+ f((NIL,NIL)) = Inl(())
+ f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
+ f((CONS M1 M2, N)) = Inr((M1, (M2,N))
+*)
+
+ Lappend_def
+ "Lappend M N == LList_corec (M,N)
+ (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2)))))
+ (%M1 M2 N. Inr((M1, (M2,N))))))"
+
+ lappend_def
+ "lappend l n == llist_corec (l,n)
+ (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2)))))
+ (%l1 l2 n. Inr((l1, (l2,n))))))"
+
+rules
+ (*faking a type definition...*)
+ Rep_llist "Rep_llist(xs): llist(range(Leaf))"
+ Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
+ Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Mutil.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,172 @@
+(* Title: HOL/ex/Mutil
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+The Mutilated Chess Board Problem, formalized inductively
+*)
+
+open Mutil;
+
+Addsimps tiling.intrs;
+
+(** The union of two disjoint tilings is a tiling **)
+
+goal thy "!!t. t: tiling A ==> \
+\ u: tiling A --> t <= Compl u --> t Un u : tiling A";
+by (etac tiling.induct 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset addsimps [Un_assoc]) 1);
+by (blast_tac (!claset addIs tiling.intrs) 1);
+qed_spec_mp "tiling_UnI";
+
+
+(*** Chess boards ***)
+
+val [below_0, below_Suc] = nat_recs below_def;
+Addsimps [below_0, below_Suc];
+
+goal thy "ALL i. (i: below k) = (i<k)";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
+by (Blast_tac 1);
+qed_spec_mp "below_less_iff";
+
+Addsimps [below_less_iff];
+
+goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "Sigma_Suc1";
+
+goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
+by (Simp_tac 1);
+by (Blast_tac 1);
+qed "Sigma_Suc2";
+
+(*Deletion is essential to allow use of Sigma_Suc1,2*)
+Delsimps [below_Suc];
+
+goal thy "{i} Times below(n + n) : tiling domino";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
+by (resolve_tac tiling.intrs 1);
+by (assume_tac 2);
+by (subgoal_tac (*seems the easiest way of turning one to the other*)
+ "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
+\ {(i, n+n), (i, Suc(n+n))}" 1);
+by (Blast_tac 2);
+by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
+by (blast_tac (!claset addEs [less_irrefl, less_asym]
+ addSDs [below_less_iff RS iffD1]) 1);
+qed "dominoes_tile_row";
+
+goal thy "(below m) Times below(n + n) : tiling domino";
+by (nat_ind_tac "m" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
+by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
+ addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
+qed "dominoes_tile_matrix";
+
+
+(*** Basic properties of evnodd ***)
+
+goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A & (i+j) mod 2 = b)";
+by (Simp_tac 1);
+qed "evnodd_iff";
+
+goalw thy [evnodd_def] "evnodd A b <= A";
+by (rtac Int_lower1 1);
+qed "evnodd_subset";
+
+(* finite X ==> finite(evnodd X b) *)
+bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
+
+goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
+by (Blast_tac 1);
+qed "evnodd_Un";
+
+goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
+by (Blast_tac 1);
+qed "evnodd_Diff";
+
+goalw thy [evnodd_def] "evnodd {} b = {}";
+by (Simp_tac 1);
+qed "evnodd_empty";
+
+goalw thy [evnodd_def]
+ "evnodd (insert (i,j) C) b = \
+\ (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
+by (asm_full_simp_tac (!simpset addsimps [evnodd_def]
+ setloop (split_tac [expand_if] THEN' Step_tac)) 1);
+qed "evnodd_insert";
+
+
+(*** Dominoes ***)
+
+goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
+by (eresolve_tac [domino.elim] 1);
+by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
+by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
+by (REPEAT_FIRST assume_tac);
+(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
+by (REPEAT (asm_full_simp_tac (!simpset addsimps
+ [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc]
+ setloop split_tac [expand_if]) 1
+ THEN Blast_tac 1));
+qed "domino_singleton";
+
+goal thy "!!d. d:domino ==> finite d";
+by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI]
+ addSEs [domino.elim]) 1);
+qed "domino_finite";
+
+
+(*** Tilings of dominoes ***)
+
+goal thy "!!t. t:tiling domino ==> finite t";
+by (eresolve_tac [tiling.induct] 1);
+by (rtac finite_emptyI 1);
+by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
+qed "tiling_domino_finite";
+
+goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
+by (eresolve_tac [tiling.induct] 1);
+by (simp_tac (!simpset addsimps [evnodd_def]) 1);
+by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
+by (Simp_tac 2 THEN assume_tac 1);
+by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
+by (Simp_tac 2 THEN assume_tac 1);
+by (Step_tac 1);
+by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
+by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left,
+ tiling_domino_finite,
+ evnodd_subset RS finite_subset,
+ card_insert_disjoint]) 1);
+by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
+qed "tiling_domino_0_1";
+
+goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n); \
+\ t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))} \
+\ |] ==> t' ~: tiling domino";
+by (rtac notI 1);
+by (dtac tiling_domino_0_1 1);
+by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "t : tiling domino" 1);
+(*Requires a small simpset that won't move the Suc applications*)
+by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
+by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
+by (asm_simp_tac (!simpset addsimps add_ac) 2);
+by (asm_full_simp_tac
+ (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty,
+ mod_less, tiling_domino_0_1 RS sym]) 1);
+by (rtac less_trans 1);
+by (REPEAT
+ (rtac card_Diff 1
+ THEN
+ asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1
+ THEN
+ asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
+qed "mutil_not_tiling";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Mutil.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,32 @@
+(* Title: HOL/ex/Mutil
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1996 University of Cambridge
+
+The Mutilated Chess Board Problem, formalized inductively
+ Originator is Max Black, according to J A Robinson.
+ Popularized as the Mutilated Checkerboard Problem by J McCarthy
+*)
+
+Mutil = Finite +
+consts
+ domino :: "(nat*nat)set set"
+ tiling :: 'a set set => 'a set set
+ below :: nat => nat set
+ evnodd :: "[(nat*nat)set, nat] => (nat*nat)set"
+
+inductive domino
+ intrs
+ horiz "{(i, j), (i, Suc j)} : domino"
+ vertl "{(i, j), (Suc i, j)} : domino"
+
+inductive "tiling A"
+ intrs
+ empty "{} : tiling A"
+ Un "[| a: A; t: tiling A; a <= Compl t |] ==> a Un t : tiling A"
+
+defs
+ below_def "below n == nat_rec {} insert n"
+ evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Perm.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,98 @@
+(* Title: HOL/ex/Perm.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+Permutations: example of an inductive definition
+*)
+
+(*It would be nice to prove
+ xs <~~> ys = (!x. count xs x = count ys x)
+See mset on HOL/ex/Sorting.thy
+*)
+
+open Perm;
+
+goal Perm.thy "l <~~> l";
+by (list.induct_tac "l" 1);
+by (REPEAT (ares_tac perm.intrs 1));
+qed "perm_refl";
+
+
+(** Some examples of rule induction on permutations **)
+
+(*The form of the premise lets the induction bind xs and ys.*)
+goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
+by (etac perm.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "perm_Nil_lemma";
+
+(*A more general version is actually easier to understand!*)
+goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
+by (etac perm.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "perm_length";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
+by (etac perm.induct 1);
+by (REPEAT (ares_tac perm.intrs 1));
+qed "perm_sym";
+
+goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
+by (etac perm.induct 1);
+by (Fast_tac 4);
+by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
+val perm_mem_lemma = result();
+
+bind_thm ("perm_mem", perm_mem_lemma RS mp);
+
+(** Ways of making new permutations **)
+
+(*We can insert the head anywhere in the list*)
+goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
+qed "perm_append_Cons";
+
+(*single steps
+by (rtac perm.trans 1);
+by (rtac perm.swap 1);
+by (rtac perm.Cons 1);
+*)
+
+goal Perm.thy "xs@ys <~~> ys@xs";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
+qed "perm_append_swap";
+
+
+goal Perm.thy "a # xs <~~> xs @ [a]";
+by (rtac perm.trans 1);
+by (rtac perm_append_swap 2);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+qed "perm_append_single";
+
+goal Perm.thy "rev xs <~~> xs";
+by (list.induct_tac "xs" 1);
+by (simp_tac (!simpset addsimps [perm_refl]) 1);
+by (Simp_tac 1);
+by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
+by (etac perm.Cons 1);
+qed "perm_rev";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
+by (list.induct_tac "l" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
+qed "perm_append1";
+
+goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
+by (rtac (perm_append_swap RS perm.trans) 1);
+by (etac (perm_append1 RS perm.trans) 1);
+by (rtac perm_append_swap 1);
+qed "perm_append2";
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Perm.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,24 @@
+(* Title: HOL/ex/Perm.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1995 University of Cambridge
+
+Permutations: example of an inductive definition
+*)
+
+Perm = List +
+
+consts perm :: "('a list * 'a list) set"
+syntax "@perm" :: ['a list, 'a list] => bool ("_ <~~> _" [50,50] 50)
+
+translations
+ "x <~~> y" == "(x,y) : perm"
+
+inductive perm
+ intrs
+ Nil "[] <~~> []"
+ swap "y#x#l <~~> x#y#l"
+ Cons "xs <~~> ys ==> z#xs <~~> z#ys"
+ trans "[| xs <~~> ys; ys <~~> zs |] ==> xs <~~> zs"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/PropLog.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,229 @@
+(* Title: HOL/ex/pl.ML
+ ID: $Id$
+ Author: Tobias Nipkow & Lawrence C Paulson
+ Copyright 1994 TU Muenchen & University of Cambridge
+
+Soundness and completeness of propositional logic w.r.t. truth-tables.
+
+Prove: If H|=p then G|=p where G:Fin(H)
+*)
+
+open PropLog;
+
+(** Monotonicity **)
+goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "thms_mono";
+
+(*Rule is called I for Identity Combinator, not for Introduction*)
+goal PropLog.thy "H |- p->p";
+by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
+qed "thms_I";
+
+(** Weakening, left and right **)
+
+(* "[| G<=H; G |- p |] ==> H |- p"
+ This order of premises is convenient with RS
+*)
+bind_thm ("weaken_left", (thms_mono RS subsetD));
+
+(* H |- p ==> insert(a,H) |- p *)
+val weaken_left_insert = subset_insertI RS weaken_left;
+
+val weaken_left_Un1 = Un_upper1 RS weaken_left;
+val weaken_left_Un2 = Un_upper2 RS weaken_left;
+
+goal PropLog.thy "!!H. H |- q ==> H |- p->q";
+by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
+qed "weaken_right";
+
+(*The deduction theorem*)
+goal PropLog.thy "!!H. insert p H |- q ==> H |- p->q";
+by (etac thms.induct 1);
+by (ALLGOALS
+ (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN,
+ thms.S RS thms.MP RS thms.MP, weaken_right])));
+qed "deduction";
+
+
+(* "[| insert p H |- q; H |- p |] ==> H |- q"
+ The cut rule - not used
+*)
+val cut = deduction RS thms.MP;
+
+(* H |- false ==> H |- p *)
+val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
+
+(* [| H |- p->false; H |- p; q: pl |] ==> H |- q *)
+bind_thm ("thms_notE", (thms.MP RS thms_falseE));
+
+(** The function eval **)
+
+goalw PropLog.thy [eval_def] "tt[false] = False";
+by (Simp_tac 1);
+qed "eval_false";
+
+goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
+by (Simp_tac 1);
+qed "eval_var";
+
+goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
+by (Simp_tac 1);
+qed "eval_imp";
+
+Addsimps [eval_false, eval_var, eval_imp];
+
+(*Soundness of the rules wrt truth-table semantics*)
+goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
+by (etac thms.induct 1);
+by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
+by (ALLGOALS Asm_simp_tac);
+qed "soundness";
+
+(*** Towards the completeness proof ***)
+
+goal PropLog.thy "!!H. H |- p->false ==> H |- p->q";
+by (rtac deduction 1);
+by (etac (weaken_left_insert RS thms_notE) 1);
+by (rtac thms.H 1);
+by (rtac insertI1 1);
+qed "false_imp";
+
+val [premp,premq] = goal PropLog.thy
+ "[| H |- p; H |- q->false |] ==> H |- (p->q)->false";
+by (rtac deduction 1);
+by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
+by (rtac (thms.H RS thms.MP) 1);
+by (rtac insertI1 1);
+by (rtac (premp RS weaken_left_insert) 1);
+qed "imp_false";
+
+(*This formulation is required for strong induction hypotheses*)
+goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
+by (rtac (expand_if RS iffD2) 1);
+by (PropLog.pl.induct_tac "p" 1);
+by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
+by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2,
+ weaken_right, imp_false]
+ addSEs [false_imp]) 1);
+qed "hyps_thms_if";
+
+(*Key lemma for completeness; yields a set of assumptions satisfying p*)
+val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
+by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
+ rtac hyps_thms_if 2);
+by (Fast_tac 1);
+qed "sat_thms_p";
+
+(*For proving certain theorems in our new propositional logic*)
+
+AddSIs [deduction];
+AddIs [thms.H, thms.H RS thms.MP];
+
+(*The excluded middle in the form of an elimination rule*)
+goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
+by (rtac (deduction RS deduction) 1);
+by (rtac (thms.DN RS thms.MP) 1);
+by (ALLGOALS (best_tac (!claset addSIs prems)));
+qed "thms_excluded_middle";
+
+(*Hard to prove directly because it requires cuts*)
+val prems = goal PropLog.thy
+ "[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q";
+by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
+by (REPEAT (resolve_tac (prems@[deduction]) 1));
+qed "thms_excluded_middle_rule";
+
+(*** Completeness -- lemmas for reducing the set of assumptions ***)
+
+(*For the case hyps(p,t)-insert(#v,Y) |- p;
+ we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
+goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
+by (PropLog.pl.induct_tac "p" 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "hyps_Diff";
+
+(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
+ we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
+goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
+by (PropLog.pl.induct_tac "p" 1);
+by (Simp_tac 1);
+by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "hyps_insert";
+
+(** Two lemmas for use with weaken_left **)
+
+goal Set.thy "B-C <= insert a (B-insert a C)";
+by (Fast_tac 1);
+qed "insert_Diff_same";
+
+goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
+by (Fast_tac 1);
+qed "insert_Diff_subset2";
+
+(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
+ could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
+goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
+by (PropLog.pl.induct_tac "p" 1);
+by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
+qed "hyps_finite";
+
+val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
+
+(*Induction on the finite set of assumptions hyps(p,t0).
+ We may repeatedly subtract assumptions until none are left!*)
+val [sat] = goal PropLog.thy
+ "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
+by (rtac (hyps_finite RS Fin_induct) 1);
+by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
+by (safe_tac (!claset));
+(*Case hyps(p,t)-insert(#v,Y) |- p *)
+by (rtac thms_excluded_middle_rule 1);
+by (rtac (insert_Diff_same RS weaken_left) 1);
+by (etac spec 1);
+by (rtac (insert_Diff_subset2 RS weaken_left) 1);
+by (rtac (hyps_Diff RS Diff_weaken_left) 1);
+by (etac spec 1);
+(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
+by (rtac thms_excluded_middle_rule 1);
+by (rtac (insert_Diff_same RS weaken_left) 2);
+by (etac spec 2);
+by (rtac (insert_Diff_subset2 RS weaken_left) 1);
+by (rtac (hyps_insert RS Diff_weaken_left) 1);
+by (etac spec 1);
+qed "completeness_0_lemma";
+
+(*The base case for completeness*)
+val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
+by (rtac (Diff_cancel RS subst) 1);
+by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
+qed "completeness_0";
+
+(*A semantic analogue of the Deduction Theorem*)
+goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
+by (Simp_tac 1);
+by (Fast_tac 1);
+qed "sat_imp";
+
+val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
+by (rtac (finite RS Fin_induct) 1);
+by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
+by (rtac (weaken_left_insert RS thms.MP) 1);
+by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
+by (Fast_tac 1);
+qed "completeness_lemma";
+
+val completeness = completeness_lemma RS spec RS mp;
+
+val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
+by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
+qed "thms_iff";
+
+writeln"Reached end of file.";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/PropLog.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,46 @@
+(* Title: HOL/ex/PropLog.thy
+ ID: $Id$
+ Author: Tobias Nipkow
+ Copyright 1994 TU Muenchen
+
+Inductive definition of propositional logic.
+*)
+
+PropLog = Finite +
+datatype
+ 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
+consts
+ thms :: 'a pl set => 'a pl set
+ "|-" :: ['a pl set, 'a pl] => bool (infixl 50)
+ "|=" :: ['a pl set, 'a pl] => bool (infixl 50)
+ eval2 :: ['a pl, 'a set] => bool
+ eval :: ['a set, 'a pl] => bool ("_[_]" [100,0] 100)
+ hyps :: ['a pl, 'a set] => 'a pl set
+
+translations
+ "H |- p" == "p : thms(H)"
+
+inductive "thms(H)"
+ intrs
+ H "p:H ==> H |- p"
+ K "H |- p->q->p"
+ S "H |- (p->q->r) -> (p->q) -> p->r"
+ DN "H |- ((p->false) -> false) -> p"
+ MP "[| H |- p->q; H |- p |] ==> H |- q"
+
+defs
+ sat_def "H |= p == (!tt. (!q:H. tt[q]) --> tt[p])"
+ eval_def "tt[p] == eval2 p tt"
+
+primrec eval2 pl
+ "eval2(false) = (%x.False)"
+ "eval2(#v) = (%tt.v:tt)"
+ "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
+
+primrec hyps pl
+ "hyps(false) = (%tt.{})"
+ "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
+ "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
+
+end
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/ROOT.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,22 @@
+(* Title: HOL/Induct/ROOT
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1997 University of Cambridge
+
+Exampled of Inductive Definitions
+*)
+
+HOL_build_completed; (*Make examples fail if HOL did*)
+
+writeln"Root file for HOL/Induct";
+proof_timing := true;
+time_use_thy "Perm";
+time_use_thy "Comb";
+time_use_thy "Mutil";
+time_use_thy "Acc";
+time_use_thy "PropLog";
+time_use_thy "SList";
+time_use_thy "LFilter";
+time_use_thy "Term";
+time_use_thy "Simult";
+time_use_thy "Exp";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/SList.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,372 @@
+(* Title: HOL/ex/SList.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Definition of type 'a list by a least fixed point
+*)
+
+open SList;
+
+val list_con_defs = [NIL_def, CONS_def];
+
+goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
+let val rew = rewrite_rule list_con_defs in
+by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
+ addEs [rew list.elim]) 1)
+end;
+qed "list_unfold";
+
+(*This justifies using list in other recursive type definitions*)
+goalw SList.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
+by (rtac lfp_mono 1);
+by (REPEAT (ares_tac basic_monos 1));
+qed "list_mono";
+
+(*Type checking -- list creates well-founded sets*)
+goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+qed "list_sexp";
+
+(* A <= sexp ==> list(A) <= sexp *)
+bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
+
+(*Induction for the type 'a list *)
+val prems = goalw SList.thy [Nil_def,Cons_def]
+ "[| P(Nil); \
+\ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)";
+by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*)
+by (rtac (Rep_list RS list.induct) 1);
+by (REPEAT (ares_tac prems 1
+ ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
+qed "list_induct2";
+
+(*Perform induction on xs. *)
+fun list_ind_tac a M =
+ EVERY [res_inst_tac [("l",a)] list_induct2 M,
+ rename_last_tac a ["1"] (M+1)];
+
+(*** Isomorphisms ***)
+
+goal SList.thy "inj(Rep_list)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_list_inverse 1);
+qed "inj_Rep_list";
+
+goal SList.thy "inj_onto Abs_list (list(range Leaf))";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_list_inverse 1);
+qed "inj_onto_Abs_list";
+
+(** Distinctness of constructors **)
+
+goalw SList.thy list_con_defs "CONS M N ~= NIL";
+by (rtac In1_not_In0 1);
+qed "CONS_not_NIL";
+bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
+
+bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
+val NIL_neq_CONS = sym RS CONS_neq_NIL;
+
+goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
+by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
+by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
+qed "Cons_not_Nil";
+
+bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
+
+(** Injectiveness of CONS and Cons **)
+
+goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
+by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
+qed "CONS_CONS_eq";
+
+(*For reasoning about abstract list constructors*)
+AddIs ([Rep_list] @ list.intrs);
+
+AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
+
+AddSDs [inj_onto_Abs_list RS inj_ontoD,
+ inj_Rep_list RS injD, Leaf_inject];
+
+goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
+by (Fast_tac 1);
+qed "Cons_Cons_eq";
+bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
+
+val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
+by (rtac (major RS setup_induction) 1);
+by (etac list.induct 1);
+by (ALLGOALS (Fast_tac));
+qed "CONS_D";
+
+val prems = goalw SList.thy [CONS_def,In1_def]
+ "CONS M N: sexp ==> M: sexp & N: sexp";
+by (cut_facts_tac prems 1);
+by (fast_tac (!claset addSDs [Scons_D]) 1);
+qed "sexp_CONS_D";
+
+
+(*Reasoning about constructors and their freeness*)
+Addsimps list.intrs;
+
+AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
+
+goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
+by (etac list.induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "not_CONS_self";
+
+goal SList.thy "!x. l ~= x#l";
+by (list_ind_tac "l" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "not_Cons_self2";
+
+
+goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
+by (list_ind_tac "xs" 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
+by (REPEAT(resolve_tac [exI,refl,conjI] 1));
+qed "neq_Nil_conv2";
+
+(** Conversion rules for List_case: case analysis operator **)
+
+goalw SList.thy [List_case_def,NIL_def] "List_case c h NIL = c";
+by (rtac Case_In0 1);
+qed "List_case_NIL";
+
+goalw SList.thy [List_case_def,CONS_def] "List_case c h (CONS M N) = h M N";
+by (simp_tac (!simpset addsimps [Split,Case_In1]) 1);
+qed "List_case_CONS";
+
+(*** List_rec -- by wf recursion on pred_sexp ***)
+
+(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
+ hold if pred_sexp^+ were changed to pred_sexp. *)
+
+goal SList.thy
+ "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
+ \ (%g. List_case c (%x y. d x y (g y)))";
+by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
+val List_rec_unfold = standard
+ ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
+ * |> standard;
+ *---------------------------------------------------------------------------*)
+
+(** pred_sexp lemmas **)
+
+goalw SList.thy [CONS_def,In1_def]
+ "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
+by (Asm_simp_tac 1);
+qed "pred_sexp_CONS_I1";
+
+goalw SList.thy [CONS_def,In1_def]
+ "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
+by (Asm_simp_tac 1);
+qed "pred_sexp_CONS_I2";
+
+val [prem] = goal SList.thy
+ "(CONS M1 M2, N) : pred_sexp^+ ==> \
+\ (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
+by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS
+ subsetD RS SigmaE2)) 1);
+by (etac (sexp_CONS_D RS conjE) 1);
+by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
+ prem RSN (2, trans_trancl RS transD)] 1));
+qed "pred_sexp_CONS_D";
+
+(** Conversion rules for List_rec **)
+
+goal SList.thy "List_rec NIL c h = c";
+by (rtac (List_rec_unfold RS trans) 1);
+by (simp_tac (!simpset addsimps [List_case_NIL]) 1);
+qed "List_rec_NIL";
+
+goal SList.thy "!!M. [| M: sexp; N: sexp |] ==> \
+\ List_rec (CONS M N) c h = h M N (List_rec N c h)";
+by (rtac (List_rec_unfold RS trans) 1);
+by (asm_simp_tac (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
+qed "List_rec_CONS";
+
+(*** list_rec -- by List_rec ***)
+
+val Rep_list_in_sexp =
+ [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
+
+local
+ val list_rec_simps = [List_rec_NIL, List_rec_CONS,
+ Abs_list_inverse, Rep_list_inverse,
+ Rep_list, rangeI, inj_Leaf, inv_f_f,
+ sexp.LeafI, Rep_list_in_sexp]
+in
+ val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
+ "list_rec Nil c h = c"
+ (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
+
+ val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def]
+ "list_rec (a#l) c h = h a l (list_rec l c h)"
+ (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
+end;
+
+Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
+
+
+(*Type checking. Useful?*)
+val major::A_subset_sexp::prems = goal SList.thy
+ "[| M: list(A); \
+\ A<=sexp; \
+\ c: C(NIL); \
+\ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) \
+\ |] ==> List_rec M c h : C(M :: 'a item)";
+val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
+val sexp_A_I = A_subset_sexp RS subsetD;
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS(asm_simp_tac (!simpset addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
+qed "List_rec_type";
+
+(** Generalized map functionals **)
+
+goalw SList.thy [Rep_map_def] "Rep_map f Nil = NIL";
+by (rtac list_rec_Nil 1);
+qed "Rep_map_Nil";
+
+goalw SList.thy [Rep_map_def]
+ "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
+by (rtac list_rec_Cons 1);
+qed "Rep_map_Cons";
+
+goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
+by (rtac list_induct2 1);
+by (ALLGOALS Asm_simp_tac);
+qed "Rep_map_type";
+
+goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil";
+by (rtac List_rec_NIL 1);
+qed "Abs_map_NIL";
+
+val prems = goalw SList.thy [Abs_map_def]
+ "[| M: sexp; N: sexp |] ==> \
+\ Abs_map g (CONS M N) = g(M) # Abs_map g N";
+by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
+qed "Abs_map_CONS";
+
+(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
+val [rew] = goal SList.thy
+ "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
+by (rewtac rew);
+by (rtac list_rec_Nil 1);
+qed "def_list_rec_Nil";
+
+val [rew] = goal SList.thy
+ "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
+by (rewtac rew);
+by (rtac list_rec_Cons 1);
+qed "def_list_rec_Cons";
+
+fun list_recs def =
+ [standard (def RS def_list_rec_Nil),
+ standard (def RS def_list_rec_Cons)];
+
+(*** Unfolding the basic combinators ***)
+
+val [null_Nil, null_Cons] = list_recs null_def;
+val [_, hd_Cons] = list_recs hd_def;
+val [_, tl_Cons] = list_recs tl_def;
+val [ttl_Nil, ttl_Cons] = list_recs ttl_def;
+val [append_Nil3, append_Cons] = list_recs append_def;
+val [mem_Nil, mem_Cons] = list_recs mem_def;
+val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
+val [map_Nil, map_Cons] = list_recs map_def;
+val [list_case_Nil, list_case_Cons] = list_recs list_case_def;
+val [filter_Nil, filter_Cons] = list_recs filter_def;
+
+Addsimps
+ [null_Nil, ttl_Nil,
+ mem_Nil, mem_Cons,
+ list_case_Nil, list_case_Cons,
+ append_Nil3, append_Cons,
+ set_of_list_Nil, set_of_list_Cons,
+ map_Nil, map_Cons,
+ filter_Nil, filter_Cons];
+
+
+(** @ - append **)
+
+goal SList.thy "(xs@ys)@zs = xs@(ys@zs)";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "append_assoc2";
+
+goal SList.thy "xs @ [] = xs";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "append_Nil4";
+
+(** mem **)
+
+goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed "mem_append2";
+
+goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+qed "mem_filter2";
+
+
+(** The functional "map" **)
+
+Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
+
+val [major,A_subset_sexp,minor] = goal SList.thy
+ "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \
+\ ==> Rep_map f (Abs_map g M) = M";
+by (rtac (major RS list.induct) 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [sexp_A_I,sexp_ListA_I,minor])));
+qed "Abs_map_inverse";
+
+(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
+
+(** list_case **)
+
+goal SList.thy
+ "P(list_case a f xs) = ((xs=[] --> P(a)) & \
+\ (!y ys. xs=y#ys --> P(f y ys)))";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Fast_tac 1);
+qed "expand_list_case2";
+
+
+(** Additional mapping lemmas **)
+
+goal SList.thy "map (%x.x) xs = xs";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "map_ident2";
+
+goal SList.thy "map f (xs@ys) = map f xs @ map f ys";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "map_append2";
+
+goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "map_compose2";
+
+goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
+\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
+by (list_ind_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac(!simpset addsimps
+ [Rep_map_type,list_sexp RS subsetD])));
+qed "Abs_Rep_map";
+
+Addsimps [append_Nil4, map_ident2];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/SList.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,119 @@
+(* Title: HOL/ex/SList.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Definition of type 'a list (strict lists) by a least fixed point
+
+We use list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
+and not list == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
+so that list can serve as a "functor" for defining other recursive types
+*)
+
+SList = Sexp +
+
+types
+ 'a list
+
+arities
+ list :: (term) term
+
+
+consts
+
+ list :: 'a item set => 'a item set
+ Rep_list :: 'a list => 'a item
+ Abs_list :: 'a item => 'a list
+ NIL :: 'a item
+ CONS :: ['a item, 'a item] => 'a item
+ Nil :: 'a list
+ "#" :: ['a, 'a list] => 'a list (infixr 65)
+ List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
+ List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
+ list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+ list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+ Rep_map :: ('b => 'a item) => ('b list => 'a item)
+ Abs_map :: ('a item => 'b) => 'a item => 'b list
+ null :: 'a list => bool
+ hd :: 'a list => 'a
+ tl,ttl :: 'a list => 'a list
+ set_of_list :: ('a list => 'a set)
+ mem :: ['a, 'a list] => bool (infixl 55)
+ map :: ('a=>'b) => ('a list => 'b list)
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
+ filter :: ['a => bool, 'a list] => 'a list
+
+ (* list Enumeration *)
+
+ "[]" :: 'a list ("[]")
+ "@list" :: args => 'a list ("[(_)]")
+
+ (* Special syntax for filter *)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+
+translations
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
+ "[]" == "Nil"
+
+ "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
+
+ "[x:xs . P]" == "filter (%x.P) xs"
+
+defs
+ (* Defining the Concrete Constructors *)
+ NIL_def "NIL == In0(Numb(0))"
+ CONS_def "CONS M N == In1(M $ N)"
+
+inductive "list(A)"
+ intrs
+ NIL_I "NIL: list(A)"
+ CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)"
+
+rules
+ (* Faking a Type Definition ... *)
+ Rep_list "Rep_list(xs): list(range(Leaf))"
+ Rep_list_inverse "Abs_list(Rep_list(xs)) = xs"
+ Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
+
+
+defs
+ (* Defining the Abstract Constructors *)
+ Nil_def "Nil == Abs_list(NIL)"
+ Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
+
+ List_case_def "List_case c d == Case (%x.c) (Split d)"
+
+ (* list Recursion -- the trancl is Essential; see list.ML *)
+
+ List_rec_def
+ "List_rec M c d == wfrec (trancl pred_sexp)
+ (%g. List_case c (%x y. d x y (g y))) M"
+
+ list_rec_def
+ "list_rec l c d ==
+ List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
+
+ (* Generalized Map Functionals *)
+
+ Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
+ Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+
+ null_def "null(xs) == list_rec xs True (%x xs r.False)"
+ hd_def "hd(xs) == list_rec xs (@x.True) (%x xs r.x)"
+ tl_def "tl(xs) == list_rec xs (@xs.True) (%x xs r.xs)"
+ (* a total version of tl: *)
+ ttl_def "ttl(xs) == list_rec xs [] (%x xs r.xs)"
+
+ set_of_list_def "set_of_list xs == list_rec xs {} (%x l r. insert x r)"
+
+ mem_def "x mem xs ==
+ list_rec xs False (%y ys r. if y=x then True else r)"
+ map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)"
+ append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
+ filter_def "filter P xs ==
+ list_rec xs [] (%x xs r. if P(x) then x#r else r)"
+
+ list_case_def "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Simult.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,298 @@
+(* Title: HOL/ex/Simult.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Primitives for simultaneous recursive type definitions
+ includes worked example of trees & forests
+
+This is essentially the same data structure that on ex/term.ML, which is
+simpler because it uses list as a new type former. The approach in this
+file may be superior for other simultaneous recursions.
+*)
+
+open Simult;
+
+(*** Monotonicity and unfolding of the function ***)
+
+goal Simult.thy "mono(%Z. A <*> Part Z In1 \
+\ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))";
+by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
+ Part_mono] 1));
+qed "TF_fun_mono";
+
+val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
+
+goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
+by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
+qed "TF_mono";
+
+goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (blast_tac (!claset addIs sexp.intrs@[sexp_In0I, sexp_In1I]
+ addSEs [PartE]) 1);
+qed "TF_sexp";
+
+(* A <= sexp ==> TF(A) <= sexp *)
+val TF_subset_sexp = standard
+ (TF_mono RS (TF_sexp RSN (2,subset_trans)));
+
+
+(** Elimination -- structural induction on the set TF **)
+
+val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
+
+val major::prems = goalw Simult.thy TF_Rep_defs
+ "[| i: TF(A); \
+\ !!M N. [| M: A; N: Part (TF A) In1; R(N) |] ==> R(TCONS M N); \
+\ R(FNIL); \
+\ !!M N. [| M: Part (TF A) In0; N: Part (TF A) In1; R(M); R(N) \
+\ |] ==> R(FCONS M N) \
+\ |] ==> R(i)";
+by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
+by (blast_tac (!claset addIs (prems@[PartI])
+ addEs [usumE, uprodE, PartE]) 1);
+qed "TF_induct";
+
+(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
+goalw Simult.thy [Part_def]
+ "!!A. ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
+\ (M: Part (TF A) In1 --> Q(M)) \
+\ ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
+by (Blast_tac 1);
+qed "TF_induct_lemma";
+
+(*Could prove ~ TCONS M N : Part (TF A) In1 etc. *)
+
+(*Induction on TF with separate predicates P, Q*)
+val prems = goalw Simult.thy TF_Rep_defs
+ "[| !!M N. [| M: A; N: Part (TF A) In1; Q(N) |] ==> P(TCONS M N); \
+\ Q(FNIL); \
+\ !!M N. [| M: Part (TF A) In0; N: Part (TF A) In1; P(M); Q(N) \
+\ |] ==> Q(FCONS M N) \
+\ |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))";
+by (rtac (ballI RS TF_induct_lemma) 1);
+by (etac TF_induct 1);
+by (rewrite_goals_tac TF_Rep_defs);
+ (*Blast_tac needs this type instantiation in order to preserve the
+ right overloading of equality. The injectiveness properties for
+ type 'a item hold only for set types.*)
+val PartE' = read_instantiate [("'a", "?'c set")] PartE;
+by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
+qed "Tree_Forest_induct";
+
+(*Induction for the abstract types 'a tree, 'a forest*)
+val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
+ "[| !!x ts. Q(ts) ==> P(Tcons x ts); \
+\ Q(Fnil); \
+\ !!t ts. [| P(t); Q(ts) |] ==> Q(Fcons t ts) \
+\ |] ==> (! t. P(t)) & (! ts. Q(ts))";
+by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
+ ("Q1","%z.Q(Abs_Forest(z))")]
+ (Tree_Forest_induct RS conjE) 1);
+(*Instantiates ?A1 to range(Leaf). *)
+by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst,
+ Rep_Forest_inverse RS subst]
+ addSIs [Rep_Tree,Rep_Forest]) 4);
+(*Cannot use simplifier: the rewrites work in the wrong direction!*)
+by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
+ Abs_Forest_inverse RS subst]
+ addSIs prems)));
+qed "tree_forest_induct";
+
+
+
+(*** Isomorphisms ***)
+
+goal Simult.thy "inj(Rep_Tree)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Tree_inverse 1);
+qed "inj_Rep_Tree";
+
+goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_Tree_inverse 1);
+qed "inj_onto_Abs_Tree";
+
+goal Simult.thy "inj(Rep_Forest)";
+by (rtac inj_inverseI 1);
+by (rtac Rep_Forest_inverse 1);
+qed "inj_Rep_Forest";
+
+goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
+by (rtac inj_onto_inverseI 1);
+by (etac Abs_Forest_inverse 1);
+qed "inj_onto_Abs_Forest";
+
+(** Introduction rules for constructors **)
+
+(* c : A <*> Part (TF A) In1
+ <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *)
+val TF_I = TF_unfold RS equalityD2 RS subsetD;
+
+(*For reasoning about the representation*)
+AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
+AddSEs [Scons_inject];
+
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| a: A; M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
+by (Blast_tac 1);
+qed "TCONS_I";
+
+(* FNIL is a TF(A) -- this also justifies the type definition*)
+goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
+by (Blast_tac 1);
+qed "FNIL_I";
+
+goalw Simult.thy TF_Rep_defs
+ "!!A. [| M: Part (TF A) In0; N: Part (TF A) In1 |] ==> \
+\ FCONS M N : Part (TF A) In1";
+by (Blast_tac 1);
+qed "FCONS_I";
+
+(** Injectiveness of TCONS and FCONS **)
+
+goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
+by (Blast_tac 1);
+qed "TCONS_TCONS_eq";
+bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
+
+goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
+by (Blast_tac 1);
+qed "FCONS_FCONS_eq";
+bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
+
+(** Distinctness of TCONS, FNIL and FCONS **)
+
+goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
+by (Blast_tac 1);
+qed "TCONS_not_FNIL";
+bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
+
+bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
+val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
+
+goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
+by (Blast_tac 1);
+qed "FCONS_not_FNIL";
+bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
+
+bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
+val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
+
+goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
+by (Blast_tac 1);
+qed "TCONS_not_FCONS";
+bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
+
+bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
+val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
+
+(*???? Too many derived rules ????
+ Automatically generate symmetric forms? Always expand TF_Rep_defs? *)
+
+(** Injectiveness of Tcons and Fcons **)
+
+(*For reasoning about abstract constructors*)
+AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
+AddSEs [TCONS_inject, FCONS_inject,
+ TCONS_neq_FNIL, FNIL_neq_TCONS,
+ FCONS_neq_FNIL, FNIL_neq_FCONS,
+ TCONS_neq_FCONS, FCONS_neq_TCONS];
+AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
+ inj_onto_Abs_Forest RS inj_ontoD,
+ inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
+ Leaf_inject];
+
+goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
+by (Blast_tac 1);
+qed "Tcons_Tcons_eq";
+bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
+
+goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
+by (Blast_tac 1);
+qed "Fcons_not_Fnil";
+
+bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
+val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
+
+
+(** Injectiveness of Fcons **)
+
+goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
+by (Blast_tac 1);
+qed "Fcons_Fcons_eq";
+bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
+
+
+(*** TF_rec -- by wf recursion on pred_sexp ***)
+
+goal Simult.thy
+ "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
+ \ (%g. Case (Split(%x y. b x y (g y))) \
+ \ (List_case c (%x y. d x y (g x) (g y))))";
+by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
+val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS
+ ((result() RS eq_reflection) RS def_wfrec);
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val TF_rec_unfold =
+ * wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
+
+(** conversion rules for TF_rec **)
+
+goalw Simult.thy [TCONS_def]
+ "!!M N. [| M: sexp; N: sexp |] ==> \
+\ TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (simp_tac (!simpset addsimps [Case_In0, Split]) 1);
+by (asm_simp_tac (!simpset addsimps [In0_def]) 1);
+qed "TF_rec_TCONS";
+
+goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
+qed "TF_rec_FNIL";
+
+goalw Simult.thy [FCONS_def]
+ "!!M N. [| M: sexp; N: sexp |] ==> \
+\ TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
+by (rtac (TF_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
+by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1);
+qed "TF_rec_FCONS";
+
+
+(*** tree_rec, forest_rec -- by TF_rec ***)
+
+val Rep_Tree_in_sexp =
+ [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
+ Rep_Tree] MRS subsetD;
+val Rep_Forest_in_sexp =
+ [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
+ Rep_Forest] MRS subsetD;
+
+val tf_rec_ss = HOL_ss addsimps
+ [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
+ TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
+ Rep_Tree_inverse, Rep_Forest_inverse,
+ Abs_Tree_inverse, Abs_Forest_inverse,
+ inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
+ Rep_Tree_in_sexp, Rep_Forest_in_sexp];
+
+goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
+ "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)";
+by (simp_tac tf_rec_ss 1);
+qed "tree_rec_Tcons";
+
+goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c";
+by (simp_tac tf_rec_ss 1);
+qed "forest_rec_Fnil";
+
+goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
+ "forest_rec (Fcons t tf) b c d = \
+\ d t tf (tree_rec t b c d) (forest_rec tf b c d)";
+by (simp_tac tf_rec_ss 1);
+qed "forest_rec_Cons";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Simult.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,82 @@
+(* Title: HOL/ex/Simult
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+A simultaneous recursive type definition: trees & forests
+
+This is essentially the same data structure that on ex/term.ML, which is
+simpler because it uses list as a new type former. The approach in this
+file may be superior for other simultaneous recursions.
+
+The inductive definition package does not help defining this sort of mutually
+recursive data structure because it uses Inl, Inr instead of In0, In1.
+*)
+
+Simult = SList +
+
+types 'a tree
+ 'a forest
+
+arities tree,forest :: (term)term
+
+consts
+ TF :: 'a item set => 'a item set
+ FNIL :: 'a item
+ TCONS,FCONS :: ['a item, 'a item] => 'a item
+ Rep_Tree :: 'a tree => 'a item
+ Abs_Tree :: 'a item => 'a tree
+ Rep_Forest :: 'a forest => 'a item
+ Abs_Forest :: 'a item => 'a forest
+ Tcons :: ['a, 'a forest] => 'a tree
+ Fcons :: ['a tree, 'a forest] => 'a forest
+ Fnil :: 'a forest
+ TF_rec :: ['a item, ['a item , 'a item, 'b]=>'b,
+ 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
+ tree_rec :: ['a tree, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
+ forest_rec :: ['a forest, ['a, 'a forest, 'b]=>'b,
+ 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
+
+defs
+ (*the concrete constants*)
+ TCONS_def "TCONS M N == In0(M $ N)"
+ FNIL_def "FNIL == In1(NIL)"
+ FCONS_def "FCONS M N == In1(CONS M N)"
+ (*the abstract constants*)
+ Tcons_def "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
+ Fnil_def "Fnil == Abs_Forest(FNIL)"
+ Fcons_def "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
+
+ TF_def "TF(A) == lfp(%Z. A <*> Part Z In1
+ <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
+
+rules
+ (*faking a type definition for tree...*)
+ Rep_Tree "Rep_Tree(n): Part (TF(range Leaf)) In0"
+ Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
+ Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
+ (*faking a type definition for forest...*)
+ Rep_Forest "Rep_Forest(n): Part (TF(range Leaf)) In1"
+ Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
+ Abs_Forest_inverse
+ "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
+
+
+defs
+ (*recursion*)
+ TF_rec_def
+ "TF_rec M b c d == wfrec (trancl pred_sexp)
+ (%g. Case (Split(%x y. b x y (g y)))
+ (List_case c (%x y. d x y (g x) (g y)))) M"
+
+ tree_rec_def
+ "tree_rec t b c d ==
+ TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r)
+ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+
+ forest_rec_def
+ "forest_rec tf b c d ==
+ TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r)
+ c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Term.ML Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,172 @@
+(* Title: HOL/ex/Term
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Terms over a given alphabet -- function applications; illustrates list functor
+ (essentially the same type as in Trees & Forests)
+*)
+
+open Term;
+
+(*** Monotonicity and unfolding of the function ***)
+
+goal Term.thy "term(A) = A <*> list(term(A))";
+by (fast_tac (!claset addSIs (equalityI :: term.intrs)
+ addEs [term.elim]) 1);
+qed "term_unfold";
+
+(*This justifies using term in other recursive type definitions*)
+goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
+qed "term_mono";
+
+(** Type checking -- term creates well-founded sets **)
+
+goalw Term.thy term.defs "term(sexp) <= sexp";
+by (rtac lfp_lowerbound 1);
+by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
+qed "term_sexp";
+
+(* A <= sexp ==> term(A) <= sexp *)
+bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
+
+
+(** Elimination -- structural induction on the set term(A) **)
+
+(*Induction for the set term(A) *)
+val [major,minor] = goal Term.thy
+ "[| M: term(A); \
+\ !!x zs. [| x: A; zs: list(term(A)); zs: list({x.R(x)}) \
+\ |] ==> R(x$zs) \
+\ |] ==> R(M)";
+by (rtac (major RS term.induct) 1);
+by (REPEAT (eresolve_tac ([minor] @
+ ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
+(*Proof could also use mono_Int RS subsetD RS IntE *)
+qed "Term_induct";
+
+(*Induction on term(A) followed by induction on list *)
+val major::prems = goal Term.thy
+ "[| M: term(A); \
+\ !!x. [| x: A |] ==> R(x$NIL); \
+\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); R(x$zs) \
+\ |] ==> R(x $ CONS z zs) \
+\ |] ==> R(M)";
+by (rtac (major RS Term_induct) 1);
+by (etac list.induct 1);
+by (REPEAT (ares_tac prems 1));
+qed "Term_induct2";
+
+(*** Structural Induction on the abstract type 'a term ***)
+
+val Rep_term_in_sexp =
+ Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
+
+(*Induction for the abstract type 'a term*)
+val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
+ "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts) \
+\ |] ==> R(t)";
+by (rtac (Rep_term_inverse RS subst) 1); (*types force good instantiation*)
+by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
+by (rtac (Rep_term RS Term_induct) 1);
+by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS
+ list_subset_sexp, range_Leaf_subset_sexp] 1
+ ORELSE etac rev_subsetD 1));
+by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
+ (Abs_map_inverse RS subst) 1);
+by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
+by (etac Abs_term_inverse 1);
+by (etac rangeE 1);
+by (hyp_subst_tac 1);
+by (resolve_tac prems 1);
+by (etac list.induct 1);
+by (etac CollectE 2);
+by (stac Abs_map_CONS 2);
+by (etac conjunct1 2);
+by (etac rev_subsetD 2);
+by (rtac list_subset_sexp 2);
+by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Fast_tac);
+qed "term_induct";
+
+(*Induction for the abstract type 'a term*)
+val prems = goal Term.thy
+ "[| !!x. R(App x Nil); \
+\ !!x t ts. R(App x ts) ==> R(App x (t#ts)) \
+\ |] ==> R(t)";
+by (rtac term_induct 1); (*types force good instantiation*)
+by (etac rev_mp 1);
+by (rtac list_induct2 1); (*types force good instantiation*)
+by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
+qed "term_induct2";
+
+(*Perform induction on xs. *)
+fun term_ind2_tac a i =
+ EVERY [res_inst_tac [("t",a)] term_induct2 i,
+ rename_last_tac a ["1","s"] (i+1)];
+
+
+
+(*** Term_rec -- by wf recursion on pred_sexp ***)
+
+goal Term.thy
+ "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
+ \ (%g. Split(%x y. d x y (Abs_map g y)))";
+by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
+bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS
+ ((result() RS eq_reflection) RS def_wfrec));
+
+(*---------------------------------------------------------------------------
+ * Old:
+ * val Term_rec_unfold =
+ * wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
+ *---------------------------------------------------------------------------*)
+
+(** conversion rules **)
+
+val [prem] = goal Term.thy
+ "N: list(term(A)) ==> \
+\ !M. (N,M): pred_sexp^+ --> \
+\ Abs_map (cut h (pred_sexp^+) M) N = \
+\ Abs_map h N";
+by (rtac (prem RS list.induct) 1);
+by (Simp_tac 1);
+by (strip_tac 1);
+by (etac (pred_sexp_CONS_D RS conjE) 1);
+by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1);
+qed "Abs_map_lemma";
+
+val [prem1,prem2,A_subset_sexp] = goal Term.thy
+ "[| M: sexp; N: list(term(A)); A<=sexp |] ==> \
+\ Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
+by (rtac (Term_rec_unfold RS trans) 1);
+by (simp_tac (HOL_ss addsimps
+ [Split,
+ prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
+ prem1, prem2 RS rev_subsetD, list_subset_sexp,
+ term_subset_sexp, A_subset_sexp]) 1);
+qed "Term_rec";
+
+(*** term_rec -- by Term_rec ***)
+
+local
+ val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
+ [("f","Rep_term")] Rep_map_type;
+ val Rep_Tlist = Rep_term RS Rep_map_type1;
+ val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
+
+ (*Now avoids conditional rewriting with the premise N: list(term(A)),
+ since A will be uninstantiated and will cause rewriting to fail. *)
+ val term_rec_ss = HOL_ss
+ addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),
+ Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
+ inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
+in
+
+val term_rec = prove_goalw Term.thy
+ [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
+ "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"
+ (fn _ => [simp_tac term_rec_ss 1])
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Term.thy Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,55 @@
+(* Title: HOL/ex/Term
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Terms over a given alphabet -- function applications; illustrates list functor
+ (essentially the same type as in Trees & Forests)
+
+There is no constructor APP because it is simply cons ($)
+*)
+
+Term = SList +
+
+types 'a term
+
+arities term :: (term)term
+
+consts
+ term :: 'a item set => 'a item set
+ Rep_term :: 'a term => 'a item
+ Abs_term :: 'a item => 'a term
+ Rep_Tlist :: 'a term list => 'a item
+ Abs_Tlist :: 'a item => 'a term list
+ App :: ['a, ('a term)list] => 'a term
+ Term_rec :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
+ term_rec :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
+
+inductive "term(A)"
+ intrs
+ APP_I "[| M: A; N : list(term(A)) |] ==> M$N : term(A)"
+ monos "[list_mono]"
+
+defs
+ (*defining abstraction/representation functions for term list...*)
+ Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
+ Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
+
+ (*defining the abstract constants*)
+ App_def "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
+
+ (*list recursion*)
+ Term_rec_def
+ "Term_rec M d == wfrec (trancl pred_sexp)
+ (%g. Split(%x y. d x y (Abs_map g y))) M"
+
+ term_rec_def
+ "term_rec t d ==
+ Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
+
+rules
+ (*faking a type definition for term...*)
+ Rep_term "Rep_term(n): term(range(Leaf))"
+ Rep_term_inverse "Abs_term(Rep_term(t)) = t"
+ Abs_term_inverse "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
+end