# HG changeset patch # User paulson # Date 863002226 -7200 # Node ID c58423c207408f7485717a28cf82bec00b8ee175 # Parent bb2ee88aa43ffef3cb5ef9f1690d8de03953d7c1 New directory to contain examples of (co)inductive definitions diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Acc.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Acc.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Com.ML --- /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"; + diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Com.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Comb.ML --- /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."; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Comb.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Exp.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Exp.thy --- /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 + diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/LFilter.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/LFilter.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/LList.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/LList.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Mutil.ML --- /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 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"; + diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Mutil.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Perm.ML --- /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"; + diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Perm.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/PropLog.ML --- /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."; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/PropLog.thy --- /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 + diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/ROOT.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/SList.ML --- /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]; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/SList.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Simult.ML --- /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"; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Simult.thy --- /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 diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Term.ML --- /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; diff -r bb2ee88aa43f -r c58423c20740 src/HOL/Induct/Term.thy --- /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