--- a/src/HOL/Induct/Com.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,44 +0,0 @@
-(* 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
-*)
-
-AddIs exec.intrs;
-
-val exec_elim_cases =
- map exec.mk_cases
- ["(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 "(WHILE b DO c,s) -[eval]-> t";
-
-AddSEs exec_elim_cases;
-
-(*This theorem justifies using "exec" in the inductive definition of "eval"*)
-Goalw exec.defs "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 "single_valued ev ==> single_valued(exec ev)";
-by (simp_tac (simpset() addsimps [single_valued_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 (rewtac single_valued_def);
-by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
-qed "single_valued_exec";
-
-Addsimps [fun_upd_same, fun_upd_other];
--- a/src/HOL/Induct/Com.thy Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/Com.thy Tue Apr 02 14:28:28 2002 +0200
@@ -6,11 +6,12 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)
-Com = Main +
+theory Com = Main:
-types loc
- state = "loc => nat"
- n2n2n = "nat => nat => nat"
+typedecl loc
+
+types state = "loc => nat"
+ n2n2n = "nat => nat => nat"
arities loc :: type
@@ -26,38 +27,285 @@
| Cond exp com com ("IF _ THEN _ ELSE _" 60)
| While exp com ("WHILE _ DO _" 60)
-(** Execution of commands **)
+text{* Execution of commands *}
consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
"@exec" :: "((exp*state) * (nat*state)) set =>
[com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
-translations "csig -[eval]-> s" == "(csig,s) : exec eval"
+translations "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
syntax eval' :: "[exp*state,nat*state] =>
((exp*state) * (nat*state)) set => bool"
- ("_/ -|[_]-> _" [50,0,50] 50)
-translations
- "esig -|[eval]-> ns" => "(esig,ns) : eval"
+ ("_/ -|[_]-> _" [50,0,50] 50)
-(*Command execution. Natural numbers represent Booleans: 0=True, 1=False*)
-inductive "exec eval"
- intrs
- Skip "(SKIP,s) -[eval]-> s"
+translations
+ "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
- Assign "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
-
- Semi "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
- ==> (c0 ;; c1, s) -[eval]-> s1"
+text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
+inductive "exec eval"
+ intros
+ Skip: "(SKIP,s) -[eval]-> s"
- IfTrue "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |]
- ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+ Assign: "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
- IfFalse "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |]
+ Semi: "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
+ ==> (c0 ;; c1, s) -[eval]-> s1"
+
+ IfTrue: "[| (e,s) -|[eval]-> (0,s'); (c0,s') -[eval]-> s1 |]
==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
- WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1"
+ IfFalse: "[| (e,s) -|[eval]-> (Suc 0, s'); (c1,s') -[eval]-> s1 |]
+ ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+ WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1)
+ ==> (WHILE e DO c, s) -[eval]-> s1"
+
+ WhileTrue: "[| (e,s) -|[eval]-> (0,s1);
+ (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
+ ==> (WHILE e DO c, s) -[eval]-> s3"
+
+declare exec.intros [intro]
+
+
+inductive_cases
+ [elim!]: "(SKIP,s) -[eval]-> t"
+ and [elim!]: "(x:=a,s) -[eval]-> t"
+ and [elim!]: "(c1;;c2, s) -[eval]-> t"
+ and [elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
+ and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
+
+
+text{*Justifies using "exec" in the inductive definition of "eval"*}
+lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
+apply (unfold exec.defs )
+apply (rule lfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+ML {*
+Unify.trace_bound := 30;
+Unify.search_bound := 60;
+*}
+
+text{*Command execution is functional (deterministic) provided evaluation is*}
+theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
+apply (simp add: single_valued_def)
+apply (intro allI)
+apply (rule impI)
+apply (erule exec.induct)
+apply (blast elim: exec_WHILE_case)+
+done
+
+
+section {* Expressions *}
+
+text{* 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) \<in> eval"
+ "esig -|-> ns" == "(esig,ns ) \<in> eval"
+
+inductive eval
+ intros
+ N [intro!]: "(N(n),s) -|-> (n,s)"
+
+ X [intro!]: "(X(x),s) -|-> (s(x),s)"
+
+ Op [intro]: "[| (e0,s) -|-> (n0,s0); (e1,s0) -|-> (n1,s1) |]
+ ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
+
+ valOf [intro]: "[| (c,s) -[eval]-> s0; (e,s0) -|-> (n,s1) |]
+ ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
+
+ monos exec_mono
+
+
+inductive_cases
+ [elim!]: "(N(n),sigma) -|-> (n',s')"
+ and [elim!]: "(X(x),sigma) -|-> (n,s')"
+ and [elim!]: "(Op f a1 a2,sigma) -|-> (n,s')"
+ and [elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
+
+
+lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
+by (rule fun_upd_same [THEN subst], fast)
+
+
+text{* Make the induction rule look nicer -- though eta_contract makes the new
+ version look worse than it is...*}
+
+lemma split_lemma:
+ "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
+by auto
+
+text{*New induction rule. Note the form of the VALOF induction hypothesis*}
+lemma eval_induct:
+ "[| (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;
+ (c,s) -[eval]-> s0;
+ (e,s0) -|-> (n,s1); P e s0 n s1 |]
+ ==> P (VALOF c RESULTIS e) s n s1
+ |] ==> P e s n s'"
+apply (erule eval.induct, blast)
+apply blast
+apply blast
+apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
+apply (auto simp add: split_lemma)
+done
+
- WhileTrue "[| (e,s) -|[eval]-> (0,s1);
- (c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
- ==> (WHILE e DO c, s) -[eval]-> s3"
+text{*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).
+*}
+lemma com_Unique:
+ "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
+ ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
+apply (erule exec.induct, simp_all)
+ apply blast
+ apply force
+ apply blast
+ apply blast
+ apply blast
+ apply (blast elim: exec_WHILE_case)
+apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
+apply clarify
+apply (erule exec_WHILE_case, blast+)
+done
+
+
+text{*Expression evaluation is functional, or deterministic*}
+theorem single_valued_eval: "single_valued eval"
+apply (unfold single_valued_def)
+apply (intro allI, rule impI)
+apply (simp (no_asm_simp) only: split_tupled_all)
+apply (erule eval_induct)
+apply (drule_tac [4] com_Unique)
+apply (simp_all (no_asm_use))
+apply blast+
+done
+
+
+lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
+by (erule eval_induct, simp_all)
+
+lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
+
+
+text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
+lemma while_true_E [rule_format]:
+ "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
+by (erule exec.induct, auto)
+
+
+subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
+ WHILE e DO c *}
+
+lemma while_if1 [rule_format]:
+ "(c',s) -[eval]-> t
+ ==> (c' = WHILE e DO c) -->
+ (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+lemma while_if2 [rule_format]:
+ "(c',s) -[eval]-> t
+ ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->
+ (WHILE e DO c, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+
+theorem while_if:
+ "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) =
+ ((WHILE e DO c, s) -[eval]-> t)"
+by (blast intro: while_if1 while_if2)
+
+
+
+subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c
+ and IF e THEN (c1;;c) ELSE (c2;;c) *}
+
+lemma if_semi1 [rule_format]:
+ "(c',s) -[eval]-> t
+ ==> (c' = (IF e THEN c1 ELSE c2);;c) -->
+ (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+lemma if_semi2 [rule_format]:
+ "(c',s) -[eval]-> t
+ ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->
+ ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
+by (erule exec.induct, auto)
+
+theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) =
+ ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
+by (blast intro: if_semi1 if_semi2)
+
+
+
+subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
+ and VALOF c1;;c2 RESULTIS e
+ *}
+
+lemma valof_valof1 [rule_format]:
+ "(e',s) -|-> (v,s')
+ ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->
+ (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+
+lemma valof_valof2 [rule_format]:
+ "(e',s) -|-> (v,s')
+ ==> (e' = VALOF c1;;c2 RESULTIS e) -->
+ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+theorem valof_valof:
+ "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) =
+ ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
+by (blast intro: valof_valof1 valof_valof2)
+
+
+subsection{* Equivalence of VALOF SKIP RESULTIS e and e *}
+
+lemma valof_skip1 [rule_format]:
+ "(e',s) -|-> (v,s')
+ ==> (e' = VALOF SKIP RESULTIS e) -->
+ (e, s) -|-> (v,s')"
+by (erule eval_induct, auto)
+
+lemma valof_skip2:
+ "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
+by blast
+
+theorem valof_skip:
+ "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))"
+by (blast intro: valof_skip1 valof_skip2)
+
+
+subsection{* Equivalence of VALOF x:=e RESULTIS x and e *}
+
+lemma valof_assign1 [rule_format]:
+ "(e',s) -|-> (v,s'')
+ ==> (e' = VALOF x:=e RESULTIS X x) -->
+ (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
+apply (erule eval_induct)
+apply (simp_all del: fun_upd_apply, clarify, auto)
+done
+
+lemma valof_assign2:
+ "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
+by blast
+
+
end
--- a/src/HOL/Induct/Comb.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,175 +0,0 @@
-(* Title: HOL/ex/comb.ML
- ID: $Id$
- Author: Lawrence C Paulson
- Copyright 1996 University of Cambridge
-
-Combinatory Logic example: the Church-Rosser Theorem
-Curiously, combinators do not include free variables.
-
-Example taken from
- J. Camilleri and T. F. Melham.
- Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
- Report 265, University of Cambridge Computer Laboratory, 1992.
-
-HOL system proofs may be found in
-/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
-*)
-
-(*** 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 [diamond_def]
- "[| 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);
-qed_spec_mp "diamond_strip_lemmaE";
-
-Goal "diamond(r) ==> diamond(r^*)";
-by (stac diamond_def 1); (*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 (best_tac (*Seems to be a brittle, undirected search*)
- (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
- addEs [diamond_strip_lemmaE RS exE]) 1);
-qed "diamond_rtrancl";
-
-
-(*** Results about Contraction ***)
-
-(*Derive a case for each combinator constructor*)
-val K_contractE = contract.mk_cases "K -1-> z";
-val S_contractE = contract.mk_cases "S -1-> z";
-val Ap_contractE = contract.mk_cases "x##y -1-> z";
-
-AddSIs [contract.K, contract.S];
-AddIs [contract.Ap1, contract.Ap2];
-AddSEs [K_contractE, S_contractE, Ap_contractE];
-
-Goalw [I_def] "I -1-> z ==> P";
-by (Blast_tac 1);
-qed "I_contract_E";
-AddSEs [I_contract_E];
-
-Goal "K##x -1-> z ==> (EX x'. z = K##x' & x -1-> x')";
-by (Blast_tac 1);
-qed "K1_contractD";
-AddSEs [K1_contractD];
-
-Goal "x ---> y ==> x##z ---> y##z";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
-qed "Ap_reduce1";
-
-Goal "x ---> y ==> z##x ---> z##y";
-by (etac rtrancl_induct 1);
-by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
-qed "Ap_reduce2";
-
-(** Counterexample to the diamond property for -1-> **)
-
-Goal "K##I##(I##I) -1-> I";
-by (rtac contract.K 1);
-qed "KIII_contract1";
-
-Goalw [I_def] "K##I##(I##I) -1-> K##I##((K##I)##(K##I))";
-by (Blast_tac 1);
-qed "KIII_contract2";
-
-Goal "K##I##((K##I)##(K##I)) -1-> I";
-by (Blast_tac 1);
-qed "KIII_contract3";
-
-Goalw [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 "K =1=> z";
-val S_parcontractE = parcontract.mk_cases "S =1=> z";
-val Ap_parcontractE = parcontract.mk_cases "x##y =1=> z";
-
-AddSIs [parcontract.refl, parcontract.K, parcontract.S];
-AddIs [parcontract.Ap];
-AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
-
-(*** Basic properties of parallel contraction ***)
-
-Goal "K##x =1=> z ==> (EX x'. z = K##x' & x =1=> x')";
-by (Blast_tac 1);
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-Goal "S##x =1=> z ==> (EX x'. z = S##x' & x =1=> x')";
-by (Blast_tac 1);
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-Goal "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 [diamond_def] "diamond parcontract";
-by (rtac (impI RS allI RS allI) 1);
-by (etac parcontract.induct 1 THEN prune_params_tac);
-by Safe_tac;
-by (ALLGOALS Blast_tac);
-qed "diamond_parcontract";
-
-
-(*** Equivalence of x--->y and x===>y ***)
-
-Goal "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 [I_def] "I##x ---> x";
-by (Blast_tac 1);
-qed "reduce_I";
-
-Goal "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 "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 "diamond(contract^*)";
-by (simp_tac (simpset() addsimps [reduce_eq_parreduce, diamond_rtrancl,
- diamond_parcontract]) 1);
-qed "diamond_reduce";
-
-
-writeln"Reached end of file.";
--- a/src/HOL/Induct/Comb.thy Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/Comb.thy Tue Apr 02 14:28:28 2002 +0200
@@ -1,74 +1,220 @@
-(* Title: HOL/ex/Comb.thy
+(* Title: HOL/Induct/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.
*)
+header {* Combinatory Logic example: the Church-Rosser Theorem *}
-Comb = Main +
+theory Comb = Main:
+
+text {*
+ Curiously, combinators do not include free variables.
+
+ Example taken from \cite{camilleri-melham}.
-(** Datatype definition of combinators S and K, with infixed application **)
+HOL system proofs may be found in the HOL distribution at
+ .../contrib/rule-induction/cl.ml
+*}
+
+subsection {* Definitions *}
+
+text {* Datatype definition of combinators @{text S} and @{text K}. *}
+
datatype comb = K
| S
| "##" comb comb (infixl 90)
-(** Inductive definition of contractions, -1->
- and (multi-step) reductions, --->
-**)
+text {*
+ Inductive definition of contractions, @{text "-1->"} and
+ (multi-step) reductions, @{text "--->"}.
+*}
+
consts
contract :: "(comb*comb) set"
- "-1->" :: [comb,comb] => bool (infixl 50)
- "--->" :: [comb,comb] => bool (infixl 50)
+ "-1->" :: "[comb,comb] => bool" (infixl 50)
+ "--->" :: "[comb,comb] => bool" (infixl 50)
translations
- "x -1-> y" == "(x,y) : contract"
- "x ---> y" == "(x,y) : contract^*"
+ "x -1-> y" == "(x,y) \<in> contract"
+ "x ---> y" == "(x,y) \<in> 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"
+ intros
+ 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"
+text {*
+ Inductive definition of parallel contractions, @{text "=1=>"} and
+ (multi-step) parallel reductions, @{text "===>"}.
+*}
-(** 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)
+ "=1=>" :: "[comb,comb] => bool" (infixl 50)
+ "===>" :: "[comb,comb] => bool" (infixl 50)
translations
- "x =1=> y" == "(x,y) : parcontract"
- "x ===> y" == "(x,y) : parcontract^*"
+ "x =1=> y" == "(x,y) \<in> parcontract"
+ "x ===> y" == "(x,y) \<in> 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"
+ intros
+ 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"
+text {*
+ Misc definitions.
+*}
-(*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))"
+ --{*confluence; Lambda/Commutation treats this more abstractly*}
+ "diamond(r) == \<forall>x y. (x,y) \<in> r -->
+ (\<forall>y'. (x,y') \<in> r -->
+ (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
+
+
+subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
+
+text{*So does the Transitive closure, with a similar proof*}
+
+text{*Strip lemma.
+ The induction hypothesis covers all but the last diamond of the strip.*}
+lemma diamond_strip_lemmaE [rule_format]:
+ "[| diamond(r); (x,y) \<in> r^* |] ==>
+ \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
+apply (unfold diamond_def)
+apply (erule rtrancl_induct, blast, clarify)
+apply (drule spec, drule mp, assumption)
+apply (blast intro: rtrancl_trans [OF _ r_into_rtrancl])
+done
+
+lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
+apply (simp (no_asm_simp) add: diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule rtrancl_induct, blast)
+apply (best intro: rtrancl_trans [OF _ r_into_rtrancl]
+ elim: diamond_strip_lemmaE [THEN exE])
+done
+
+
+subsection {* Non-contraction results *}
+
+text {* Derive a case for each combinator constructor. *}
+
+inductive_cases
+ K_contractE [elim!]: "K -1-> r"
+ and S_contractE [elim!]: "S -1-> r"
+ and Ap_contractE [elim!]: "p##q -1-> r"
+
+declare contract.K [intro!] contract.S [intro!]
+declare contract.Ap1 [intro] contract.Ap2 [intro]
+
+lemma I_contract_E [elim!]: "I -1-> z ==> P"
+by (unfold I_def, blast)
+
+lemma K1_contractD [elim!]: "K##x -1-> z ==> (\<exists>x'. z = K##x' & x -1-> x')"
+by blast
+
+lemma Ap_reduce1 [intro]: "x ---> y ==> x##z ---> y##z"
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_trans)+
+done
+
+lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y"
+apply (erule rtrancl_induct)
+apply (blast intro: rtrancl_trans)+
+done
+
+(** Counterexample to the diamond property for -1-> **)
+
+lemma KIII_contract1: "K##I##(I##I) -1-> I"
+by (rule contract.K)
+
+lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))"
+by (unfold I_def, blast)
+
+lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I"
+by blast
+
+lemma not_diamond_contract: "~ diamond(contract)"
+apply (unfold diamond_def)
+apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3)
+done
+
+
+subsection {* Results about Parallel Contraction *}
+
+text {* Derive a case for each combinator constructor. *}
+
+inductive_cases
+ K_parcontractE [elim!]: "K =1=> r"
+ and S_parcontractE [elim!]: "S =1=> r"
+ and Ap_parcontractE [elim!]: "p##q =1=> r"
+
+declare parcontract.intros [intro]
+
+(*** Basic properties of parallel contraction ***)
+
+subsection {* Basic properties of parallel contraction *}
+
+lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')"
+by blast
+
+lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')"
+by blast
+
+lemma S2_parcontractD [dest!]:
+ "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')"
+by blast
+
+text{*The rules above are not essential but make proofs much faster*}
+
+text{*Church-Rosser property for parallel contraction*}
+lemma diamond_parcontract: "diamond parcontract"
+apply (unfold diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule parcontract.induct, fast+)
+done
+
+text {*
+ \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
+*}
+
+lemma contract_subset_parcontract: "contract <= parcontract"
+apply (rule subsetI)
+apply (simp only: split_tupled_all)
+apply (erule contract.induct, blast+)
+done
+
+text{*Reductions: simply throw together reflexivity, transitivity and
+ the one-step reductions*}
+
+declare r_into_rtrancl [intro] rtrancl_trans [intro]
+
+(*Example only: not used*)
+lemma reduce_I: "I##x ---> x"
+by (unfold I_def, blast)
+
+lemma parcontract_subset_reduce: "parcontract <= contract^*"
+apply (rule subsetI)
+apply (simp only: split_tupled_all)
+apply (erule parcontract.induct , blast+)
+done
+
+lemma reduce_eq_parreduce: "contract^* = parcontract^*"
+by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono]
+ parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+
+
+lemma diamond_reduce: "diamond(contract^*)"
+by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)
end
--- a/src/HOL/Induct/Exp.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,233 +0,0 @@
-(* 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
-*)
-
-AddSIs [eval.N, eval.X];
-AddIs [eval.Op, eval.valOf];
-
-val eval_elim_cases =
- map eval.mk_cases
- ["(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;
-
-
-Goal "(X x, s(x:=n)) -|-> (n, s(x:=n))";
-by (rtac (fun_upd_same RS subst) 1 THEN resolve_tac eval.intrs 1);
-qed "var_assign_eval";
-
-AddSIs [var_assign_eval];
-
-
-(** Make the induction rule look nicer -- though eta_contract makes the new
- version look worse than it is...**)
-
-Goal "{((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; \
-\ (c,s) -[eval]-> 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 (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
-by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
-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 "(c,s) -[eval Int {((e,s),(n,t)). ALL nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 \
-\ ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
-by (etac exec.induct 1);
-by (ALLGOALS Full_simp_tac);
- by (Blast_tac 1);
- by (Force_tac 1);
- 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 (Clarify_tac 1);
-by (etac exec_WHILE_case 1);
- by (ALLGOALS Blast_tac);
-qed "com_Unique";
-
-
-(*Expression evaluation is functional, or deterministic*)
-Goalw [single_valued_def] "single_valued eval";
-by (EVERY1[rtac allI, rtac allI, rtac impI]);
-by (split_all_tac 1);
-by (etac eval_induct 1);
-by (dtac com_Unique 4);
-by (ALLGOALS Full_simp_tac);
-by (ALLGOALS Blast_tac);
-qed "single_valued_eval";
-
-
-Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-val lemma = result();
-bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
-
-AddSEs [eval_N_E];
-
-
-(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
-Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
-by (etac exec.induct 1);
-by Auto_tac;
-bind_thm ("while_true_E", refl RSN (2, result() RS mp));
-
-
-(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and WHILE e DO c **)
-
-Goal "(c',s) -[eval]-> t ==> \
-\ (c' = WHILE e DO c) --> \
-\ (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
-bind_thm ("while_if1", refl RSN (2, result() RS mp));
-
-
-Goal "(c',s) -[eval]-> t ==> \
-\ (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
-\ (WHILE e DO c, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
-bind_thm ("while_if2", refl RSN (2, result() RS mp));
-
-
-Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t) = \
-\ ((WHILE e DO c, s) -[eval]-> t)";
-by (blast_tac (claset() addIs [while_if1, while_if2]) 1);
-qed "while_if";
-
-
-
-(** Equivalence of (IF e THEN c1 ELSE c2);;c
- and IF e THEN (c1;;c) ELSE (c2;;c) **)
-
-Goal "(c',s) -[eval]-> t ==> \
-\ (c' = (IF e THEN c1 ELSE c2);;c) --> \
-\ (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-bind_thm ("if_semi1", refl RSN (2, result() RS mp));
-
-
-Goal "(c',s) -[eval]-> t ==> \
-\ (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
-\ ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
-by (etac exec.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS Blast_tac);
-bind_thm ("if_semi2", refl RSN (2, result() RS mp));
-
-
-Goal "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t) = \
-\ ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)";
-by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1);
-qed "if_semi";
-
-
-
-(** Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
- and VALOF c1;;c2 RESULTIS e
- **)
-
-Goal "(e',s) -|-> (v,s') ==> \
-\ (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
-\ (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
-
-
-Goal "(e',s) -|-> (v,s') ==> \
-\ (e' = VALOF c1;;c2 RESULTIS e) --> \
-\ (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
-
-
-Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')) = \
-\ ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))";
-by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1);
-qed "valof_valof";
-
-
-(** Equivalence of VALOF SKIP RESULTIS e and e **)
-
-Goal "(e',s) -|-> (v,s') ==> \
-\ (e' = VALOF SKIP RESULTIS e) --> \
-\ (e, s) -|-> (v,s')";
-by (etac eval_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
-
-Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
-by (Blast_tac 1);
-qed "valof_skip2";
-
-Goal "((VALOF SKIP RESULTIS e, s) -|-> (v,s')) = ((e, s) -|-> (v,s'))";
-by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1);
-qed "valof_skip";
-
-
-(** Equivalence of VALOF x:=e RESULTIS x and e **)
-
-Delsimps [fun_upd_apply];
-Goal "(e',s) -|-> (v,s'') ==> \
-\ (e' = VALOF x:=e RESULTIS X x) --> \
-\ (EX s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))";
-by (etac eval_induct 1);
- by (ALLGOALS Asm_simp_tac);
-by (thin_tac "?PP-->?QQ" 1);
-by (Clarify_tac 1);
-by (Simp_tac 1);
-by (Blast_tac 1);
-bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
-
-
-Goal "(e,s) -|-> (v,s') ==> \
-\ (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))";
-by (Blast_tac 1);
-qed "valof_assign2";
--- a/src/HOL/Induct/Exp.thy Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-(* 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
-
--- a/src/HOL/Induct/LFilter.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,337 +0,0 @@
-(* Title: HOL/ex/LFilter
- ID: $Id$
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-
-The "filter" functional for coinductive lists
- --defined by a combination of induction and coinduction
-*)
-
-(*** findRel: basic laws ****)
-
-val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p";
-
-AddSEs [findRel_LConsE];
-
-
-Goal "(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 "(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 "(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 "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 "[| l: Domain (findRel p); \
-\ !!x l'. [| (l, LCons x l') : findRel p; p x |] ==> Q \
-\ |] ==> Q";
-by (rtac (major RS DomainE) 1);
-by (ftac 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 (Clarify_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 [find_def] "find p LNil = LNil";
-by (Blast_tac 1);
-qed "find_LNil";
-Addsimps [find_LNil];
-
-Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
-by (blast_tac (claset() addDs [findRel_functional]) 1);
-qed "findRel_imp_find";
-Addsimps [findRel_imp_find];
-
-Goal "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";
-Addsimps [find_LCons_found];
-
-Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
-by (Blast_tac 1);
-qed "diverge_find_LNil";
-Addsimps [diverge_find_LNil];
-
-Goal "~ (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 (Clarify_tac 1);
-by (Asm_simp_tac 1);
-by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
-qed "find_LCons_seek";
-Addsimps [find_LCons_seek];
-
-Goal "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (Asm_simp_tac 1);
-qed "find_LCons";
-
-
-
-(*** lfilter: basic equations ***)
-
-Goal "lfilter p LNil = LNil";
-by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lfilter_LNil";
-Addsimps [lfilter_LNil];
-
-Goal "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";
-
-Addsimps [diverge_lfilter_LNil];
-
-
-Goal "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 1);
-qed "lfilter_LCons_found";
-(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
- subsumes both*)
-
-
-Goal "(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 1);
-qed "findRel_imp_lfilter";
-
-Addsimps [findRel_imp_lfilter];
-
-
-Goal "~ (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 2);
-by (etac Domain_findRelE 1);
-by (safe_tac (claset() delrules [conjI]));
-by (Asm_full_simp_tac 1);
-qed "lfilter_LCons_seek";
-
-
-Goal "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]) 1);
-qed "lfilter_LCons";
-
-AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LCons];
-
-
-Goal "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 1);
-qed "lfilter_eq_LNil";
-
-
-Goal "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 1);
-by (Blast_tac 1);
-qed_spec_mp "lfilter_eq_LCons";
-
-
-Goal "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 2);
-by (blast_tac (claset() addSEs [Domain_findRelE]
- addIs [findRel_imp_lfilter]) 1);
-qed "lfilter_cases";
-
-
-(*** lfilter: simple facts by coinduction ***)
-
-Goal "lfilter (%x. True) l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lfilter_K_True";
-
-Goal "lfilter p (lfilter p l) = lfilter p l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-by Safe_tac;
-(*Cases: p x is true or false*)
-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 "(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 "(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 "(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 "(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 "(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);
-by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
-qed_spec_mp "findRel_conj_lfilter";
-
-
-
-Goal "(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 2);
-by (etac Domain_findRelE 1);
-(*case q x*)
-by (case_tac "p x" 1);
-by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
-(*case q x and ~(p x) *)
-by (Asm_simp_tac 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 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 1);
-val lemma = result();
-
-
-Goal "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);
-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 "(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 "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 "(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 "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);
-by Safe_tac;
-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 2);
-by (etac Domain_findRelE 1);
-by (ftac lmap_LCons_findRel 1);
-by (Clarify_tac 1);
-by (Asm_simp_tac 1);
-qed "lfilter_lmap";
--- a/src/HOL/Induct/LFilter.thy Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/LFilter.thy Tue Apr 02 14:28:28 2002 +0200
@@ -2,28 +2,271 @@
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 +
+header {*The "filter" functional for coinductive lists
+ --defined by a combination of induction and coinduction*}
+
+theory LFilter = LList:
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"
+ intros
+ found: "p x ==> (LCons x l, LCons x l) \<in> findRel p"
+ seek: "[| ~p x; (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
+
+declare findRel.intros [intro]
constdefs
- find :: ['a => bool, 'a llist] => 'a llist
+ 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 :: "['a => bool, 'a llist] => 'a llist"
"lfilter p l == llist_corec l (%l. case find p l of
LNil => None
| LCons y z => Some(y,z))"
+
+subsection {* findRel: basic laws *}
+
+inductive_cases
+ findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
+
+
+lemma findRel_functional [rule_format]:
+ "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"
+by (erule findRel.induct, auto)
+
+lemma findRel_imp_LCons [rule_format]:
+ "(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x"
+by (erule findRel.induct, auto)
+
+lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R"
+by (blast elim: findRel.cases)
+
+
+subsection {* Properties of Domain (findRel p) *}
+
+lemma LCons_Domain_findRel [simp]:
+ "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
+by auto
+
+lemma Domain_findRel_iff:
+ "(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p & p x)"
+by (blast dest: findRel_imp_LCons)
+
+lemma Domain_findRel_mono:
+ "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"
+apply clarify
+apply (erule findRel.induct, blast+)
+done
+
+
+subsection {* find: basic equations *}
+
+lemma find_LNil [simp]: "find p LNil = LNil"
+by (unfold find_def, blast)
+
+lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'"
+apply (unfold find_def)
+apply (blast dest: findRel_functional)
+done
+
+lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l"
+by (blast intro: findRel_imp_find)
+
+lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil"
+by (unfold find_def, blast)
+
+lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l"
+apply (case_tac "LCons x l \<in> Domain (findRel p) ")
+ apply auto
+apply (blast intro: findRel_imp_find)
+done
+
+lemma find_LCons [simp]:
+ "find p (LCons x l) = (if p x then LCons x l else find p l)"
+by (simp add: find_LCons_seek find_LCons_found)
+
+
+
+subsection {* lfilter: basic equations *}
+
+lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma diverge_lfilter_LNil [simp]:
+ "l ~: Domain(findRel p) ==> lfilter p l = LNil"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lfilter_LCons_found:
+ "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma findRel_imp_lfilter [simp]:
+ "(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')"
+by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
+apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
+apply (case_tac "LCons x l \<in> Domain (findRel p) ")
+ apply (simp add: Domain_findRel_iff, auto)
+done
+
+lemma lfilter_LCons [simp]:
+ "lfilter p (LCons x l) =
+ (if p x then LCons x (lfilter p l) else lfilter p l)"
+by (simp add: lfilter_LCons_found lfilter_LCons_seek)
+
+declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!]
+
+
+lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)"
+apply (auto iff: Domain_findRel_iff)
+apply (rotate_tac 1, simp)
+done
+
+lemma lfilter_eq_LCons [rule_format]:
+ "lfilter p l = LCons x l' -->
+ (\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)"
+apply (subst lfilter_def [THEN def_llist_corec])
+apply (case_tac "l \<in> Domain (findRel p) ")
+ apply (auto iff: Domain_findRel_iff)
+done
+
+
+lemma lfilter_cases: "lfilter p l = LNil |
+ (\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)"
+apply (case_tac "l \<in> Domain (findRel p) ")
+apply (auto iff: Domain_findRel_iff)
+done
+
+
+subsection {* lfilter: simple facts by coinduction *}
+
+lemma lfilter_K_True: "lfilter (%x. True) l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply safe
+txt{*Cases: p x is true or false*}
+apply (rule lfilter_cases [THEN disjE])
+ apply (erule ssubst, auto)
+done
+
+
+subsection {* Numerous lemmas required to prove @{text lfilter_conj} *}
+
+lemma findRel_conj_lemma [rule_format]:
+ "(l,l') \<in> findRel q
+ ==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)"
+by (erule findRel.induct, auto)
+
+lemmas findRel_conj = findRel_conj_lemma [OF _ refl]
+
+lemma findRel_not_conj_Domain [rule_format]:
+ "(l,l'') \<in> findRel (%x. p x & q x)
+ ==> (l, LCons x l') \<in> findRel q --> ~ p x -->
+ l' \<in> Domain (findRel (%x. p x & q x))"
+by (erule findRel.induct, auto)
+
+lemma findRel_conj2 [rule_format]:
+ "(l,lxx) \<in> findRel q
+ ==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x
+ --> (l,lz) \<in> findRel (%x. p x & q x)"
+by (erule findRel.induct, auto)
+
+lemma findRel_lfilter_Domain_conj [rule_format]:
+ "(lx,ly) \<in> findRel p
+ ==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))"
+apply (erule findRel.induct)
+ apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto)
+apply (drule sym [THEN lfilter_eq_LCons], auto)
+apply (drule spec)
+apply (drule refl [THEN rev_mp])
+apply (blast intro: findRel_conj2)
+done
+
+
+lemma findRel_conj_lfilter [rule_format]:
+ "(l,l'') \<in> findRel(%x. p x & q x)
+ ==> l'' = LCons y l' -->
+ (lfilter q l, LCons y (lfilter q l')) \<in> findRel p"
+by (erule findRel.induct, auto)
+
+lemma lfilter_conj_lemma:
+ "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)
+ \<in> llistD_Fun (range (%u. (lfilter p (lfilter q u),
+ lfilter (%x. p x & q x) u)))"
+apply (case_tac "l \<in> Domain (findRel q)")
+ apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
+ prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
+ txt{*There are no qs in l: both lists are LNil*}
+ apply (simp_all add: Domain_findRel_iff, clarify)
+txt{*case q x*}
+apply (case_tac "p x")
+ apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
+ txt{*case q x and ~(p x) *}
+apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
+ txt{*subcase: there is no p&q in l' and therefore none in l*}
+ apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
+ prefer 3 apply (blast intro: findRel_not_conj_Domain)
+ apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
+ prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
+ txt{* ...and therefore too, no p in lfilter q l'. Both results are Lnil*}
+ apply (simp_all add: Domain_findRel_iff, clarify)
+txt{*subcase: there is a p&q in l' and therefore also one in l*}
+apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
+ prefer 2 apply (blast intro: findRel_conj2)
+apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
+ apply simp
+apply (blast intro: findRel_conj_lfilter)
+done
+
+
+lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono])
+done
+
+
+subsection {* Numerous lemmas required to prove ??:
+ lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
+ *}
+
+lemma findRel_lmap_Domain:
+ "(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)"
+by (erule findRel.induct, auto)
+
+lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' -->
+ (\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"
+apply (subst lmap_def [THEN def_llist_corec])
+apply (rule_tac l = "l" in llistE, auto)
+done
+
+
+lemma lmap_LCons_findRel_lemma [rule_format]:
+ "(lx,ly) \<in> findRel p
+ ==> \<forall>l. lmap f l = lx --> ly = LCons x l' -->
+ (\<exists>y l''. x = f y & l' = lmap f l'' &
+ (l, LCons y l'') \<in> findRel(%x. p(f x)))"
+apply (erule findRel.induct, simp_all)
+apply (blast dest!: lmap_eq_LCons)+
+done
+
+lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl]
+
+lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+apply safe
+apply (case_tac "lmap f l \<in> Domain (findRel p)")
+ apply (simp add: Domain_findRel_iff, clarify)
+ apply (frule lmap_LCons_findRel, force)
+apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp)
+apply (blast intro: findRel_lmap_Domain)
+done
+
end
--- a/src/HOL/Induct/LList.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,876 +0,0 @@
-(* Title: HOL/Induct/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)?
-*)
-
-bind_thm ("UN1_I", UNIV_I RS UN_I);
-
-(** Simplification **)
-
-Addsplits [option.split];
-
-(*This justifies using llist in other recursive type definitions*)
-Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
-by (rtac gfp_mono 1);
-by (REPEAT (ares_tac basic_monos 1));
-qed "llist_mono";
-
-
-Goal "llist(A) = usum {Numb(0)} (uprod A (llist A))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in
-by (fast_tac (claset() addSIs (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 [list_Fun_def]
- "[| 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 [list_Fun_def, NIL_def] "NIL: list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_NIL_I";
-AddIffs [list_Fun_NIL_I];
-
-Goalw [list_Fun_def,CONS_def]
- "[| M: A; N: X |] ==> CONS M N : list_Fun A X";
-by (Fast_tac 1);
-qed "list_Fun_CONS_I";
-Addsimps [list_Fun_CONS_I];
-AddSIs [list_Fun_CONS_I];
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw (llist.defs @ [list_Fun_def])
- "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 [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";
-
-Goalw [CONS_def] "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'";
-by (REPEAT (ares_tac [In1_mono,Scons_mono] 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_corec_def]
- "LList_corec a f <= \
-\ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
-by (rtac UN_least 1);
-by (case_tac "k" 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono,
- UNIV_I RS UN_upper] 1));
-qed "LList_corec_subset1";
-
-Goalw [LList_corec_def]
- "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
-\ LList_corec a f";
-by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
-by Safe_tac;
-by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I));
-by (ALLGOALS Asm_simp_tac);
-qed "LList_corec_subset2";
-
-(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-Goal "LList_corec a f = \
-\ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
-by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
- LList_corec_subset2] 1));
-qed "LList_corec";
-
-(*definitional version of same*)
-val [rew] =
-Goal "[| !!x. h(x) == LList_corec x f |] \
-\ ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
-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_corec a f : llist UNIV";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Simp_tac 1);
-qed "LList_corec_type";
-
-
-(**** llist equality as a gfp; the bisimulation principle ****)
-
-(*This theorem is actually used, unlike the many similar ones in ZF*)
-Goal "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))";
-let val rew = rewrite_rule [NIL_def, CONS_def] in
-by (fast_tac (claset() addSIs (map rew LListD.intrs)
- addEs [rew LListD.elim]) 1)
-end;
-qed "LListD_unfold";
-
-Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
-by (induct_thm_tac nat_less_induct "k" 1);
-by (safe_tac (claset() delrules [equalityI]));
-by (etac LListD.elim 1);
-by (safe_tac (claset() delrules [equalityI]));
-by (case_tac "n" 1);
-by (Asm_simp_tac 1);
-by (rename_tac "n'" 1);
-by (case_tac "n'" 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
-qed "LListD_implies_ntrunc_equality";
-
-(*The domain of the LListD relation*)
-Goalw (llist.defs @ [NIL_def, CONS_def])
- "Domain (LListD(diag A)) <= llist(A)";
-by (rtac gfp_upperbound 1);
-(*avoids unfolding LListD on the rhs*)
-by (res_inst_tac [("P", "%x. Domain x <= ?B")] (LListD_unfold RS ssubst) 1);
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "Domain_LListD";
-
-(*This inclusion justifies the use of coinduction to show M=N*)
-Goal "LListD(diag A) <= diag(llist(A))";
-by (rtac subsetI 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by Safe_tac;
-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 (DomainI RS (Domain_LListD RS subsetD)) 1);
-qed "LListD_subset_diag";
-
-
-(** Coinduction, using LListD_Fun
- THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
- **)
-
-Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
-by (REPEAT (ares_tac basic_monos 1));
-qed "LListD_Fun_mono";
-
-Goalw [LListD_Fun_def]
- "[| 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 [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
-by (Fast_tac 1);
-qed "LListD_Fun_NIL_I";
-
-Goalw [LListD_Fun_def,CONS_def]
- "[| 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 (LListD.defs @ [LListD_Fun_def])
- "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 "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 "LListD(diag A) = diag(llist(A))";
-by (REPEAT (resolve_tac [equalityI, LListD_subset_diag,
- diag_subset_LListD] 1));
-qed "LListD_eq_diag";
-
-Goal "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 "[| (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;
-qed "LList_equalityI";
-
-
-(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
-
-(*We must remove Pair_eq because it may turn an instance of reflexivity
- (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction!
- (or strengthen the Solver?)
-*)
-Delsimps [Pair_eq];
-
-(*abstract proof using a bisimulation*)
-val [prem1,prem2] =
-Goal
- "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w)); \
-\ !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
-\ ==> h1=h2";
-by (rtac ext 1);
-(*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "UNIV"),
- ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac prem1 1);
-by (stac prem2 1);
-by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
- UNIV_I RS LListD_Fun_CONS_I]) 1);
-qed "LList_corec_unique";
-
-val [prem] =
-Goal
- "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
-\ ==> 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 [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
-by (rtac ntrunc_one_In1 1);
-qed "ntrunc_one_CONS";
-
-Goalw [CONS_def]
- "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
-by (Simp_tac 1);
-qed "ntrunc_CONS";
-
-Addsimps [ntrunc_one_CONS, ntrunc_CONS];
-
-
-val [prem1,prem2] =
-Goal
- "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w)); \
-\ !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
-\ ==> h1=h2";
-by (rtac (ntrunc_equality RS ext) 1);
-by (rename_tac "x k" 1);
-by (res_inst_tac [("x", "x")] spec 1);
-by (induct_thm_tac nat_less_induct "k" 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 1);
-by (strip_tac 1);
-by (case_tac "n" 1);
-by (rename_tac "m" 2);
-by (case_tac "m" 2);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
-result();
-
-
-(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
-
-Goal "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_unfold)));
-
-(*A typical use of co-induction to show membership in the gfp.
- The containing set is simply the singleton {Lconst(M)}. *)
-Goal "M:A ==> Lconst(M): llist(A)";
-by (rtac (singletonI RS llist_coinduct) 1);
-by Safe_tac;
-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 "Lconst(M) = LList_corec M (%x. Some(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 "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))";
-by (rtac (equals_LList_corec RS fun_cong) 1);
-by (Simp_tac 1);
-by (rtac (Lconst_fun_mono RS gfp_unfold) 1);
-qed "gfp_Lconst_eq_LList_corec";
-
-
-(*** Isomorphisms ***)
-
-Goal "inj Rep_LList";
-by (rtac inj_inverseI 1);
-by (rtac Rep_LList_inverse 1);
-qed "inj_Rep_LList";
-
-
-Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
-by (Asm_simp_tac 1);
-qed "LListI";
-
-Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
-by (Asm_simp_tac 1);
-qed "LListD";
-
-
-(** Distinctness of constructors **)
-
-Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
-by (stac (thm "Abs_LList_inject") 1);
-by (REPEAT (resolve_tac (llist.intrs @ [CONS_not_NIL, rangeI,
- LListI, Rep_LList RS LListD]) 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 [LNil_def] "Rep_LList LNil = NIL";
-by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
-qed "Rep_LList_LNil";
-
-Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
-by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
- rangeI, Rep_LList RS LListD] 1));
-qed "Rep_LList_LCons";
-
-(** Injectiveness of CONS and LCons **)
-
-Goalw [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
-by (fast_tac (claset() addSEs [Scons_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 RS LListD, LListI];
-AddIs llist.intrs;
-
-Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
-by (stac (thm "Abs_LList_inject") 1);
-by (auto_tac (claset(), simpset() addsimps [thm "Rep_LList_inject"]));
-qed "LCons_LCons_eq";
-
-AddIffs [LCons_LCons_eq];
-
-Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
-by (etac 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
- "[| 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 image_subsetI 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 "Lmap f NIL = NIL";
-by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lmap_NIL";
-
-Goal "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";
-
-Addsimps [Lmap_NIL, Lmap_CONS];
-
-(*Another type-checking proof by coinduction*)
-val [major,minor] =
-Goal "[| 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;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-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*)
-Goal "M: llist(A) ==> Lmap f M: llist(f`A)";
-by (etac Lmap_type 1);
-by (etac imageI 1);
-qed "Lmap_type2";
-
-(** Two easy results about Lmap **)
-
-Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
-by (dtac imageI 1);
-by (etac LList_equalityI 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
- rangeI RS LListD_Fun_CONS_I] 1));
-qed "Lmap_compose";
-
-Goal "M: llist(A) ==> Lmap (%x. x) M = M";
-by (dtac imageI 1);
-by (etac LList_equalityI 1);
-by Safe_tac;
-by (etac llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-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 [Lappend_def] "Lappend NIL NIL = NIL";
-by (rtac (LList_corec RS trans) 1);
-by (Simp_tac 1);
-qed "Lappend_NIL_NIL";
-
-Goalw [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 [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];
-
-
-Goal "M: llist(A) ==> Lappend NIL M = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL";
-
-Goal "M: llist(A) ==> Lappend M NIL = M";
-by (etac LList_fun_equalityI 1);
-by (ALLGOALS Asm_simp_tac);
-qed "Lappend_NIL2";
-
-Addsimps [Lappend_NIL, Lappend_NIL2];
-
-
-(** Alternative type-checking proofs for Lappend **)
-
-(*weak co-induction: bisimulation and case analysis on both variables*)
-Goal "[| 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;
-by (eres_inst_tac [("aa", "u")] llist.elim 1);
-by (eres_inst_tac [("aa", "v")] llist.elim 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-qed "Lappend_type";
-
-(*strong co-induction: bisimulation and case analysis on one variable*)
-Goal "[| 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 image_subsetI 1);
-by (eres_inst_tac [("aa", "x")] llist.elim 1);
-by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
-by (Asm_simp_tac 1);
-qed "Lappend_type";
-
-(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
-
-(** llist_case: case analysis for 'a llist **)
-
-Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
- Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
-
-Goalw [llist_case_def,LNil_def] "llist_case c d LNil = c";
-by (Simp_tac 1);
-qed "llist_case_LNil";
-
-Goalw [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 [NIL_def,CONS_def]
- "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P |] ==> P";
-by (rtac (Rep_LList RS LListD RS llist.elim) 1);
-by (asm_full_simp_tac
- (simpset() addsimps [Rep_LList_LNil RS sym, thm "Rep_LList_inject"]) 1);
-by (etac prem1 1);
-by (etac (LListI RS thm "Rep_LList_cases") 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac
- (simpset() addsimps [Rep_LList_LCons RS sym, thm "Rep_LList_inject"]) 1);
-by (etac prem2 1);
-qed "llistE";
-
-(** llist_corec: corecursion for 'a llist **)
-
-(*Lemma for the proof of llist_corec*)
-Goal "LList_corec a \
-\ (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
-\ llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Force_tac 1);
-qed "LList_corec_type2";
-
-Goalw [llist_corec_def,LNil_def,LCons_def]
- "llist_corec a f = \
-\ (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
-by (stac LList_corec 1);
-by (case_tac "f a" 1);
-by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
-qed "llist_corec";
-
-(*definitional version of same*)
-val [rew] =
-Goal "[| !!x. h(x) == llist_corec x f |] ==> \
-\ h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
-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 [LListD_Fun_def]
- "r <= (llist A) <*> (llist A) ==> \
-\ LListD_Fun (diag A) r <= (llist A) <*> (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_Times_llist";
-
-Goal "prod_fun Rep_LList Rep_LList ` r <= \
-\ (llist(range Leaf)) <*> (llist(range Leaf))";
-by (fast_tac (claset() delrules [image_subsetI]
- addIs [Rep_LList RS LListD]) 1);
-qed "subset_Times_llist";
-
-Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
-\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r";
-by Safe_tac;
-by (etac (subsetD RS SigmaE2) 1);
-by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
-qed "prod_fun_lemma";
-
-Goal "prod_fun Rep_LList Rep_LList ` range(%x. (x, x)) = \
-\ diag(llist(range Leaf))";
-by (rtac equalityI 1);
-by (Blast_tac 1);
-by (fast_tac (claset() delSWrapper "split_all_tac"
- addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
-qed "prod_fun_range_eq_diag";
-
-(*Used with lfilter*)
-Goalw [llistD_Fun_def, prod_fun_def]
- "A<=B ==> llistD_Fun A <= llistD_Fun B";
-by Auto_tac;
-by (rtac image_eqI 1);
-by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
-by (Force_tac 1);
-qed "llistD_Fun_mono";
-
-(** To show two llists are equal, exhibit a bisimulation!
- [also admits true equality] **)
-Goalw [llistD_Fun_def]
- "[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
-by (rtac (thm "Rep_LList_inject" RS iffD1) 1);
-by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList `r"),
- ("A", "range(Leaf)")]
- LList_equalityI 1);
-by (etac prod_fun_imageI 1);
-by (etac (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_Times_llist RS prod_fun_lemma) 1);
-by (rtac (subset_Times_llist RS Un_least) 1);
-by (rtac diag_subset_Times 1);
-qed "llist_equalityI";
-
-(** Rules to prove the 2nd premise of llist_equalityI **)
-Goalw [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";
-
-Goalw [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 (etac prod_fun_imageI 1);
-qed "llistD_Fun_LCons_I";
-
-(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw [llistD_Fun_def] "(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 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 "[| 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 "lmap f LNil = LNil";
-by (rtac (lmap_def RS def_llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lmap_LNil";
-
-Goal "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 "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 "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 "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 "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;
-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 "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 "nat_rec (LCons b l) (%m. lmap(f)) n = \
-\ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (induct_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 (induct_tac "n" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "fun_power_Suc";
-
-val Pair_cong = read_instantiate_sg (sign_of (theory "Product_Type"))
- [("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 "(!!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 (Clarify_tac 1);
-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 [lappend_def] "lappend LNil LNil = LNil";
-by (rtac (llist_corec RS trans) 1);
-by (Simp_tac 1);
-qed "lappend_LNil_LNil";
-
-Goalw [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 [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 "lappend LNil l = l";
-by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS Simp_tac);
-qed "lappend_LNil";
-
-Goal "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 "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;
-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 "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;
-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 "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 "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
-by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
-by (Simp_tac 1);
-by (Simp_tac 1);
-qed "lappend_assoc";
--- a/src/HOL/Induct/LList.thy Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/LList.thy Tue Apr 02 14:28:28 2002 +0200
@@ -1,13 +1,11 @@
-(* Title: HOL/LList.thy
+(* Title: HOL/Induct/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
+Still needs flatten function -- hard because it need
bounds on the amount of lookahead required.
Could try (but would it work for the gfp analogue of term?)
@@ -23,49 +21,53 @@
(UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
*)
-LList = Main + SList +
+header {*Definition of type 'a llist by a greatest fixed point*}
+
+theory LList = Main + SList:
consts
- llist :: 'a item set => 'a item set
- LListD :: "('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"
coinductive "llist(A)"
- intrs
- NIL_I "NIL: llist(A)"
- CONS_I "[| a: A; M: llist(A) |] ==> CONS a M : llist(A)"
+ intros
+ NIL_I: "NIL \<in> llist(A)"
+ CONS_I: "[| a \<in> A; M \<in> llist(A) |] ==> CONS a M \<in> 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)"
+ intros
+ NIL_I: "(NIL, NIL) \<in> LListD(r)"
+ CONS_I: "[| (a,b) \<in> r; (M,N) \<in> LListD(r) |]
+ ==> (CONS a M, CONS b N) \<in> LListD(r)"
typedef (LList)
- 'a llist = "llist(range Leaf) :: 'a item set" (llist.NIL_I)
+ 'a llist = "llist(range Leaf) :: 'a item set"
+ by (blast intro: llist.NIL_I)
constdefs
- (*Now used exclusively for abbreviating the coinduction rule*)
- list_Fun :: ['a item set, 'a item set] => 'a item set
- "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+ list_Fun :: "['a item set, 'a item set] => 'a item set"
+ --{*Now used exclusively for abbreviating the coinduction rule*}
+ "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
LListD_Fun ::
"[('a item * 'a item)set, ('a item * 'a item)set] =>
('a item * 'a item)set"
"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)}"
+ (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
- (*the abstract constructors*)
- LNil :: 'a llist
+ LNil :: "'a llist"
+ --{*abstract constructor*}
"LNil == Abs_LList NIL"
- LCons :: ['a, 'a llist] => 'a llist
+ LCons :: "['a, 'a llist] => 'a llist"
+ --{*abstract constructor*}
"LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
- llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
+ llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
"llist_case c d l ==
List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
@@ -77,7 +79,7 @@
k"
LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item"
- "LList_corec a f == UN k. LList_corec_fun k f a"
+ "LList_corec a f == \<Union>k. LList_corec_fun k f a"
llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist"
"llist_corec a f ==
@@ -93,41 +95,810 @@
-(*The case syntax for type 'a llist*)
+text{*The case syntax for type 'a llist*}
translations
"case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
-(** Sample function definitions. Item-based ones start with L ***)
+subsubsection{* Sample function definitions. Item-based ones start with L *}
constdefs
- Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ Lmap :: "('a item => 'b item) => ('a item => 'b item)"
"Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
- lmap :: ('a=>'b) => ('a llist => 'b llist)
+ lmap :: "('a=>'b) => ('a llist => 'b llist)"
"lmap f l == llist_corec l (%z. case z of LNil => None
| LCons y z => Some(f(y), z))"
- iterates :: ['a => 'a, 'a] => 'a llist
+ iterates :: "['a => 'a, 'a] => 'a llist"
"iterates f a == llist_corec a (%x. Some((x, f(x))))"
- Lconst :: 'a item => 'a item
- "Lconst(M) == lfp(%N. CONS M N)"
+ Lconst :: "'a item => 'a item"
+ "Lconst(M) == lfp(%N. CONS M N)"
-(*Append generates its result by applying f, where
- f((NIL,NIL)) = None
- f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2))
- f((CONS M1 M2, N)) = Some((M1, (M2,N))
-*)
-
- Lappend :: ['a item, 'a item] => 'a item
+ Lappend :: "['a item, 'a item] => 'a item"
"Lappend M N == LList_corec (M,N)
(split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
(%M1 M2 N. Some((M1, (M2,N))))))"
- lappend :: ['a llist, 'a llist] => 'a llist
+ lappend :: "['a llist, 'a llist] => 'a llist"
"lappend l n == llist_corec (l,n)
(split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
(%l1 l2 n. Some((l1, (l2,n))))))"
+
+text{*Append generates its result by applying f, where
+ f((NIL,NIL)) = None
+ f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2))
+ f((CONS M1 M2, N)) = Some((M1, (M2,N))
+*}
+
+text{*
+SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
+*}
+
+lemmas UN1_I = UNIV_I [THEN UN_I, standard]
+
+subsubsection{* Simplification *}
+
+declare option.split [split]
+
+text{*This justifies using llist in other recursive type definitions*}
+lemma llist_mono: "A<=B ==> llist(A) <= llist(B)"
+apply (unfold llist.defs )
+apply (rule gfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+
+lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))"
+ by (fast intro!: llist.intros [unfolded NIL_def CONS_def]
+ elim: llist.cases [unfolded NIL_def CONS_def])
+
+
+subsection{* Type checking by coinduction, using list_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+*}
+
+lemma llist_coinduct:
+ "[| M \<in> X; X <= list_Fun A (X Un llist(A)) |] ==> M \<in> llist(A)"
+apply (unfold list_Fun_def)
+apply (erule llist.coinduct)
+apply (erule subsetD [THEN CollectD], assumption)
+done
+
+lemma list_Fun_NIL_I [iff]: "NIL \<in> list_Fun A X"
+by (unfold list_Fun_def NIL_def, fast)
+
+lemma list_Fun_CONS_I [intro!,simp]:
+ "[| M \<in> A; N \<in> X |] ==> CONS M N \<in> list_Fun A X"
+apply (unfold list_Fun_def CONS_def, fast)
+done
+
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
+apply (unfold llist.defs list_Fun_def)
+apply (rule gfp_fun_UnI2)
+apply (rule monoI, blast)
+apply assumption
+done
+
+subsection{* LList_corec satisfies the desired recurion equation *}
+
+text{*A continuity result?*}
+lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
+apply (unfold CONS_def)
+apply (simp add: In1_UN1 Scons_UN1_y)
+done
+
+lemma CONS_mono: "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'"
+apply (unfold CONS_def)
+apply (assumption | rule In1_mono Scons_mono)+
+done
+
+declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
+ LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
+
+subsubsection{* The directions of the equality are proved separately *}
+
+lemma LList_corec_subset1:
+ "LList_corec a f <=
+ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
+apply (unfold LList_corec_def)
+apply (rule UN_least)
+apply (case_tac "k")
+apply (simp_all (no_asm_simp))
+apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
+done
+
+lemma LList_corec_subset2:
+ "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <=
+ LList_corec a f"
+apply (unfold LList_corec_def)
+apply (simp add: CONS_UN1, safe)
+apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+
+done
+
+text{*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*}
+lemma LList_corec:
+ "LList_corec a f =
+ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
+by (rule equalityI LList_corec_subset1 LList_corec_subset2)+
+
+text{*definitional version of same*}
+lemma def_LList_corec:
+ "[| !!x. h(x) == LList_corec x f |]
+ ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
+by (simp add: LList_corec)
+
+text{*A typical use of co-induction to show membership in the gfp.
+ Bisimulation is range(%x. LList_corec x f) *}
+lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
+apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
+apply (rule rangeI, safe)
+apply (subst LList_corec, simp)
+done
+
+
+subsection{* llist equality as a gfp; the bisimulation principle *}
+
+text{*This theorem is actually used, unlike the many similar ones in ZF*}
+lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
+ by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
+ elim: LListD.cases [unfolded NIL_def CONS_def])
+
+lemma LListD_implies_ntrunc_equality [rule_format]:
+ "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
+apply (induct_tac "k" rule: nat_less_induct)
+apply (safe del: equalityI)
+apply (erule LListD.cases)
+apply (safe del: equalityI)
+apply (case_tac "n", simp)
+apply (rename_tac "n'")
+apply (case_tac "n'")
+apply (simp_all add: CONS_def less_Suc_eq)
+done
+
+text{*The domain of the LListD relation*}
+lemma Domain_LListD:
+ "Domain (LListD(diag A)) <= llist(A)"
+apply (unfold llist.defs NIL_def CONS_def)
+apply (rule gfp_upperbound)
+txt{*avoids unfolding LListD on the rhs*}
+apply (rule_tac P = "%x. Domain x <= ?B" in LListD_unfold [THEN ssubst], simp)
+apply blast
+done
+
+text{*This inclusion justifies the use of coinduction to show M=N*}
+lemma LListD_subset_diag: "LListD(diag A) <= diag(llist(A))"
+apply (rule subsetI)
+apply (rule_tac p = "x" in PairE, safe)
+apply (rule diag_eqI)
+apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption)
+apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
+done
+
+
+subsubsection{* Coinduction, using LListD_Fun
+ THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
+ *}
+
+lemma LListD_Fun_mono: "A<=B ==> LListD_Fun r A <= LListD_Fun r B"
+apply (unfold LListD_Fun_def)
+apply (assumption | rule basic_monos)+
+done
+
+lemma LListD_coinduct:
+ "[| M \<in> X; X <= LListD_Fun r (X Un LListD(r)) |] ==> M \<in> LListD(r)"
+apply (unfold LListD_Fun_def)
+apply (erule LListD.coinduct)
+apply (erule subsetD [THEN CollectD], assumption)
+done
+
+lemma LListD_Fun_NIL_I: "(NIL,NIL) \<in> LListD_Fun r s"
+by (unfold LListD_Fun_def NIL_def, fast)
+
+lemma LListD_Fun_CONS_I:
+ "[| x\<in>A; (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
+apply (unfold LListD_Fun_def CONS_def, blast)
+done
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma LListD_Fun_LListD_I:
+ "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
+apply (unfold LListD.defs LListD_Fun_def)
+apply (rule gfp_fun_UnI2)
+apply (rule monoI, blast)
+apply assumption
+done
+
+
+text{*This converse inclusion helps to strengthen LList_equalityI*}
+lemma diag_subset_LListD: "diag(llist(A)) <= LListD(diag A)"
+apply (rule subsetI)
+apply (erule LListD_coinduct)
+apply (rule subsetI)
+apply (erule diagE)
+apply (erule ssubst)
+apply (erule llist.cases)
+apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
+done
+
+lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
+apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
+done
+
+lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
+apply (rule LListD_eq_diag [THEN subst])
+apply (rule LListD_Fun_LListD_I)
+apply (simp add: LListD_eq_diag diagI)
+done
+
+
+subsubsection{* To show two LLists are equal, exhibit a bisimulation!
+ [also admits true equality]
+ Replace "A" by some particular set, like {x.True}??? *}
+lemma LList_equalityI:
+ "[| (M,N) \<in> r; r <= LListD_Fun (diag A) (r Un diag(llist(A))) |]
+ ==> M=N"
+apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
+apply (erule LListD_coinduct)
+apply (simp add: LListD_eq_diag, safe)
+done
+
+
+subsection{* Finality of llist(A): Uniqueness of functions defined by corecursion *}
+
+text{*We must remove Pair_eq because it may turn an instance of reflexivity
+ (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction!
+ (or strengthen the Solver?)
+*}
+declare Pair_eq [simp del]
+
+text{*abstract proof using a bisimulation*}
+lemma LList_corec_unique:
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));
+ !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]
+ ==> h1=h2"
+apply (rule ext)
+txt{*next step avoids an unknown (and flexflex pair) in simplification*}
+apply (rule_tac A = "UNIV" and r = "range(%u. (h1 u, h2 u))"
+ in LList_equalityI)
+apply (rule rangeI, safe)
+apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I])
+done
+
+lemma equals_LList_corec:
+ "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |]
+ ==> h = (%x. LList_corec x f)"
+by (simp add: LList_corec_unique LList_corec)
+
+
+subsubsection{*Obsolete proof of @{text LList_corec_unique}:
+ complete induction, not coinduction *}
+
+lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}"
+by (simp add: CONS_def ntrunc_one_In1)
+
+lemma ntrunc_CONS [simp]:
+ "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"
+by (simp add: CONS_def)
+
+
+lemma
+ assumes prem1:
+ "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))"
+ and prem2:
+ "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))"
+ shows "h1=h2"
+apply (rule ntrunc_equality [THEN ext])
+apply (rule_tac x = "x" in spec)
+apply (induct_tac "k" rule: nat_less_induct)
+apply (rename_tac "n")
+apply (rule allI)
+apply (subst prem1)
+apply (subst prem2, simp)
+apply (intro strip)
+apply (case_tac "n")
+apply (rename_tac [2] "m")
+apply (case_tac [2] "m")
+apply simp_all
+done
+
+
+subsection{*Lconst: defined directly by lfp *}
+
+text{*But it could be defined by corecursion.*}
+
+lemma Lconst_fun_mono: "mono(CONS(M))"
+apply (rule monoI subset_refl CONS_mono)+
+apply assumption
+done
+
+text{* Lconst(M) = CONS M (Lconst M) *}
+lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
+
+text{*A typical use of co-induction to show membership in the gfp.
+ The containing set is simply the singleton {Lconst(M)}. *}
+lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
+apply (rule singletonI [THEN llist_coinduct], safe)
+apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
+apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+
+done
+
+lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))"
+apply (rule equals_LList_corec [THEN fun_cong], simp)
+apply (rule Lconst)
+done
+
+text{*Thus we could have used gfp in the definition of Lconst*}
+lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))"
+apply (rule equals_LList_corec [THEN fun_cong], simp)
+apply (rule Lconst_fun_mono [THEN gfp_unfold])
+done
+
+
+subsection{* Isomorphisms *}
+
+lemma inj_Rep_LList: "inj Rep_LList"
+apply (rule inj_inverseI)
+apply (rule Rep_LList_inverse)
+done
+
+
+lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
+by (unfold LList_def, simp)
+
+lemma LListD: "x \<in> LList ==> x \<in> llist (range Leaf)"
+by (unfold LList_def, simp)
+
+
+subsubsection{* Distinctness of constructors *}
+
+lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil"
+apply (unfold LNil_def LCons_def)
+apply (subst Abs_LList_inject)
+apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+
+done
+
+lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard]
+
+
+subsubsection{* llist constructors *}
+
+lemma Rep_LList_LNil: "Rep_LList LNil = NIL"
+apply (unfold LNil_def)
+apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse])
+done
+
+lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"
+apply (unfold LCons_def)
+apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse]
+ rangeI Rep_LList [THEN LListD])+
+done
+
+subsubsection{* Injectiveness of CONS and LCons *}
+
+lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
+apply (unfold CONS_def)
+apply (fast elim!: Scons_inject)
+done
+
+lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard]
+
+
+text{*For reasoning about abstract llist constructors*}
+
+declare Rep_LList [THEN LListD, intro] LListI [intro]
+declare llist.intros [intro]
+
+lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)"
+apply (unfold LCons_def)
+apply (subst Abs_LList_inject)
+apply (auto simp add: Rep_LList_inject)
+done
+
+lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
+apply (erule llist.cases)
+apply (erule CONS_neq_NIL, fast)
+done
+
+
+subsection{* Reasoning about llist(A) *}
+
+text{*A special case of list_equality for functions over lazy lists*}
+lemma LList_fun_equalityI:
+ "[| M \<in> llist(A); g(NIL): llist(A);
+ f(NIL)=g(NIL);
+ !!x l. [| x\<in>A; l \<in> llist(A) |] ==>
+ (f(CONS x l),g(CONS x l)) \<in>
+ LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un
+ diag(llist(A)))
+ |] ==> f(M) = g(M)"
+apply (rule LList_equalityI)
+apply (erule imageI)
+apply (rule image_subsetI)
+apply (erule_tac aa=x in llist.cases)
+apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast)
+done
+
+
+subsection{* The functional "Lmap" *}
+
+lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
+by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
+
+lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
+by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
+
+
+
+text{*Another type-checking proof by coinduction*}
+lemma Lmap_type:
+ "[| M \<in> llist(A); !!x. x\<in>A ==> f(x):B |] ==> Lmap f M \<in> llist(B)"
+apply (erule imageI [THEN llist_coinduct], safe)
+apply (erule llist.cases, simp_all)
+done
+
+text{*This type checking rule synthesises a sufficiently large set for f*}
+lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
+apply (erule Lmap_type)
+apply (erule imageI)
+done
+
+subsubsection{* Two easy results about Lmap *}
+
+lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
+apply (unfold o_def)
+apply (drule imageI)
+apply (erule LList_equalityI, safe)
+apply (erule llist.cases, simp_all)
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply assumption
+done
+
+lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
+apply (drule imageI)
+apply (erule LList_equalityI, safe)
+apply (erule llist.cases, simp_all)
+apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
+apply assumption
+done
+
+
+subsection{* Lappend -- its two arguments cause some complications! *}
+
+lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+lemma Lappend_NIL_CONS [simp]:
+ "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+lemma Lappend_CONS [simp]:
+ "Lappend (CONS M M') N = CONS M (Lappend M' N)"
+apply (unfold Lappend_def)
+apply (rule LList_corec [THEN trans], simp)
+done
+
+declare llist.intros [simp] LListD_Fun_CONS_I [simp]
+ range_eqI [simp] image_eqI [simp]
+
+
+lemma Lappend_NIL [simp]: "M \<in> llist(A) ==> Lappend NIL M = M"
+by (erule LList_fun_equalityI, simp_all)
+
+lemma Lappend_NIL2: "M \<in> llist(A) ==> Lappend M NIL = M"
+by (erule LList_fun_equalityI, simp_all)
+
+
+subsubsection{* Alternative type-checking proofs for Lappend *}
+
+text{*weak co-induction: bisimulation and case analysis on both variables*}
+lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct)
+apply fast
+apply safe
+apply (erule_tac aa = "u" in llist.cases)
+apply (erule_tac aa = "v" in llist.cases, simp_all)
+apply blast
+done
+
+text{*strong co-induction: bisimulation and case analysis on one variable*}
+lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
+apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
+apply (erule imageI)
+apply (rule image_subsetI)
+apply (erule_tac aa = "x" in llist.cases)
+apply (simp add: list_Fun_llist_I, simp)
+done
+
+subsection{* Lazy lists as the type 'a llist -- strongly typed versions of above *}
+
+subsubsection{* llist_case: case analysis for 'a llist *}
+
+declare LListI [THEN Abs_LList_inverse, simp]
+declare Rep_LList_inverse [simp]
+declare Rep_LList [THEN LListD, simp]
+declare rangeI [simp] inj_Leaf [simp]
+
+lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
+by (unfold llist_case_def LNil_def, simp)
+
+lemma llist_case_LCons [simp]:
+ "llist_case c d (LCons M N) = d M N"
+apply (unfold llist_case_def LCons_def, simp)
+done
+
+text{*Elimination is case analysis, not induction.*}
+lemma llistE: "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P |] ==> P"
+apply (rule Rep_LList [THEN LListD, THEN llist.cases])
+ apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject)
+ apply blast
+apply (erule LListI [THEN Rep_LList_cases], clarify)
+apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast)
+done
+
+subsubsection{* llist_corec: corecursion for 'a llist *}
+
+text{*Lemma for the proof of llist_corec*}
+lemma LList_corec_type2:
+ "LList_corec a
+ (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w))
+ \<in> llist(range Leaf)"
+apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
+apply (rule rangeI, safe)
+apply (subst LList_corec, force)
+done
+
+lemma llist_corec:
+ "llist_corec a f =
+ (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
+apply (unfold llist_corec_def LNil_def LCons_def)
+apply (subst LList_corec)
+apply (case_tac "f a")
+apply (simp add: LList_corec_type2)
+apply (force simp add: LList_corec_type2)
+done
+
+text{*definitional version of same*}
+lemma def_llist_corec:
+ "[| !!x. h(x) == llist_corec x f |] ==>
+ h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
+by (simp add: llist_corec)
+
+subsection{* Proofs about type 'a llist functions *}
+
+subsection{* Deriving llist_equalityI -- llist equality is a bisimulation *}
+
+lemma LListD_Fun_subset_Times_llist:
+ "r <= (llist A) <*> (llist A) ==>
+ LListD_Fun (diag A) r <= (llist A) <*> (llist A)"
+apply (unfold LListD_Fun_def)
+apply (subst llist_unfold)
+apply (simp add: NIL_def CONS_def, fast)
+done
+
+lemma subset_Times_llist:
+ "prod_fun Rep_LList Rep_LList ` r <=
+ (llist(range Leaf)) <*> (llist(range Leaf))"
+by (blast intro: Rep_LList [THEN LListD])
+
+lemma prod_fun_lemma:
+ "r <= (llist(range Leaf)) <*> (llist(range Leaf))
+ ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r"
+apply safe
+apply (erule subsetD [THEN SigmaE2], assumption)
+apply (simp add: LListI [THEN Abs_LList_inverse])
+done
+
+lemma prod_fun_range_eq_diag:
+ "prod_fun Rep_LList Rep_LList ` range(%x. (x, x)) =
+ diag(llist(range Leaf))"
+apply (rule equalityI, blast)
+apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
+done
+
+text{*Used with lfilter*}
+lemma llistD_Fun_mono:
+ "A<=B ==> llistD_Fun A <= llistD_Fun B"
+apply (unfold llistD_Fun_def prod_fun_def, auto)
+apply (rule image_eqI)
+ prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force)
+done
+
+subsubsection{* To show two llists are equal, exhibit a bisimulation!
+ [also admits true equality] *}
+lemma llist_equalityI:
+ "[| (l1,l2) \<in> r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"
+apply (unfold llistD_Fun_def)
+apply (rule Rep_LList_inject [THEN iffD1])
+apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf) " in LList_equalityI)
+apply (erule prod_fun_imageI)
+apply (erule image_mono [THEN subset_trans])
+apply (rule image_compose [THEN subst])
+apply (rule prod_fun_compose [THEN subst])
+apply (subst image_Un)
+apply (subst prod_fun_range_eq_diag)
+apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
+apply (rule subset_Times_llist [THEN Un_least])
+apply (rule diag_subset_Times)
+done
+
+subsubsection{* Rules to prove the 2nd premise of llist_equalityI *}
+lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
+apply (unfold llistD_Fun_def LNil_def)
+apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
+done
+
+lemma llistD_Fun_LCons_I [simp]:
+ "(l1,l2):r ==> (LCons x l1, LCons x l2) \<in> llistD_Fun(r)"
+apply (unfold llistD_Fun_def LCons_def)
+apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI])
+apply (erule prod_fun_imageI)
+done
+
+text{*Utilise the "strong" part, i.e. gfp(f)*}
+lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
+apply (unfold llistD_Fun_def)
+apply (rule Rep_LList_inverse [THEN subst])
+apply (rule prod_fun_imageI)
+apply (subst image_Un)
+apply (subst prod_fun_range_eq_diag)
+apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
+done
+
+text{*A special case of list_equality for functions over lazy lists*}
+lemma llist_fun_equalityI:
+ "[| f(LNil)=g(LNil);
+ !!x l. (f(LCons x l),g(LCons x l))
+ \<in> llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))
+ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"
+apply (rule_tac r = "range (%u. (f (u),g (u))) " in llist_equalityI)
+apply (rule rangeI, clarify)
+apply (rule_tac l = "u" in llistE)
+apply (simp_all add: llistD_Fun_range_I)
+done
+
+
+subsection{* The functional "lmap" *}
+
+lemma lmap_LNil [simp]: "lmap f LNil = LNil"
+by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
+by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
+
+
+subsubsection{* Two easy results about lmap *}
+
+lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lmap_ident [simp]: "lmap (%x. x) l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+
+subsection{* iterates -- llist_fun_equalityI cannot be used! *}
+
+lemma iterates: "iterates f x = LCons x (iterates f (f x))"
+by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
+
+lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
+apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u))) " in llist_equalityI)
+apply (rule rangeI, safe)
+apply (rule_tac x1 = "f (u) " in iterates [THEN ssubst])
+apply (rule_tac x1 = "u" in iterates [THEN ssubst], simp)
+done
+
+lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
+apply (subst lmap_iterates)
+apply (rule iterates)
+done
+
+subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
+
+subsubsection{* Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) *}
+
+lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =
+ LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
+apply (induct_tac "n", simp_all)
+done
+
+lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"
+by (induct_tac "n", simp_all)
+
+lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
+
+
+text{*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
+ for all u and all n::nat.*}
+lemma iterates_equality:
+ "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
+apply (rule ext)
+apply (rule_tac
+ r = "\<Union>u. range (%n. (nat_rec (h u) (%m y. lmap f y) n,
+ nat_rec (iterates f u) (%m y. lmap f y) n))"
+ in llist_equalityI)
+apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+
+apply clarify
+apply (subst iterates, atomize)
+apply (drule_tac x=u in spec)
+apply (erule ssubst)
+apply (subst fun_power_lmap)
+apply (subst fun_power_lmap)
+apply (rule llistD_Fun_LCons_I)
+apply (rule lmap_iterates [THEN subst])
+apply (subst fun_power_Suc)
+apply (subst fun_power_Suc, blast)
+done
+
+
+subsection{* lappend -- its two arguments cause some complications! *}
+
+lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LNil_LCons [simp]:
+ "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LCons [simp]:
+ "lappend (LCons l l') N = LCons l (lappend l' N)"
+apply (unfold lappend_def)
+apply (rule llist_corec [THEN trans], simp)
+done
+
+lemma lappend_LNil [simp]: "lappend LNil l = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+lemma lappend_LNil2 [simp]: "lappend l LNil = l"
+by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
+
+
+text{*The infinite first argument blocks the second*}
+lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x"
+apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))"
+ in llist_equalityI)
+apply (rule rangeI, safe)
+apply (subst iterates, simp)
+done
+
+subsubsection{* Two proofs that lmap distributes over lappend *}
+
+text{*Long proof requiring case analysis on both both arguments*}
+lemma lmap_lappend_distrib:
+ "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
+apply (rule_tac r = "\<Union>n. range (%l. (lmap f (lappend l n),
+ lappend (lmap f l) (lmap f n)))"
+ in llist_equalityI)
+apply (rule UN1_I)
+apply (rule rangeI, safe)
+apply (rule_tac l = "l" in llistE)
+apply (rule_tac l = "n" in llistE, simp_all)
+apply (blast intro: llistD_Fun_LCons_I)
+done
+
+text{*Shorter proof of theorem above using llist_equalityI as strong coinduction*}
+lemma lmap_lappend_distrib:
+ "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
+apply (rule_tac l = "l" in llist_fun_equalityI, simp)
+apply simp
+done
+
+text{*Without strong coinduction, three case analyses might be needed*}
+lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
+apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
+apply simp
+done
+
end
--- a/src/HOL/Induct/PropLog.ML Tue Apr 02 13:47:01 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,209 +0,0 @@
-(* Title: HOL/ex/pl.ML
- ID: $Id$
- Author: Tobias Nipkow & Lawrence C Paulson
- Copyright 1994 TU Muenchen & University of Cambridge
-
-Soundness and completeness of propositional logic w.r.t. truth-tables.
-
-Prove: If H|=p then G|=p where G:Fin(H)
-*)
-
-(** Monotonicity **)
-Goalw thms.defs "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 "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 "H |- q ==> H |- p->q";
-by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
-qed "weaken_right";
-
-(*The deduction theorem*)
-Goal "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));
-
-
-(*Soundness of the rules wrt truth-table semantics*)
-Goalw [sat_def] "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 "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 "hyps p tt |- (if tt[[p]] then p else p->false)";
-by (rtac (split_if RS iffD2) 1);
-by (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 (Simp_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 "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 "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-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 "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-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";
-
-Goal "finite(hyps p t)";
-by (induct_tac "p" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "hyps_finite";
-
-Goal "hyps p t <= (UN v. {#v, #v->false})";
-by (induct_tac "p" 1);
-by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
-qed "hyps_subset";
-
-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_subset RS (hyps_finite RS finite_subset_induct)) 1);
-by (simp_tac (simpset() addsimps [sat RS sat_thms_p]) 1);
-by Safe_tac;
-(*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 [sat_def] "insert p H |= q ==> H |= p->q";
-by (Simp_tac 1);
-by (Fast_tac 1);
-qed "sat_imp";
-
-Goal "finite H ==> !p. H |= p --> H |- p";
-by (etac finite_induct 1);
-by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
-by (rtac (weaken_left_insert RS thms.MP) 1);
-by (fast_tac ((claset_of Fun.thy) addSIs [sat_imp]) 1);
-by (Fast_tac 1);
-qed "completeness_lemma";
-
-val completeness = completeness_lemma RS spec RS mp;
-
-Goal "finite H ==> (H |- p) = (H |= p)";
-by (fast_tac (claset() addSEs [soundness, completeness]) 1);
-qed "syntax_iff_semantics";
--- a/src/HOL/Induct/PropLog.thy Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/PropLog.thy Tue Apr 02 14:28:28 2002 +0200
@@ -1,45 +1,276 @@
-(* Title: HOL/ex/PropLog.thy
+(* Title: HOL/Induct/PropLog.thy
ID: $Id$
Author: Tobias Nipkow
- Copyright 1994 TU Muenchen
-
-Inductive definition of propositional logic.
+ Copyright 1994 TU Muenchen & University of Cambridge
*)
-PropLog = Main +
+header {* Meta-theory of propositional logic *}
+
+theory PropLog = Main:
+
+text {*
+ Datatype definition of propositional logic formulae and inductive
+ definition of the propositional tautologies.
+
+ Inductive definition of propositional logic. Soundness and
+ completeness w.r.t.\ truth-tables.
+
+ Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
+ Fin(H)"}
+*}
+
+subsection {* The datatype of propositions *}
datatype
- 'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
+ 'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
+
+subsection {* The proof system *}
+
consts
- thms :: 'a pl set => 'a pl set
- "|-" :: ['a pl set, 'a pl] => bool (infixl 50)
- "|=" :: ['a pl set, 'a pl] => bool (infixl 50)
- eval :: ['a set, 'a pl] => bool ("_[[_]]" [100,0] 100)
- hyps :: ['a pl, 'a set] => 'a pl set
+ thms :: "'a pl set => 'a pl set"
+ "|-" :: "['a pl set, 'a pl] => bool" (infixl 50)
translations
- "H |- p" == "p : thms(H)"
+ "H |- p" == "p \<in> 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"
+ intros
+ H [intro]: "p\<in>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"
+
+subsection {* The semantics *}
+
+subsubsection {* Semantics of propositional logic. *}
-defs
- sat_def "H |= p == (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
+consts
+ eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100)
+
+primrec "tt[[false]] = False"
+ "tt[[#v]] = (v \<in> tt)"
+ eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
-primrec
- "tt[[false]] = False"
- "tt[[#v]] = (v:tt)"
-eval_imp "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
+text {*
+ A finite set of hypotheses from @{text t} and the @{text Var}s in
+ @{text p}.
+*}
+
+consts
+ hyps :: "['a pl, 'a set] => 'a pl set"
primrec
"hyps false tt = {}"
- "hyps (#v) tt = {if v:tt then #v else #v->false}"
+ "hyps (#v) tt = {if v \<in> tt then #v else #v->false}"
"hyps (p->q) tt = hyps p tt Un hyps q tt"
+subsubsection {* Logical consequence *}
+
+text {*
+ For every valuation, if all elements of @{text H} are true then so
+ is @{text p}.
+*}
+
+constdefs
+ sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50)
+ "H |= p == (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
+
+
+subsection {* Proof theory of propositional logic *}
+
+lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
+apply (unfold thms.defs )
+apply (rule lfp_mono)
+apply (assumption | rule basic_monos)+
+done
+
+lemma thms_I: "H |- p->p"
+ -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
+by (best intro: thms.K thms.S thms.MP)
+
+
+subsubsection {* Weakening, left and right *}
+
+lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p"
+ -- {* Order of premises is convenient with @{text THEN} *}
+ by (erule thms_mono [THEN subsetD])
+
+lemmas weaken_left_insert = subset_insertI [THEN weaken_left]
+
+lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left]
+lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left]
+
+lemma weaken_right: "H |- q ==> H |- p->q"
+by (fast intro: thms.K thms.MP)
+
+
+subsubsection {* The deduction theorem *}
+
+theorem deduction: "insert p H |- q ==> H |- p->q"
+apply (erule thms.induct)
+apply (fast intro: thms_I thms.H thms.K thms.S thms.DN
+ thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
+done
+
+
+subsubsection {* The cut rule *}
+
+lemmas cut = deduction [THEN thms.MP]
+
+lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
+
+lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
+
+
+subsubsection {* Soundness of the rules wrt truth-table semantics *}
+
+theorem soundness: "H |- p ==> H |= p"
+apply (unfold sat_def)
+apply (erule thms.induct, auto)
+done
+
+subsection {* Completeness *}
+
+subsubsection {* Towards the completeness proof *}
+
+lemma false_imp: "H |- p->false ==> H |- p->q"
+apply (rule deduction)
+apply (erule weaken_left_insert [THEN thms_notE])
+apply blast
+done
+
+lemma imp_false:
+ "[| H |- p; H |- q->false |] ==> H |- (p->q)->false"
+apply (rule deduction)
+apply (blast intro: weaken_left_insert thms.MP thms.H)
+done
+
+lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
+ -- {* Typical example of strengthening the induction statement. *}
+apply simp
+apply (induct_tac "p")
+apply (simp_all add: thms_I thms.H)
+apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
+ imp_false false_imp)
+done
+
+lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
+ -- {* Key lemma for completeness; yields a set of assumptions
+ satisfying @{text p} *}
+apply (unfold sat_def)
+apply (drule spec, erule mp [THEN if_P, THEN subst],
+ rule_tac [2] hyps_thms_if, simp)
+done
+
+text {*
+ For proving certain theorems in our new propositional logic.
+*}
+
+declare deduction [intro!]
+declare thms.H [THEN thms.MP, intro]
+
+text {*
+ The excluded middle in the form of an elimination rule.
+*}
+
+lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
+apply (rule deduction [THEN deduction])
+apply (rule thms.DN [THEN thms.MP], best)
+done
+
+lemma thms_excluded_middle_rule:
+ "[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q"
+ -- {* Hard to prove directly because it requires cuts *}
+by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)
+
+
+subsection{* Completeness -- lemmas for reducing the set of assumptions*}
+
+text {*
+ For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
+ "hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
+*}
+
+lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
+by (induct_tac "p", auto)
+
+text {*
+ For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
+ @{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
+*}
+
+lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
+by (induct_tac "p", auto)
+
+text {* Two lemmas for use with @{text weaken_left} *}
+
+lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
+by fast
+
+lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
+by fast
+
+text {*
+ The set @{term "hyps p t"} is finite, and elements have the form
+ @{term "#v"} or @{term "#v->Fls"}.
+*}
+
+lemma hyps_finite: "finite(hyps p t)"
+by (induct_tac "p", auto)
+
+lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
+by (induct_tac "p", auto)
+
+lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
+
+subsubsection {* Completeness theorem *}
+
+text {*
+ Induction on the finite set of assumptions @{term "hyps p t0"}. We
+ may repeatedly subtract assumptions until none are left!
+*}
+
+lemma completeness_0_lemma:
+ "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p"
+apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
+ apply (simp add: sat_thms_p, safe)
+(*Case hyps p t-insert(#v,Y) |- p *)
+ apply (rule thms_excluded_middle_rule)
+ apply (rule insert_Diff_same [THEN weaken_left])
+ apply (erule spec)
+ apply (rule insert_Diff_subset2 [THEN weaken_left])
+ apply (rule hyps_Diff [THEN Diff_weaken_left])
+ apply (erule spec)
+(*Case hyps p t-insert(#v -> false,Y) |- p *)
+apply (rule thms_excluded_middle_rule)
+ apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
+ apply (erule_tac [2] spec)
+apply (rule insert_Diff_subset2 [THEN weaken_left])
+apply (rule hyps_insert [THEN Diff_weaken_left])
+apply (erule spec)
+done
+
+text{*The base case for completeness*}
+lemma completeness_0: "{} |= p ==> {} |- p"
+apply (rule Diff_cancel [THEN subst])
+apply (erule completeness_0_lemma [THEN spec])
+done
+
+text{*A semantic analogue of the Deduction Theorem*}
+lemma sat_imp: "insert p H |= q ==> H |= p->q"
+by (unfold sat_def, auto)
+
+theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
+apply (erule finite_induct)
+apply (safe intro!: completeness_0)
+apply (drule sat_imp)
+apply (drule spec)
+apply (blast intro: weaken_left_insert [THEN thms.MP])
+done
+
+theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
+by (fast elim!: soundness completeness)
+
end
--- a/src/HOL/Induct/ROOT.ML Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/Induct/ROOT.ML Tue Apr 02 14:28:28 2002 +0200
@@ -9,4 +9,3 @@
time_use_thy "PropLog";
time_use_thy "SList";
time_use_thy "LFilter";
-time_use_thy "Exp";
--- a/src/HOL/IsaMakefile Tue Apr 02 13:47:01 2002 +0200
+++ b/src/HOL/IsaMakefile Tue Apr 02 14:28:28 2002 +0200
@@ -220,10 +220,9 @@
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
$(LOG)/HOL-Induct.gz: $(OUT)/HOL \
- Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
- Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
- Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
- Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
+ Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
+ Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
+ Induct/PropLog.thy Induct/ROOT.ML \
Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
Induct/Tree.thy Induct/document/root.tex