conversion of some HOL/Induct proof scripts to Isar
authorpaulson
Tue Apr 02 14:28:28 2002 +0200 (2002-04-02)
changeset 13075d3e1d554cd6d
parent 13074 96bf406fd3e5
child 13076 70704dd48bd5
conversion of some HOL/Induct proof scripts to Isar
src/HOL/Induct/Com.ML
src/HOL/Induct/Com.thy
src/HOL/Induct/Comb.ML
src/HOL/Induct/Comb.thy
src/HOL/Induct/Exp.ML
src/HOL/Induct/Exp.thy
src/HOL/Induct/LFilter.ML
src/HOL/Induct/LFilter.thy
src/HOL/Induct/LList.ML
src/HOL/Induct/LList.thy
src/HOL/Induct/PropLog.ML
src/HOL/Induct/PropLog.thy
src/HOL/Induct/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Induct/Com.ML	Tue Apr 02 13:47:01 2002 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,44 +0,0 @@
     1.4 -(*  Title:      HOL/Induct/Com
     1.5 -    ID:         $Id$
     1.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1997  University of Cambridge
     1.8 -
     1.9 -Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    1.10 -*)
    1.11 -
    1.12 -AddIs exec.intrs;
    1.13 -
    1.14 -val exec_elim_cases = 
    1.15 -    map exec.mk_cases
    1.16 -       ["(SKIP,s) -[eval]-> t",
    1.17 -	"(x:=a,s) -[eval]-> t", 
    1.18 -	"(c1;;c2, s) -[eval]-> t",
    1.19 -	"(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
    1.20 -
    1.21 -val exec_WHILE_case = exec.mk_cases "(WHILE b DO c,s) -[eval]-> t";
    1.22 -
    1.23 -AddSEs exec_elim_cases;
    1.24 -
    1.25 -(*This theorem justifies using "exec" in the inductive definition of "eval"*)
    1.26 -Goalw exec.defs "A<=B ==> exec(A) <= exec(B)";
    1.27 -by (rtac lfp_mono 1);
    1.28 -by (REPEAT (ares_tac basic_monos 1));
    1.29 -qed "exec_mono";
    1.30 -
    1.31 -
    1.32 -Unify.trace_bound := 30;
    1.33 -Unify.search_bound := 60;
    1.34 -
    1.35 -(*Command execution is functional (deterministic) provided evaluation is*)
    1.36 -Goal "single_valued ev ==> single_valued(exec ev)";
    1.37 -by (simp_tac (simpset() addsimps [single_valued_def]) 1);
    1.38 -by (REPEAT (rtac allI 1));
    1.39 -by (rtac impI 1);
    1.40 -by (etac exec.induct 1);
    1.41 -by (Blast_tac 3);
    1.42 -by (Blast_tac 1);
    1.43 -by (rewtac single_valued_def);
    1.44 -by (REPEAT (blast_tac (claset() addEs [exec_WHILE_case]) 1));
    1.45 -qed "single_valued_exec";
    1.46 -
    1.47 -Addsimps [fun_upd_same, fun_upd_other];
     2.1 --- a/src/HOL/Induct/Com.thy	Tue Apr 02 13:47:01 2002 +0200
     2.2 +++ b/src/HOL/Induct/Com.thy	Tue Apr 02 14:28:28 2002 +0200
     2.3 @@ -6,11 +6,12 @@
     2.4  Example of Mutual Induction via Iteratived Inductive Definitions: Commands
     2.5  *)
     2.6  
     2.7 -Com = Main +
     2.8 +theory Com = Main:
     2.9  
    2.10 -types loc
    2.11 -      state = "loc => nat"
    2.12 -      n2n2n = "nat => nat => nat"
    2.13 +typedecl loc
    2.14 +
    2.15 +types  state = "loc => nat"
    2.16 +       n2n2n = "nat => nat => nat"
    2.17  
    2.18  arities loc :: type
    2.19  
    2.20 @@ -26,38 +27,285 @@
    2.21        | Cond  exp com com      ("IF _ THEN _ ELSE _"  60)
    2.22        | While exp com          ("WHILE _ DO _"  60)
    2.23  
    2.24 -(** Execution of commands **)
    2.25 +text{* Execution of commands *}
    2.26  consts  exec    :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
    2.27         "@exec"  :: "((exp*state) * (nat*state)) set => 
    2.28                      [com*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    2.29  
    2.30 -translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    2.31 +translations  "csig -[eval]-> s" == "(csig,s) \<in> exec eval"
    2.32  
    2.33  syntax  eval'   :: "[exp*state,nat*state] => 
    2.34  		    ((exp*state) * (nat*state)) set => bool"
    2.35 -						   ("_/ -|[_]-> _" [50,0,50] 50)
    2.36 -translations
    2.37 -    "esig -|[eval]-> ns" => "(esig,ns) : eval"
    2.38 +					   ("_/ -|[_]-> _" [50,0,50] 50)
    2.39  
    2.40 -(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    2.41 -inductive "exec eval"
    2.42 -  intrs
    2.43 -    Skip    "(SKIP,s) -[eval]-> s"
    2.44 +translations
    2.45 +    "esig -|[eval]-> ns" => "(esig,ns) \<in> eval"
    2.46  
    2.47 -    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    2.48 -
    2.49 -    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    2.50 -            ==> (c0 ;; c1, s) -[eval]-> s1"
    2.51 +text{*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*}
    2.52 +inductive "exec eval"
    2.53 +  intros
    2.54 +    Skip:    "(SKIP,s) -[eval]-> s"
    2.55  
    2.56 -    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
    2.57 -            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    2.58 +    Assign:  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
    2.59  
    2.60 -    IfFalse "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
    2.61 +    Semi:    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    2.62 +             ==> (c0 ;; c1, s) -[eval]-> s1"
    2.63 +
    2.64 +    IfTrue: "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
    2.65               ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    2.66  
    2.67 -    WhileFalse "(e,s) -|[eval]-> (Suc 0, s1) ==> (WHILE e DO c, s) -[eval]-> s1"
    2.68 +    IfFalse: "[| (e,s) -|[eval]->  (Suc 0, s');  (c1,s') -[eval]-> s1 |] 
    2.69 +              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    2.70 +
    2.71 +    WhileFalse: "(e,s) -|[eval]-> (Suc 0, s1) 
    2.72 +                 ==> (WHILE e DO c, s) -[eval]-> s1"
    2.73 +
    2.74 +    WhileTrue:  "[| (e,s) -|[eval]-> (0,s1);
    2.75 +                    (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    2.76 +                 ==> (WHILE e DO c, s) -[eval]-> s3"
    2.77 +
    2.78 +declare exec.intros [intro]
    2.79 +
    2.80 +
    2.81 +inductive_cases
    2.82 +	[elim!]: "(SKIP,s) -[eval]-> t"
    2.83 +    and [elim!]: "(x:=a,s) -[eval]-> t"
    2.84 +    and	[elim!]: "(c1;;c2, s) -[eval]-> t"
    2.85 +    and	[elim!]: "(IF e THEN c1 ELSE c2, s) -[eval]-> t"
    2.86 +    and	exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
    2.87 +
    2.88 +
    2.89 +text{*Justifies using "exec" in the inductive definition of "eval"*}
    2.90 +lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
    2.91 +apply (unfold exec.defs )
    2.92 +apply (rule lfp_mono)
    2.93 +apply (assumption | rule basic_monos)+
    2.94 +done
    2.95 +
    2.96 +ML {*
    2.97 +Unify.trace_bound := 30;
    2.98 +Unify.search_bound := 60;
    2.99 +*}
   2.100 +
   2.101 +text{*Command execution is functional (deterministic) provided evaluation is*}
   2.102 +theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
   2.103 +apply (simp add: single_valued_def)
   2.104 +apply (intro allI) 
   2.105 +apply (rule impI)
   2.106 +apply (erule exec.induct)
   2.107 +apply (blast elim: exec_WHILE_case)+
   2.108 +done
   2.109 +
   2.110 +
   2.111 +section {* Expressions *}
   2.112 +
   2.113 +text{* Evaluation of arithmetic expressions *}
   2.114 +consts  eval    :: "((exp*state) * (nat*state)) set"
   2.115 +       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
   2.116 +
   2.117 +translations
   2.118 +    "esig -|-> (n,s)" <= "(esig,n,s) \<in> eval"
   2.119 +    "esig -|-> ns"    == "(esig,ns ) \<in> eval"
   2.120 +  
   2.121 +inductive eval
   2.122 +  intros 
   2.123 +    N [intro!]: "(N(n),s) -|-> (n,s)"
   2.124 +
   2.125 +    X [intro!]: "(X(x),s) -|-> (s(x),s)"
   2.126 +
   2.127 +    Op [intro]: "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
   2.128 +                 ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
   2.129 +
   2.130 +    valOf [intro]: "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
   2.131 +                    ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
   2.132 +
   2.133 +  monos exec_mono
   2.134 +
   2.135 +
   2.136 +inductive_cases
   2.137 +	[elim!]: "(N(n),sigma) -|-> (n',s')"
   2.138 +    and [elim!]: "(X(x),sigma) -|-> (n,s')"
   2.139 +    and	[elim!]: "(Op f a1 a2,sigma)  -|-> (n,s')"
   2.140 +    and	[elim!]: "(VALOF c RESULTIS e, s) -|-> (n, s1)"
   2.141 +
   2.142 +
   2.143 +lemma var_assign_eval [intro!]: "(X x, s(x:=n)) -|-> (n, s(x:=n))"
   2.144 +by (rule fun_upd_same [THEN subst], fast)
   2.145 +
   2.146 +
   2.147 +text{* Make the induction rule look nicer -- though eta_contract makes the new
   2.148 +    version look worse than it is...*}
   2.149 +
   2.150 +lemma split_lemma:
   2.151 +     "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
   2.152 +by auto
   2.153 +
   2.154 +text{*New induction rule.  Note the form of the VALOF induction hypothesis*}
   2.155 +lemma eval_induct:
   2.156 +  "[| (e,s) -|-> (n,s');                                          
   2.157 +      !!n s. P (N n) s n s;                                       
   2.158 +      !!s x. P (X x) s (s x) s;                                   
   2.159 +      !!e0 e1 f n0 n1 s s0 s1.                                    
   2.160 +         [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                    
   2.161 +            (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                   
   2.162 +         |] ==> P (Op f e0 e1) s (f n0 n1) s1;                    
   2.163 +      !!c e n s s0 s1.                                            
   2.164 +         [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0;  
   2.165 +            (c,s) -[eval]-> s0;                                   
   2.166 +            (e,s0) -|-> (n,s1); P e s0 n s1 |]                    
   2.167 +         ==> P (VALOF c RESULTIS e) s n s1                        
   2.168 +   |] ==> P e s n s'"
   2.169 +apply (erule eval.induct, blast) 
   2.170 +apply blast 
   2.171 +apply blast 
   2.172 +apply (frule Int_lower1 [THEN exec_mono, THEN subsetD])
   2.173 +apply (auto simp add: split_lemma)
   2.174 +done
   2.175 +
   2.176  
   2.177 -    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
   2.178 -                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
   2.179 -                ==> (WHILE e DO c, s) -[eval]-> s3"
   2.180 +text{*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
   2.181 +  using eval restricted to its functional part.  Note that the execution
   2.182 +  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
   2.183 +  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
   2.184 +  functional on the argument (c,s).
   2.185 +*}
   2.186 +lemma com_Unique:
   2.187 + "(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1  
   2.188 +  ==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
   2.189 +apply (erule exec.induct, simp_all)
   2.190 +      apply blast
   2.191 +     apply force
   2.192 +    apply blast
   2.193 +   apply blast
   2.194 +  apply blast
   2.195 + apply (blast elim: exec_WHILE_case)
   2.196 +apply (erule_tac V = "(?c,s2) -[?ev]-> s3" in thin_rl)
   2.197 +apply clarify
   2.198 +apply (erule exec_WHILE_case, blast+) 
   2.199 +done
   2.200 +
   2.201 +
   2.202 +text{*Expression evaluation is functional, or deterministic*}
   2.203 +theorem single_valued_eval: "single_valued eval"
   2.204 +apply (unfold single_valued_def)
   2.205 +apply (intro allI, rule impI) 
   2.206 +apply (simp (no_asm_simp) only: split_tupled_all)
   2.207 +apply (erule eval_induct)
   2.208 +apply (drule_tac [4] com_Unique)
   2.209 +apply (simp_all (no_asm_use))
   2.210 +apply blast+
   2.211 +done
   2.212 +
   2.213 +
   2.214 +lemma eval_N_E_lemma: "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)"
   2.215 +by (erule eval_induct, simp_all)
   2.216 +
   2.217 +lemmas eval_N_E [dest!] = eval_N_E_lemma [THEN mp, OF _ refl]
   2.218 +
   2.219 +
   2.220 +text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
   2.221 +lemma while_true_E [rule_format]:
   2.222 +     "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False"
   2.223 +by (erule exec.induct, auto)
   2.224 +
   2.225 +
   2.226 +subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  
   2.227 +       WHILE e DO c *}
   2.228 +
   2.229 +lemma while_if1 [rule_format]:
   2.230 +     "(c',s) -[eval]-> t 
   2.231 +      ==> (c' = WHILE e DO c) -->  
   2.232 +          (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t"
   2.233 +by (erule exec.induct, auto)
   2.234 +
   2.235 +lemma while_if2 [rule_format]:
   2.236 +     "(c',s) -[eval]-> t
   2.237 +      ==> (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) -->  
   2.238 +          (WHILE e DO c, s) -[eval]-> t"
   2.239 +by (erule exec.induct, auto)
   2.240 +
   2.241 +
   2.242 +theorem while_if:
   2.243 +     "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =   
   2.244 +      ((WHILE e DO c, s) -[eval]-> t)"
   2.245 +by (blast intro: while_if1 while_if2)
   2.246 +
   2.247 +
   2.248 +
   2.249 +subsection{* Equivalence of  (IF e THEN c1 ELSE c2);;c
   2.250 +                         and  IF e THEN (c1;;c) ELSE (c2;;c)   *}
   2.251 +
   2.252 +lemma if_semi1 [rule_format]:
   2.253 +     "(c',s) -[eval]-> t
   2.254 +      ==> (c' = (IF e THEN c1 ELSE c2);;c) -->  
   2.255 +          (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t"
   2.256 +by (erule exec.induct, auto)
   2.257 +
   2.258 +lemma if_semi2 [rule_format]:
   2.259 +     "(c',s) -[eval]-> t
   2.260 +      ==> (c' = IF e THEN (c1;;c) ELSE (c2;;c)) -->  
   2.261 +          ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t"
   2.262 +by (erule exec.induct, auto)
   2.263 +
   2.264 +theorem if_semi: "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =   
   2.265 +                  ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)"
   2.266 +by (blast intro: if_semi1 if_semi2)
   2.267 +
   2.268 +
   2.269 +
   2.270 +subsection{* Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   2.271 +                  and  VALOF c1;;c2 RESULTIS e
   2.272 + *}
   2.273 +
   2.274 +lemma valof_valof1 [rule_format]:
   2.275 +     "(e',s) -|-> (v,s')  
   2.276 +      ==> (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) -->  
   2.277 +          (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')"
   2.278 +by (erule eval_induct, auto)
   2.279 +
   2.280 +
   2.281 +lemma valof_valof2 [rule_format]:
   2.282 +     "(e',s) -|-> (v,s')
   2.283 +      ==> (e' = VALOF c1;;c2 RESULTIS e) -->  
   2.284 +          (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')"
   2.285 +by (erule eval_induct, auto)
   2.286 +
   2.287 +theorem valof_valof:
   2.288 +     "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =   
   2.289 +      ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))"
   2.290 +by (blast intro: valof_valof1 valof_valof2)
   2.291 +
   2.292 +
   2.293 +subsection{* Equivalence of  VALOF SKIP RESULTIS e  and  e *}
   2.294 +
   2.295 +lemma valof_skip1 [rule_format]:
   2.296 +     "(e',s) -|-> (v,s')
   2.297 +      ==> (e' = VALOF SKIP RESULTIS e) -->  
   2.298 +          (e, s) -|-> (v,s')"
   2.299 +by (erule eval_induct, auto)
   2.300 +
   2.301 +lemma valof_skip2:
   2.302 +     "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')"
   2.303 +by blast
   2.304 +
   2.305 +theorem valof_skip:
   2.306 +     "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))"
   2.307 +by (blast intro: valof_skip1 valof_skip2)
   2.308 +
   2.309 +
   2.310 +subsection{* Equivalence of  VALOF x:=e RESULTIS x  and  e *}
   2.311 +
   2.312 +lemma valof_assign1 [rule_format]:
   2.313 +     "(e',s) -|-> (v,s'')
   2.314 +      ==> (e' = VALOF x:=e RESULTIS X x) -->  
   2.315 +          (\<exists>s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))"
   2.316 +apply (erule eval_induct)
   2.317 +apply (simp_all del: fun_upd_apply, clarify, auto) 
   2.318 +done
   2.319 +
   2.320 +lemma valof_assign2:
   2.321 +     "(e,s) -|-> (v,s') ==> (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))"
   2.322 +by blast
   2.323 +
   2.324 +
   2.325  end
     3.1 --- a/src/HOL/Induct/Comb.ML	Tue Apr 02 13:47:01 2002 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,175 +0,0 @@
     3.4 -(*  Title:      HOL/ex/comb.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     Lawrence C Paulson
     3.7 -    Copyright   1996  University of Cambridge
     3.8 -
     3.9 -Combinatory Logic example: the Church-Rosser Theorem
    3.10 -Curiously, combinators do not include free variables.
    3.11 -
    3.12 -Example taken from
    3.13 -    J. Camilleri and T. F. Melham.
    3.14 -    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    3.15 -    Report 265, University of Cambridge Computer Laboratory, 1992.
    3.16 -
    3.17 -HOL system proofs may be found in
    3.18 -/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    3.19 -*)
    3.20 -
    3.21 -(*** Reflexive/Transitive closure preserves the Church-Rosser property 
    3.22 -     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
    3.23 -***)
    3.24 -
    3.25 -val [_, spec_mp] = [spec] RL [mp];
    3.26 -
    3.27 -(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
    3.28 -Goalw [diamond_def]
    3.29 -    "[| diamond(r);  (x,y):r^* |] ==> \ 
    3.30 -\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
    3.31 -by (etac rtrancl_induct 1);
    3.32 -by (Blast_tac 1);
    3.33 -by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    3.34 -                          addSDs [spec_mp]) 1);
    3.35 -qed_spec_mp "diamond_strip_lemmaE";
    3.36 -
    3.37 -Goal "diamond(r) ==> diamond(r^*)";
    3.38 -by (stac diamond_def 1);  (*unfold only in goal, not in premise!*)
    3.39 -by (rtac (impI RS allI RS allI) 1);
    3.40 -by (etac rtrancl_induct 1);
    3.41 -by (Blast_tac 1);
    3.42 -by (best_tac  (*Seems to be a brittle, undirected search*)
    3.43 -    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    3.44 -            addEs [diamond_strip_lemmaE RS exE]) 1);
    3.45 -qed "diamond_rtrancl";
    3.46 -
    3.47 -
    3.48 -(*** Results about Contraction ***)
    3.49 -
    3.50 -(*Derive a case for each combinator constructor*)
    3.51 -val K_contractE  = contract.mk_cases "K -1-> z";
    3.52 -val S_contractE  = contract.mk_cases "S -1-> z";
    3.53 -val Ap_contractE = contract.mk_cases "x##y -1-> z";
    3.54 -
    3.55 -AddSIs [contract.K, contract.S];
    3.56 -AddIs  [contract.Ap1, contract.Ap2];
    3.57 -AddSEs [K_contractE, S_contractE, Ap_contractE];
    3.58 -
    3.59 -Goalw [I_def] "I -1-> z ==> P";
    3.60 -by (Blast_tac 1);
    3.61 -qed "I_contract_E";
    3.62 -AddSEs [I_contract_E];
    3.63 -
    3.64 -Goal "K##x -1-> z ==> (EX x'. z = K##x' & x -1-> x')";
    3.65 -by (Blast_tac 1);
    3.66 -qed "K1_contractD";
    3.67 -AddSEs [K1_contractD];
    3.68 -
    3.69 -Goal "x ---> y ==> x##z ---> y##z";
    3.70 -by (etac rtrancl_induct 1);
    3.71 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
    3.72 -qed "Ap_reduce1";
    3.73 -
    3.74 -Goal "x ---> y ==> z##x ---> z##y";
    3.75 -by (etac rtrancl_induct 1);
    3.76 -by (ALLGOALS (blast_tac (claset() addIs [rtrancl_trans])));
    3.77 -qed "Ap_reduce2";
    3.78 -
    3.79 -(** Counterexample to the diamond property for -1-> **)
    3.80 -
    3.81 -Goal "K##I##(I##I) -1-> I";
    3.82 -by (rtac contract.K 1);
    3.83 -qed "KIII_contract1";
    3.84 -
    3.85 -Goalw [I_def] "K##I##(I##I) -1-> K##I##((K##I)##(K##I))";
    3.86 -by (Blast_tac 1);
    3.87 -qed "KIII_contract2";
    3.88 -
    3.89 -Goal "K##I##((K##I)##(K##I)) -1-> I";
    3.90 -by (Blast_tac 1);
    3.91 -qed "KIII_contract3";
    3.92 -
    3.93 -Goalw [diamond_def] "~ diamond(contract)";
    3.94 -by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
    3.95 -qed "not_diamond_contract";
    3.96 -
    3.97 -
    3.98 -
    3.99 -(*** Results about Parallel Contraction ***)
   3.100 -
   3.101 -(*Derive a case for each combinator constructor*)
   3.102 -val K_parcontractE  = parcontract.mk_cases "K =1=> z";
   3.103 -val S_parcontractE  = parcontract.mk_cases "S =1=> z";
   3.104 -val Ap_parcontractE = parcontract.mk_cases "x##y =1=> z";
   3.105 -
   3.106 -AddSIs [parcontract.refl, parcontract.K, parcontract.S];
   3.107 -AddIs  [parcontract.Ap];
   3.108 -AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
   3.109 -
   3.110 -(*** Basic properties of parallel contraction ***)
   3.111 -
   3.112 -Goal "K##x =1=> z ==> (EX x'. z = K##x' & x =1=> x')";
   3.113 -by (Blast_tac 1);
   3.114 -qed "K1_parcontractD";
   3.115 -AddSDs [K1_parcontractD];
   3.116 -
   3.117 -Goal "S##x =1=> z ==> (EX x'. z = S##x' & x =1=> x')";
   3.118 -by (Blast_tac 1);
   3.119 -qed "S1_parcontractD";
   3.120 -AddSDs [S1_parcontractD];
   3.121 -
   3.122 -Goal "S##x##y =1=> z ==> (EX x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')";
   3.123 -by (Blast_tac 1);
   3.124 -qed "S2_parcontractD";
   3.125 -AddSDs [S2_parcontractD];
   3.126 -
   3.127 -(*The rules above are not essential but make proofs much faster*)
   3.128 -
   3.129 -
   3.130 -(*Church-Rosser property for parallel contraction*)
   3.131 -Goalw [diamond_def] "diamond parcontract";
   3.132 -by (rtac (impI RS allI RS allI) 1);
   3.133 -by (etac parcontract.induct 1 THEN prune_params_tac);
   3.134 -by Safe_tac;
   3.135 -by (ALLGOALS Blast_tac);
   3.136 -qed "diamond_parcontract";
   3.137 -
   3.138 -
   3.139 -(*** Equivalence of x--->y and x===>y ***)
   3.140 -
   3.141 -Goal "contract <= parcontract";
   3.142 -by (rtac subsetI 1);
   3.143 -by (split_all_tac 1);
   3.144 -by (etac contract.induct 1);
   3.145 -by (ALLGOALS Blast_tac);
   3.146 -qed "contract_subset_parcontract";
   3.147 -
   3.148 -(*Reductions: simply throw together reflexivity, transitivity and
   3.149 -  the one-step reductions*)
   3.150 -
   3.151 -AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
   3.152 -
   3.153 -(*Example only: not used*)
   3.154 -Goalw [I_def] "I##x ---> x";
   3.155 -by (Blast_tac 1);
   3.156 -qed "reduce_I";
   3.157 -
   3.158 -Goal "parcontract <= contract^*";
   3.159 -by (rtac subsetI 1);
   3.160 -by (split_all_tac 1);
   3.161 -by (etac parcontract.induct 1 THEN prune_params_tac);
   3.162 -by (ALLGOALS Blast_tac);
   3.163 -qed "parcontract_subset_reduce";
   3.164 -
   3.165 -Goal "contract^* = parcontract^*";
   3.166 -by (REPEAT 
   3.167 -    (resolve_tac [equalityI, 
   3.168 -                  contract_subset_parcontract RS rtrancl_mono, 
   3.169 -                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
   3.170 -qed "reduce_eq_parreduce";
   3.171 -
   3.172 -Goal "diamond(contract^*)";
   3.173 -by (simp_tac (simpset() addsimps [reduce_eq_parreduce, diamond_rtrancl, 
   3.174 -                                 diamond_parcontract]) 1);
   3.175 -qed "diamond_reduce";
   3.176 -
   3.177 -
   3.178 -writeln"Reached end of file.";
     4.1 --- a/src/HOL/Induct/Comb.thy	Tue Apr 02 13:47:01 2002 +0200
     4.2 +++ b/src/HOL/Induct/Comb.thy	Tue Apr 02 14:28:28 2002 +0200
     4.3 @@ -1,74 +1,220 @@
     4.4 -(*  Title:      HOL/ex/Comb.thy
     4.5 +(*  Title:      HOL/Induct/Comb.thy
     4.6      ID:         $Id$
     4.7      Author:     Lawrence C Paulson
     4.8      Copyright   1996  University of Cambridge
     4.9 -
    4.10 -Combinatory Logic example: the Church-Rosser Theorem
    4.11 -Curiously, combinators do not include free variables.
    4.12 -
    4.13 -Example taken from
    4.14 -    J. Camilleri and T. F. Melham.
    4.15 -    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    4.16 -    Report 265, University of Cambridge Computer Laboratory, 1992.
    4.17  *)
    4.18  
    4.19 +header {* Combinatory Logic example: the Church-Rosser Theorem *}
    4.20  
    4.21 -Comb = Main +
    4.22 +theory Comb = Main:
    4.23 +
    4.24 +text {*
    4.25 +  Curiously, combinators do not include free variables.
    4.26 +
    4.27 +  Example taken from \cite{camilleri-melham}.
    4.28  
    4.29 -(** Datatype definition of combinators S and K, with infixed application **)
    4.30 +HOL system proofs may be found in the HOL distribution at
    4.31 +   .../contrib/rule-induction/cl.ml
    4.32 +*}
    4.33 +
    4.34 +subsection {* Definitions *}
    4.35 +
    4.36 +text {* Datatype definition of combinators @{text S} and @{text K}. *}
    4.37 +
    4.38  datatype comb = K
    4.39                | S
    4.40                | "##" comb comb (infixl 90)
    4.41  
    4.42 -(** Inductive definition of contractions, -1->
    4.43 -             and (multi-step) reductions, --->
    4.44 -**)
    4.45 +text {*
    4.46 +  Inductive definition of contractions, @{text "-1->"} and
    4.47 +  (multi-step) reductions, @{text "--->"}.
    4.48 +*}
    4.49 +
    4.50  consts
    4.51    contract  :: "(comb*comb) set"
    4.52 -  "-1->"    :: [comb,comb] => bool   (infixl 50)
    4.53 -  "--->"    :: [comb,comb] => bool   (infixl 50)
    4.54 +  "-1->"    :: "[comb,comb] => bool"   (infixl 50)
    4.55 +  "--->"    :: "[comb,comb] => bool"   (infixl 50)
    4.56  
    4.57  translations
    4.58 -  "x -1-> y" == "(x,y) : contract"
    4.59 -  "x ---> y" == "(x,y) : contract^*"
    4.60 +  "x -1-> y" == "(x,y) \<in> contract"
    4.61 +  "x ---> y" == "(x,y) \<in> contract^*"
    4.62  
    4.63  inductive contract
    4.64 -  intrs
    4.65 -    K     "K##x##y -1-> x"
    4.66 -    S     "S##x##y##z -1-> (x##z)##(y##z)"
    4.67 -    Ap1   "x-1->y ==> x##z -1-> y##z"
    4.68 -    Ap2   "x-1->y ==> z##x -1-> z##y"
    4.69 +  intros
    4.70 +    K:     "K##x##y -1-> x"
    4.71 +    S:     "S##x##y##z -1-> (x##z)##(y##z)"
    4.72 +    Ap1:   "x-1->y ==> x##z -1-> y##z"
    4.73 +    Ap2:   "x-1->y ==> z##x -1-> z##y"
    4.74  
    4.75 +text {*
    4.76 +  Inductive definition of parallel contractions, @{text "=1=>"} and
    4.77 +  (multi-step) parallel reductions, @{text "===>"}.
    4.78 +*}
    4.79  
    4.80 -(** Inductive definition of parallel contractions, =1=>
    4.81 -             and (multi-step) parallel reductions, ===>
    4.82 -**)
    4.83  consts
    4.84    parcontract :: "(comb*comb) set"
    4.85 -  "=1=>"    :: [comb,comb] => bool   (infixl 50)
    4.86 -  "===>"    :: [comb,comb] => bool   (infixl 50)
    4.87 +  "=1=>"      :: "[comb,comb] => bool"   (infixl 50)
    4.88 +  "===>"      :: "[comb,comb] => bool"   (infixl 50)
    4.89  
    4.90  translations
    4.91 -  "x =1=> y" == "(x,y) : parcontract"
    4.92 -  "x ===> y" == "(x,y) : parcontract^*"
    4.93 +  "x =1=> y" == "(x,y) \<in> parcontract"
    4.94 +  "x ===> y" == "(x,y) \<in> parcontract^*"
    4.95  
    4.96  inductive parcontract
    4.97 -  intrs
    4.98 -    refl  "x =1=> x"
    4.99 -    K     "K##x##y =1=> x"
   4.100 -    S     "S##x##y##z =1=> (x##z)##(y##z)"
   4.101 -    Ap    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
   4.102 +  intros
   4.103 +    refl:  "x =1=> x"
   4.104 +    K:     "K##x##y =1=> x"
   4.105 +    S:     "S##x##y##z =1=> (x##z)##(y##z)"
   4.106 +    Ap:    "[| x=1=>y;  z=1=>w |] ==> x##z =1=> y##w"
   4.107  
   4.108 +text {*
   4.109 +  Misc definitions.
   4.110 +*}
   4.111  
   4.112 -(*Misc definitions*)
   4.113  constdefs
   4.114    I :: comb
   4.115    "I == S##K##K"
   4.116  
   4.117 -  (*confluence; Lambda/Commutation treats this more abstractly*)
   4.118    diamond   :: "('a * 'a)set => bool"	
   4.119 -  "diamond(r) == ALL x y. (x,y):r --> 
   4.120 -                  (ALL y'. (x,y'):r --> 
   4.121 -                    (EX z. (y,z):r & (y',z) : r))"
   4.122 +    --{*confluence; Lambda/Commutation treats this more abstractly*}
   4.123 +  "diamond(r) == \<forall>x y. (x,y) \<in> r --> 
   4.124 +                  (\<forall>y'. (x,y') \<in> r --> 
   4.125 +                    (\<exists>z. (y,z) \<in> r & (y',z) \<in> r))"
   4.126 +
   4.127 +
   4.128 +subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
   4.129 +
   4.130 +text{*So does the Transitive closure, with a similar proof*}
   4.131 +
   4.132 +text{*Strip lemma.  
   4.133 +   The induction hypothesis covers all but the last diamond of the strip.*}
   4.134 +lemma diamond_strip_lemmaE [rule_format]: 
   4.135 +    "[| diamond(r);  (x,y) \<in> r^* |] ==>   
   4.136 +          \<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
   4.137 +apply (unfold diamond_def)
   4.138 +apply (erule rtrancl_induct, blast, clarify)
   4.139 +apply (drule spec, drule mp, assumption)
   4.140 +apply (blast intro: rtrancl_trans [OF _ r_into_rtrancl])
   4.141 +done
   4.142 +
   4.143 +lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)"
   4.144 +apply (simp (no_asm_simp) add: diamond_def)
   4.145 +apply (rule impI [THEN allI, THEN allI])
   4.146 +apply (erule rtrancl_induct, blast)
   4.147 +apply (best intro: rtrancl_trans [OF _ r_into_rtrancl] 
   4.148 +            elim: diamond_strip_lemmaE [THEN exE])
   4.149 +done
   4.150 +
   4.151 +
   4.152 +subsection {* Non-contraction results *}
   4.153 +
   4.154 +text {* Derive a case for each combinator constructor. *}
   4.155 +
   4.156 +inductive_cases
   4.157 +      K_contractE [elim!]: "K -1-> r"
   4.158 +  and S_contractE [elim!]: "S -1-> r"
   4.159 +  and Ap_contractE [elim!]: "p##q -1-> r"
   4.160 +
   4.161 +declare contract.K [intro!] contract.S [intro!]
   4.162 +declare contract.Ap1 [intro] contract.Ap2 [intro]
   4.163 +
   4.164 +lemma I_contract_E [elim!]: "I -1-> z ==> P"
   4.165 +by (unfold I_def, blast)
   4.166 +
   4.167 +lemma K1_contractD [elim!]: "K##x -1-> z ==> (\<exists>x'. z = K##x' & x -1-> x')"
   4.168 +by blast
   4.169 +
   4.170 +lemma Ap_reduce1 [intro]: "x ---> y ==> x##z ---> y##z"
   4.171 +apply (erule rtrancl_induct)
   4.172 +apply (blast intro: rtrancl_trans)+
   4.173 +done
   4.174 +
   4.175 +lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y"
   4.176 +apply (erule rtrancl_induct)
   4.177 +apply (blast intro: rtrancl_trans)+
   4.178 +done
   4.179 +
   4.180 +(** Counterexample to the diamond property for -1-> **)
   4.181 +
   4.182 +lemma KIII_contract1: "K##I##(I##I) -1-> I"
   4.183 +by (rule contract.K)
   4.184 +
   4.185 +lemma KIII_contract2: "K##I##(I##I) -1-> K##I##((K##I)##(K##I))"
   4.186 +by (unfold I_def, blast)
   4.187 +
   4.188 +lemma KIII_contract3: "K##I##((K##I)##(K##I)) -1-> I"
   4.189 +by blast
   4.190 +
   4.191 +lemma not_diamond_contract: "~ diamond(contract)"
   4.192 +apply (unfold diamond_def) 
   4.193 +apply (best intro: KIII_contract1 KIII_contract2 KIII_contract3)
   4.194 +done
   4.195 +
   4.196 +
   4.197 +subsection {* Results about Parallel Contraction *}
   4.198 +
   4.199 +text {* Derive a case for each combinator constructor. *}
   4.200 +
   4.201 +inductive_cases
   4.202 +      K_parcontractE [elim!]: "K =1=> r"
   4.203 +  and S_parcontractE [elim!]: "S =1=> r"
   4.204 +  and Ap_parcontractE [elim!]: "p##q =1=> r"
   4.205 +
   4.206 +declare parcontract.intros [intro]
   4.207 +
   4.208 +(*** Basic properties of parallel contraction ***)
   4.209 +
   4.210 +subsection {* Basic properties of parallel contraction *}
   4.211 +
   4.212 +lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')"
   4.213 +by blast
   4.214 +
   4.215 +lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\<exists>x'. z = S##x' & x =1=> x')"
   4.216 +by blast
   4.217 +
   4.218 +lemma S2_parcontractD [dest!]:
   4.219 +     "S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')"
   4.220 +by blast
   4.221 +
   4.222 +text{*The rules above are not essential but make proofs much faster*}
   4.223 +
   4.224 +text{*Church-Rosser property for parallel contraction*}
   4.225 +lemma diamond_parcontract: "diamond parcontract"
   4.226 +apply (unfold diamond_def)
   4.227 +apply (rule impI [THEN allI, THEN allI])
   4.228 +apply (erule parcontract.induct, fast+)
   4.229 +done
   4.230 +
   4.231 +text {*
   4.232 +  \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
   4.233 +*}
   4.234 +
   4.235 +lemma contract_subset_parcontract: "contract <= parcontract"
   4.236 +apply (rule subsetI)
   4.237 +apply (simp only: split_tupled_all)
   4.238 +apply (erule contract.induct, blast+)
   4.239 +done
   4.240 +
   4.241 +text{*Reductions: simply throw together reflexivity, transitivity and
   4.242 +  the one-step reductions*}
   4.243 +
   4.244 +declare r_into_rtrancl [intro]  rtrancl_trans [intro]
   4.245 +
   4.246 +(*Example only: not used*)
   4.247 +lemma reduce_I: "I##x ---> x"
   4.248 +by (unfold I_def, blast)
   4.249 +
   4.250 +lemma parcontract_subset_reduce: "parcontract <= contract^*"
   4.251 +apply (rule subsetI)
   4.252 +apply (simp only: split_tupled_all)
   4.253 +apply (erule parcontract.induct , blast+)
   4.254 +done
   4.255 +
   4.256 +lemma reduce_eq_parreduce: "contract^* = parcontract^*"
   4.257 +by (rule equalityI contract_subset_parcontract [THEN rtrancl_mono] 
   4.258 +         parcontract_subset_reduce [THEN rtrancl_subset_rtrancl])+
   4.259 +
   4.260 +lemma diamond_reduce: "diamond(contract^*)"
   4.261 +by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract)
   4.262  
   4.263  end
     5.1 --- a/src/HOL/Induct/Exp.ML	Tue Apr 02 13:47:01 2002 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,233 +0,0 @@
     5.4 -(*  Title:      HOL/Induct/Exp
     5.5 -    ID:         $Id$
     5.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 -    Copyright   1997  University of Cambridge
     5.8 -
     5.9 -Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
    5.10 -*)
    5.11 -
    5.12 -AddSIs [eval.N, eval.X];
    5.13 -AddIs  [eval.Op, eval.valOf];
    5.14 -
    5.15 -val eval_elim_cases = 
    5.16 -    map eval.mk_cases 
    5.17 -       ["(N(n),sigma) -|-> (n',s')", 
    5.18 -	"(X(x),sigma) -|-> (n,s')",
    5.19 -	"(Op f a1 a2,sigma)  -|-> (n,s')",
    5.20 -	"(VALOF c RESULTIS e, s) -|-> (n, s1)"];
    5.21 -
    5.22 -AddSEs eval_elim_cases;
    5.23 -
    5.24 -
    5.25 -Goal "(X x, s(x:=n)) -|-> (n, s(x:=n))";
    5.26 -by (rtac (fun_upd_same RS subst) 1 THEN resolve_tac eval.intrs 1);
    5.27 -qed "var_assign_eval";
    5.28 -
    5.29 -AddSIs [var_assign_eval];
    5.30 -
    5.31 -
    5.32 -(** Make the induction rule look nicer -- though eta_contract makes the new
    5.33 -    version look worse than it is...**)
    5.34 -
    5.35 -Goal "{((e,s),(n,s')). P e s n s'} = \
    5.36 -\         Collect (split (%v. split (split P v)))";
    5.37 -by (rtac Collect_cong 1);
    5.38 -by (split_all_tac 1);
    5.39 -by (Simp_tac 1);
    5.40 -val split_lemma = result();
    5.41 -
    5.42 -(*New induction rule.  Note the form of the VALOF induction hypothesis*)
    5.43 -val major::prems = goal thy
    5.44 -  "[| (e,s) -|-> (n,s');                                         \
    5.45 -\     !!n s. P (N n) s n s;                                      \
    5.46 -\     !!s x. P (X x) s (s x) s;                                  \
    5.47 -\     !!e0 e1 f n0 n1 s s0 s1.                                   \
    5.48 -\        [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                   \
    5.49 -\           (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                  \
    5.50 -\        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
    5.51 -\     !!c e n s s0 s1.                                           \
    5.52 -\        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
    5.53 -\           (c,s) -[eval]-> s0;                                  \
    5.54 -\           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
    5.55 -\        ==> P (VALOF c RESULTIS e) s n s1                       \
    5.56 -\  |] ==> P e s n s'";
    5.57 -by (rtac (major RS eval.induct) 1);
    5.58 -by (blast_tac (claset() addIs prems) 1);
    5.59 -by (blast_tac (claset() addIs prems) 1);
    5.60 -by (blast_tac (claset() addIs prems) 1);
    5.61 -by (forward_tac [impOfSubs (Int_lower1 RS exec_mono)] 1);
    5.62 -by (auto_tac (claset() addIs prems,simpset() addsimps [split_lemma]));
    5.63 -qed "eval_induct";
    5.64 -
    5.65 -
    5.66 -(*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
    5.67 -  using eval restricted to its functional part.  Note that the execution
    5.68 -  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
    5.69 -  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
    5.70 -  functional on the argument (c,s).
    5.71 -*)
    5.72 -Goal "(c,s) -[eval Int {((e,s),(n,t)). ALL nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1 \
    5.73 -\     ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
    5.74 -by (etac exec.induct 1);
    5.75 -by (ALLGOALS Full_simp_tac);
    5.76 -      by (Blast_tac 1);
    5.77 -     by (Force_tac 1);
    5.78 -    by (Blast_tac 1);
    5.79 -   by (Blast_tac 1);
    5.80 -  by (Blast_tac 1);
    5.81 - by (blast_tac (claset() addEs [exec_WHILE_case]) 1);
    5.82 -by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
    5.83 -by (Clarify_tac 1);
    5.84 -by (etac exec_WHILE_case 1);
    5.85 - by (ALLGOALS Blast_tac);
    5.86 -qed "com_Unique";
    5.87 -
    5.88 -
    5.89 -(*Expression evaluation is functional, or deterministic*)
    5.90 -Goalw [single_valued_def] "single_valued eval";
    5.91 -by (EVERY1[rtac allI, rtac allI, rtac impI]);
    5.92 -by (split_all_tac 1);
    5.93 -by (etac eval_induct 1);
    5.94 -by (dtac com_Unique 4);
    5.95 -by (ALLGOALS Full_simp_tac);
    5.96 -by (ALLGOALS Blast_tac);
    5.97 -qed "single_valued_eval";
    5.98 -
    5.99 -
   5.100 -Goal "(e,s) -|-> (v,s') ==> (e = N n) --> (v=n & s'=s)";
   5.101 -by (etac eval_induct 1);
   5.102 -by (ALLGOALS Asm_simp_tac);
   5.103 -val lemma = result();
   5.104 -bind_thm ("eval_N_E", refl RSN (2, lemma RS mp));
   5.105 -
   5.106 -AddSEs [eval_N_E];
   5.107 -
   5.108 -
   5.109 -(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
   5.110 -Goal "(c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
   5.111 -by (etac exec.induct 1);
   5.112 -by Auto_tac;
   5.113 -bind_thm ("while_true_E", refl RSN (2, result() RS mp));
   5.114 -
   5.115 -
   5.116 -(** Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP  and  WHILE e DO c **)
   5.117 -
   5.118 -Goal "(c',s) -[eval]-> t ==> \
   5.119 -\              (c' = WHILE e DO c) --> \
   5.120 -\              (IF e THEN c;;c' ELSE SKIP, s) -[eval]-> t";
   5.121 -by (etac exec.induct 1);
   5.122 -by (ALLGOALS Asm_simp_tac);
   5.123 -by (ALLGOALS Blast_tac); 
   5.124 -bind_thm ("while_if1", refl RSN (2, result() RS mp));
   5.125 -
   5.126 -
   5.127 -Goal "(c',s) -[eval]-> t ==> \
   5.128 -\              (c' = IF e THEN c;;(WHILE e DO c) ELSE SKIP) --> \
   5.129 -\              (WHILE e DO c, s) -[eval]-> t";
   5.130 -by (etac exec.induct 1);
   5.131 -by (ALLGOALS Asm_simp_tac);
   5.132 -by (ALLGOALS Blast_tac); 
   5.133 -bind_thm ("while_if2", refl RSN (2, result() RS mp));
   5.134 -
   5.135 -
   5.136 -Goal "((IF e THEN c;;(WHILE e DO c) ELSE SKIP, s) -[eval]-> t)  =  \
   5.137 -\         ((WHILE e DO c, s) -[eval]-> t)";
   5.138 -by (blast_tac (claset() addIs [while_if1, while_if2]) 1);
   5.139 -qed "while_if";
   5.140 -
   5.141 -
   5.142 -
   5.143 -(** Equivalence of  (IF e THEN c1 ELSE c2);;c
   5.144 -               and  IF e THEN (c1;;c) ELSE (c2;;c)   **)
   5.145 -
   5.146 -Goal "(c',s) -[eval]-> t ==> \
   5.147 -\              (c' = (IF e THEN c1 ELSE c2);;c) --> \
   5.148 -\              (IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t";
   5.149 -by (etac exec.induct 1);
   5.150 -by (ALLGOALS Asm_simp_tac);
   5.151 -by (Blast_tac 1); 
   5.152 -bind_thm ("if_semi1", refl RSN (2, result() RS mp));
   5.153 -
   5.154 -
   5.155 -Goal "(c',s) -[eval]-> t ==> \
   5.156 -\              (c' = IF e THEN (c1;;c) ELSE (c2;;c)) --> \
   5.157 -\              ((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t";
   5.158 -by (etac exec.induct 1);
   5.159 -by (ALLGOALS Asm_simp_tac);
   5.160 -by (ALLGOALS Blast_tac); 
   5.161 -bind_thm ("if_semi2", refl RSN (2, result() RS mp));
   5.162 -
   5.163 -
   5.164 -Goal "(((IF e THEN c1 ELSE c2);;c, s) -[eval]-> t)  =  \
   5.165 -\         ((IF e THEN (c1;;c) ELSE (c2;;c), s) -[eval]-> t)";
   5.166 -by (blast_tac (claset() addIs [if_semi1, if_semi2]) 1);
   5.167 -qed "if_semi";
   5.168 -
   5.169 -
   5.170 -
   5.171 -(** Equivalence of  VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
   5.172 -               and  VALOF c1;;c2 RESULTIS e
   5.173 - **)
   5.174 -
   5.175 -Goal "(e',s) -|-> (v,s') ==> \
   5.176 -\              (e' = VALOF c1 RESULTIS (VALOF c2 RESULTIS e)) --> \
   5.177 -\              (VALOF c1;;c2 RESULTIS e, s) -|-> (v,s')";
   5.178 -by (etac eval_induct 1);
   5.179 -by (ALLGOALS Asm_simp_tac);
   5.180 -by (Blast_tac 1); 
   5.181 -bind_thm ("valof_valof1", refl RSN (2, result() RS mp));
   5.182 -
   5.183 -
   5.184 -Goal "(e',s) -|-> (v,s') ==> \
   5.185 -\              (e' = VALOF c1;;c2 RESULTIS e) --> \
   5.186 -\              (VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s')";
   5.187 -by (etac eval_induct 1);
   5.188 -by (ALLGOALS Asm_simp_tac);
   5.189 -by (Blast_tac 1); 
   5.190 -bind_thm ("valof_valof2", refl RSN (2, result() RS mp));
   5.191 -
   5.192 -
   5.193 -Goal "((VALOF c1 RESULTIS (VALOF c2 RESULTIS e), s) -|-> (v,s'))  =  \
   5.194 -\         ((VALOF c1;;c2 RESULTIS e, s) -|-> (v,s'))";
   5.195 -by (blast_tac (claset() addIs [valof_valof1, valof_valof2]) 1);
   5.196 -qed "valof_valof";
   5.197 -
   5.198 -
   5.199 -(** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
   5.200 -
   5.201 -Goal "(e',s) -|-> (v,s') ==> \
   5.202 -\              (e' = VALOF SKIP RESULTIS e) --> \
   5.203 -\              (e, s) -|-> (v,s')";
   5.204 -by (etac eval_induct 1);
   5.205 -by (ALLGOALS Asm_simp_tac);
   5.206 -by (Blast_tac 1); 
   5.207 -bind_thm ("valof_skip1", refl RSN (2, result() RS mp));
   5.208 -
   5.209 -Goal "(e,s) -|-> (v,s') ==> (VALOF SKIP RESULTIS e, s) -|-> (v,s')";
   5.210 -by (Blast_tac 1);
   5.211 -qed "valof_skip2";
   5.212 -
   5.213 -Goal "((VALOF SKIP RESULTIS e, s) -|-> (v,s'))  =  ((e, s) -|-> (v,s'))";
   5.214 -by (blast_tac (claset() addIs [valof_skip1, valof_skip2]) 1);
   5.215 -qed "valof_skip";
   5.216 -
   5.217 -
   5.218 -(** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
   5.219 -
   5.220 -Delsimps [fun_upd_apply];
   5.221 -Goal "(e',s) -|-> (v,s'') ==> \
   5.222 -\              (e' = VALOF x:=e RESULTIS X x) --> \
   5.223 -\              (EX s'. (e, s) -|-> (v,s') & (s'' = s'(x:=v)))";
   5.224 -by (etac eval_induct 1);
   5.225 -   by (ALLGOALS Asm_simp_tac);
   5.226 -by (thin_tac "?PP-->?QQ" 1);
   5.227 -by (Clarify_tac 1);
   5.228 -by (Simp_tac 1);
   5.229 -by (Blast_tac 1); 
   5.230 -bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
   5.231 -
   5.232 -
   5.233 -Goal "(e,s) -|-> (v,s') ==> \
   5.234 -\              (VALOF x:=e RESULTIS X x, s) -|-> (v,s'(x:=v))";
   5.235 -by (Blast_tac 1);
   5.236 -qed "valof_assign2";
     6.1 --- a/src/HOL/Induct/Exp.thy	Tue Apr 02 13:47:01 2002 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,33 +0,0 @@
     6.4 -(*  Title:      HOL/Induct/Exp
     6.5 -    ID:         $Id$
     6.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     6.7 -    Copyright   1997  University of Cambridge
     6.8 -
     6.9 -Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
    6.10 -*)
    6.11 -
    6.12 -Exp = Com +
    6.13 -
    6.14 -(** Evaluation of arithmetic expressions **)
    6.15 -consts  eval    :: "((exp*state) * (nat*state)) set"
    6.16 -       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
    6.17 -translations
    6.18 -    "esig -|-> (n,s)" <= "(esig,n,s) : eval"
    6.19 -    "esig -|-> ns"    == "(esig,ns ) : eval"
    6.20 -  
    6.21 -inductive eval
    6.22 -  intrs 
    6.23 -    N      "(N(n),s) -|-> (n,s)"
    6.24 -
    6.25 -    X      "(X(x),s) -|-> (s(x),s)"
    6.26 -
    6.27 -    Op     "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
    6.28 -            ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
    6.29 -
    6.30 -    valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
    6.31 -            ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
    6.32 -
    6.33 -  monos exec_mono
    6.34 -
    6.35 -end
    6.36 -
     7.1 --- a/src/HOL/Induct/LFilter.ML	Tue Apr 02 13:47:01 2002 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,337 +0,0 @@
     7.4 -(*  Title:      HOL/ex/LFilter
     7.5 -    ID:         $Id$
     7.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.7 -    Copyright   1997  University of Cambridge
     7.8 -
     7.9 -The "filter" functional for coinductive lists
    7.10 -  --defined by a combination of induction and coinduction
    7.11 -*)
    7.12 -
    7.13 -(*** findRel: basic laws ****)
    7.14 -
    7.15 -val findRel_LConsE = findRel.mk_cases "(LCons x l, l'') : findRel p";
    7.16 -
    7.17 -AddSEs [findRel_LConsE];
    7.18 -
    7.19 -
    7.20 -Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    7.21 -by (etac findRel.induct 1);
    7.22 -by (Blast_tac 1);
    7.23 -by (Blast_tac 1);
    7.24 -qed_spec_mp "findRel_functional";
    7.25 -
    7.26 -Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
    7.27 -by (etac findRel.induct 1);
    7.28 -by (Blast_tac 1);
    7.29 -by (Blast_tac 1);
    7.30 -qed_spec_mp "findRel_imp_LCons";
    7.31 -
    7.32 -Goal "(LNil,l): findRel p ==> R";
    7.33 -by (blast_tac (claset() addEs [findRel.elim]) 1);
    7.34 -qed "findRel_LNil";
    7.35 -
    7.36 -AddSEs [findRel_LNil];
    7.37 -
    7.38 -
    7.39 -(*** Properties of Domain (findRel p) ***)
    7.40 -
    7.41 -Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
    7.42 -by (case_tac "p x" 1);
    7.43 -by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
    7.44 -qed "LCons_Domain_findRel";
    7.45 -
    7.46 -Addsimps [LCons_Domain_findRel];
    7.47 -
    7.48 -val major::prems = 
    7.49 -Goal "[| l: Domain (findRel p);                                   \
    7.50 -\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
    7.51 -\         |] ==> Q";
    7.52 -by (rtac (major RS DomainE) 1);
    7.53 -by (ftac findRel_imp_LCons 1);
    7.54 -by (REPEAT (eresolve_tac [exE,conjE] 1));
    7.55 -by (hyp_subst_tac 1);
    7.56 -by (REPEAT (ares_tac prems 1));
    7.57 -qed "Domain_findRelE";
    7.58 -
    7.59 -val prems = goal thy
    7.60 -    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
    7.61 -by (Clarify_tac 1);
    7.62 -by (etac findRel.induct 1);
    7.63 -by (blast_tac (claset() addIs findRel.intrs @ prems) 1);
    7.64 -by (blast_tac (claset() addIs findRel.intrs) 1);
    7.65 -qed "Domain_findRel_mono";
    7.66 -
    7.67 -
    7.68 -(*** find: basic equations ***)
    7.69 -
    7.70 -Goalw [find_def] "find p LNil = LNil";
    7.71 -by (Blast_tac 1);
    7.72 -qed "find_LNil";
    7.73 -Addsimps [find_LNil];
    7.74 -
    7.75 -Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
    7.76 -by (blast_tac (claset() addDs [findRel_functional]) 1);
    7.77 -qed "findRel_imp_find";
    7.78 -Addsimps [findRel_imp_find];
    7.79 -
    7.80 -Goal "p x ==> find p (LCons x l) = LCons x l";
    7.81 -by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    7.82 -qed "find_LCons_found";
    7.83 -Addsimps [find_LCons_found];
    7.84 -
    7.85 -Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
    7.86 -by (Blast_tac 1);
    7.87 -qed "diverge_find_LNil";
    7.88 -Addsimps [diverge_find_LNil];
    7.89 -
    7.90 -Goal "~ (p x) ==> find p (LCons x l) = find p l";
    7.91 -by (case_tac "LCons x l : Domain(findRel p)" 1);
    7.92 -by (Asm_full_simp_tac 2);
    7.93 -by (Clarify_tac 1);
    7.94 -by (Asm_simp_tac 1);
    7.95 -by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    7.96 -qed "find_LCons_seek";
    7.97 -Addsimps [find_LCons_seek];
    7.98 -
    7.99 -Goal "find p (LCons x l) = (if p x then LCons x l else find p l)";
   7.100 -by (Asm_simp_tac 1);
   7.101 -qed "find_LCons";
   7.102 -
   7.103 -
   7.104 -
   7.105 -(*** lfilter: basic equations ***)
   7.106 -
   7.107 -Goal "lfilter p LNil = LNil";
   7.108 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   7.109 -by (Simp_tac 1);
   7.110 -qed "lfilter_LNil";
   7.111 -Addsimps [lfilter_LNil];
   7.112 -
   7.113 -Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
   7.114 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   7.115 -by (Asm_simp_tac 1);
   7.116 -qed "diverge_lfilter_LNil";
   7.117 -
   7.118 -Addsimps [diverge_lfilter_LNil];
   7.119 -
   7.120 -
   7.121 -Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
   7.122 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   7.123 -by (Asm_simp_tac 1);
   7.124 -qed "lfilter_LCons_found";
   7.125 -(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
   7.126 -  subsumes both*)
   7.127 -
   7.128 -
   7.129 -Goal "(l, LCons x l') : findRel p \
   7.130 -\              ==> lfilter p l = LCons x (lfilter p l')";
   7.131 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   7.132 -by (Asm_simp_tac 1);
   7.133 -qed "findRel_imp_lfilter";
   7.134 -
   7.135 -Addsimps [findRel_imp_lfilter];
   7.136 -
   7.137 -
   7.138 -Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
   7.139 -by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   7.140 -by (case_tac "LCons x l : Domain(findRel p)" 1);
   7.141 -by (Asm_full_simp_tac 2);
   7.142 -by (etac Domain_findRelE 1);
   7.143 -by (safe_tac (claset() delrules [conjI]));
   7.144 -by (Asm_full_simp_tac 1);
   7.145 -qed "lfilter_LCons_seek";
   7.146 -
   7.147 -
   7.148 -Goal "lfilter p (LCons x l) = \
   7.149 -\         (if p x then LCons x (lfilter p l) else lfilter p l)";
   7.150 -by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
   7.151 -qed "lfilter_LCons";
   7.152 -
   7.153 -AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   7.154 -Addsimps [lfilter_LCons];
   7.155 -
   7.156 -
   7.157 -Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
   7.158 -by (rtac notI 1);
   7.159 -by (etac Domain_findRelE 1);
   7.160 -by (etac rev_mp 1);
   7.161 -by (Asm_simp_tac 1);
   7.162 -qed "lfilter_eq_LNil";
   7.163 -
   7.164 -
   7.165 -Goal "lfilter p l = LCons x l' -->     \
   7.166 -\              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
   7.167 -by (stac (lfilter_def RS def_llist_corec) 1);
   7.168 -by (case_tac "l : Domain(findRel p)" 1);
   7.169 -by (etac Domain_findRelE 1);
   7.170 -by (Asm_simp_tac 2);
   7.171 -by (Asm_simp_tac 1);
   7.172 -by (Blast_tac 1);
   7.173 -qed_spec_mp "lfilter_eq_LCons";
   7.174 -
   7.175 -
   7.176 -Goal "lfilter p l = LNil  |  \
   7.177 -\         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
   7.178 -by (case_tac "l : Domain(findRel p)" 1);
   7.179 -by (Asm_simp_tac 2);
   7.180 -by (blast_tac (claset() addSEs [Domain_findRelE] 
   7.181 -                        addIs  [findRel_imp_lfilter]) 1);
   7.182 -qed "lfilter_cases";
   7.183 -
   7.184 -
   7.185 -(*** lfilter: simple facts by coinduction ***)
   7.186 -
   7.187 -Goal "lfilter (%x. True) l = l";
   7.188 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   7.189 -by (ALLGOALS Simp_tac);
   7.190 -qed "lfilter_K_True";
   7.191 -
   7.192 -Goal "lfilter p (lfilter p l) = lfilter p l";
   7.193 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   7.194 -by (ALLGOALS Simp_tac);
   7.195 -by Safe_tac;
   7.196 -(*Cases: p x is true or false*)
   7.197 -by (rtac (lfilter_cases RS disjE) 1);
   7.198 -by (etac ssubst 1);
   7.199 -by Auto_tac;
   7.200 -qed "lfilter_idem";
   7.201 -
   7.202 -
   7.203 -(*** Numerous lemmas required to prove lfilter_conj:
   7.204 -     lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
   7.205 - ***)
   7.206 -
   7.207 -Goal "(l,l') : findRel q \
   7.208 -\           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
   7.209 -by (etac findRel.induct 1);
   7.210 -by (blast_tac (claset() addIs findRel.intrs) 1);
   7.211 -by (blast_tac (claset() addIs findRel.intrs) 1);
   7.212 -qed_spec_mp "findRel_conj_lemma";
   7.213 -
   7.214 -val findRel_conj = refl RSN (2, findRel_conj_lemma);
   7.215 -
   7.216 -Goal "(l,l'') : findRel (%x. p x & q x) \
   7.217 -\              ==> (l, LCons x l') : findRel q --> ~ p x     \
   7.218 -\                  --> l' : Domain (findRel (%x. p x & q x))";
   7.219 -by (etac findRel.induct 1);
   7.220 -by Auto_tac;
   7.221 -qed_spec_mp "findRel_not_conj_Domain";
   7.222 -
   7.223 -
   7.224 -Goal "(l,lxx) : findRel q ==> \
   7.225 -\            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
   7.226 -\            --> (l,lz) : findRel (%x. p x & q x)";
   7.227 -by (etac findRel.induct 1);
   7.228 -by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
   7.229 -qed_spec_mp "findRel_conj2";
   7.230 -
   7.231 -
   7.232 -Goal "(lx,ly) : findRel p \
   7.233 -\              ==> ALL l. lx = lfilter q l \
   7.234 -\                  --> l : Domain (findRel(%x. p x & q x))";
   7.235 -by (etac findRel.induct 1);
   7.236 -by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
   7.237 -                        addIs  [findRel_conj]) 1);
   7.238 -by Auto_tac;
   7.239 -by (dtac (sym RS lfilter_eq_LCons) 1);
   7.240 -by Auto_tac;
   7.241 -by (dtac spec 1);
   7.242 -by (dtac (refl RS rev_mp) 1);
   7.243 -by (blast_tac (claset() addIs [findRel_conj2]) 1);
   7.244 -qed_spec_mp "findRel_lfilter_Domain_conj";
   7.245 -
   7.246 -
   7.247 -Goal "(l,l'') : findRel(%x. p x & q x) \
   7.248 -\              ==> l'' = LCons y l' --> \
   7.249 -\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
   7.250 -by (etac findRel.induct 1);
   7.251 -by (ALLGOALS Asm_simp_tac);
   7.252 -by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
   7.253 -qed_spec_mp "findRel_conj_lfilter";
   7.254 -
   7.255 -
   7.256 -
   7.257 -Goal "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)  \
   7.258 -\         : llistD_Fun (range                                   \
   7.259 -\                       (%u. (lfilter p (lfilter q u),          \
   7.260 -\                             lfilter (%x. p x & q x) u)))";
   7.261 -by (case_tac "l : Domain(findRel q)" 1);
   7.262 -by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   7.263 -by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
   7.264 -(*There are no qs in l: both lists are LNil*)
   7.265 -by (Asm_simp_tac 2);
   7.266 -by (etac Domain_findRelE 1);
   7.267 -(*case q x*)
   7.268 -by (case_tac "p x" 1);
   7.269 -by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
   7.270 -(*case q x and ~(p x) *)
   7.271 -by (Asm_simp_tac 1);
   7.272 -by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
   7.273 -(*subcase: there is no p&q in l' and therefore none in l*)
   7.274 -by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   7.275 -by (blast_tac (claset() addIs [findRel_not_conj_Domain]) 3);
   7.276 -by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
   7.277 -by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
   7.278 -(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
   7.279 -by (Asm_simp_tac 2);
   7.280 -(*subcase: there is a p&q in l' and therefore also one in l*)
   7.281 -by (etac Domain_findRelE 1);
   7.282 -by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
   7.283 -by (blast_tac (claset() addIs [findRel_conj2]) 2);
   7.284 -by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
   7.285 -by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
   7.286 -by (Asm_simp_tac 1);
   7.287 -val lemma = result();
   7.288 -
   7.289 -
   7.290 -Goal "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
   7.291 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   7.292 -by (ALLGOALS Simp_tac);
   7.293 -by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
   7.294 -qed "lfilter_conj";
   7.295 -
   7.296 -
   7.297 -(*** Numerous lemmas required to prove ??:
   7.298 -     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
   7.299 - ***)
   7.300 -
   7.301 -Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
   7.302 -by (etac findRel.induct 1);
   7.303 -by (ALLGOALS Asm_full_simp_tac);
   7.304 -qed "findRel_lmap_Domain";
   7.305 -
   7.306 -
   7.307 -Goal "lmap f l = LCons x l' -->     \
   7.308 -\              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
   7.309 -by (stac (lmap_def RS def_llist_corec) 1);
   7.310 -by (res_inst_tac [("l", "l")] llistE 1);
   7.311 -by Auto_tac;
   7.312 -qed_spec_mp "lmap_eq_LCons";
   7.313 -
   7.314 -
   7.315 -Goal "(lx,ly) : findRel p ==>  \
   7.316 -\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
   7.317 -\    (EX y l''. x = f y & l' = lmap f l'' &       \
   7.318 -\    (l, LCons y l'') : findRel(%x. p(f x)))";
   7.319 -by (etac findRel.induct 1);
   7.320 -by (ALLGOALS Asm_simp_tac);
   7.321 -by (safe_tac (claset() addSDs [lmap_eq_LCons]));
   7.322 -by (blast_tac (claset() addIs findRel.intrs) 1);
   7.323 -by (blast_tac (claset() addIs findRel.intrs) 1);
   7.324 -qed_spec_mp "lmap_LCons_findRel_lemma";
   7.325 -
   7.326 -val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
   7.327 -
   7.328 -Goal "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
   7.329 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   7.330 -by (ALLGOALS Simp_tac);
   7.331 -by Safe_tac;
   7.332 -by (case_tac "lmap f l : Domain (findRel p)" 1);
   7.333 -by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
   7.334 -by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
   7.335 -by (Asm_simp_tac 2);
   7.336 -by (etac Domain_findRelE 1);
   7.337 -by (ftac lmap_LCons_findRel 1);
   7.338 -by (Clarify_tac 1);
   7.339 -by (Asm_simp_tac 1);
   7.340 -qed "lfilter_lmap";
     8.1 --- a/src/HOL/Induct/LFilter.thy	Tue Apr 02 13:47:01 2002 +0200
     8.2 +++ b/src/HOL/Induct/LFilter.thy	Tue Apr 02 14:28:28 2002 +0200
     8.3 @@ -2,28 +2,271 @@
     8.4      ID:         $Id$
     8.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.6      Copyright   1997  University of Cambridge
     8.7 -
     8.8 -The "filter" functional for coinductive lists
     8.9 -  --defined by a combination of induction and coinduction
    8.10  *)
    8.11  
    8.12 -LFilter = LList +
    8.13 +header {*The "filter" functional for coinductive lists
    8.14 +  --defined by a combination of induction and coinduction*}
    8.15 +
    8.16 +theory LFilter = LList:
    8.17  
    8.18  consts
    8.19    findRel	:: "('a => bool) => ('a llist * 'a llist)set"
    8.20  
    8.21  inductive "findRel p"
    8.22 -  intrs
    8.23 -    found  "p x ==> (LCons x l, LCons x l) : findRel p"
    8.24 -    seek   "[| ~p x;  (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
    8.25 +  intros
    8.26 +    found:  "p x ==> (LCons x l, LCons x l) \<in> findRel p"
    8.27 +    seek:   "[| ~p x;  (l,l') \<in> findRel p |] ==> (LCons x l, l') \<in> findRel p"
    8.28 +
    8.29 +declare findRel.intros [intro]
    8.30  
    8.31  constdefs
    8.32 -  find		:: ['a => bool, 'a llist] => 'a llist
    8.33 +  find    :: "['a => bool, 'a llist] => 'a llist"
    8.34      "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
    8.35  
    8.36 -  lfilter	:: ['a => bool, 'a llist] => 'a llist
    8.37 +  lfilter :: "['a => bool, 'a llist] => 'a llist"
    8.38      "lfilter p l == llist_corec l (%l. case find p l of
    8.39                                              LNil => None
    8.40                                            | LCons y z => Some(y,z))"
    8.41  
    8.42 +
    8.43 +subsection {* findRel: basic laws *}
    8.44 +
    8.45 +inductive_cases
    8.46 +  findRel_LConsE [elim!]: "(LCons x l, l'') \<in> findRel p"
    8.47 +
    8.48 +
    8.49 +lemma findRel_functional [rule_format]:
    8.50 +     "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'"
    8.51 +by (erule findRel.induct, auto)
    8.52 +
    8.53 +lemma findRel_imp_LCons [rule_format]:
    8.54 +     "(l,l'): findRel p ==> \<exists>x l''. l' = LCons x l'' & p x"
    8.55 +by (erule findRel.induct, auto)
    8.56 +
    8.57 +lemma findRel_LNil [elim!]: "(LNil,l): findRel p ==> R"
    8.58 +by (blast elim: findRel.cases)
    8.59 +
    8.60 +
    8.61 +subsection {* Properties of Domain (findRel p) *}
    8.62 +
    8.63 +lemma LCons_Domain_findRel [simp]:
    8.64 +     "LCons x l \<in> Domain(findRel p) = (p x | l \<in> Domain(findRel p))"
    8.65 +by auto
    8.66 +
    8.67 +lemma Domain_findRel_iff:
    8.68 +     "(l \<in> Domain (findRel p)) = (\<exists>x l'. (l, LCons x l') \<in> findRel p &  p x)" 
    8.69 +by (blast dest: findRel_imp_LCons) 
    8.70 +
    8.71 +lemma Domain_findRel_mono:
    8.72 +    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)"
    8.73 +apply clarify
    8.74 +apply (erule findRel.induct, blast+)
    8.75 +done
    8.76 +
    8.77 +
    8.78 +subsection {* find: basic equations *}
    8.79 +
    8.80 +lemma find_LNil [simp]: "find p LNil = LNil"
    8.81 +by (unfold find_def, blast)
    8.82 +
    8.83 +lemma findRel_imp_find [simp]: "(l,l') \<in> findRel p ==> find p l = l'"
    8.84 +apply (unfold find_def)
    8.85 +apply (blast dest: findRel_functional)
    8.86 +done
    8.87 +
    8.88 +lemma find_LCons_found: "p x ==> find p (LCons x l) = LCons x l"
    8.89 +by (blast intro: findRel_imp_find)
    8.90 +
    8.91 +lemma diverge_find_LNil [simp]: "l ~: Domain(findRel p) ==> find p l = LNil"
    8.92 +by (unfold find_def, blast)
    8.93 +
    8.94 +lemma find_LCons_seek: "~ (p x) ==> find p (LCons x l) = find p l"
    8.95 +apply (case_tac "LCons x l \<in> Domain (findRel p) ")
    8.96 + apply auto 
    8.97 +apply (blast intro: findRel_imp_find)
    8.98 +done
    8.99 +
   8.100 +lemma find_LCons [simp]:
   8.101 +     "find p (LCons x l) = (if p x then LCons x l else find p l)"
   8.102 +by (simp add: find_LCons_seek find_LCons_found)
   8.103 +
   8.104 +
   8.105 +
   8.106 +subsection {* lfilter: basic equations *}
   8.107 +
   8.108 +lemma lfilter_LNil [simp]: "lfilter p LNil = LNil"
   8.109 +by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   8.110 +
   8.111 +lemma diverge_lfilter_LNil [simp]:
   8.112 +     "l ~: Domain(findRel p) ==> lfilter p l = LNil"
   8.113 +by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   8.114 +
   8.115 +lemma lfilter_LCons_found:
   8.116 +     "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)"
   8.117 +by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   8.118 +
   8.119 +lemma findRel_imp_lfilter [simp]:
   8.120 +     "(l, LCons x l') \<in> findRel p ==> lfilter p l = LCons x (lfilter p l')"
   8.121 +by (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   8.122 +
   8.123 +lemma lfilter_LCons_seek: "~ (p x) ==> lfilter p (LCons x l) = lfilter p l"
   8.124 +apply (rule lfilter_def [THEN def_llist_corec, THEN trans], simp)
   8.125 +apply (case_tac "LCons x l \<in> Domain (findRel p) ")
   8.126 + apply (simp add: Domain_findRel_iff, auto) 
   8.127 +done
   8.128 +
   8.129 +lemma lfilter_LCons [simp]:
   8.130 +     "lfilter p (LCons x l) =  
   8.131 +          (if p x then LCons x (lfilter p l) else lfilter p l)"
   8.132 +by (simp add: lfilter_LCons_found lfilter_LCons_seek)
   8.133 +
   8.134 +declare llistD_Fun_LNil_I [intro!] llistD_Fun_LCons_I [intro!]
   8.135 +
   8.136 +
   8.137 +lemma lfilter_eq_LNil: "lfilter p l = LNil ==> l ~: Domain(findRel p)" 
   8.138 +apply (auto iff: Domain_findRel_iff)
   8.139 +apply (rotate_tac 1, simp) 
   8.140 +done
   8.141 +
   8.142 +lemma lfilter_eq_LCons [rule_format]:
   8.143 +     "lfilter p l = LCons x l' -->      
   8.144 +               (\<exists>l''. l' = lfilter p l'' & (l, LCons x l'') \<in> findRel p)"
   8.145 +apply (subst lfilter_def [THEN def_llist_corec])
   8.146 +apply (case_tac "l \<in> Domain (findRel p) ")
   8.147 + apply (auto iff: Domain_findRel_iff)
   8.148 +done
   8.149 +
   8.150 +
   8.151 +lemma lfilter_cases: "lfilter p l = LNil  |   
   8.152 +          (\<exists>y l'. lfilter p l = LCons y (lfilter p l') & p y)"
   8.153 +apply (case_tac "l \<in> Domain (findRel p) ")
   8.154 +apply (auto iff: Domain_findRel_iff)
   8.155 +done
   8.156 +
   8.157 +
   8.158 +subsection {* lfilter: simple facts by coinduction *}
   8.159 +
   8.160 +lemma lfilter_K_True: "lfilter (%x. True) l = l"
   8.161 +by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   8.162 +
   8.163 +lemma lfilter_idem: "lfilter p (lfilter p l) = lfilter p l"
   8.164 +apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   8.165 +apply safe
   8.166 +txt{*Cases: p x is true or false*}
   8.167 +apply (rule lfilter_cases [THEN disjE])
   8.168 + apply (erule ssubst, auto)
   8.169 +done
   8.170 +
   8.171 +
   8.172 +subsection {* Numerous lemmas required to prove @{text lfilter_conj} *}
   8.173 +
   8.174 +lemma findRel_conj_lemma [rule_format]:
   8.175 +     "(l,l') \<in> findRel q  
   8.176 +      ==> l' = LCons x l'' --> p x --> (l,l') \<in> findRel (%x. p x & q x)"
   8.177 +by (erule findRel.induct, auto)
   8.178 +
   8.179 +lemmas findRel_conj = findRel_conj_lemma [OF _ refl]
   8.180 +
   8.181 +lemma findRel_not_conj_Domain [rule_format]:
   8.182 +     "(l,l'') \<in> findRel (%x. p x & q x)  
   8.183 +      ==> (l, LCons x l') \<in> findRel q --> ~ p x --> 
   8.184 +          l' \<in> Domain (findRel (%x. p x & q x))"
   8.185 +by (erule findRel.induct, auto)
   8.186 +
   8.187 +lemma findRel_conj2 [rule_format]:
   8.188 +     "(l,lxx) \<in> findRel q 
   8.189 +      ==> lxx = LCons x lx --> (lx,lz) \<in> findRel(%x. p x & q x) --> ~ p x  
   8.190 +          --> (l,lz) \<in> findRel (%x. p x & q x)"
   8.191 +by (erule findRel.induct, auto)
   8.192 +
   8.193 +lemma findRel_lfilter_Domain_conj [rule_format]:
   8.194 +     "(lx,ly) \<in> findRel p  
   8.195 +      ==> \<forall>l. lx = lfilter q l --> l \<in> Domain (findRel(%x. p x & q x))"
   8.196 +apply (erule findRel.induct)
   8.197 + apply (blast dest!: sym [THEN lfilter_eq_LCons] intro: findRel_conj, auto)
   8.198 +apply (drule sym [THEN lfilter_eq_LCons], auto)
   8.199 +apply (drule spec)
   8.200 +apply (drule refl [THEN rev_mp])
   8.201 +apply (blast intro: findRel_conj2)
   8.202 +done
   8.203 +
   8.204 +
   8.205 +lemma findRel_conj_lfilter [rule_format]:
   8.206 +     "(l,l'') \<in> findRel(%x. p x & q x)  
   8.207 +      ==> l'' = LCons y l' --> 
   8.208 +          (lfilter q l, LCons y (lfilter q l')) \<in> findRel p"
   8.209 +by (erule findRel.induct, auto)
   8.210 +
   8.211 +lemma lfilter_conj_lemma:
   8.212 +     "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)   
   8.213 +      \<in> llistD_Fun (range (%u. (lfilter p (lfilter q u),           
   8.214 +                                lfilter (%x. p x & q x) u)))"
   8.215 +apply (case_tac "l \<in> Domain (findRel q)")
   8.216 + apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   8.217 +  prefer 3 apply (blast intro: rev_subsetD [OF _ Domain_findRel_mono])
   8.218 + txt{*There are no qs in l: both lists are LNil*}
   8.219 + apply (simp_all add: Domain_findRel_iff, clarify) 
   8.220 +txt{*case q x*}
   8.221 +apply (case_tac "p x")
   8.222 + apply (simp_all add: findRel_conj [THEN findRel_imp_lfilter])
   8.223 + txt{*case q x and ~(p x) *}
   8.224 +apply (case_tac "l' \<in> Domain (findRel (%x. p x & q x))")
   8.225 + txt{*subcase: there is no p&q in l' and therefore none in l*}
   8.226 + apply (subgoal_tac [2] "l ~: Domain (findRel (%x. p x & q x))")
   8.227 +  prefer 3 apply (blast intro: findRel_not_conj_Domain)
   8.228 + apply (subgoal_tac [2] "lfilter q l' ~: Domain (findRel p) ")
   8.229 +  prefer 3 apply (blast intro: findRel_lfilter_Domain_conj)
   8.230 + txt{*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*}
   8.231 + apply (simp_all add: Domain_findRel_iff, clarify) 
   8.232 +txt{*subcase: there is a p&q in l' and therefore also one in l*}
   8.233 +apply (subgoal_tac " (l, LCons xa l'a) \<in> findRel (%x. p x & q x) ")
   8.234 + prefer 2 apply (blast intro: findRel_conj2)
   8.235 +apply (subgoal_tac " (lfilter q l', LCons xa (lfilter q l'a)) \<in> findRel p")
   8.236 + apply simp 
   8.237 +apply (blast intro: findRel_conj_lfilter)
   8.238 +done
   8.239 +
   8.240 +
   8.241 +lemma lfilter_conj: "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l"
   8.242 +apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   8.243 +apply (blast intro: lfilter_conj_lemma rev_subsetD [OF _ llistD_Fun_mono])
   8.244 +done
   8.245 +
   8.246 +
   8.247 +subsection {* Numerous lemmas required to prove ??:
   8.248 +     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
   8.249 + *}
   8.250 +
   8.251 +lemma findRel_lmap_Domain:
   8.252 +     "(l,l') \<in> findRel(%x. p (f x)) ==> lmap f l \<in> Domain(findRel p)"
   8.253 +by (erule findRel.induct, auto)
   8.254 +
   8.255 +lemma lmap_eq_LCons [rule_format]: "lmap f l = LCons x l' -->      
   8.256 +               (\<exists>y l''. x = f y & l' = lmap f l'' & l = LCons y l'')"
   8.257 +apply (subst lmap_def [THEN def_llist_corec])
   8.258 +apply (rule_tac l = "l" in llistE, auto)
   8.259 +done
   8.260 +
   8.261 +
   8.262 +lemma lmap_LCons_findRel_lemma [rule_format]:
   8.263 +     "(lx,ly) \<in> findRel p
   8.264 +      ==> \<forall>l. lmap f l = lx --> ly = LCons x l' -->  
   8.265 +          (\<exists>y l''. x = f y & l' = lmap f l'' &        
   8.266 +          (l, LCons y l'') \<in> findRel(%x. p(f x)))"
   8.267 +apply (erule findRel.induct, simp_all)
   8.268 +apply (blast dest!: lmap_eq_LCons)+
   8.269 +done
   8.270 +
   8.271 +lemmas lmap_LCons_findRel = lmap_LCons_findRel_lemma [OF _ refl refl]
   8.272 +
   8.273 +lemma lfilter_lmap: "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)"
   8.274 +apply (rule_tac l = "l" in llist_fun_equalityI, simp_all)
   8.275 +apply safe
   8.276 +apply (case_tac "lmap f l \<in> Domain (findRel p)")
   8.277 + apply (simp add: Domain_findRel_iff, clarify)
   8.278 + apply (frule lmap_LCons_findRel, force) 
   8.279 +apply (subgoal_tac "l ~: Domain (findRel (%x. p (f x)))", simp)
   8.280 +apply (blast intro: findRel_lmap_Domain)
   8.281 +done
   8.282 +
   8.283  end
     9.1 --- a/src/HOL/Induct/LList.ML	Tue Apr 02 13:47:01 2002 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,876 +0,0 @@
     9.4 -(*  Title:      HOL/Induct/LList
     9.5 -    ID:         $Id$
     9.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 -    Copyright   1993  University of Cambridge
     9.8 -
     9.9 -SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
    9.10 -*)
    9.11 -
    9.12 -bind_thm ("UN1_I", UNIV_I RS UN_I);
    9.13 -
    9.14 -(** Simplification **)
    9.15 -
    9.16 -Addsplits [option.split];
    9.17 -
    9.18 -(*This justifies using llist in other recursive type definitions*)
    9.19 -Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
    9.20 -by (rtac gfp_mono 1);
    9.21 -by (REPEAT (ares_tac basic_monos 1));
    9.22 -qed "llist_mono";
    9.23 -
    9.24 -
    9.25 -Goal "llist(A) = usum {Numb(0)} (uprod A (llist A))";
    9.26 -let val rew = rewrite_rule [NIL_def, CONS_def] in  
    9.27 -by (fast_tac (claset() addSIs (map rew llist.intrs)
    9.28 -                       addEs [rew llist.elim]) 1)
    9.29 -end;
    9.30 -qed "llist_unfold";
    9.31 -
    9.32 -
    9.33 -(*** Type checking by coinduction, using list_Fun 
    9.34 -     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
    9.35 -***)
    9.36 -
    9.37 -Goalw [list_Fun_def]
    9.38 -    "[| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
    9.39 -by (etac llist.coinduct 1);
    9.40 -by (etac (subsetD RS CollectD) 1);
    9.41 -by (assume_tac 1);
    9.42 -qed "llist_coinduct";
    9.43 -
    9.44 -Goalw [list_Fun_def, NIL_def] "NIL: list_Fun A X";
    9.45 -by (Fast_tac 1);
    9.46 -qed "list_Fun_NIL_I";
    9.47 -AddIffs [list_Fun_NIL_I];
    9.48 -
    9.49 -Goalw [list_Fun_def,CONS_def]
    9.50 -    "[| M: A;  N: X |] ==> CONS M N : list_Fun A X";
    9.51 -by (Fast_tac 1);
    9.52 -qed "list_Fun_CONS_I";
    9.53 -Addsimps [list_Fun_CONS_I];
    9.54 -AddSIs   [list_Fun_CONS_I];
    9.55 -
    9.56 -(*Utilise the "strong" part, i.e. gfp(f)*)
    9.57 -Goalw (llist.defs @ [list_Fun_def])
    9.58 -    "M: llist(A) ==> M : list_Fun A (X Un llist(A))";
    9.59 -by (etac (llist.mono RS gfp_fun_UnI2) 1);
    9.60 -qed "list_Fun_llist_I";
    9.61 -
    9.62 -(*** LList_corec satisfies the desired recurion equation ***)
    9.63 -
    9.64 -(*A continuity result?*)
    9.65 -Goalw [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))";
    9.66 -by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
    9.67 -qed "CONS_UN1";
    9.68 -
    9.69 -Goalw [CONS_def] "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
    9.70 -by (REPEAT (ares_tac [In1_mono,Scons_mono] 1));
    9.71 -qed "CONS_mono";
    9.72 -
    9.73 -Addsimps [LList_corec_fun_def RS def_nat_rec_0,
    9.74 -          LList_corec_fun_def RS def_nat_rec_Suc];
    9.75 -
    9.76 -(** The directions of the equality are proved separately **)
    9.77 -
    9.78 -Goalw [LList_corec_def]
    9.79 -    "LList_corec a f <= \
    9.80 -\    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
    9.81 -by (rtac UN_least 1);
    9.82 -by (case_tac "k" 1);
    9.83 -by (ALLGOALS Asm_simp_tac);
    9.84 -by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
    9.85 -			 UNIV_I RS UN_upper] 1));
    9.86 -qed "LList_corec_subset1";
    9.87 -
    9.88 -Goalw [LList_corec_def]
    9.89 -    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
    9.90 -\    LList_corec a f";
    9.91 -by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
    9.92 -by Safe_tac;
    9.93 -by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I));
    9.94 -by (ALLGOALS Asm_simp_tac);
    9.95 -qed "LList_corec_subset2";
    9.96 -
    9.97 -(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
    9.98 -Goal "LList_corec a f =  \
    9.99 -\     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
   9.100 -by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
   9.101 -                         LList_corec_subset2] 1));
   9.102 -qed "LList_corec";
   9.103 -
   9.104 -(*definitional version of same*)
   9.105 -val [rew] = 
   9.106 -Goal "[| !!x. h(x) == LList_corec x f |]     \
   9.107 -\     ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
   9.108 -by (rewtac rew);
   9.109 -by (rtac LList_corec 1);
   9.110 -qed "def_LList_corec";
   9.111 -
   9.112 -(*A typical use of co-induction to show membership in the gfp. 
   9.113 -  Bisimulation is  range(%x. LList_corec x f) *)
   9.114 -Goal "LList_corec a f : llist UNIV";
   9.115 -by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
   9.116 -by (rtac rangeI 1);
   9.117 -by Safe_tac;
   9.118 -by (stac LList_corec 1);
   9.119 -by (Simp_tac 1);
   9.120 -qed "LList_corec_type";
   9.121 -
   9.122 -
   9.123 -(**** llist equality as a gfp; the bisimulation principle ****)
   9.124 -
   9.125 -(*This theorem is actually used, unlike the many similar ones in ZF*)
   9.126 -Goal "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))";
   9.127 -let val rew = rewrite_rule [NIL_def, CONS_def] in  
   9.128 -by (fast_tac (claset() addSIs (map rew LListD.intrs)
   9.129 -                      addEs [rew LListD.elim]) 1)
   9.130 -end;
   9.131 -qed "LListD_unfold";
   9.132 -
   9.133 -Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
   9.134 -by (induct_thm_tac nat_less_induct "k" 1);
   9.135 -by (safe_tac (claset() delrules [equalityI]));
   9.136 -by (etac LListD.elim 1);
   9.137 -by (safe_tac (claset() delrules [equalityI]));
   9.138 -by (case_tac "n" 1);
   9.139 -by (Asm_simp_tac 1);
   9.140 -by (rename_tac "n'" 1);
   9.141 -by (case_tac "n'" 1);
   9.142 -by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
   9.143 -by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
   9.144 -qed "LListD_implies_ntrunc_equality";
   9.145 -
   9.146 -(*The domain of the LListD relation*)
   9.147 -Goalw (llist.defs @ [NIL_def, CONS_def])
   9.148 -    "Domain (LListD(diag A)) <= llist(A)";
   9.149 -by (rtac gfp_upperbound 1);
   9.150 -(*avoids unfolding LListD on the rhs*)
   9.151 -by (res_inst_tac [("P", "%x. Domain x <= ?B")] (LListD_unfold RS ssubst) 1);
   9.152 -by (Simp_tac 1);
   9.153 -by (Fast_tac 1);
   9.154 -qed "Domain_LListD";
   9.155 -
   9.156 -(*This inclusion justifies the use of coinduction to show M=N*)
   9.157 -Goal "LListD(diag A) <= diag(llist(A))";
   9.158 -by (rtac subsetI 1);
   9.159 -by (res_inst_tac [("p","x")] PairE 1);
   9.160 -by Safe_tac;
   9.161 -by (rtac diag_eqI 1);
   9.162 -by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
   9.163 -          ntrunc_equality) 1);
   9.164 -by (assume_tac 1);
   9.165 -by (etac (DomainI RS (Domain_LListD RS subsetD)) 1);
   9.166 -qed "LListD_subset_diag";
   9.167 -
   9.168 -
   9.169 -(** Coinduction, using LListD_Fun
   9.170 -    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
   9.171 - **)
   9.172 -
   9.173 -Goalw [LListD_Fun_def] "A<=B ==> LListD_Fun r A <= LListD_Fun r B";
   9.174 -by (REPEAT (ares_tac basic_monos 1));
   9.175 -qed "LListD_Fun_mono";
   9.176 -
   9.177 -Goalw [LListD_Fun_def]
   9.178 -    "[| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
   9.179 -by (etac LListD.coinduct 1);
   9.180 -by (etac (subsetD RS CollectD) 1);
   9.181 -by (assume_tac 1);
   9.182 -qed "LListD_coinduct";
   9.183 -
   9.184 -Goalw [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
   9.185 -by (Fast_tac 1);
   9.186 -qed "LListD_Fun_NIL_I";
   9.187 -
   9.188 -Goalw [LListD_Fun_def,CONS_def]
   9.189 - "[| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
   9.190 -by (Fast_tac 1);
   9.191 -qed "LListD_Fun_CONS_I";
   9.192 -
   9.193 -(*Utilise the "strong" part, i.e. gfp(f)*)
   9.194 -Goalw (LListD.defs @ [LListD_Fun_def])
   9.195 -    "M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
   9.196 -by (etac (LListD.mono RS gfp_fun_UnI2) 1);
   9.197 -qed "LListD_Fun_LListD_I";
   9.198 -
   9.199 -
   9.200 -(*This converse inclusion helps to strengthen LList_equalityI*)
   9.201 -Goal "diag(llist(A)) <= LListD(diag A)";
   9.202 -by (rtac subsetI 1);
   9.203 -by (etac LListD_coinduct 1);
   9.204 -by (rtac subsetI 1);
   9.205 -by (etac diagE 1);
   9.206 -by (etac ssubst 1);
   9.207 -by (eresolve_tac [llist.elim] 1);
   9.208 -by (ALLGOALS
   9.209 -    (asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
   9.210 -				       LListD_Fun_CONS_I])));
   9.211 -qed "diag_subset_LListD";
   9.212 -
   9.213 -Goal "LListD(diag A) = diag(llist(A))";
   9.214 -by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
   9.215 -                         diag_subset_LListD] 1));
   9.216 -qed "LListD_eq_diag";
   9.217 -
   9.218 -Goal "M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
   9.219 -by (rtac (LListD_eq_diag RS subst) 1);
   9.220 -by (rtac LListD_Fun_LListD_I 1);
   9.221 -by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
   9.222 -qed "LListD_Fun_diag_I";
   9.223 -
   9.224 -
   9.225 -(** To show two LLists are equal, exhibit a bisimulation! 
   9.226 -      [also admits true equality]
   9.227 -   Replace "A" by some particular set, like {x.True}??? *)
   9.228 -Goal "[| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
   9.229 -\         |] ==>  M=N";
   9.230 -by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
   9.231 -by (etac LListD_coinduct 1);
   9.232 -by (asm_simp_tac (simpset() addsimps [LListD_eq_diag]) 1);
   9.233 -by Safe_tac;
   9.234 -qed "LList_equalityI";
   9.235 -
   9.236 -
   9.237 -(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
   9.238 -
   9.239 -(*We must remove Pair_eq because it may turn an instance of reflexivity
   9.240 -  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
   9.241 -  (or strengthen the Solver?) 
   9.242 -*)
   9.243 -Delsimps [Pair_eq];
   9.244 -
   9.245 -(*abstract proof using a bisimulation*)
   9.246 -val [prem1,prem2] = 
   9.247 -Goal
   9.248 - "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
   9.249 -\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
   9.250 -\ ==> h1=h2";
   9.251 -by (rtac ext 1);
   9.252 -(*next step avoids an unknown (and flexflex pair) in simplification*)
   9.253 -by (res_inst_tac [("A", "UNIV"),
   9.254 -                  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
   9.255 -by (rtac rangeI 1);
   9.256 -by Safe_tac;
   9.257 -by (stac prem1 1);
   9.258 -by (stac prem2 1);
   9.259 -by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
   9.260 -				  UNIV_I RS LListD_Fun_CONS_I]) 1);
   9.261 -qed "LList_corec_unique";
   9.262 -
   9.263 -val [prem] = 
   9.264 -Goal 
   9.265 - "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
   9.266 -\ ==> h = (%x. LList_corec x f)";
   9.267 -by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
   9.268 -qed "equals_LList_corec";
   9.269 -
   9.270 -
   9.271 -(** Obsolete LList_corec_unique proof: complete induction, not coinduction **)
   9.272 -
   9.273 -Goalw [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
   9.274 -by (rtac ntrunc_one_In1 1);
   9.275 -qed "ntrunc_one_CONS";
   9.276 -
   9.277 -Goalw [CONS_def]
   9.278 -    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
   9.279 -by (Simp_tac 1);
   9.280 -qed "ntrunc_CONS";
   9.281 -
   9.282 -Addsimps [ntrunc_one_CONS, ntrunc_CONS];
   9.283 -
   9.284 -
   9.285 -val [prem1,prem2] = 
   9.286 -Goal 
   9.287 - "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
   9.288 -\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
   9.289 -\ ==> h1=h2";
   9.290 -by (rtac (ntrunc_equality RS ext) 1);
   9.291 -by (rename_tac "x k" 1);
   9.292 -by (res_inst_tac [("x", "x")] spec 1);
   9.293 -by (induct_thm_tac nat_less_induct "k" 1);
   9.294 -by (rename_tac "n" 1);
   9.295 -by (rtac allI 1);
   9.296 -by (rename_tac "y" 1);
   9.297 -by (stac prem1 1);
   9.298 -by (stac prem2 1);
   9.299 -by (Simp_tac 1);
   9.300 -by (strip_tac 1);
   9.301 -by (case_tac "n" 1);
   9.302 -by (rename_tac "m" 2);
   9.303 -by (case_tac "m" 2);
   9.304 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   9.305 -result();
   9.306 -
   9.307 -
   9.308 -(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
   9.309 -
   9.310 -Goal "mono(CONS(M))";
   9.311 -by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1));
   9.312 -qed "Lconst_fun_mono";
   9.313 -
   9.314 -(* Lconst(M) = CONS M (Lconst M) *)
   9.315 -bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_unfold)));
   9.316 -
   9.317 -(*A typical use of co-induction to show membership in the gfp.
   9.318 -  The containing set is simply the singleton {Lconst(M)}. *)
   9.319 -Goal "M:A ==> Lconst(M): llist(A)";
   9.320 -by (rtac (singletonI RS llist_coinduct) 1);
   9.321 -by Safe_tac;
   9.322 -by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
   9.323 -by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
   9.324 -qed "Lconst_type";
   9.325 -
   9.326 -Goal "Lconst(M) = LList_corec M (%x. Some(x,x))";
   9.327 -by (rtac (equals_LList_corec RS fun_cong) 1);
   9.328 -by (Simp_tac 1);
   9.329 -by (rtac Lconst 1);
   9.330 -qed "Lconst_eq_LList_corec";
   9.331 -
   9.332 -(*Thus we could have used gfp in the definition of Lconst*)
   9.333 -Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))";
   9.334 -by (rtac (equals_LList_corec RS fun_cong) 1);
   9.335 -by (Simp_tac 1);
   9.336 -by (rtac (Lconst_fun_mono RS gfp_unfold) 1);
   9.337 -qed "gfp_Lconst_eq_LList_corec";
   9.338 -
   9.339 -
   9.340 -(*** Isomorphisms ***)
   9.341 -
   9.342 -Goal "inj Rep_LList";
   9.343 -by (rtac inj_inverseI 1);
   9.344 -by (rtac Rep_LList_inverse 1);
   9.345 -qed "inj_Rep_LList";
   9.346 -
   9.347 -
   9.348 -Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
   9.349 -by (Asm_simp_tac 1);
   9.350 -qed "LListI";
   9.351 -
   9.352 -Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
   9.353 -by (Asm_simp_tac 1);
   9.354 -qed "LListD";
   9.355 -
   9.356 -
   9.357 -(** Distinctness of constructors **)
   9.358 -
   9.359 -Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
   9.360 -by (stac (thm "Abs_LList_inject") 1);
   9.361 -by (REPEAT (resolve_tac (llist.intrs @ [CONS_not_NIL, rangeI, 
   9.362 -                                        LListI, Rep_LList RS LListD]) 1));
   9.363 -qed "LCons_not_LNil";
   9.364 -
   9.365 -bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
   9.366 -
   9.367 -AddIffs [LCons_not_LNil, LNil_not_LCons];
   9.368 -
   9.369 -
   9.370 -(** llist constructors **)
   9.371 -
   9.372 -Goalw [LNil_def] "Rep_LList LNil = NIL";
   9.373 -by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
   9.374 -qed "Rep_LList_LNil";
   9.375 -
   9.376 -Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
   9.377 -by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
   9.378 -                         rangeI, Rep_LList RS LListD] 1));
   9.379 -qed "Rep_LList_LCons";
   9.380 -
   9.381 -(** Injectiveness of CONS and LCons **)
   9.382 -
   9.383 -Goalw [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
   9.384 -by (fast_tac (claset() addSEs [Scons_inject]) 1);
   9.385 -qed "CONS_CONS_eq2";
   9.386 -
   9.387 -bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE);
   9.388 -
   9.389 -
   9.390 -(*For reasoning about abstract llist constructors*)
   9.391 -
   9.392 -AddIs [Rep_LList RS LListD, LListI];
   9.393 -AddIs llist.intrs;
   9.394 -
   9.395 -Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
   9.396 -by (stac (thm "Abs_LList_inject") 1);
   9.397 -by (auto_tac (claset(), simpset() addsimps [thm "Rep_LList_inject"])); 
   9.398 -qed "LCons_LCons_eq";
   9.399 -
   9.400 -AddIffs [LCons_LCons_eq];
   9.401 -
   9.402 -Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
   9.403 -by (etac llist.elim 1);
   9.404 -by (etac CONS_neq_NIL 1);
   9.405 -by (Fast_tac 1);
   9.406 -qed "CONS_D2";
   9.407 -
   9.408 -
   9.409 -(****** Reasoning about llist(A) ******)
   9.410 -
   9.411 -Addsimps [List_case_NIL, List_case_CONS];
   9.412 -
   9.413 -(*A special case of list_equality for functions over lazy lists*)
   9.414 -val [Mlist,gMlist,NILcase,CONScase] = 
   9.415 -Goal
   9.416 - "[| M: llist(A); g(NIL): llist(A);                             \
   9.417 -\    f(NIL)=g(NIL);                                             \
   9.418 -\    !!x l. [| x:A;  l: llist(A) |] ==>                         \
   9.419 -\           (f(CONS x l),g(CONS x l)) :                         \
   9.420 -\               LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un  \
   9.421 -\                                   diag(llist(A)))             \
   9.422 -\ |] ==> f(M) = g(M)";
   9.423 -by (rtac LList_equalityI 1);
   9.424 -by (rtac (Mlist RS imageI) 1);
   9.425 -by (rtac image_subsetI 1);
   9.426 -by (etac llist.elim 1);
   9.427 -by (etac ssubst 1);
   9.428 -by (stac NILcase 1);
   9.429 -by (rtac (gMlist RS LListD_Fun_diag_I) 1);
   9.430 -by (etac ssubst 1);
   9.431 -by (REPEAT (ares_tac [CONScase] 1));
   9.432 -qed "LList_fun_equalityI";
   9.433 -
   9.434 -
   9.435 -(*** The functional "Lmap" ***)
   9.436 -
   9.437 -Goal "Lmap f NIL = NIL";
   9.438 -by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
   9.439 -by (Simp_tac 1);
   9.440 -qed "Lmap_NIL";
   9.441 -
   9.442 -Goal "Lmap f (CONS M N) = CONS (f M) (Lmap f N)";
   9.443 -by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
   9.444 -by (Simp_tac 1);
   9.445 -qed "Lmap_CONS";
   9.446 -
   9.447 -Addsimps [Lmap_NIL, Lmap_CONS];
   9.448 -
   9.449 -(*Another type-checking proof by coinduction*)
   9.450 -val [major,minor] = 
   9.451 -Goal "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
   9.452 -by (rtac (major RS imageI RS llist_coinduct) 1);
   9.453 -by Safe_tac;
   9.454 -by (etac llist.elim 1);
   9.455 -by (ALLGOALS Asm_simp_tac);
   9.456 -by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
   9.457 -                      minor, imageI, UnI1] 1));
   9.458 -qed "Lmap_type";
   9.459 -
   9.460 -(*This type checking rule synthesises a sufficiently large set for f*)
   9.461 -Goal "M: llist(A) ==> Lmap f M: llist(f`A)";
   9.462 -by (etac Lmap_type 1);
   9.463 -by (etac imageI 1);
   9.464 -qed "Lmap_type2";
   9.465 -
   9.466 -(** Two easy results about Lmap **)
   9.467 -
   9.468 -Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
   9.469 -by (dtac imageI 1);
   9.470 -by (etac LList_equalityI 1);
   9.471 -by Safe_tac;
   9.472 -by (etac llist.elim 1);
   9.473 -by (ALLGOALS Asm_simp_tac);
   9.474 -by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
   9.475 -                      rangeI RS LListD_Fun_CONS_I] 1));
   9.476 -qed "Lmap_compose";
   9.477 -
   9.478 -Goal "M: llist(A) ==> Lmap (%x. x) M = M";
   9.479 -by (dtac imageI 1);
   9.480 -by (etac LList_equalityI 1);
   9.481 -by Safe_tac;
   9.482 -by (etac llist.elim 1);
   9.483 -by (ALLGOALS Asm_simp_tac);
   9.484 -by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
   9.485 -                      rangeI RS LListD_Fun_CONS_I] 1));
   9.486 -qed "Lmap_ident";
   9.487 -
   9.488 -
   9.489 -(*** Lappend -- its two arguments cause some complications! ***)
   9.490 -
   9.491 -Goalw [Lappend_def] "Lappend NIL NIL = NIL";
   9.492 -by (rtac (LList_corec RS trans) 1);
   9.493 -by (Simp_tac 1);
   9.494 -qed "Lappend_NIL_NIL";
   9.495 -
   9.496 -Goalw [Lappend_def]
   9.497 -    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')";
   9.498 -by (rtac (LList_corec RS trans) 1);
   9.499 -by (Simp_tac 1);
   9.500 -qed "Lappend_NIL_CONS";
   9.501 -
   9.502 -Goalw [Lappend_def]
   9.503 -    "Lappend (CONS M M') N = CONS M (Lappend M' N)";
   9.504 -by (rtac (LList_corec RS trans) 1);
   9.505 -by (Simp_tac 1);
   9.506 -qed "Lappend_CONS";
   9.507 -
   9.508 -Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
   9.509 -          Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
   9.510 -
   9.511 -
   9.512 -Goal "M: llist(A) ==> Lappend NIL M = M";
   9.513 -by (etac LList_fun_equalityI 1);
   9.514 -by (ALLGOALS Asm_simp_tac);
   9.515 -qed "Lappend_NIL";
   9.516 -
   9.517 -Goal "M: llist(A) ==> Lappend M NIL = M";
   9.518 -by (etac LList_fun_equalityI 1);
   9.519 -by (ALLGOALS Asm_simp_tac);
   9.520 -qed "Lappend_NIL2";
   9.521 -
   9.522 -Addsimps [Lappend_NIL, Lappend_NIL2];
   9.523 -
   9.524 -
   9.525 -(** Alternative type-checking proofs for Lappend **)
   9.526 -
   9.527 -(*weak co-induction: bisimulation and case analysis on both variables*)
   9.528 -Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   9.529 -by (res_inst_tac
   9.530 -    [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
   9.531 -by (Fast_tac 1);
   9.532 -by Safe_tac;
   9.533 -by (eres_inst_tac [("aa", "u")] llist.elim 1);
   9.534 -by (eres_inst_tac [("aa", "v")] llist.elim 1);
   9.535 -by (ALLGOALS Asm_simp_tac);
   9.536 -by (Blast_tac 1);
   9.537 -qed "Lappend_type";
   9.538 -
   9.539 -(*strong co-induction: bisimulation and case analysis on one variable*)
   9.540 -Goal "[| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
   9.541 -by (res_inst_tac [("X", "(%u. Lappend u N)`llist(A)")] llist_coinduct 1);
   9.542 -by (etac imageI 1);
   9.543 -by (rtac image_subsetI 1);
   9.544 -by (eres_inst_tac [("aa", "x")] llist.elim 1);
   9.545 -by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
   9.546 -by (Asm_simp_tac 1);
   9.547 -qed "Lappend_type";
   9.548 -
   9.549 -(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
   9.550 -
   9.551 -(** llist_case: case analysis for 'a llist **)
   9.552 -
   9.553 -Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
   9.554 -           Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
   9.555 -
   9.556 -Goalw [llist_case_def,LNil_def]  "llist_case c d LNil = c";
   9.557 -by (Simp_tac 1);
   9.558 -qed "llist_case_LNil";
   9.559 -
   9.560 -Goalw [llist_case_def,LCons_def]
   9.561 -    "llist_case c d (LCons M N) = d M N";
   9.562 -by (Simp_tac 1);
   9.563 -qed "llist_case_LCons";
   9.564 -
   9.565 -(*Elimination is case analysis, not induction.*)
   9.566 -val [prem1,prem2] = 
   9.567 -Goalw [NIL_def,CONS_def]
   9.568 -     "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P";
   9.569 -by (rtac (Rep_LList RS LListD RS llist.elim) 1);
   9.570 -by (asm_full_simp_tac
   9.571 -    (simpset() addsimps [Rep_LList_LNil RS sym, thm "Rep_LList_inject"]) 1);
   9.572 -by (etac prem1 1); 
   9.573 -by (etac (LListI RS thm "Rep_LList_cases") 1); 
   9.574 -by (Clarify_tac 1);  
   9.575 -by (asm_full_simp_tac
   9.576 -    (simpset() addsimps [Rep_LList_LCons RS sym, thm "Rep_LList_inject"]) 1); 
   9.577 -by (etac prem2 1); 
   9.578 -qed "llistE";
   9.579 -
   9.580 -(** llist_corec: corecursion for 'a llist **)
   9.581 -
   9.582 -(*Lemma for the proof of llist_corec*)
   9.583 -Goal "LList_corec a \
   9.584 -\          (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
   9.585 -\       llist(range Leaf)";
   9.586 -by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
   9.587 -by (rtac rangeI 1);
   9.588 -by Safe_tac;
   9.589 -by (stac LList_corec 1);
   9.590 -by (Force_tac 1);
   9.591 -qed "LList_corec_type2";
   9.592 -
   9.593 -Goalw [llist_corec_def,LNil_def,LCons_def]
   9.594 -    "llist_corec a f =  \
   9.595 -\    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
   9.596 -by (stac LList_corec 1);
   9.597 -by (case_tac "f a" 1);
   9.598 -by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   9.599 -by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
   9.600 -qed "llist_corec";
   9.601 -
   9.602 -(*definitional version of same*)
   9.603 -val [rew] = 
   9.604 -Goal "[| !!x. h(x) == llist_corec x f |] ==>     \
   9.605 -\     h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
   9.606 -by (rewtac rew);
   9.607 -by (rtac llist_corec 1);
   9.608 -qed "def_llist_corec";
   9.609 -
   9.610 -(**** Proofs about type 'a llist functions ****)
   9.611 -
   9.612 -(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
   9.613 -
   9.614 -Goalw [LListD_Fun_def]
   9.615 -    "r <= (llist A) <*> (llist A) ==> \
   9.616 -\           LListD_Fun (diag A) r <= (llist A) <*> (llist A)";
   9.617 -by (stac llist_unfold 1);
   9.618 -by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   9.619 -by (Fast_tac 1);
   9.620 -qed "LListD_Fun_subset_Times_llist";
   9.621 -
   9.622 -Goal "prod_fun Rep_LList Rep_LList ` r <= \
   9.623 -\    (llist(range Leaf)) <*> (llist(range Leaf))";
   9.624 -by (fast_tac (claset() delrules [image_subsetI]
   9.625 -		       addIs [Rep_LList RS LListD]) 1);
   9.626 -qed "subset_Times_llist";
   9.627 -
   9.628 -Goal "r <= (llist(range Leaf)) <*> (llist(range Leaf)) ==> \
   9.629 -\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r";
   9.630 -by Safe_tac;
   9.631 -by (etac (subsetD RS SigmaE2) 1);
   9.632 -by (assume_tac 1);
   9.633 -by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
   9.634 -qed "prod_fun_lemma";
   9.635 -
   9.636 -Goal "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) = \
   9.637 -\    diag(llist(range Leaf))";
   9.638 -by (rtac equalityI 1);
   9.639 -by (Blast_tac 1);
   9.640 -by (fast_tac (claset() delSWrapper "split_all_tac"
   9.641 -		       addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
   9.642 -qed "prod_fun_range_eq_diag";
   9.643 -
   9.644 -(*Used with lfilter*)
   9.645 -Goalw [llistD_Fun_def, prod_fun_def]
   9.646 -    "A<=B ==> llistD_Fun A <= llistD_Fun B";
   9.647 -by Auto_tac;
   9.648 -by (rtac image_eqI 1);
   9.649 -by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
   9.650 -by (Force_tac 1);
   9.651 -qed "llistD_Fun_mono";
   9.652 -
   9.653 -(** To show two llists are equal, exhibit a bisimulation! 
   9.654 -      [also admits true equality] **)
   9.655 -Goalw [llistD_Fun_def]
   9.656 -    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
   9.657 -by (rtac (thm "Rep_LList_inject" RS iffD1) 1);
   9.658 -by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList `r"),
   9.659 -                  ("A", "range(Leaf)")] 
   9.660 -        LList_equalityI 1);
   9.661 -by (etac prod_fun_imageI 1);
   9.662 -by (etac (image_mono RS subset_trans) 1);
   9.663 -by (rtac (image_compose RS subst) 1);
   9.664 -by (rtac (prod_fun_compose RS subst) 1);
   9.665 -by (stac image_Un 1);
   9.666 -by (stac prod_fun_range_eq_diag 1);
   9.667 -by (rtac (LListD_Fun_subset_Times_llist RS prod_fun_lemma) 1);
   9.668 -by (rtac (subset_Times_llist RS Un_least) 1);
   9.669 -by (rtac diag_subset_Times 1);
   9.670 -qed "llist_equalityI";
   9.671 -
   9.672 -(** Rules to prove the 2nd premise of llist_equalityI **)
   9.673 -Goalw [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
   9.674 -by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
   9.675 -qed "llistD_Fun_LNil_I";
   9.676 -
   9.677 -Goalw [llistD_Fun_def,LCons_def]
   9.678 -    "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
   9.679 -by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
   9.680 -by (etac prod_fun_imageI 1);
   9.681 -qed "llistD_Fun_LCons_I";
   9.682 -
   9.683 -(*Utilise the "strong" part, i.e. gfp(f)*)
   9.684 -Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   9.685 -by (rtac (Rep_LList_inverse RS subst) 1);
   9.686 -by (rtac prod_fun_imageI 1);
   9.687 -by (stac image_Un 1);
   9.688 -by (stac prod_fun_range_eq_diag 1);
   9.689 -by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1);
   9.690 -qed "llistD_Fun_range_I";
   9.691 -
   9.692 -(*A special case of list_equality for functions over lazy lists*)
   9.693 -val [prem1,prem2] =
   9.694 -Goal "[| f(LNil)=g(LNil);                                                \
   9.695 -\        !!x l. (f(LCons x l),g(LCons x l)) :                            \
   9.696 -\               llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
   9.697 -\     |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
   9.698 -by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
   9.699 -by (rtac rangeI 1);
   9.700 -by (rtac subsetI 1);
   9.701 -by (etac rangeE 1);
   9.702 -by (etac ssubst 1);
   9.703 -by (res_inst_tac [("l", "u")] llistE 1);
   9.704 -by (etac ssubst 1);
   9.705 -by (stac prem1 1);
   9.706 -by (rtac llistD_Fun_range_I 1);
   9.707 -by (etac ssubst 1);
   9.708 -by (rtac prem2 1);
   9.709 -qed "llist_fun_equalityI";
   9.710 -
   9.711 -(*simpset for llist bisimulations*)
   9.712 -Addsimps [llist_case_LNil, llist_case_LCons, 
   9.713 -          llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   9.714 -
   9.715 -
   9.716 -(*** The functional "lmap" ***)
   9.717 -
   9.718 -Goal "lmap f LNil = LNil";
   9.719 -by (rtac (lmap_def RS def_llist_corec RS trans) 1);
   9.720 -by (Simp_tac 1);
   9.721 -qed "lmap_LNil";
   9.722 -
   9.723 -Goal "lmap f (LCons M N) = LCons (f M) (lmap f N)";
   9.724 -by (rtac (lmap_def RS def_llist_corec RS trans) 1);
   9.725 -by (Simp_tac 1);
   9.726 -qed "lmap_LCons";
   9.727 -
   9.728 -Addsimps [lmap_LNil, lmap_LCons];
   9.729 -
   9.730 -
   9.731 -(** Two easy results about lmap **)
   9.732 -
   9.733 -Goal "lmap (f o g) l = lmap f (lmap g l)";
   9.734 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.735 -by (ALLGOALS Simp_tac);
   9.736 -qed "lmap_compose";
   9.737 -
   9.738 -Goal "lmap (%x. x) l = l";
   9.739 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.740 -by (ALLGOALS Simp_tac);
   9.741 -qed "lmap_ident";
   9.742 -
   9.743 -
   9.744 -(*** iterates -- llist_fun_equalityI cannot be used! ***)
   9.745 -
   9.746 -Goal "iterates f x = LCons x (iterates f (f x))";
   9.747 -by (rtac (iterates_def RS def_llist_corec RS trans) 1);
   9.748 -by (Simp_tac 1);
   9.749 -qed "iterates";
   9.750 -
   9.751 -Goal "lmap f (iterates f x) = iterates f (f x)";
   9.752 -by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
   9.753 -    llist_equalityI 1);
   9.754 -by (rtac rangeI 1);
   9.755 -by Safe_tac;
   9.756 -by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
   9.757 -by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
   9.758 -by (Simp_tac 1);
   9.759 -qed "lmap_iterates";
   9.760 -
   9.761 -Goal "iterates f x = LCons x (lmap f (iterates f x))";
   9.762 -by (stac lmap_iterates 1);
   9.763 -by (rtac iterates 1);
   9.764 -qed "iterates_lmap";
   9.765 -
   9.766 -(*** A rather complex proof about iterates -- cf Andy Pitts ***)
   9.767 -
   9.768 -(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
   9.769 -
   9.770 -Goal "nat_rec (LCons b l) (%m. lmap(f)) n =      \
   9.771 -\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
   9.772 -by (induct_tac "n" 1);
   9.773 -by (ALLGOALS Asm_simp_tac);
   9.774 -qed "fun_power_lmap";
   9.775 -
   9.776 -goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
   9.777 -by (induct_tac "n" 1);
   9.778 -by (ALLGOALS Asm_simp_tac);
   9.779 -qed "fun_power_Suc";
   9.780 -
   9.781 -val Pair_cong = read_instantiate_sg (sign_of (theory "Product_Type"))
   9.782 - [("f","Pair")] (standard(refl RS cong RS cong));
   9.783 -
   9.784 -(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
   9.785 -  for all u and all n::nat.*)
   9.786 -val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
   9.787 -by (rtac ext 1);
   9.788 -by (res_inst_tac [("r", 
   9.789 -   "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
   9.790 -\                    nat_rec (iterates f u) (%m y. lmap f y) n))")] 
   9.791 -    llist_equalityI 1);
   9.792 -by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
   9.793 -by (Clarify_tac 1);
   9.794 -by (stac iterates 1);
   9.795 -by (stac prem 1);
   9.796 -by (stac fun_power_lmap 1);
   9.797 -by (stac fun_power_lmap 1);
   9.798 -by (rtac llistD_Fun_LCons_I 1);
   9.799 -by (rtac (lmap_iterates RS subst) 1);
   9.800 -by (stac fun_power_Suc 1);
   9.801 -by (stac fun_power_Suc 1);
   9.802 -by (rtac (UN1_I RS UnI1) 1);
   9.803 -by (rtac rangeI 1);
   9.804 -qed "iterates_equality";
   9.805 -
   9.806 -
   9.807 -(*** lappend -- its two arguments cause some complications! ***)
   9.808 -
   9.809 -Goalw [lappend_def] "lappend LNil LNil = LNil";
   9.810 -by (rtac (llist_corec RS trans) 1);
   9.811 -by (Simp_tac 1);
   9.812 -qed "lappend_LNil_LNil";
   9.813 -
   9.814 -Goalw [lappend_def]
   9.815 -    "lappend LNil (LCons l l') = LCons l (lappend LNil l')";
   9.816 -by (rtac (llist_corec RS trans) 1);
   9.817 -by (Simp_tac 1);
   9.818 -qed "lappend_LNil_LCons";
   9.819 -
   9.820 -Goalw [lappend_def]
   9.821 -    "lappend (LCons l l') N = LCons l (lappend l' N)";
   9.822 -by (rtac (llist_corec RS trans) 1);
   9.823 -by (Simp_tac 1);
   9.824 -qed "lappend_LCons";
   9.825 -
   9.826 -Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
   9.827 -
   9.828 -Goal "lappend LNil l = l";
   9.829 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.830 -by (ALLGOALS Simp_tac);
   9.831 -qed "lappend_LNil";
   9.832 -
   9.833 -Goal "lappend l LNil = l";
   9.834 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.835 -by (ALLGOALS Simp_tac);
   9.836 -qed "lappend_LNil2";
   9.837 -
   9.838 -Addsimps [lappend_LNil, lappend_LNil2];
   9.839 -
   9.840 -(*The infinite first argument blocks the second*)
   9.841 -Goal "lappend (iterates f x) N = iterates f x";
   9.842 -by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
   9.843 -    llist_equalityI 1);
   9.844 -by (rtac rangeI 1);
   9.845 -by Safe_tac;
   9.846 -by (stac iterates 1);
   9.847 -by (Simp_tac 1);
   9.848 -qed "lappend_iterates";
   9.849 -
   9.850 -(** Two proofs that lmap distributes over lappend **)
   9.851 -
   9.852 -(*Long proof requiring case analysis on both both arguments*)
   9.853 -Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
   9.854 -by (res_inst_tac 
   9.855 -    [("r",  
   9.856 -      "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
   9.857 -    llist_equalityI 1);
   9.858 -by (rtac UN1_I 1);
   9.859 -by (rtac rangeI 1);
   9.860 -by Safe_tac;
   9.861 -by (res_inst_tac [("l", "l")] llistE 1);
   9.862 -by (res_inst_tac [("l", "n")] llistE 1);
   9.863 -by (ALLGOALS Asm_simp_tac);
   9.864 -by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
   9.865 -qed "lmap_lappend_distrib";
   9.866 -
   9.867 -(*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
   9.868 -Goal "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
   9.869 -by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.870 -by (Simp_tac 1);
   9.871 -by (Simp_tac 1);
   9.872 -qed "lmap_lappend_distrib";
   9.873 -
   9.874 -(*Without strong coinduction, three case analyses might be needed*)
   9.875 -Goal "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
   9.876 -by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
   9.877 -by (Simp_tac 1);
   9.878 -by (Simp_tac 1);
   9.879 -qed "lappend_assoc";
    10.1 --- a/src/HOL/Induct/LList.thy	Tue Apr 02 13:47:01 2002 +0200
    10.2 +++ b/src/HOL/Induct/LList.thy	Tue Apr 02 14:28:28 2002 +0200
    10.3 @@ -1,13 +1,11 @@
    10.4 -(*  Title:      HOL/LList.thy
    10.5 +(*  Title:      HOL/Induct/LList.thy
    10.6      ID:         $Id$
    10.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.8      Copyright   1994  University of Cambridge
    10.9  
   10.10 -Definition of type 'a llist by a greatest fixed point
   10.11 -
   10.12  Shares NIL, CONS, List_case with List.thy
   10.13  
   10.14 -Still needs filter and flatten functions -- hard because they need
   10.15 +Still needs flatten function -- hard because it need
   10.16  bounds on the amount of lookahead required.
   10.17  
   10.18  Could try (but would it work for the gfp analogue of term?)
   10.19 @@ -23,49 +21,53 @@
   10.20         (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))`r)"
   10.21  *)
   10.22  
   10.23 -LList = Main + SList +
   10.24 +header {*Definition of type 'a llist by a greatest fixed point*}
   10.25 +
   10.26 +theory LList = Main + SList:
   10.27  
   10.28  consts
   10.29  
   10.30 -  llist      :: 'a item set => 'a item set
   10.31 -  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   10.32 +  llist  :: "'a item set => 'a item set"
   10.33 +  LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
   10.34  
   10.35  
   10.36  coinductive "llist(A)"
   10.37 -  intrs
   10.38 -    NIL_I  "NIL: llist(A)"
   10.39 -    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : llist(A)"
   10.40 +  intros
   10.41 +    NIL_I:  "NIL \<in> llist(A)"
   10.42 +    CONS_I:         "[| a \<in> A;  M \<in> llist(A) |] ==> CONS a M \<in> llist(A)"
   10.43  
   10.44  coinductive "LListD(r)"
   10.45 -  intrs
   10.46 -    NIL_I  "(NIL, NIL) : LListD(r)"
   10.47 -    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
   10.48 -            |] ==> (CONS a M, CONS b N) : LListD(r)"
   10.49 +  intros
   10.50 +    NIL_I:  "(NIL, NIL) \<in> LListD(r)"
   10.51 +    CONS_I:         "[| (a,b) \<in> r;  (M,N) \<in> LListD(r) |] 
   10.52 +                     ==> (CONS a M, CONS b N) \<in> LListD(r)"
   10.53  
   10.54  
   10.55  typedef (LList)
   10.56 -  'a llist = "llist(range Leaf) :: 'a item set" (llist.NIL_I)
   10.57 +  'a llist = "llist(range Leaf) :: 'a item set"
   10.58 +  by (blast intro: llist.NIL_I)
   10.59  
   10.60  constdefs
   10.61 -  (*Now used exclusively for abbreviating the coinduction rule*)
   10.62 -  list_Fun   :: ['a item set, 'a item set] => 'a item set
   10.63 -     "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   10.64 +  list_Fun   :: "['a item set, 'a item set] => 'a item set"
   10.65 +    --{*Now used exclusively for abbreviating the coinduction rule*}
   10.66 +     "list_Fun A X == {z. z = NIL | (\<exists>M a. z = CONS a M & a \<in> A & M \<in> X)}"
   10.67  
   10.68    LListD_Fun :: 
   10.69        "[('a item * 'a item)set, ('a item * 'a item)set] => 
   10.70         ('a item * 'a item)set"
   10.71      "LListD_Fun r X ==   
   10.72         {z. z = (NIL, NIL) |   
   10.73 -           (? M N a b. z = (CONS a M, CONS b N) & (a, b) : r & (M, N) : X)}"
   10.74 +           (\<exists>M N a b. z = (CONS a M, CONS b N) & (a, b) \<in> r & (M, N) \<in> X)}"
   10.75  
   10.76 -  (*the abstract constructors*)
   10.77 -  LNil       :: 'a llist
   10.78 +  LNil :: "'a llist"
   10.79 +     --{*abstract constructor*}
   10.80      "LNil == Abs_LList NIL"
   10.81  
   10.82 -  LCons      :: ['a, 'a llist] => 'a llist
   10.83 +  LCons :: "['a, 'a llist] => 'a llist"
   10.84 +     --{*abstract constructor*}
   10.85      "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
   10.86  
   10.87 -  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
   10.88 +  llist_case :: "['b, ['a, 'a llist]=>'b, 'a llist] => 'b"
   10.89      "llist_case c d l == 
   10.90         List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
   10.91  
   10.92 @@ -77,7 +79,7 @@
   10.93               k"
   10.94  
   10.95    LList_corec     :: "['a, 'a => ('b item * 'a) option] => 'b item"
   10.96 -    "LList_corec a f == UN k. LList_corec_fun k f a"
   10.97 +    "LList_corec a f == \<Union>k. LList_corec_fun k f a"
   10.98  
   10.99    llist_corec     :: "['a, 'a => ('b * 'a) option] => 'b llist"
  10.100      "llist_corec a f == 
  10.101 @@ -93,41 +95,810 @@
  10.102  
  10.103  
  10.104  
  10.105 -(*The case syntax for type 'a llist*)
  10.106 +text{*The case syntax for type 'a llist*}
  10.107  translations
  10.108    "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
  10.109  
  10.110  
  10.111 -(** Sample function definitions.  Item-based ones start with L ***)
  10.112 +subsubsection{* Sample function definitions.  Item-based ones start with L *}
  10.113  
  10.114  constdefs
  10.115 -  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
  10.116 +  Lmap       :: "('a item => 'b item) => ('a item => 'b item)"
  10.117      "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
  10.118  
  10.119 -  lmap       :: ('a=>'b) => ('a llist => 'b llist)
  10.120 +  lmap       :: "('a=>'b) => ('a llist => 'b llist)"
  10.121      "lmap f l == llist_corec l (%z. case z of LNil => None 
  10.122                                             | LCons y z => Some(f(y), z))"
  10.123  
  10.124 -  iterates   :: ['a => 'a, 'a] => 'a llist
  10.125 +  iterates   :: "['a => 'a, 'a] => 'a llist"
  10.126      "iterates f a == llist_corec a (%x. Some((x, f(x))))"     
  10.127  
  10.128 -  Lconst     :: 'a item => 'a item
  10.129 -    "Lconst(M) == lfp(%N. CONS M N)"     
  10.130 +  Lconst     :: "'a item => 'a item"
  10.131 +    "Lconst(M) == lfp(%N. CONS M N)"
  10.132  
  10.133 -(*Append generates its result by applying f, where
  10.134 -    f((NIL,NIL))          = None
  10.135 -    f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
  10.136 -    f((CONS M1 M2, N))    = Some((M1, (M2,N))
  10.137 -*)
  10.138 -
  10.139 -  Lappend    :: ['a item, 'a item] => 'a item
  10.140 +  Lappend    :: "['a item, 'a item] => 'a item"
  10.141     "Lappend M N == LList_corec (M,N)                                         
  10.142       (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) 
  10.143                        (%M1 M2 N. Some((M1, (M2,N))))))"
  10.144  
  10.145 -  lappend    :: ['a llist, 'a llist] => 'a llist
  10.146 +  lappend    :: "['a llist, 'a llist] => 'a llist"
  10.147      "lappend l n == llist_corec (l,n)                                         
  10.148         (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) 
  10.149                           (%l1 l2 n. Some((l1, (l2,n))))))"
  10.150  
  10.151 +
  10.152 +text{*Append generates its result by applying f, where
  10.153 +    f((NIL,NIL))          = None
  10.154 +    f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
  10.155 +    f((CONS M1 M2, N))    = Some((M1, (M2,N))
  10.156 +*}
  10.157 +
  10.158 +text{*
  10.159 +SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
  10.160 +*}
  10.161 +
  10.162 +lemmas UN1_I = UNIV_I [THEN UN_I, standard]
  10.163 +
  10.164 +subsubsection{* Simplification *}
  10.165 +
  10.166 +declare option.split [split]
  10.167 +
  10.168 +text{*This justifies using llist in other recursive type definitions*}
  10.169 +lemma llist_mono: "A<=B ==> llist(A) <= llist(B)"
  10.170 +apply (unfold llist.defs )
  10.171 +apply (rule gfp_mono)
  10.172 +apply (assumption | rule basic_monos)+
  10.173 +done
  10.174 +
  10.175 +
  10.176 +lemma llist_unfold: "llist(A) = usum {Numb(0)} (uprod A (llist A))"
  10.177 +  by (fast intro!: llist.intros [unfolded NIL_def CONS_def]
  10.178 +           elim: llist.cases [unfolded NIL_def CONS_def])
  10.179 +
  10.180 +
  10.181 +subsection{* Type checking by coinduction, using list_Fun 
  10.182 +     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  10.183 +*}
  10.184 +
  10.185 +lemma llist_coinduct: 
  10.186 +    "[| M \<in> X;  X <= list_Fun A (X Un llist(A)) |] ==>  M \<in> llist(A)"
  10.187 +apply (unfold list_Fun_def)
  10.188 +apply (erule llist.coinduct)
  10.189 +apply (erule subsetD [THEN CollectD], assumption)
  10.190 +done
  10.191 +
  10.192 +lemma list_Fun_NIL_I [iff]: "NIL \<in> list_Fun A X"
  10.193 +by (unfold list_Fun_def NIL_def, fast)
  10.194 +
  10.195 +lemma list_Fun_CONS_I [intro!,simp]: 
  10.196 +    "[| M \<in> A;  N \<in> X |] ==> CONS M N \<in> list_Fun A X"
  10.197 +apply (unfold list_Fun_def CONS_def, fast)
  10.198 +done
  10.199 +
  10.200 +
  10.201 +text{*Utilise the "strong" part, i.e. gfp(f)*}
  10.202 +lemma list_Fun_llist_I: "M \<in> llist(A) ==> M \<in> list_Fun A (X Un llist(A))"
  10.203 +apply (unfold llist.defs list_Fun_def)
  10.204 +apply (rule gfp_fun_UnI2) 
  10.205 +apply (rule monoI, blast) 
  10.206 +apply assumption
  10.207 +done
  10.208 +
  10.209 +subsection{* LList_corec satisfies the desired recurion equation *}
  10.210 +
  10.211 +text{*A continuity result?*}
  10.212 +lemma CONS_UN1: "CONS M (\<Union>x. f(x)) = (\<Union>x. CONS M (f x))"
  10.213 +apply (unfold CONS_def)
  10.214 +apply (simp add: In1_UN1 Scons_UN1_y)
  10.215 +done
  10.216 +
  10.217 +lemma CONS_mono: "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'"
  10.218 +apply (unfold CONS_def)
  10.219 +apply (assumption | rule In1_mono Scons_mono)+
  10.220 +done
  10.221 +
  10.222 +declare LList_corec_fun_def [THEN def_nat_rec_0, simp]
  10.223 +        LList_corec_fun_def [THEN def_nat_rec_Suc, simp]
  10.224 +
  10.225 +subsubsection{* The directions of the equality are proved separately *}
  10.226 +
  10.227 +lemma LList_corec_subset1: 
  10.228 +    "LList_corec a f <=  
  10.229 +     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
  10.230 +apply (unfold LList_corec_def)
  10.231 +apply (rule UN_least)
  10.232 +apply (case_tac "k")
  10.233 +apply (simp_all (no_asm_simp))
  10.234 +apply (rule allI impI subset_refl [THEN CONS_mono] UNIV_I [THEN UN_upper])+
  10.235 +done
  10.236 +
  10.237 +lemma LList_corec_subset2: 
  10.238 +    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <=  
  10.239 +     LList_corec a f"
  10.240 +apply (unfold LList_corec_def)
  10.241 +apply (simp add: CONS_UN1, safe) 
  10.242 +apply (rule_tac a="Suc(?k)" in UN_I, simp, simp)+ 
  10.243 +done
  10.244 +
  10.245 +text{*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*}
  10.246 +lemma LList_corec:
  10.247 +     "LList_corec a f =   
  10.248 +      (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))"
  10.249 +by (rule equalityI LList_corec_subset1 LList_corec_subset2)+
  10.250 +
  10.251 +text{*definitional version of same*}
  10.252 +lemma def_LList_corec: 
  10.253 +     "[| !!x. h(x) == LList_corec x f |]      
  10.254 +      ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))"
  10.255 +by (simp add: LList_corec)
  10.256 +
  10.257 +text{*A typical use of co-induction to show membership in the gfp. 
  10.258 +  Bisimulation is  range(%x. LList_corec x f) *}
  10.259 +lemma LList_corec_type: "LList_corec a f \<in> llist UNIV"
  10.260 +apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
  10.261 +apply (rule rangeI, safe)
  10.262 +apply (subst LList_corec, simp)
  10.263 +done
  10.264 +
  10.265 +
  10.266 +subsection{* llist equality as a gfp; the bisimulation principle *}
  10.267 +
  10.268 +text{*This theorem is actually used, unlike the many similar ones in ZF*}
  10.269 +lemma LListD_unfold: "LListD r = dsum (diag {Numb 0}) (dprod r (LListD r))"
  10.270 +  by (fast intro!: LListD.intros [unfolded NIL_def CONS_def]
  10.271 +           elim: LListD.cases [unfolded NIL_def CONS_def])
  10.272 +
  10.273 +lemma LListD_implies_ntrunc_equality [rule_format]:
  10.274 +     "\<forall>M N. (M,N) \<in> LListD(diag A) --> ntrunc k M = ntrunc k N"
  10.275 +apply (induct_tac "k" rule: nat_less_induct)
  10.276 +apply (safe del: equalityI)
  10.277 +apply (erule LListD.cases)
  10.278 +apply (safe del: equalityI)
  10.279 +apply (case_tac "n", simp)
  10.280 +apply (rename_tac "n'")
  10.281 +apply (case_tac "n'")
  10.282 +apply (simp_all add: CONS_def less_Suc_eq)
  10.283 +done
  10.284 +
  10.285 +text{*The domain of the LListD relation*}
  10.286 +lemma Domain_LListD: 
  10.287 +    "Domain (LListD(diag A)) <= llist(A)"
  10.288 +apply (unfold llist.defs NIL_def CONS_def)
  10.289 +apply (rule gfp_upperbound)
  10.290 +txt{*avoids unfolding LListD on the rhs*}
  10.291 +apply (rule_tac P = "%x. Domain x <= ?B" in LListD_unfold [THEN ssubst], simp)
  10.292 +apply blast 
  10.293 +done
  10.294 +
  10.295 +text{*This inclusion justifies the use of coinduction to show M=N*}
  10.296 +lemma LListD_subset_diag: "LListD(diag A) <= diag(llist(A))"
  10.297 +apply (rule subsetI)
  10.298 +apply (rule_tac p = "x" in PairE, safe)
  10.299 +apply (rule diag_eqI)
  10.300 +apply (rule LListD_implies_ntrunc_equality [THEN ntrunc_equality], assumption)
  10.301 +apply (erule DomainI [THEN Domain_LListD [THEN subsetD]])
  10.302 +done
  10.303 +
  10.304 +
  10.305 +subsubsection{* Coinduction, using LListD_Fun
  10.306 +    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  10.307 + *}
  10.308 +
  10.309 +lemma LListD_Fun_mono: "A<=B ==> LListD_Fun r A <= LListD_Fun r B"
  10.310 +apply (unfold LListD_Fun_def)
  10.311 +apply (assumption | rule basic_monos)+
  10.312 +done
  10.313 +
  10.314 +lemma LListD_coinduct: 
  10.315 +    "[| M \<in> X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M \<in> LListD(r)"
  10.316 +apply (unfold LListD_Fun_def)
  10.317 +apply (erule LListD.coinduct)
  10.318 +apply (erule subsetD [THEN CollectD], assumption)
  10.319 +done
  10.320 +
  10.321 +lemma LListD_Fun_NIL_I: "(NIL,NIL) \<in> LListD_Fun r s"
  10.322 +by (unfold LListD_Fun_def NIL_def, fast)
  10.323 +
  10.324 +lemma LListD_Fun_CONS_I: 
  10.325 +     "[| x\<in>A;  (M,N):s |] ==> (CONS x M, CONS x N) \<in> LListD_Fun (diag A) s"
  10.326 +apply (unfold LListD_Fun_def CONS_def, blast)
  10.327 +done
  10.328 +
  10.329 +text{*Utilise the "strong" part, i.e. gfp(f)*}
  10.330 +lemma LListD_Fun_LListD_I:
  10.331 +     "M \<in> LListD(r) ==> M \<in> LListD_Fun r (X Un LListD(r))"
  10.332 +apply (unfold LListD.defs LListD_Fun_def)
  10.333 +apply (rule gfp_fun_UnI2) 
  10.334 +apply (rule monoI, blast) 
  10.335 +apply assumption
  10.336 +done
  10.337 +
  10.338 +
  10.339 +text{*This converse inclusion helps to strengthen LList_equalityI*}
  10.340 +lemma diag_subset_LListD: "diag(llist(A)) <= LListD(diag A)"
  10.341 +apply (rule subsetI)
  10.342 +apply (erule LListD_coinduct)
  10.343 +apply (rule subsetI)
  10.344 +apply (erule diagE)
  10.345 +apply (erule ssubst)
  10.346 +apply (erule llist.cases)
  10.347 +apply (simp_all add: diagI LListD_Fun_NIL_I LListD_Fun_CONS_I)
  10.348 +done
  10.349 +
  10.350 +lemma LListD_eq_diag: "LListD(diag A) = diag(llist(A))"
  10.351 +apply (rule equalityI LListD_subset_diag diag_subset_LListD)+
  10.352 +done
  10.353 +
  10.354 +lemma LListD_Fun_diag_I: "M \<in> llist(A) ==> (M,M) \<in> LListD_Fun (diag A) (X Un diag(llist(A)))"
  10.355 +apply (rule LListD_eq_diag [THEN subst])
  10.356 +apply (rule LListD_Fun_LListD_I)
  10.357 +apply (simp add: LListD_eq_diag diagI)
  10.358 +done
  10.359 +
  10.360 +
  10.361 +subsubsection{* To show two LLists are equal, exhibit a bisimulation! 
  10.362 +      [also admits true equality]
  10.363 +   Replace "A" by some particular set, like {x.True}??? *}
  10.364 +lemma LList_equalityI:
  10.365 +     "[| (M,N) \<in> r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) |] 
  10.366 +      ==>  M=N"
  10.367 +apply (rule LListD_subset_diag [THEN subsetD, THEN diagE])
  10.368 +apply (erule LListD_coinduct)
  10.369 +apply (simp add: LListD_eq_diag, safe)
  10.370 +done
  10.371 +
  10.372 +
  10.373 +subsection{* Finality of llist(A): Uniqueness of functions defined by corecursion *}
  10.374 +
  10.375 +text{*We must remove Pair_eq because it may turn an instance of reflexivity
  10.376 +  (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction! 
  10.377 +  (or strengthen the Solver?) 
  10.378 +*}
  10.379 +declare Pair_eq [simp del]
  10.380 +
  10.381 +text{*abstract proof using a bisimulation*}
  10.382 +lemma LList_corec_unique:
  10.383 + "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));   
  10.384 +     !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |] 
  10.385 +  ==> h1=h2"
  10.386 +apply (rule ext)
  10.387 +txt{*next step avoids an unknown (and flexflex pair) in simplification*}
  10.388 +apply (rule_tac A = "UNIV" and r = "range(%u. (h1 u, h2 u))" 
  10.389 +       in LList_equalityI)
  10.390 +apply (rule rangeI, safe)
  10.391 +apply (simp add: LListD_Fun_NIL_I UNIV_I [THEN LListD_Fun_CONS_I])
  10.392 +done
  10.393 +
  10.394 +lemma equals_LList_corec:
  10.395 + "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |]  
  10.396 +  ==> h = (%x. LList_corec x f)"
  10.397 +by (simp add: LList_corec_unique LList_corec) 
  10.398 +
  10.399 +
  10.400 +subsubsection{*Obsolete proof of @{text LList_corec_unique}: 
  10.401 +               complete induction, not coinduction *}
  10.402 +
  10.403 +lemma ntrunc_one_CONS [simp]: "ntrunc (Suc 0) (CONS M N) = {}"
  10.404 +by (simp add: CONS_def ntrunc_one_In1)
  10.405 +
  10.406 +lemma ntrunc_CONS [simp]: 
  10.407 +    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)"
  10.408 +by (simp add: CONS_def)
  10.409 +
  10.410 +
  10.411 +lemma
  10.412 + assumes prem1:
  10.413 +          "!!x. h1 x = (case f x of None => NIL | Some(z,w) => CONS z (h1 w))"
  10.414 +     and prem2:
  10.415 +          "!!x. h2 x = (case f x of None => NIL | Some(z,w) => CONS z (h2 w))"
  10.416 + shows "h1=h2"
  10.417 +apply (rule ntrunc_equality [THEN ext])
  10.418 +apply (rule_tac x = "x" in spec)
  10.419 +apply (induct_tac "k" rule: nat_less_induct)
  10.420 +apply (rename_tac "n")
  10.421 +apply (rule allI)
  10.422 +apply (subst prem1)
  10.423 +apply (subst prem2, simp)
  10.424 +apply (intro strip) 
  10.425 +apply (case_tac "n") 
  10.426 +apply (rename_tac [2] "m")
  10.427 +apply (case_tac [2] "m")
  10.428 +apply simp_all
  10.429 +done
  10.430 +
  10.431 +
  10.432 +subsection{*Lconst: defined directly by lfp *}
  10.433 +
  10.434 +text{*But it could be defined by corecursion.*}
  10.435 +
  10.436 +lemma Lconst_fun_mono: "mono(CONS(M))"
  10.437 +apply (rule monoI subset_refl CONS_mono)+
  10.438 +apply assumption 
  10.439 +done
  10.440 +
  10.441 +text{* Lconst(M) = CONS M (Lconst M) *}
  10.442 +lemmas Lconst = Lconst_fun_mono [THEN Lconst_def [THEN def_lfp_unfold]]
  10.443 +
  10.444 +text{*A typical use of co-induction to show membership in the gfp.
  10.445 +  The containing set is simply the singleton {Lconst(M)}. *}
  10.446 +lemma Lconst_type: "M\<in>A ==> Lconst(M): llist(A)"
  10.447 +apply (rule singletonI [THEN llist_coinduct], safe)
  10.448 +apply (rule_tac P = "%u. u \<in> ?A" in Lconst [THEN ssubst])
  10.449 +apply (assumption | rule list_Fun_CONS_I singletonI UnI1)+
  10.450 +done
  10.451 +
  10.452 +lemma Lconst_eq_LList_corec: "Lconst(M) = LList_corec M (%x. Some(x,x))"
  10.453 +apply (rule equals_LList_corec [THEN fun_cong], simp)
  10.454 +apply (rule Lconst)
  10.455 +done
  10.456 +
  10.457 +text{*Thus we could have used gfp in the definition of Lconst*}
  10.458 +lemma gfp_Lconst_eq_LList_corec: "gfp(%N. CONS M N) = LList_corec M (%x. Some(x,x))"
  10.459 +apply (rule equals_LList_corec [THEN fun_cong], simp)
  10.460 +apply (rule Lconst_fun_mono [THEN gfp_unfold])
  10.461 +done
  10.462 +
  10.463 +
  10.464 +subsection{* Isomorphisms *}
  10.465 +
  10.466 +lemma inj_Rep_LList: "inj Rep_LList"
  10.467 +apply (rule inj_inverseI)
  10.468 +apply (rule Rep_LList_inverse)
  10.469 +done
  10.470 +
  10.471 +
  10.472 +lemma LListI: "x \<in> llist (range Leaf) ==> x \<in> LList"
  10.473 +by (unfold LList_def, simp)
  10.474 +
  10.475 +lemma LListD: "x \<in> LList ==> x \<in> llist (range Leaf)"
  10.476 +by (unfold LList_def, simp)
  10.477 +
  10.478 +
  10.479 +subsubsection{* Distinctness of constructors *}
  10.480 +
  10.481 +lemma LCons_not_LNil [iff]: "~ LCons x xs = LNil"
  10.482 +apply (unfold LNil_def LCons_def)
  10.483 +apply (subst Abs_LList_inject)
  10.484 +apply (rule llist.intros CONS_not_NIL rangeI LListI Rep_LList [THEN LListD])+
  10.485 +done
  10.486 +
  10.487 +lemmas LNil_not_LCons [iff] = LCons_not_LNil [THEN not_sym, standard]
  10.488 +
  10.489 +
  10.490 +subsubsection{* llist constructors *}
  10.491 +
  10.492 +lemma Rep_LList_LNil: "Rep_LList LNil = NIL"
  10.493 +apply (unfold LNil_def)
  10.494 +apply (rule llist.NIL_I [THEN LListI, THEN Abs_LList_inverse])
  10.495 +done
  10.496 +
  10.497 +lemma Rep_LList_LCons: "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)"
  10.498 +apply (unfold LCons_def)
  10.499 +apply (rule llist.CONS_I [THEN LListI, THEN Abs_LList_inverse] 
  10.500 +            rangeI Rep_LList [THEN LListD])+
  10.501 +done
  10.502 +
  10.503 +subsubsection{* Injectiveness of CONS and LCons *}
  10.504 +
  10.505 +lemma CONS_CONS_eq2: "(CONS M N=CONS M' N') = (M=M' & N=N')"
  10.506 +apply (unfold CONS_def)
  10.507 +apply (fast elim!: Scons_inject)
  10.508 +done
  10.509 +
  10.510 +lemmas CONS_inject = CONS_CONS_eq [THEN iffD1, THEN conjE, standard]
  10.511 +
  10.512 +
  10.513 +text{*For reasoning about abstract llist constructors*}
  10.514 +
  10.515 +declare Rep_LList [THEN LListD, intro] LListI [intro]
  10.516 +declare llist.intros [intro]
  10.517 +
  10.518 +lemma LCons_LCons_eq [iff]: "(LCons x xs=LCons y ys) = (x=y & xs=ys)"
  10.519 +apply (unfold LCons_def)
  10.520 +apply (subst Abs_LList_inject)
  10.521 +apply (auto simp add: Rep_LList_inject)
  10.522 +done
  10.523 +
  10.524 +lemma LList_fun_equalityI: "CONS M N \<in> llist(A) ==> M \<in> A & N \<in> llist(A)"
  10.525 +apply (erule llist.cases)
  10.526 +apply (erule CONS_neq_NIL, fast)
  10.527 +done
  10.528 +
  10.529 +
  10.530 +subsection{* Reasoning about llist(A) *}
  10.531 +
  10.532 +text{*A special case of list_equality for functions over lazy lists*}
  10.533 +lemma LList_fun_equalityI:
  10.534 + "[| M \<in> llist(A); g(NIL): llist(A);                              
  10.535 +     f(NIL)=g(NIL);                                              
  10.536 +     !!x l. [| x\<in>A;  l \<in> llist(A) |] ==>                          
  10.537 +            (f(CONS x l),g(CONS x l)) \<in>                          
  10.538 +                LListD_Fun (diag A) ((%u.(f(u),g(u)))`llist(A) Un   
  10.539 +                                    diag(llist(A)))              
  10.540 +  |] ==> f(M) = g(M)"
  10.541 +apply (rule LList_equalityI)
  10.542 +apply (erule imageI)
  10.543 +apply (rule image_subsetI)
  10.544 +apply (erule_tac aa=x in llist.cases)
  10.545 +apply (erule ssubst, erule ssubst, erule LListD_Fun_diag_I, blast) 
  10.546 +done
  10.547 +
  10.548 +
  10.549 +subsection{* The functional "Lmap" *}
  10.550 +
  10.551 +lemma Lmap_NIL [simp]: "Lmap f NIL = NIL"
  10.552 +by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
  10.553 +
  10.554 +lemma Lmap_CONS [simp]: "Lmap f (CONS M N) = CONS (f M) (Lmap f N)"
  10.555 +by (rule Lmap_def [THEN def_LList_corec, THEN trans], simp)
  10.556 +
  10.557 +
  10.558 +
  10.559 +text{*Another type-checking proof by coinduction*}
  10.560 +lemma Lmap_type:
  10.561 +     "[| M \<in> llist(A);  !!x. x\<in>A ==> f(x):B |] ==> Lmap f M \<in> llist(B)"
  10.562 +apply (erule imageI [THEN llist_coinduct], safe)
  10.563 +apply (erule llist.cases, simp_all)
  10.564 +done
  10.565 +
  10.566 +text{*This type checking rule synthesises a sufficiently large set for f*}
  10.567 +lemma Lmap_type2: "M \<in> llist(A) ==> Lmap f M \<in> llist(f`A)"
  10.568 +apply (erule Lmap_type)
  10.569 +apply (erule imageI)
  10.570 +done
  10.571 +
  10.572 +subsubsection{* Two easy results about Lmap *}
  10.573 +
  10.574 +lemma Lmap_compose: "M \<in> llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)"
  10.575 +apply (unfold o_def)
  10.576 +apply (drule imageI)
  10.577 +apply (erule LList_equalityI, safe)
  10.578 +apply (erule llist.cases, simp_all)
  10.579 +apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
  10.580 +apply assumption  
  10.581 +done
  10.582 +
  10.583 +lemma Lmap_ident: "M \<in> llist(A) ==> Lmap (%x. x) M = M"
  10.584 +apply (drule imageI)
  10.585 +apply (erule LList_equalityI, safe)
  10.586 +apply (erule llist.cases, simp_all)
  10.587 +apply (rule LListD_Fun_NIL_I imageI UnI1 rangeI [THEN LListD_Fun_CONS_I])+
  10.588 +apply assumption 
  10.589 +done
  10.590 +
  10.591 +
  10.592 +subsection{* Lappend -- its two arguments cause some complications! *}
  10.593 +
  10.594 +lemma Lappend_NIL_NIL [simp]: "Lappend NIL NIL = NIL"
  10.595 +apply (unfold Lappend_def)
  10.596 +apply (rule LList_corec [THEN trans], simp)
  10.597 +done
  10.598 +
  10.599 +lemma Lappend_NIL_CONS [simp]: 
  10.600 +    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')"
  10.601 +apply (unfold Lappend_def)
  10.602 +apply (rule LList_corec [THEN trans], simp)
  10.603 +done
  10.604 +
  10.605 +lemma Lappend_CONS [simp]: 
  10.606 +    "Lappend (CONS M M') N = CONS M (Lappend M' N)"
  10.607 +apply (unfold Lappend_def)
  10.608 +apply (rule LList_corec [THEN trans], simp)
  10.609 +done
  10.610 +
  10.611 +declare llist.intros [simp] LListD_Fun_CONS_I [simp] 
  10.612 +        range_eqI [simp] image_eqI [simp]
  10.613 +
  10.614 +
  10.615 +lemma Lappend_NIL [simp]: "M \<in> llist(A) ==> Lappend NIL M = M"
  10.616 +by (erule LList_fun_equalityI, simp_all)
  10.617 +
  10.618 +lemma Lappend_NIL2: "M \<in> llist(A) ==> Lappend M NIL = M"
  10.619 +by (erule LList_fun_equalityI, simp_all)
  10.620 +
  10.621 +
  10.622 +subsubsection{* Alternative type-checking proofs for Lappend *}
  10.623 +
  10.624 +text{*weak co-induction: bisimulation and case analysis on both variables*}
  10.625 +lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
  10.626 +apply (rule_tac X = "\<Union>u\<in>llist (A) . \<Union>v \<in> llist (A) . {Lappend u v}" in llist_coinduct)
  10.627 +apply fast
  10.628 +apply safe
  10.629 +apply (erule_tac aa = "u" in llist.cases)
  10.630 +apply (erule_tac aa = "v" in llist.cases, simp_all)
  10.631 +apply blast
  10.632 +done
  10.633 +
  10.634 +text{*strong co-induction: bisimulation and case analysis on one variable*}
  10.635 +lemma Lappend_type: "[| M \<in> llist(A); N \<in> llist(A) |] ==> Lappend M N \<in> llist(A)"
  10.636 +apply (rule_tac X = " (%u. Lappend u N) `llist (A) " in llist_coinduct)
  10.637 +apply (erule imageI)
  10.638 +apply (rule image_subsetI)
  10.639 +apply (erule_tac aa = "x" in llist.cases)
  10.640 +apply (simp add: list_Fun_llist_I, simp)
  10.641 +done
  10.642 +
  10.643 +subsection{* Lazy lists as the type 'a llist -- strongly typed versions of above *}
  10.644 +
  10.645 +subsubsection{* llist_case: case analysis for 'a llist *}
  10.646 +
  10.647 +declare LListI [THEN Abs_LList_inverse, simp]
  10.648 +declare Rep_LList_inverse [simp]
  10.649 +declare Rep_LList [THEN LListD, simp]
  10.650 +declare rangeI [simp] inj_Leaf [simp] 
  10.651 +
  10.652 +lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
  10.653 +by (unfold llist_case_def LNil_def, simp)
  10.654 +
  10.655 +lemma llist_case_LCons [simp]: 
  10.656 +    "llist_case c d (LCons M N) = d M N"
  10.657 +apply (unfold llist_case_def LCons_def, simp)
  10.658 +done
  10.659 +
  10.660 +text{*Elimination is case analysis, not induction.*}
  10.661 +lemma llistE: "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P"
  10.662 +apply (rule Rep_LList [THEN LListD, THEN llist.cases])
  10.663 + apply (simp add: Rep_LList_LNil [symmetric] Rep_LList_inject)
  10.664 + apply blast 
  10.665 +apply (erule LListI [THEN Rep_LList_cases], clarify)
  10.666 +apply (simp add: Rep_LList_LCons [symmetric] Rep_LList_inject, blast) 
  10.667 +done
  10.668 +
  10.669 +subsubsection{* llist_corec: corecursion for 'a llist *}
  10.670 +
  10.671 +text{*Lemma for the proof of llist_corec*}
  10.672 +lemma LList_corec_type2:
  10.673 +     "LList_corec a  
  10.674 +           (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) 
  10.675 +       \<in> llist(range Leaf)"
  10.676 +apply (rule_tac X = "range (%x. LList_corec x ?g) " in llist_coinduct)
  10.677 +apply (rule rangeI, safe)
  10.678 +apply (subst LList_corec, force)
  10.679 +done
  10.680 +
  10.681 +lemma llist_corec: 
  10.682 +    "llist_corec a f =   
  10.683 +     (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))"
  10.684 +apply (unfold llist_corec_def LNil_def LCons_def)
  10.685 +apply (subst LList_corec)
  10.686 +apply (case_tac "f a")
  10.687 +apply (simp add: LList_corec_type2)
  10.688 +apply (force simp add: LList_corec_type2)
  10.689 +done
  10.690 +
  10.691 +text{*definitional version of same*}
  10.692 +lemma def_llist_corec: 
  10.693 +     "[| !!x. h(x) == llist_corec x f |] ==>      
  10.694 +      h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))"
  10.695 +by (simp add: llist_corec)
  10.696 +
  10.697 +subsection{* Proofs about type 'a llist functions *}
  10.698 +
  10.699 +subsection{* Deriving llist_equalityI -- llist equality is a bisimulation *}
  10.700 +
  10.701 +lemma LListD_Fun_subset_Times_llist: 
  10.702 +    "r <= (llist A) <*> (llist A) ==>  
  10.703 +            LListD_Fun (diag A) r <= (llist A) <*> (llist A)"
  10.704 +apply (unfold LListD_Fun_def)
  10.705 +apply (subst llist_unfold)
  10.706 +apply (simp add: NIL_def CONS_def, fast)
  10.707 +done
  10.708 +
  10.709 +lemma subset_Times_llist:
  10.710 +     "prod_fun Rep_LList Rep_LList ` r <=  
  10.711 +     (llist(range Leaf)) <*> (llist(range Leaf))"
  10.712 +by (blast intro: Rep_LList [THEN LListD])
  10.713 +
  10.714 +lemma prod_fun_lemma:
  10.715 +     "r <= (llist(range Leaf)) <*> (llist(range Leaf)) 
  10.716 +      ==> prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) ` r <= r"
  10.717 +apply safe
  10.718 +apply (erule subsetD [THEN SigmaE2], assumption)
  10.719 +apply (simp add: LListI [THEN Abs_LList_inverse])
  10.720 +done
  10.721 +
  10.722 +lemma prod_fun_range_eq_diag:
  10.723 +     "prod_fun Rep_LList  Rep_LList ` range(%x. (x, x)) =  
  10.724 +      diag(llist(range Leaf))"
  10.725 +apply (rule equalityI, blast) 
  10.726 +apply (fast elim: LListI [THEN Abs_LList_inverse, THEN subst])
  10.727 +done
  10.728 +
  10.729 +text{*Used with lfilter*}
  10.730 +lemma llistD_Fun_mono: 
  10.731 +    "A<=B ==> llistD_Fun A <= llistD_Fun B"
  10.732 +apply (unfold llistD_Fun_def prod_fun_def, auto)
  10.733 +apply (rule image_eqI)
  10.734 + prefer 2 apply (blast intro: rev_subsetD [OF _ LListD_Fun_mono], force)
  10.735 +done
  10.736 +
  10.737 +subsubsection{* To show two llists are equal, exhibit a bisimulation! 
  10.738 +      [also admits true equality] *}
  10.739 +lemma llist_equalityI: 
  10.740 +    "[| (l1,l2) \<in> r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2"
  10.741 +apply (unfold llistD_Fun_def)
  10.742 +apply (rule Rep_LList_inject [THEN iffD1])
  10.743 +apply (rule_tac r = "prod_fun Rep_LList Rep_LList `r" and A = "range (Leaf) " in LList_equalityI)
  10.744 +apply (erule prod_fun_imageI)
  10.745 +apply (erule image_mono [THEN subset_trans])
  10.746 +apply (rule image_compose [THEN subst])
  10.747 +apply (rule prod_fun_compose [THEN subst])
  10.748 +apply (subst image_Un)
  10.749 +apply (subst prod_fun_range_eq_diag)
  10.750 +apply (rule LListD_Fun_subset_Times_llist [THEN prod_fun_lemma])
  10.751 +apply (rule subset_Times_llist [THEN Un_least])
  10.752 +apply (rule diag_subset_Times)
  10.753 +done
  10.754 +
  10.755 +subsubsection{* Rules to prove the 2nd premise of llist_equalityI *}
  10.756 +lemma llistD_Fun_LNil_I [simp]: "(LNil,LNil) \<in> llistD_Fun(r)"
  10.757 +apply (unfold llistD_Fun_def LNil_def)
  10.758 +apply (rule LListD_Fun_NIL_I [THEN prod_fun_imageI])
  10.759 +done
  10.760 +
  10.761 +lemma llistD_Fun_LCons_I [simp]: 
  10.762 +    "(l1,l2):r ==> (LCons x l1, LCons x l2) \<in> llistD_Fun(r)"
  10.763 +apply (unfold llistD_Fun_def LCons_def)
  10.764 +apply (rule rangeI [THEN LListD_Fun_CONS_I, THEN prod_fun_imageI])
  10.765 +apply (erule prod_fun_imageI)
  10.766 +done
  10.767 +
  10.768 +text{*Utilise the "strong" part, i.e. gfp(f)*}
  10.769 +lemma llistD_Fun_range_I: "(l,l) \<in> llistD_Fun(r Un range(%x.(x,x)))"
  10.770 +apply (unfold llistD_Fun_def)
  10.771 +apply (rule Rep_LList_inverse [THEN subst])
  10.772 +apply (rule prod_fun_imageI)
  10.773 +apply (subst image_Un)
  10.774 +apply (subst prod_fun_range_eq_diag)
  10.775 +apply (rule Rep_LList [THEN LListD, THEN LListD_Fun_diag_I])
  10.776 +done
  10.777 +
  10.778 +text{*A special case of list_equality for functions over lazy lists*}
  10.779 +lemma llist_fun_equalityI:
  10.780 +     "[| f(LNil)=g(LNil);                                                 
  10.781 +         !!x l. (f(LCons x l),g(LCons x l)) 
  10.782 +                \<in> llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))    
  10.783 +      |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)"
  10.784 +apply (rule_tac r = "range (%u. (f (u),g (u))) " in llist_equalityI)
  10.785 +apply (rule rangeI, clarify) 
  10.786 +apply (rule_tac l = "u" in llistE)
  10.787 +apply (simp_all add: llistD_Fun_range_I) 
  10.788 +done
  10.789 +
  10.790 +
  10.791 +subsection{* The functional "lmap" *}
  10.792 +
  10.793 +lemma lmap_LNil [simp]: "lmap f LNil = LNil"
  10.794 +by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
  10.795 +
  10.796 +lemma lmap_LCons [simp]: "lmap f (LCons M N) = LCons (f M) (lmap f N)"
  10.797 +by (rule lmap_def [THEN def_llist_corec, THEN trans], simp)
  10.798 +
  10.799 +
  10.800 +subsubsection{* Two easy results about lmap *}
  10.801 +
  10.802 +lemma lmap_compose [simp]: "lmap (f o g) l = lmap f (lmap g l)"
  10.803 +by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
  10.804 +
  10.805 +lemma lmap_ident [simp]: "lmap (%x. x) l = l"
  10.806 +by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
  10.807 +
  10.808 +
  10.809 +subsection{* iterates -- llist_fun_equalityI cannot be used! *}
  10.810 +
  10.811 +lemma iterates: "iterates f x = LCons x (iterates f (f x))"
  10.812 +by (rule iterates_def [THEN def_llist_corec, THEN trans], simp)
  10.813 +
  10.814 +lemma lmap_iterates [simp]: "lmap f (iterates f x) = iterates f (f x)"
  10.815 +apply (rule_tac r = "range (%u. (lmap f (iterates f u),iterates f (f u))) " in llist_equalityI)
  10.816 +apply (rule rangeI, safe)
  10.817 +apply (rule_tac x1 = "f (u) " in iterates [THEN ssubst])
  10.818 +apply (rule_tac x1 = "u" in iterates [THEN ssubst], simp)
  10.819 +done
  10.820 +
  10.821 +lemma iterates_lmap: "iterates f x = LCons x (lmap f (iterates f x))"
  10.822 +apply (subst lmap_iterates)
  10.823 +apply (rule iterates)
  10.824 +done
  10.825 +
  10.826 +subsection{* A rather complex proof about iterates -- cf Andy Pitts *}
  10.827 +
  10.828 +subsubsection{* Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) *}
  10.829 +
  10.830 +lemma fun_power_lmap: "nat_rec (LCons b l) (%m. lmap(f)) n =       
  10.831 +     LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)"
  10.832 +apply (induct_tac "n", simp_all)
  10.833 +done
  10.834 +
  10.835 +lemma fun_power_Suc: "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)"
  10.836 +by (induct_tac "n", simp_all)
  10.837 +
  10.838 +lemmas Pair_cong = refl [THEN cong, THEN cong, of concl: Pair]
  10.839 +
  10.840 +
  10.841 +text{*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
  10.842 +  for all u and all n::nat.*}
  10.843 +lemma iterates_equality:
  10.844 +     "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)"
  10.845 +apply (rule ext)
  10.846 +apply (rule_tac 
  10.847 +       r = "\<Union>u. range (%n. (nat_rec (h u) (%m y. lmap f y) n, 
  10.848 +                             nat_rec (iterates f u) (%m y. lmap f y) n))" 
  10.849 +       in llist_equalityI)
  10.850 +apply (rule UN1_I range_eqI Pair_cong nat_rec_0 [symmetric])+
  10.851 +apply clarify
  10.852 +apply (subst iterates, atomize)
  10.853 +apply (drule_tac x=u in spec) 
  10.854 +apply (erule ssubst) 
  10.855 +apply (subst fun_power_lmap)
  10.856 +apply (subst fun_power_lmap)
  10.857 +apply (rule llistD_Fun_LCons_I)
  10.858 +apply (rule lmap_iterates [THEN subst])
  10.859 +apply (subst fun_power_Suc)
  10.860 +apply (subst fun_power_Suc, blast)
  10.861 +done
  10.862 +
  10.863 +
  10.864 +subsection{* lappend -- its two arguments cause some complications! *}
  10.865 +
  10.866 +lemma lappend_LNil_LNil [simp]: "lappend LNil LNil = LNil"
  10.867 +apply (unfold lappend_def)
  10.868 +apply (rule llist_corec [THEN trans], simp)
  10.869 +done
  10.870 +
  10.871 +lemma lappend_LNil_LCons [simp]: 
  10.872 +    "lappend LNil (LCons l l') = LCons l (lappend LNil l')"
  10.873 +apply (unfold lappend_def)
  10.874 +apply (rule llist_corec [THEN trans], simp)
  10.875 +done
  10.876 +
  10.877 +lemma lappend_LCons [simp]: 
  10.878 +    "lappend (LCons l l') N = LCons l (lappend l' N)"
  10.879 +apply (unfold lappend_def)
  10.880 +apply (rule llist_corec [THEN trans], simp)
  10.881 +done
  10.882 +
  10.883 +lemma lappend_LNil [simp]: "lappend LNil l = l"
  10.884 +by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
  10.885 +
  10.886 +lemma lappend_LNil2 [simp]: "lappend l LNil = l"
  10.887 +by (rule_tac l = "l" in llist_fun_equalityI, simp_all)
  10.888 +
  10.889 +
  10.890 +text{*The infinite first argument blocks the second*}
  10.891 +lemma lappend_iterates [simp]: "lappend (iterates f x) N = iterates f x"
  10.892 +apply (rule_tac r = "range (%u. (lappend (iterates f u) N,iterates f u))" 
  10.893 +       in llist_equalityI)
  10.894 +apply (rule rangeI, safe)
  10.895 +apply (subst iterates, simp)
  10.896 +done
  10.897 +
  10.898 +subsubsection{* Two proofs that lmap distributes over lappend *}
  10.899 +
  10.900 +text{*Long proof requiring case analysis on both both arguments*}
  10.901 +lemma lmap_lappend_distrib:
  10.902 +     "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
  10.903 +apply (rule_tac r = "\<Union>n. range (%l. (lmap f (lappend l n),
  10.904 +                                      lappend (lmap f l) (lmap f n)))" 
  10.905 +       in llist_equalityI)
  10.906 +apply (rule UN1_I)
  10.907 +apply (rule rangeI, safe)
  10.908 +apply (rule_tac l = "l" in llistE)
  10.909 +apply (rule_tac l = "n" in llistE, simp_all)
  10.910 +apply (blast intro: llistD_Fun_LCons_I) 
  10.911 +done
  10.912 +
  10.913 +text{*Shorter proof of theorem above using llist_equalityI as strong coinduction*}
  10.914 +lemma lmap_lappend_distrib:
  10.915 +     "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)"
  10.916 +apply (rule_tac l = "l" in llist_fun_equalityI, simp)
  10.917 +apply simp
  10.918 +done
  10.919 +
  10.920 +text{*Without strong coinduction, three case analyses might be needed*}
  10.921 +lemma lappend_assoc: "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)"
  10.922 +apply (rule_tac l = "l1" in llist_fun_equalityI, simp)
  10.923 +apply simp
  10.924 +done
  10.925 +
  10.926  end
    11.1 --- a/src/HOL/Induct/PropLog.ML	Tue Apr 02 13:47:01 2002 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,209 +0,0 @@
    11.4 -(*  Title:      HOL/ex/pl.ML
    11.5 -    ID:         $Id$
    11.6 -    Author:     Tobias Nipkow & Lawrence C Paulson
    11.7 -    Copyright   1994  TU Muenchen & University of Cambridge
    11.8 -
    11.9 -Soundness and completeness of propositional logic w.r.t. truth-tables.
   11.10 -
   11.11 -Prove: If H|=p then G|=p where G:Fin(H)
   11.12 -*)
   11.13 -
   11.14 -(** Monotonicity **)
   11.15 -Goalw thms.defs "G<=H ==> thms(G) <= thms(H)";
   11.16 -by (rtac lfp_mono 1);
   11.17 -by (REPEAT (ares_tac basic_monos 1));
   11.18 -qed "thms_mono";
   11.19 -
   11.20 -(*Rule is called I for Identity Combinator, not for Introduction*)
   11.21 -Goal "H |- p->p";
   11.22 -by (best_tac (claset() addIs [thms.K,thms.S,thms.MP]) 1);
   11.23 -qed "thms_I";
   11.24 -
   11.25 -(** Weakening, left and right **)
   11.26 -
   11.27 -(* "[| G<=H;  G |- p |] ==> H |- p"
   11.28 -   This order of premises is convenient with RS
   11.29 -*)
   11.30 -bind_thm ("weaken_left", (thms_mono RS subsetD));
   11.31 -
   11.32 -(* H |- p ==> insert(a,H) |- p *)
   11.33 -val weaken_left_insert = subset_insertI RS weaken_left;
   11.34 -
   11.35 -val weaken_left_Un1  =    Un_upper1 RS weaken_left;
   11.36 -val weaken_left_Un2  =    Un_upper2 RS weaken_left;
   11.37 -
   11.38 -Goal "H |- q ==> H |- p->q";
   11.39 -by (fast_tac (claset() addIs [thms.K,thms.MP]) 1);
   11.40 -qed "weaken_right";
   11.41 -
   11.42 -(*The deduction theorem*)
   11.43 -Goal "insert p H |- q  ==>  H |- p->q";
   11.44 -by (etac thms.induct 1);
   11.45 -by (ALLGOALS 
   11.46 -    (fast_tac (claset() addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
   11.47 -			       thms.S RS thms.MP RS thms.MP, weaken_right])));
   11.48 -qed "deduction";
   11.49 -
   11.50 -
   11.51 -(* "[| insert p H |- q; H |- p |] ==> H |- q"
   11.52 -    The cut rule - not used
   11.53 -*)
   11.54 -val cut = deduction RS thms.MP;
   11.55 -
   11.56 -(* H |- false ==> H |- p *)
   11.57 -val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
   11.58 -
   11.59 -(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
   11.60 -bind_thm ("thms_notE", (thms.MP RS thms_falseE));
   11.61 -
   11.62 -
   11.63 -(*Soundness of the rules wrt truth-table semantics*)
   11.64 -Goalw [sat_def] "H |- p ==> H |= p";
   11.65 -by (etac thms.induct 1);
   11.66 -by (fast_tac (claset() addSDs [eval_imp RS iffD1 RS mp]) 5);
   11.67 -by (ALLGOALS Asm_simp_tac);
   11.68 -qed "soundness";
   11.69 -
   11.70 -(*** Towards the completeness proof ***)
   11.71 -
   11.72 -Goal "H |- p->false ==> H |- p->q";
   11.73 -by (rtac deduction 1);
   11.74 -by (etac (weaken_left_insert RS thms_notE) 1);
   11.75 -by (rtac thms.H 1);
   11.76 -by (rtac insertI1 1);
   11.77 -qed "false_imp";
   11.78 -
   11.79 -val [premp,premq] = goal PropLog.thy
   11.80 -    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
   11.81 -by (rtac deduction 1);
   11.82 -by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
   11.83 -by (rtac (thms.H RS thms.MP) 1);
   11.84 -by (rtac insertI1 1);
   11.85 -by (rtac (premp RS weaken_left_insert) 1);
   11.86 -qed "imp_false";
   11.87 -
   11.88 -(*This formulation is required for strong induction hypotheses*)
   11.89 -Goal "hyps p tt |- (if tt[[p]] then p else p->false)";
   11.90 -by (rtac (split_if RS iffD2) 1);
   11.91 -by (induct_tac "p" 1);
   11.92 -by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
   11.93 -by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
   11.94 -			      weaken_right, imp_false]
   11.95 -                       addSEs [false_imp]) 1);
   11.96 -qed "hyps_thms_if";
   11.97 -
   11.98 -(*Key lemma for completeness; yields a set of assumptions satisfying p*)
   11.99 -val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
  11.100 -by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
  11.101 -    rtac hyps_thms_if 2);
  11.102 -by (Simp_tac 1);
  11.103 -qed "sat_thms_p";
  11.104 -
  11.105 -(*For proving certain theorems in our new propositional logic*)
  11.106 -
  11.107 -AddSIs [deduction];
  11.108 -AddIs [thms.H, thms.H RS thms.MP];
  11.109 -
  11.110 -(*The excluded middle in the form of an elimination rule*)
  11.111 -Goal "H |- (p->q) -> ((p->false)->q) -> q";
  11.112 -by (rtac (deduction RS deduction) 1);
  11.113 -by (rtac (thms.DN RS thms.MP) 1);
  11.114 -by (ALLGOALS (best_tac (claset() addSIs prems)));
  11.115 -qed "thms_excluded_middle";
  11.116 -
  11.117 -(*Hard to prove directly because it requires cuts*)
  11.118 -val prems = goal PropLog.thy
  11.119 -    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q";
  11.120 -by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
  11.121 -by (REPEAT (resolve_tac (prems@[deduction]) 1));
  11.122 -qed "thms_excluded_middle_rule";
  11.123 -
  11.124 -(*** Completeness -- lemmas for reducing the set of assumptions ***)
  11.125 -
  11.126 -(*For the case hyps(p,t)-insert(#v,Y) |- p;
  11.127 -  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
  11.128 -Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
  11.129 -by (induct_tac "p" 1);
  11.130 -by (ALLGOALS Simp_tac);
  11.131 -by (Fast_tac 1);
  11.132 -qed "hyps_Diff";
  11.133 -
  11.134 -(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
  11.135 -  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
  11.136 -Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
  11.137 -by (induct_tac "p" 1);
  11.138 -by (ALLGOALS Simp_tac);
  11.139 -by (Fast_tac 1);
  11.140 -qed "hyps_insert";
  11.141 -
  11.142 -(** Two lemmas for use with weaken_left **)
  11.143 -
  11.144 -goal Set.thy "B-C <= insert a (B-insert a C)";
  11.145 -by (Fast_tac 1);
  11.146 -qed "insert_Diff_same";
  11.147 -
  11.148 -goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
  11.149 -by (Fast_tac 1);
  11.150 -qed "insert_Diff_subset2";
  11.151 -
  11.152 -Goal "finite(hyps p t)";
  11.153 -by (induct_tac "p" 1);
  11.154 -by (ALLGOALS Asm_simp_tac);
  11.155 -qed "hyps_finite";
  11.156 -
  11.157 -Goal "hyps p t <= (UN v. {#v, #v->false})";
  11.158 -by (induct_tac "p" 1);
  11.159 -by (ALLGOALS Simp_tac);
  11.160 -by (Blast_tac 1);
  11.161 -qed "hyps_subset";
  11.162 -
  11.163 -val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
  11.164 -
  11.165 -(*Induction on the finite set of assumptions hyps(p,t0).
  11.166 -  We may repeatedly subtract assumptions until none are left!*)
  11.167 -val [sat] = goal PropLog.thy
  11.168 -    "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
  11.169 -by (rtac (hyps_subset RS (hyps_finite RS finite_subset_induct)) 1);
  11.170 -by (simp_tac (simpset() addsimps [sat RS sat_thms_p]) 1);
  11.171 -by Safe_tac;
  11.172 -(*Case hyps(p,t)-insert(#v,Y) |- p *)
  11.173 -by (rtac thms_excluded_middle_rule 1);
  11.174 -by (rtac (insert_Diff_same RS weaken_left) 1);
  11.175 -by (etac spec 1);
  11.176 -by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  11.177 -by (rtac (hyps_Diff RS Diff_weaken_left) 1);
  11.178 -by (etac spec 1);
  11.179 -(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
  11.180 -by (rtac thms_excluded_middle_rule 1);
  11.181 -by (rtac (insert_Diff_same RS weaken_left) 2);
  11.182 -by (etac spec 2);
  11.183 -by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  11.184 -by (rtac (hyps_insert RS Diff_weaken_left) 1);
  11.185 -by (etac spec 1);
  11.186 -qed "completeness_0_lemma";
  11.187 -
  11.188 -(*The base case for completeness*)
  11.189 -val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
  11.190 -by (rtac (Diff_cancel RS subst) 1);
  11.191 -by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
  11.192 -qed "completeness_0";
  11.193 -
  11.194 -(*A semantic analogue of the Deduction Theorem*)
  11.195 -Goalw [sat_def] "insert p H |= q ==> H |= p->q";
  11.196 -by (Simp_tac 1);
  11.197 -by (Fast_tac 1);
  11.198 -qed "sat_imp";
  11.199 -
  11.200 -Goal "finite H ==> !p. H |= p --> H |- p";
  11.201 -by (etac finite_induct 1);
  11.202 -by (safe_tac ((claset_of Fun.thy) addSIs [completeness_0]));
  11.203 -by (rtac (weaken_left_insert RS thms.MP) 1);
  11.204 -by (fast_tac ((claset_of Fun.thy) addSIs [sat_imp]) 1);
  11.205 -by (Fast_tac 1);
  11.206 -qed "completeness_lemma";
  11.207 -
  11.208 -val completeness = completeness_lemma RS spec RS mp;
  11.209 -
  11.210 -Goal "finite H ==> (H |- p) = (H |= p)";
  11.211 -by (fast_tac (claset() addSEs [soundness, completeness]) 1);
  11.212 -qed "syntax_iff_semantics";
    12.1 --- a/src/HOL/Induct/PropLog.thy	Tue Apr 02 13:47:01 2002 +0200
    12.2 +++ b/src/HOL/Induct/PropLog.thy	Tue Apr 02 14:28:28 2002 +0200
    12.3 @@ -1,45 +1,276 @@
    12.4 -(*  Title:      HOL/ex/PropLog.thy
    12.5 +(*  Title:      HOL/Induct/PropLog.thy
    12.6      ID:         $Id$
    12.7      Author:     Tobias Nipkow
    12.8 -    Copyright   1994  TU Muenchen
    12.9 -
   12.10 -Inductive definition of propositional logic.
   12.11 +    Copyright   1994  TU Muenchen & University of Cambridge
   12.12  *)
   12.13  
   12.14 -PropLog = Main +
   12.15 +header {* Meta-theory of propositional logic *}
   12.16 +
   12.17 +theory PropLog = Main:
   12.18 +
   12.19 +text {*
   12.20 +  Datatype definition of propositional logic formulae and inductive
   12.21 +  definition of the propositional tautologies.
   12.22 +
   12.23 +  Inductive definition of propositional logic.  Soundness and
   12.24 +  completeness w.r.t.\ truth-tables.
   12.25 +
   12.26 +  Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
   12.27 +  Fin(H)"}
   12.28 +*}
   12.29 +
   12.30 +subsection {* The datatype of propositions *}
   12.31  
   12.32  datatype
   12.33 -    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
   12.34 +    'a pl = false | var 'a ("#_" [1000]) | "->" "'a pl" "'a pl" (infixr 90)
   12.35 +
   12.36 +subsection {* The proof system *}
   12.37 +
   12.38  consts
   12.39 -  thms :: 'a pl set => 'a pl set
   12.40 -  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   12.41 -  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
   12.42 -  eval  :: ['a set, 'a pl] => bool      ("_[[_]]" [100,0] 100)
   12.43 -  hyps  :: ['a pl, 'a set] => 'a pl set
   12.44 +  thms  :: "'a pl set => 'a pl set"
   12.45 +  "|-"  :: "['a pl set, 'a pl] => bool"   (infixl 50)
   12.46  
   12.47  translations
   12.48 -  "H |- p" == "p : thms(H)"
   12.49 +  "H |- p" == "p \<in> thms(H)"
   12.50  
   12.51  inductive "thms(H)"
   12.52 -  intrs
   12.53 -  H   "p:H ==> H |- p"
   12.54 -  K   "H |- p->q->p"
   12.55 -  S   "H |- (p->q->r) -> (p->q) -> p->r"
   12.56 -  DN  "H |- ((p->false) -> false) -> p"
   12.57 -  MP  "[| H |- p->q; H |- p |] ==> H |- q"
   12.58 +  intros
   12.59 +  H [intro]:  "p\<in>H ==> H |- p"
   12.60 +  K:          "H |- p->q->p"
   12.61 +  S:          "H |- (p->q->r) -> (p->q) -> p->r"
   12.62 +  DN:         "H |- ((p->false) -> false) -> p"
   12.63 +  MP:         "[| H |- p->q; H |- p |] ==> H |- q"
   12.64 +
   12.65 +subsection {* The semantics *}
   12.66 +
   12.67 +subsubsection {* Semantics of propositional logic. *}
   12.68  
   12.69 -defs
   12.70 -  sat_def  "H |= p  ==  (!tt. (!q:H. tt[[q]]) --> tt[[p]])"
   12.71 +consts
   12.72 +  eval  :: "['a set, 'a pl] => bool"      ("_[[_]]" [100,0] 100)
   12.73 +
   12.74 +primrec     "tt[[false]] = False"
   12.75 +	    "tt[[#v]]    = (v \<in> tt)"
   12.76 +  eval_imp: "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
   12.77  
   12.78 -primrec
   12.79 -         "tt[[false]] = False"
   12.80 -         "tt[[#v]]    = (v:tt)"
   12.81 -eval_imp "tt[[p->q]]  = (tt[[p]] --> tt[[q]])"
   12.82 +text {*
   12.83 +  A finite set of hypotheses from @{text t} and the @{text Var}s in
   12.84 +  @{text p}.
   12.85 +*}
   12.86 +
   12.87 +consts
   12.88 +  hyps  :: "['a pl, 'a set] => 'a pl set"
   12.89  
   12.90  primrec
   12.91    "hyps false  tt = {}"
   12.92 -  "hyps (#v)   tt = {if v:tt then #v else #v->false}"
   12.93 +  "hyps (#v)   tt = {if v \<in> tt then #v else #v->false}"
   12.94    "hyps (p->q) tt = hyps p tt Un hyps q tt"
   12.95  
   12.96 +subsubsection {* Logical consequence *}
   12.97 +
   12.98 +text {*
   12.99 +  For every valuation, if all elements of @{text H} are true then so
  12.100 +  is @{text p}.
  12.101 +*}
  12.102 +
  12.103 +constdefs
  12.104 +  sat :: "['a pl set, 'a pl] => bool"   (infixl "|=" 50)
  12.105 +    "H |= p  ==  (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
  12.106 +
  12.107 +
  12.108 +subsection {* Proof theory of propositional logic *}
  12.109 +
  12.110 +lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
  12.111 +apply (unfold thms.defs )
  12.112 +apply (rule lfp_mono)
  12.113 +apply (assumption | rule basic_monos)+
  12.114 +done
  12.115 +
  12.116 +lemma thms_I: "H |- p->p"
  12.117 +  -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
  12.118 +by (best intro: thms.K thms.S thms.MP)
  12.119 +
  12.120 +
  12.121 +subsubsection {* Weakening, left and right *}
  12.122 +
  12.123 +lemma weaken_left: "[| G \<subseteq> H;  G|-p |] ==> H|-p"
  12.124 +  -- {* Order of premises is convenient with @{text THEN} *}
  12.125 +  by (erule thms_mono [THEN subsetD])
  12.126 +
  12.127 +lemmas weaken_left_insert = subset_insertI [THEN weaken_left]
  12.128 +
  12.129 +lemmas weaken_left_Un1  = Un_upper1 [THEN weaken_left]
  12.130 +lemmas weaken_left_Un2  = Un_upper2 [THEN weaken_left]
  12.131 +
  12.132 +lemma weaken_right: "H |- q ==> H |- p->q"
  12.133 +by (fast intro: thms.K thms.MP)
  12.134 +
  12.135 +
  12.136 +subsubsection {* The deduction theorem *}
  12.137 +
  12.138 +theorem deduction: "insert p H |- q  ==>  H |- p->q"
  12.139 +apply (erule thms.induct)
  12.140 +apply (fast intro: thms_I thms.H thms.K thms.S thms.DN 
  12.141 +                   thms.S [THEN thms.MP, THEN thms.MP] weaken_right)+
  12.142 +done
  12.143 +
  12.144 +
  12.145 +subsubsection {* The cut rule *}
  12.146 +
  12.147 +lemmas cut = deduction [THEN thms.MP]
  12.148 +
  12.149 +lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
  12.150 +
  12.151 +lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
  12.152 +
  12.153 +
  12.154 +subsubsection {* Soundness of the rules wrt truth-table semantics *}
  12.155 +
  12.156 +theorem soundness: "H |- p ==> H |= p"
  12.157 +apply (unfold sat_def)
  12.158 +apply (erule thms.induct, auto) 
  12.159 +done
  12.160 +
  12.161 +subsection {* Completeness *}
  12.162 +
  12.163 +subsubsection {* Towards the completeness proof *}
  12.164 +
  12.165 +lemma false_imp: "H |- p->false ==> H |- p->q"
  12.166 +apply (rule deduction)
  12.167 +apply (erule weaken_left_insert [THEN thms_notE])
  12.168 +apply blast
  12.169 +done
  12.170 +
  12.171 +lemma imp_false:
  12.172 +    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false"
  12.173 +apply (rule deduction)
  12.174 +apply (blast intro: weaken_left_insert thms.MP thms.H) 
  12.175 +done
  12.176 +
  12.177 +lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
  12.178 +  -- {* Typical example of strengthening the induction statement. *}
  12.179 +apply simp 
  12.180 +apply (induct_tac "p")
  12.181 +apply (simp_all add: thms_I thms.H)
  12.182 +apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right
  12.183 +                    imp_false false_imp)
  12.184 +done
  12.185 +
  12.186 +lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
  12.187 +  -- {* Key lemma for completeness; yields a set of assumptions 
  12.188 +        satisfying @{text p} *}
  12.189 +apply (unfold sat_def) 
  12.190 +apply (drule spec, erule mp [THEN if_P, THEN subst], 
  12.191 +       rule_tac [2] hyps_thms_if, simp)
  12.192 +done
  12.193 +
  12.194 +text {*
  12.195 +  For proving certain theorems in our new propositional logic.
  12.196 +*}
  12.197 +
  12.198 +declare deduction [intro!]
  12.199 +declare thms.H [THEN thms.MP, intro]
  12.200 +
  12.201 +text {*
  12.202 +  The excluded middle in the form of an elimination rule.
  12.203 +*}
  12.204 +
  12.205 +lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
  12.206 +apply (rule deduction [THEN deduction])
  12.207 +apply (rule thms.DN [THEN thms.MP], best) 
  12.208 +done
  12.209 +
  12.210 +lemma thms_excluded_middle_rule:
  12.211 +    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q"
  12.212 +  -- {* Hard to prove directly because it requires cuts *}
  12.213 +by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto) 
  12.214 +
  12.215 +
  12.216 +subsection{* Completeness -- lemmas for reducing the set of assumptions*}
  12.217 +
  12.218 +text {*
  12.219 +  For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
  12.220 +  "hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
  12.221 +*}
  12.222 +
  12.223 +lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
  12.224 +by (induct_tac "p", auto) 
  12.225 +
  12.226 +text {*
  12.227 +  For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
  12.228 +  @{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
  12.229 +*}
  12.230 +
  12.231 +lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
  12.232 +by (induct_tac "p", auto)
  12.233 +
  12.234 +text {* Two lemmas for use with @{text weaken_left} *}
  12.235 +
  12.236 +lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
  12.237 +by fast
  12.238 +
  12.239 +lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
  12.240 +by fast
  12.241 +
  12.242 +text {*
  12.243 +  The set @{term "hyps p t"} is finite, and elements have the form
  12.244 +  @{term "#v"} or @{term "#v->Fls"}.
  12.245 +*}
  12.246 +
  12.247 +lemma hyps_finite: "finite(hyps p t)"
  12.248 +by (induct_tac "p", auto)
  12.249 +
  12.250 +lemma hyps_subset: "hyps p t <= (UN v. {#v, #v->false})"
  12.251 +by (induct_tac "p", auto)
  12.252 +
  12.253 +lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
  12.254 +
  12.255 +subsubsection {* Completeness theorem *}
  12.256 +
  12.257 +text {*
  12.258 +  Induction on the finite set of assumptions @{term "hyps p t0"}.  We
  12.259 +  may repeatedly subtract assumptions until none are left!
  12.260 +*}
  12.261 +
  12.262 +lemma completeness_0_lemma:
  12.263 +    "{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p" 
  12.264 +apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
  12.265 + apply (simp add: sat_thms_p, safe)
  12.266 +(*Case hyps p t-insert(#v,Y) |- p *)
  12.267 + apply (rule thms_excluded_middle_rule)
  12.268 +  apply (rule insert_Diff_same [THEN weaken_left])
  12.269 +  apply (erule spec)
  12.270 + apply (rule insert_Diff_subset2 [THEN weaken_left])
  12.271 + apply (rule hyps_Diff [THEN Diff_weaken_left])
  12.272 + apply (erule spec)
  12.273 +(*Case hyps p t-insert(#v -> false,Y) |- p *)
  12.274 +apply (rule thms_excluded_middle_rule)
  12.275 + apply (rule_tac [2] insert_Diff_same [THEN weaken_left])
  12.276 + apply (erule_tac [2] spec)
  12.277 +apply (rule insert_Diff_subset2 [THEN weaken_left])
  12.278 +apply (rule hyps_insert [THEN Diff_weaken_left])
  12.279 +apply (erule spec)
  12.280 +done
  12.281 +
  12.282 +text{*The base case for completeness*}
  12.283 +lemma completeness_0:  "{} |= p ==> {} |- p"
  12.284 +apply (rule Diff_cancel [THEN subst])
  12.285 +apply (erule completeness_0_lemma [THEN spec])
  12.286 +done
  12.287 +
  12.288 +text{*A semantic analogue of the Deduction Theorem*}
  12.289 +lemma sat_imp: "insert p H |= q ==> H |= p->q"
  12.290 +by (unfold sat_def, auto)
  12.291 +
  12.292 +theorem completeness [rule_format]: "finite H ==> \<forall>p. H |= p --> H |- p"
  12.293 +apply (erule finite_induct)
  12.294 +apply (safe intro!: completeness_0)
  12.295 +apply (drule sat_imp)
  12.296 +apply (drule spec) 
  12.297 +apply (blast intro: weaken_left_insert [THEN thms.MP])  
  12.298 +done
  12.299 +
  12.300 +theorem syntax_iff_semantics: "finite H ==> (H |- p) = (H |= p)"
  12.301 +by (fast elim!: soundness completeness)
  12.302 +
  12.303  end
  12.304  
    13.1 --- a/src/HOL/Induct/ROOT.ML	Tue Apr 02 13:47:01 2002 +0200
    13.2 +++ b/src/HOL/Induct/ROOT.ML	Tue Apr 02 14:28:28 2002 +0200
    13.3 @@ -9,4 +9,3 @@
    13.4  time_use_thy "PropLog";
    13.5  time_use_thy "SList";
    13.6  time_use_thy "LFilter";
    13.7 -time_use_thy "Exp";
    14.1 --- a/src/HOL/IsaMakefile	Tue Apr 02 13:47:01 2002 +0200
    14.2 +++ b/src/HOL/IsaMakefile	Tue Apr 02 14:28:28 2002 +0200
    14.3 @@ -220,10 +220,9 @@
    14.4  HOL-Induct: HOL $(LOG)/HOL-Induct.gz
    14.5  
    14.6  $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
    14.7 -  Induct/Com.ML Induct/Com.thy Induct/Comb.ML Induct/Comb.thy \
    14.8 -  Induct/Exp.ML Induct/Exp.thy Induct/LFilter.ML Induct/LFilter.thy \
    14.9 -  Induct/LList.ML Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   14.10 -  Induct/PropLog.ML Induct/PropLog.thy Induct/ROOT.ML \
   14.11 +  Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
   14.12 +  Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
   14.13 +  Induct/PropLog.thy Induct/ROOT.ML \
   14.14    Induct/Sexp.ML Induct/Sexp.thy Induct/Sigma_Algebra.thy \
   14.15    Induct/SList.ML Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
   14.16    Induct/Tree.thy Induct/document/root.tex