New directory to contain examples of (co)inductive definitions
authorpaulson
Wed May 07 12:50:26 1997 +0200 (1997-05-07)
changeset 3120c58423c20740
parent 3119 bb2ee88aa43f
child 3121 cbb6c0c1c58a
New directory to contain examples of (co)inductive definitions
src/HOL/Induct/Acc.ML
src/HOL/Induct/Acc.thy
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/Mutil.ML
src/HOL/Induct/Mutil.thy
src/HOL/Induct/Perm.ML
src/HOL/Induct/Perm.thy
src/HOL/Induct/PropLog.ML
src/HOL/Induct/PropLog.thy
src/HOL/Induct/ROOT.ML
src/HOL/Induct/SList.ML
src/HOL/Induct/SList.thy
src/HOL/Induct/Simult.ML
src/HOL/Induct/Simult.thy
src/HOL/Induct/Term.ML
src/HOL/Induct/Term.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Induct/Acc.ML	Wed May 07 12:50:26 1997 +0200
     1.3 @@ -0,0 +1,63 @@
     1.4 +(*  Title:      HOL/ex/Acc
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1994  University of Cambridge
     1.8 +
     1.9 +Inductive definition of acc(r)
    1.10 +
    1.11 +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    1.12 +Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    1.13 +*)
    1.14 +
    1.15 +open Acc;
    1.16 +
    1.17 +(*The intended introduction rule*)
    1.18 +val prems = goal Acc.thy
    1.19 +    "[| !!b. (b,a):r ==> b: acc(r) |] ==> a: acc(r)";
    1.20 +by (fast_tac (!claset addIs (prems @ 
    1.21 +                            map (rewrite_rule [pred_def]) acc.intrs)) 1);
    1.22 +qed "accI";
    1.23 +
    1.24 +goal Acc.thy "!!a b r. [| b: acc(r);  (a,b): r |] ==> a: acc(r)";
    1.25 +by (etac acc.elim 1);
    1.26 +by (rewtac pred_def);
    1.27 +by (Fast_tac 1);
    1.28 +qed "acc_downward";
    1.29 +
    1.30 +val [major,indhyp] = goal Acc.thy
    1.31 +    "[| a : acc(r);                                             \
    1.32 +\       !!x. [| x: acc(r);  ALL y. (y,x):r --> P(y) |] ==> P(x) \
    1.33 +\    |] ==> P(a)";
    1.34 +by (rtac (major RS acc.induct) 1);
    1.35 +by (rtac indhyp 1);
    1.36 +by (resolve_tac acc.intrs 1);
    1.37 +by (rewtac pred_def);
    1.38 +by (Fast_tac 2);
    1.39 +by (etac (Int_lower1 RS Pow_mono RS subsetD) 1);
    1.40 +qed "acc_induct";
    1.41 +
    1.42 +
    1.43 +val [major] = goal Acc.thy "r <= (acc r) Times (acc r) ==> wf(r)";
    1.44 +by (rtac (major RS wfI) 1);
    1.45 +by (etac acc.induct 1);
    1.46 +by (rewtac pred_def);
    1.47 +by (Fast_tac 1);
    1.48 +qed "acc_wfI";
    1.49 +
    1.50 +val [major] = goal Acc.thy "wf(r) ==> ALL x. (x,y): r | (y,x):r --> y: acc(r)";
    1.51 +by (rtac (major RS wf_induct) 1);
    1.52 +by (rtac (impI RS allI) 1);
    1.53 +by (rtac accI 1);
    1.54 +by (Fast_tac 1);
    1.55 +qed "acc_wfD_lemma";
    1.56 +
    1.57 +val [major] = goal Acc.thy "wf(r) ==> r <= (acc r) Times (acc r)";
    1.58 +by (rtac subsetI 1);
    1.59 +by (res_inst_tac [("p", "x")] PairE 1);
    1.60 +by (fast_tac (!claset addSIs [SigmaI,
    1.61 +                             major RS acc_wfD_lemma RS spec RS mp]) 1);
    1.62 +qed "acc_wfD";
    1.63 +
    1.64 +goal Acc.thy "wf(r)  =  (r <= (acc r) Times (acc r))";
    1.65 +by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
    1.66 +qed "wf_acc_iff";
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Induct/Acc.thy	Wed May 07 12:50:26 1997 +0200
     2.3 @@ -0,0 +1,26 @@
     2.4 +(*  Title:      HOL/ex/Acc.thy
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1994  University of Cambridge
     2.8 +
     2.9 +Inductive definition of acc(r)
    2.10 +
    2.11 +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
    2.12 +Research Report 92-49, LIP, ENS Lyon.  Dec 1992.
    2.13 +*)
    2.14 +
    2.15 +Acc = WF + 
    2.16 +
    2.17 +constdefs
    2.18 +  pred :: "['b, ('a * 'b)set] => 'a set"        (*Set of predecessors*)
    2.19 +  "pred x r == {y. (y,x):r}"
    2.20 +
    2.21 +consts
    2.22 +  acc  :: "('a * 'a)set => 'a set"              (*Accessible part*)
    2.23 +
    2.24 +inductive "acc(r)"
    2.25 +  intrs
    2.26 +    pred    "pred a r: Pow(acc(r)) ==> a: acc(r)"
    2.27 +  monos     "[Pow_mono]"
    2.28 +
    2.29 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Induct/Com.ML	Wed May 07 12:50:26 1997 +0200
     3.3 @@ -0,0 +1,43 @@
     3.4 +(*  Title:      HOL/Induct/Com
     3.5 +    ID:         $Id$
     3.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.7 +    Copyright   1997  University of Cambridge
     3.8 +
     3.9 +Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    3.10 +*)
    3.11 +
    3.12 +open Com;
    3.13 +
    3.14 +AddIs exec.intrs;
    3.15 +
    3.16 +val exec_elim_cases = map (exec.mk_cases exp.simps)
    3.17 +   ["(SKIP,s) -[eval]-> t", "(x:=a,s) -[eval]-> t", "(c1;;c2, s) -[eval]-> t",
    3.18 +    "(IF e THEN c1 ELSE c2, s) -[eval]-> t"];
    3.19 +
    3.20 +val exec_WHILE_case = exec.mk_cases exp.simps "(WHILE b DO c,s) -[eval]-> t";
    3.21 +
    3.22 +AddSEs exec_elim_cases;
    3.23 +
    3.24 +(*This theorem justifies using "exec" in the inductive definition of "eval"*)
    3.25 +goalw thy exec.defs "!!A B. A<=B ==> exec(A) <= exec(B)";
    3.26 +by (rtac lfp_mono 1);
    3.27 +by (REPEAT (ares_tac basic_monos 1));
    3.28 +qed "exec_mono";
    3.29 +
    3.30 +
    3.31 +Unify.trace_bound := 30;
    3.32 +Unify.search_bound := 60;
    3.33 +
    3.34 +(*Command execution is functional (deterministic) provided evaluation is*)
    3.35 +goal thy "!!x. Function ev ==> Function(exec ev)";
    3.36 +by (simp_tac (!simpset addsimps [Function_def, Unique_def]) 1);
    3.37 +by (REPEAT (rtac allI 1));
    3.38 +by (rtac impI 1);
    3.39 +by (etac exec.induct 1);
    3.40 +by (Blast_tac 3);
    3.41 +by (Blast_tac 1);
    3.42 +by (rewrite_goals_tac [Function_def, Unique_def]);
    3.43 +(*Takes ONE MINUTE due to slow proof reconstruction*)
    3.44 +by (ALLGOALS (blast_tac (!claset addEs [exec_WHILE_case])));
    3.45 +qed "Function_exec";
    3.46 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Induct/Com.thy	Wed May 07 12:50:26 1997 +0200
     4.3 @@ -0,0 +1,69 @@
     4.4 +(*  Title:      HOL/Induct/Com
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1997  University of Cambridge
     4.8 +
     4.9 +Example of Mutual Induction via Iteratived Inductive Definitions: Commands
    4.10 +*)
    4.11 +
    4.12 +Com = Arith +
    4.13 +
    4.14 +types loc
    4.15 +      state = "loc => nat"
    4.16 +      n2n2n = "nat => nat => nat"
    4.17 +
    4.18 +arities loc :: term
    4.19 +
    4.20 +(*To avoid a mutually recursive datatype declaration, expressions and commands
    4.21 +  are combined to form a single datatype.*)
    4.22 +datatype
    4.23 +  exp = N nat
    4.24 +      | X loc
    4.25 +      | Op n2n2n exp exp
    4.26 +      | valOf exp exp          ("VALOF _ RESULTIS _"  60)
    4.27 +      | SKIP
    4.28 +      | ":="  loc exp          (infixl  60)
    4.29 +      | Semi  exp exp          ("_;;_"  [60, 60] 10)
    4.30 +      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
    4.31 +      | While exp exp          ("WHILE _ DO _"  60)
    4.32 +
    4.33 +(** Execution of commands **)
    4.34 +consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
    4.35 +       "@exec"  :: "((exp*state) * (nat*state)) set => 
    4.36 +                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
    4.37 +
    4.38 +translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
    4.39 +
    4.40 +constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
    4.41 +  "s[m/x] ==  (%y. if y=x then m else s y)"
    4.42 +
    4.43 +
    4.44 +(*Command execution.  Natural numbers represent Booleans: 0=True, 1=False*)
    4.45 +inductive "exec eval"
    4.46 +  intrs
    4.47 +    Skip    "(SKIP,s) -[eval]-> s"
    4.48 +
    4.49 +    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
    4.50 +
    4.51 +    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
    4.52 +            ==> (c0 ;; c1, s) -[eval]-> s1"
    4.53 +
    4.54 +    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
    4.55 +            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    4.56 +
    4.57 +    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
    4.58 +             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
    4.59 +
    4.60 +    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
    4.61 +
    4.62 +    WhileTrue  "[| ((e,s), (0,s1)) : eval;
    4.63 +                (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
    4.64 +                ==> (WHILE e DO c, s) -[eval]-> s3"
    4.65 +
    4.66 +constdefs
    4.67 +    Unique   :: "['a, 'b, ('a*'b) set] => bool"
    4.68 +    "Unique x y r == ALL y'. (x,y'): r --> y = y'"
    4.69 +
    4.70 +    Function :: "('a*'b) set => bool"
    4.71 +    "Function r == ALL x y. (x,y): r --> Unique x y r"
    4.72 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Induct/Comb.ML	Wed May 07 12:50:26 1997 +0200
     5.3 @@ -0,0 +1,179 @@
     5.4 +(*  Title:      HOL/ex/comb.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson
     5.7 +    Copyright   1996  University of Cambridge
     5.8 +
     5.9 +Combinatory Logic example: the Church-Rosser Theorem
    5.10 +Curiously, combinators do not include free variables.
    5.11 +
    5.12 +Example taken from
    5.13 +    J. Camilleri and T. F. Melham.
    5.14 +    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    5.15 +    Report 265, University of Cambridge Computer Laboratory, 1992.
    5.16 +
    5.17 +HOL system proofs may be found in
    5.18 +/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
    5.19 +*)
    5.20 +
    5.21 +open Comb;
    5.22 +
    5.23 +(*** Reflexive/Transitive closure preserves the Church-Rosser property 
    5.24 +     So does the Transitive closure; use r_into_trancl instead of rtrancl_refl
    5.25 +***)
    5.26 +
    5.27 +val [_, spec_mp] = [spec] RL [mp];
    5.28 +
    5.29 +(*Strip lemma.  The induction hyp is all but the last diamond of the strip.*)
    5.30 +goalw Comb.thy [diamond_def]
    5.31 +    "!!r. [| diamond(r);  (x,y):r^* |] ==> \ 
    5.32 +\         ALL y'. (x,y'):r --> (EX z. (y',z): r^* & (y,z): r)";
    5.33 +by (etac rtrancl_induct 1);
    5.34 +by (Blast_tac 1);
    5.35 +by (slow_best_tac (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    5.36 +                           addSDs [spec_mp]) 1);
    5.37 +val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
    5.38 +
    5.39 +val [major] = goal Comb.thy "diamond(r) ==> diamond(r^*)";
    5.40 +by (rewtac diamond_def);  (*unfold only in goal, not in premise!*)
    5.41 +by (rtac (impI RS allI RS allI) 1);
    5.42 +by (etac rtrancl_induct 1);
    5.43 +by (Blast_tac 1);
    5.44 +by (slow_best_tac  (*Seems to be a brittle, undirected search*)
    5.45 +    (set_cs addIs [r_into_rtrancl RSN (2, rtrancl_trans)]
    5.46 +            addEs [major RS diamond_strip_lemmaE]) 1);
    5.47 +qed "diamond_rtrancl";
    5.48 +
    5.49 +
    5.50 +(*** Results about Contraction ***)
    5.51 +
    5.52 +(*Derive a case for each combinator constructor*)
    5.53 +val K_contractE = contract.mk_cases comb.simps "K -1-> z";
    5.54 +val S_contractE = contract.mk_cases comb.simps "S -1-> z";
    5.55 +val Ap_contractE = contract.mk_cases comb.simps "x#y -1-> z";
    5.56 +
    5.57 +AddSIs [contract.K, contract.S];
    5.58 +AddIs  [contract.Ap1, contract.Ap2];
    5.59 +AddSEs [K_contractE, S_contractE, Ap_contractE];
    5.60 +Unsafe_Addss  (!simpset);
    5.61 +
    5.62 +goalw Comb.thy [I_def] "!!z. I -1-> z ==> P";
    5.63 +by (Blast_tac 1);
    5.64 +qed "I_contract_E";
    5.65 +AddSEs [I_contract_E];
    5.66 +
    5.67 +goal Comb.thy "!!x z. K#x -1-> z ==> (EX x'. z = K#x' & x -1-> x')";
    5.68 +by (Blast_tac 1);
    5.69 +qed "K1_contractD";
    5.70 +AddSEs [K1_contractD];
    5.71 +
    5.72 +goal Comb.thy "!!x z. x ---> y ==> x#z ---> y#z";
    5.73 +by (etac rtrancl_induct 1);
    5.74 +by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
    5.75 +qed "Ap_reduce1";
    5.76 +
    5.77 +goal Comb.thy "!!x z. x ---> y ==> z#x ---> z#y";
    5.78 +by (etac rtrancl_induct 1);
    5.79 +by (ALLGOALS (blast_tac (!claset addIs [r_into_rtrancl, rtrancl_trans])));
    5.80 +qed "Ap_reduce2";
    5.81 +
    5.82 +(** Counterexample to the diamond property for -1-> **)
    5.83 +
    5.84 +goal Comb.thy "K#I#(I#I) -1-> I";
    5.85 +by (rtac contract.K 1);
    5.86 +qed "KIII_contract1";
    5.87 +
    5.88 +goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
    5.89 +by (Blast_tac 1);
    5.90 +qed "KIII_contract2";
    5.91 +
    5.92 +goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
    5.93 +by (Blast_tac 1);
    5.94 +qed "KIII_contract3";
    5.95 +
    5.96 +goalw Comb.thy [diamond_def] "~ diamond(contract)";
    5.97 +by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]) 1);
    5.98 +qed "not_diamond_contract";
    5.99 +
   5.100 +
   5.101 +
   5.102 +(*** Results about Parallel Contraction ***)
   5.103 +
   5.104 +(*Derive a case for each combinator constructor*)
   5.105 +val K_parcontractE = parcontract.mk_cases comb.simps "K =1=> z";
   5.106 +val S_parcontractE = parcontract.mk_cases comb.simps "S =1=> z";
   5.107 +val Ap_parcontractE = parcontract.mk_cases comb.simps "x#y =1=> z";
   5.108 +
   5.109 +AddIs  parcontract.intrs;
   5.110 +AddSEs [K_parcontractE, S_parcontractE,Ap_parcontractE];
   5.111 +Unsafe_Addss  (!simpset);
   5.112 +
   5.113 +(*** Basic properties of parallel contraction ***)
   5.114 +
   5.115 +goal Comb.thy "!!x z. K#x =1=> z ==> (EX x'. z = K#x' & x =1=> x')";
   5.116 +by (Blast_tac 1);
   5.117 +qed "K1_parcontractD";
   5.118 +AddSDs [K1_parcontractD];
   5.119 +
   5.120 +goal Comb.thy "!!x z. S#x =1=> z ==> (EX x'. z = S#x' & x =1=> x')";
   5.121 +by (Blast_tac 1);
   5.122 +qed "S1_parcontractD";
   5.123 +AddSDs [S1_parcontractD];
   5.124 +
   5.125 +goal Comb.thy
   5.126 + "!!x y z. S#x#y =1=> z ==> (EX x' y'. z = S#x'#y' & x =1=> x' & y =1=> y')";
   5.127 +by (Blast_tac 1);
   5.128 +qed "S2_parcontractD";
   5.129 +AddSDs [S2_parcontractD];
   5.130 +
   5.131 +(*The rules above are not essential but make proofs much faster*)
   5.132 +
   5.133 +
   5.134 +(*Church-Rosser property for parallel contraction*)
   5.135 +goalw Comb.thy [diamond_def] "diamond parcontract";
   5.136 +by (rtac (impI RS allI RS allI) 1);
   5.137 +by (etac parcontract.induct 1 THEN prune_params_tac);
   5.138 +by (Step_tac 1);
   5.139 +by (ALLGOALS Blast_tac);
   5.140 +qed "diamond_parcontract";
   5.141 +
   5.142 +
   5.143 +(*** Equivalence of x--->y and x===>y ***)
   5.144 +
   5.145 +goal Comb.thy "contract <= parcontract";
   5.146 +by (rtac subsetI 1);
   5.147 +by (split_all_tac 1);
   5.148 +by (etac contract.induct 1);
   5.149 +by (ALLGOALS Blast_tac);
   5.150 +qed "contract_subset_parcontract";
   5.151 +
   5.152 +(*Reductions: simply throw together reflexivity, transitivity and
   5.153 +  the one-step reductions*)
   5.154 +
   5.155 +AddIs [Ap_reduce1, Ap_reduce2, r_into_rtrancl, rtrancl_trans];
   5.156 +
   5.157 +(*Example only: not used*)
   5.158 +goalw Comb.thy [I_def] "I#x ---> x";
   5.159 +by (Blast_tac 1);
   5.160 +qed "reduce_I";
   5.161 +
   5.162 +goal Comb.thy "parcontract <= contract^*";
   5.163 +by (rtac subsetI 1);
   5.164 +by (split_all_tac 1);
   5.165 +by (etac parcontract.induct 1 THEN prune_params_tac);
   5.166 +by (ALLGOALS Blast_tac);
   5.167 +qed "parcontract_subset_reduce";
   5.168 +
   5.169 +goal Comb.thy "contract^* = parcontract^*";
   5.170 +by (REPEAT 
   5.171 +    (resolve_tac [equalityI, 
   5.172 +                  contract_subset_parcontract RS rtrancl_mono, 
   5.173 +                  parcontract_subset_reduce RS rtrancl_subset_rtrancl] 1));
   5.174 +qed "reduce_eq_parreduce";
   5.175 +
   5.176 +goal Comb.thy "diamond(contract^*)";
   5.177 +by (simp_tac (!simpset addsimps [reduce_eq_parreduce, diamond_rtrancl, 
   5.178 +                                 diamond_parcontract]) 1);
   5.179 +qed "diamond_reduce";
   5.180 +
   5.181 +
   5.182 +writeln"Reached end of file.";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Induct/Comb.thy	Wed May 07 12:50:26 1997 +0200
     6.3 @@ -0,0 +1,74 @@
     6.4 +(*  Title:      HOL/ex/Comb.thy
     6.5 +    ID:         $Id$
     6.6 +    Author:     Lawrence C Paulson
     6.7 +    Copyright   1996  University of Cambridge
     6.8 +
     6.9 +Combinatory Logic example: the Church-Rosser Theorem
    6.10 +Curiously, combinators do not include free variables.
    6.11 +
    6.12 +Example taken from
    6.13 +    J. Camilleri and T. F. Melham.
    6.14 +    Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
    6.15 +    Report 265, University of Cambridge Computer Laboratory, 1992.
    6.16 +*)
    6.17 +
    6.18 +
    6.19 +Comb = Trancl +
    6.20 +
    6.21 +(** Datatype definition of combinators S and K, with infixed application **)
    6.22 +datatype comb = K
    6.23 +              | S
    6.24 +              | "#" comb comb (infixl 90)
    6.25 +
    6.26 +(** Inductive definition of contractions, -1->
    6.27 +             and (multi-step) reductions, --->
    6.28 +**)
    6.29 +consts
    6.30 +  contract  :: "(comb*comb) set"
    6.31 +  "-1->"    :: [comb,comb] => bool   (infixl 50)
    6.32 +  "--->"    :: [comb,comb] => bool   (infixl 50)
    6.33 +
    6.34 +translations
    6.35 +  "x -1-> y" == "(x,y) : contract"
    6.36 +  "x ---> y" == "(x,y) : contract^*"
    6.37 +
    6.38 +inductive contract
    6.39 +  intrs
    6.40 +    K     "K#x#y -1-> x"
    6.41 +    S     "S#x#y#z -1-> (x#z)#(y#z)"
    6.42 +    Ap1   "x-1->y ==> x#z -1-> y#z"
    6.43 +    Ap2   "x-1->y ==> z#x -1-> z#y"
    6.44 +
    6.45 +
    6.46 +(** Inductive definition of parallel contractions, =1=>
    6.47 +             and (multi-step) parallel reductions, ===>
    6.48 +**)
    6.49 +consts
    6.50 +  parcontract :: "(comb*comb) set"
    6.51 +  "=1=>"    :: [comb,comb] => bool   (infixl 50)
    6.52 +  "===>"    :: [comb,comb] => bool   (infixl 50)
    6.53 +
    6.54 +translations
    6.55 +  "x =1=> y" == "(x,y) : parcontract"
    6.56 +  "x ===> y" == "(x,y) : parcontract^*"
    6.57 +
    6.58 +inductive parcontract
    6.59 +  intrs
    6.60 +    refl  "x =1=> x"
    6.61 +    K     "K#x#y =1=> x"
    6.62 +    S     "S#x#y#z =1=> (x#z)#(y#z)"
    6.63 +    Ap    "[| x=1=>y;  z=1=>w |] ==> x#z =1=> y#w"
    6.64 +
    6.65 +
    6.66 +(*Misc definitions*)
    6.67 +constdefs
    6.68 +  I :: comb
    6.69 +  "I == S#K#K"
    6.70 +
    6.71 +  (*confluence; Lambda/Commutation treats this more abstractly*)
    6.72 +  diamond   :: "('a * 'a)set => bool"	
    6.73 +  "diamond(r) == ALL x y. (x,y):r --> 
    6.74 +                  (ALL y'. (x,y'):r --> 
    6.75 +                    (EX z. (y,z):r & (y',z) : r))"
    6.76 +
    6.77 +end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Induct/Exp.ML	Wed May 07 12:50:26 1997 +0200
     7.3 @@ -0,0 +1,86 @@
     7.4 +(*  Title:      HOL/Induct/Exp
     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 +Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
    7.10 +*)
    7.11 +
    7.12 +open Exp;
    7.13 +
    7.14 +val eval_elim_cases = map (eval.mk_cases exp.simps)
    7.15 +   ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
    7.16 +    "(Op f a1 a2,sigma)  -|-> (n,s')",
    7.17 +    "(VALOF c RESULTIS e, s) -|-> (n, s1)"
    7.18 +   ];
    7.19 +
    7.20 +AddSEs eval_elim_cases;
    7.21 +
    7.22 +
    7.23 +(** Make the induction rule look nicer -- though eta_contract makes the new
    7.24 +    version look worse than it is...**)
    7.25 +
    7.26 +goal thy "{((e,s),(n,s')). P e s n s'} = \
    7.27 +\         Collect (split (%v. split (split P v)))";
    7.28 +by (rtac Collect_cong 1);
    7.29 +by (split_all_tac 1);
    7.30 +by (Simp_tac 1);
    7.31 +val split_lemma = result();
    7.32 +
    7.33 +(*New induction rule.  Note the form of the VALOF induction hypothesis*)
    7.34 +val major::prems = goal thy
    7.35 +  "[| (e,s) -|-> (n,s');                                         \
    7.36 +\     !!n s. P (N n) s n s;                                      \
    7.37 +\     !!s x. P (X x) s (s x) s;                                  \
    7.38 +\     !!e0 e1 f n0 n1 s s0 s1.                                   \
    7.39 +\        [| (e0,s) -|-> (n0,s0); P e0 s n0 s0;                   \
    7.40 +\           (e1,s0) -|-> (n1,s1); P e1 s0 n1 s1                  \
    7.41 +\        |] ==> P (Op f e0 e1) s (f n0 n1) s1;                   \
    7.42 +\     !!c e n s s0 s1.                                           \
    7.43 +\        [| (c,s) -[eval Int {((e,s),(n,s')). P e s n s'}]-> s0; \
    7.44 +\           (e,s0) -|-> (n,s1); P e s0 n s1 |]                   \
    7.45 +\        ==> P (VALOF c RESULTIS e) s n s1                       \
    7.46 +\  |] ==> P e s n s'";
    7.47 +by (rtac (major RS eval.induct) 1);
    7.48 +by (blast_tac (!claset addIs prems) 1);
    7.49 +by (blast_tac (!claset addIs prems) 1);
    7.50 +by (blast_tac (!claset addIs prems) 1);
    7.51 +by (fast_tac (!claset addIs prems addss (!simpset addsimps [split_lemma])) 1);
    7.52 +qed "eval_induct";
    7.53 +
    7.54 +
    7.55 +(*Lemma for Function_eval.  The major premise is that (c,s) executes to s1
    7.56 +  using eval restricted to its functional part.  Note that the execution
    7.57 +  (c,s) -[eval]-> s2 can use unrestricted eval!  The reason is that 
    7.58 +  the execution (c,s) -[eval Int {...}]-> s1 assures us that execution is
    7.59 +  functional on the argument (c,s).
    7.60 +*)
    7.61 +goal thy
    7.62 +    "!!x. (c,s) -[eval Int {((e,s),(n,s')). Unique (e,s) (n,s') eval}]-> s1 \
    7.63 +\         ==> (ALL s2. (c,s) -[eval]-> s2 --> s2=s1)";
    7.64 +by (etac exec.induct 1);
    7.65 +by (ALLGOALS Full_simp_tac);
    7.66 +by (Blast_tac 3);
    7.67 +by (Blast_tac 1);
    7.68 +by (rewtac Unique_def);
    7.69 +by (Blast_tac 1);
    7.70 +by (Blast_tac 1);
    7.71 +by (Blast_tac 1);
    7.72 +by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
    7.73 +by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
    7.74 +by (Step_tac 1);
    7.75 +by (etac exec_WHILE_case 1);
    7.76 +by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
    7.77 +qed "com_Unique";
    7.78 +
    7.79 +
    7.80 +(*Expression evaluation is functional, or deterministic*)
    7.81 +goal thy "Function eval";
    7.82 +by (simp_tac (!simpset addsimps [Function_def]) 1);
    7.83 +by (REPEAT (rtac allI 1));
    7.84 +by (rtac impI 1);
    7.85 +by (etac eval_induct 1);
    7.86 +by (dtac com_Unique 4);
    7.87 +by (ALLGOALS (full_simp_tac (!simpset addsimps [Unique_def])));
    7.88 +by (ALLGOALS Blast_tac);
    7.89 +qed "Function_eval";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Induct/Exp.thy	Wed May 07 12:50:26 1997 +0200
     8.3 @@ -0,0 +1,33 @@
     8.4 +(*  Title:      HOL/Induct/Exp
     8.5 +    ID:         $Id$
     8.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 +    Copyright   1997  University of Cambridge
     8.8 +
     8.9 +Example of Mutual Induction via Iteratived Inductive Definitions: Expressions
    8.10 +*)
    8.11 +
    8.12 +Exp = Com +
    8.13 +
    8.14 +(** Evaluation of arithmetic expressions **)
    8.15 +consts  eval    :: "((exp*state) * (nat*state)) set"
    8.16 +       "-|->"   :: "[exp*state,nat*state] => bool"         (infixl 50)
    8.17 +translations
    8.18 +    "esig -|-> (n,s)" <= "(esig,n,s) : eval"
    8.19 +    "esig -|-> ns"    == "(esig,ns) : eval"
    8.20 +  
    8.21 +inductive eval
    8.22 +  intrs 
    8.23 +    N      "(N(n),s) -|-> (n,s)"
    8.24 +
    8.25 +    X      "(X(x),s) -|-> (s(x),s)"
    8.26 +
    8.27 +    Op     "[| (e0,s) -|-> (n0,s0);  (e1,s0)  -|-> (n1,s1) |] 
    8.28 +            ==> (Op f e0 e1, s) -|-> (f n0 n1, s1)"
    8.29 +
    8.30 +    valOf  "[| (c,s) -[eval]-> s0;  (e,s0)  -|-> (n,s1) |] 
    8.31 +            ==> (VALOF c RESULTIS e, s) -|-> (n, s1)"
    8.32 +
    8.33 +  monos "[exec_mono]"
    8.34 +
    8.35 +end
    8.36 +
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Induct/LFilter.ML	Wed May 07 12:50:26 1997 +0200
     9.3 @@ -0,0 +1,341 @@
     9.4 +(*  Title:      HOL/ex/LFilter
     9.5 +    ID:         $Id$
     9.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7 +    Copyright   1997  University of Cambridge
     9.8 +
     9.9 +The "filter" functional for coinductive lists
    9.10 +  --defined by a combination of induction and coinduction
    9.11 +*)
    9.12 +
    9.13 +open LFilter;
    9.14 +
    9.15 +
    9.16 +(*** findRel: basic laws ****)
    9.17 +
    9.18 +val findRel_LConsE = 
    9.19 +    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
    9.20 +
    9.21 +AddSEs [findRel_LConsE];
    9.22 +
    9.23 +
    9.24 +goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
    9.25 +by (etac findRel.induct 1);
    9.26 +by (Blast_tac 1);
    9.27 +by (Blast_tac 1);
    9.28 +qed_spec_mp "findRel_functional";
    9.29 +
    9.30 +goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
    9.31 +by (etac findRel.induct 1);
    9.32 +by (Blast_tac 1);
    9.33 +by (Blast_tac 1);
    9.34 +qed_spec_mp "findRel_imp_LCons";
    9.35 +
    9.36 +goal thy "!!p. (LNil,l): findRel p ==> R";
    9.37 +by (blast_tac (!claset addEs [findRel.elim]) 1);
    9.38 +qed "findRel_LNil";
    9.39 +
    9.40 +AddSEs [findRel_LNil];
    9.41 +
    9.42 +
    9.43 +(*** Properties of Domain (findRel p) ***)
    9.44 +
    9.45 +goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
    9.46 +by (case_tac "p x" 1);
    9.47 +by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
    9.48 +qed "LCons_Domain_findRel";
    9.49 +
    9.50 +Addsimps [LCons_Domain_findRel];
    9.51 +
    9.52 +val major::prems = 
    9.53 +goal thy "[| l: Domain (findRel p);                                   \
    9.54 +\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
    9.55 +\         |] ==> Q";
    9.56 +by (rtac (major RS DomainE) 1);
    9.57 +by (forward_tac [findRel_imp_LCons] 1);
    9.58 +by (REPEAT (eresolve_tac [exE,conjE] 1));
    9.59 +by (hyp_subst_tac 1);
    9.60 +by (REPEAT (ares_tac prems 1));
    9.61 +qed "Domain_findRelE";
    9.62 +
    9.63 +val prems = goal thy
    9.64 +    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
    9.65 +by (Step_tac 1);
    9.66 +by (etac findRel.induct 1);
    9.67 +by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
    9.68 +by (blast_tac (!claset addIs findRel.intrs) 1);
    9.69 +qed "Domain_findRel_mono";
    9.70 +
    9.71 +
    9.72 +(*** find: basic equations ***)
    9.73 +
    9.74 +goalw thy [find_def] "find p LNil = LNil";
    9.75 +by (blast_tac (!claset addIs [select_equality]) 1);
    9.76 +qed "find_LNil";
    9.77 +
    9.78 +goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
    9.79 +by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
    9.80 +qed "findRel_imp_find";
    9.81 +
    9.82 +goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
    9.83 +by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
    9.84 +qed "find_LCons_found";
    9.85 +
    9.86 +goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
    9.87 +by (blast_tac (!claset addIs [select_equality]) 1);
    9.88 +qed "diverge_find_LNil";
    9.89 +
    9.90 +Addsimps [diverge_find_LNil];
    9.91 +
    9.92 +goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
    9.93 +by (case_tac "LCons x l : Domain(findRel p)" 1);
    9.94 +by (Asm_full_simp_tac 2);
    9.95 +by (Step_tac 1);
    9.96 +by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
    9.97 +by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
    9.98 +qed "find_LCons_seek";
    9.99 +
   9.100 +goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
   9.101 +by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
   9.102 +                           setloop split_tac[expand_if]) 1);
   9.103 +qed "find_LCons";
   9.104 +
   9.105 +
   9.106 +
   9.107 +(*** lfilter: basic equations ***)
   9.108 +
   9.109 +goal thy "lfilter p LNil = LNil";
   9.110 +by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   9.111 +by (simp_tac (!simpset addsimps [find_LNil]) 1);
   9.112 +qed "lfilter_LNil";
   9.113 +
   9.114 +goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
   9.115 +by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   9.116 +by (Asm_simp_tac 1);
   9.117 +qed "diverge_lfilter_LNil";
   9.118 +
   9.119 +
   9.120 +goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
   9.121 +by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   9.122 +by (asm_simp_tac (!simpset addsimps [find_LCons_found]) 1);
   9.123 +qed "lfilter_LCons_found";
   9.124 +
   9.125 +
   9.126 +goal thy "!!p. (l, LCons x l') : findRel p \
   9.127 +\              ==> lfilter p l = LCons x (lfilter p l')";
   9.128 +by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   9.129 +by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
   9.130 +qed "findRel_imp_lfilter";
   9.131 +
   9.132 +goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
   9.133 +by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
   9.134 +by (case_tac "LCons x l : Domain(findRel p)" 1);
   9.135 +by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   9.136 +by (etac Domain_findRelE 1);
   9.137 +by (safe_tac (!claset delrules [conjI]));
   9.138 +by (asm_full_simp_tac 
   9.139 +    (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
   9.140 +                        find_LCons_seek]) 1);
   9.141 +qed "lfilter_LCons_seek";
   9.142 +
   9.143 +
   9.144 +goal thy "lfilter p (LCons x l) = \
   9.145 +\         (if p x then LCons x (lfilter p l) else lfilter p l)";
   9.146 +by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
   9.147 +                           setloop split_tac[expand_if]) 1);
   9.148 +qed "lfilter_LCons";
   9.149 +
   9.150 +AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   9.151 +Addsimps [lfilter_LNil, lfilter_LCons];
   9.152 +
   9.153 +
   9.154 +goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
   9.155 +by (rtac notI 1);
   9.156 +by (etac Domain_findRelE 1);
   9.157 +by (etac rev_mp 1);
   9.158 +by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   9.159 +qed "lfilter_eq_LNil";
   9.160 +
   9.161 +
   9.162 +goal thy "!!p. lfilter p l = LCons x l' -->     \
   9.163 +\              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
   9.164 +by (stac (lfilter_def RS def_llist_corec) 1);
   9.165 +by (case_tac "l : Domain(findRel p)" 1);
   9.166 +by (etac Domain_findRelE 1);
   9.167 +by (Asm_simp_tac 2);
   9.168 +by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
   9.169 +by (Blast_tac 1);
   9.170 +qed_spec_mp "lfilter_eq_LCons";
   9.171 +
   9.172 +
   9.173 +goal thy "lfilter p l = LNil  |  \
   9.174 +\         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
   9.175 +by (case_tac "l : Domain(findRel p)" 1);
   9.176 +by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   9.177 +by (blast_tac (!claset addSEs [Domain_findRelE] 
   9.178 +                       addIs [findRel_imp_lfilter]) 1);
   9.179 +qed "lfilter_cases";
   9.180 +
   9.181 +
   9.182 +(*** lfilter: simple facts by coinduction ***)
   9.183 +
   9.184 +goal thy "lfilter (%x.True) l = l";
   9.185 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.186 +by (ALLGOALS Simp_tac);
   9.187 +by (Blast_tac 1);
   9.188 +qed "lfilter_K_True";
   9.189 +
   9.190 +goal thy "lfilter p (lfilter p l) = lfilter p l";
   9.191 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.192 +by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   9.193 +by (Step_tac 1);
   9.194 +(*Cases: p x is true or false*)
   9.195 +by (Blast_tac 1);
   9.196 +by (rtac (lfilter_cases RS disjE) 1);
   9.197 +by (etac ssubst 1);
   9.198 +by (Auto_tac());
   9.199 +qed "lfilter_idem";
   9.200 +
   9.201 +
   9.202 +(*** Numerous lemmas required to prove lfilter_conj:
   9.203 +     lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
   9.204 + ***)
   9.205 +
   9.206 +goal thy "!!p. (l,l') : findRel q \
   9.207 +\           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
   9.208 +by (etac findRel.induct 1);
   9.209 +by (blast_tac (!claset addIs findRel.intrs) 1);
   9.210 +by (blast_tac (!claset addIs findRel.intrs) 1);
   9.211 +qed_spec_mp "findRel_conj_lemma";
   9.212 +
   9.213 +val findRel_conj = refl RSN (2, findRel_conj_lemma);
   9.214 +
   9.215 +goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
   9.216 +\              ==> (l, LCons x l') : findRel q --> ~ p x     \
   9.217 +\                  --> l' : Domain (findRel (%x. p x & q x))";
   9.218 +by (etac findRel.induct 1);
   9.219 +by (Auto_tac());
   9.220 +qed_spec_mp "findRel_not_conj_Domain";
   9.221 +
   9.222 +
   9.223 +goal thy "!!p. (l,lxx) : findRel q ==> \
   9.224 +\            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
   9.225 +\            --> (l,lz) : findRel (%x. p x & q x)";
   9.226 +by (etac findRel.induct 1);
   9.227 +by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
   9.228 +qed_spec_mp "findRel_conj2";
   9.229 +
   9.230 +
   9.231 +goal thy "!!p. (lx,ly) : findRel p \
   9.232 +\              ==> ALL l. lx = lfilter q l \
   9.233 +\                  --> l : Domain (findRel(%x. p x & q x))";
   9.234 +by (etac findRel.induct 1);
   9.235 +by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
   9.236 +                       addIs  [findRel_conj]) 1);
   9.237 +by (Auto_tac());
   9.238 +by (dtac (sym RS lfilter_eq_LCons) 1);
   9.239 +by (Auto_tac());
   9.240 +by (dtac spec 1);
   9.241 +by (dtac (refl RS rev_mp) 1);
   9.242 +by (blast_tac (!claset addIs [findRel_conj2]) 1);
   9.243 +qed_spec_mp "findRel_lfilter_Domain_conj";
   9.244 +
   9.245 +
   9.246 +goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
   9.247 +\              ==> l'' = LCons y l' --> \
   9.248 +\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
   9.249 +by (etac findRel.induct 1);
   9.250 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
   9.251 +by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
   9.252 +qed_spec_mp "findRel_conj_lfilter";
   9.253 +
   9.254 +
   9.255 +
   9.256 +goal thy "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)  \
   9.257 +\         : llistD_Fun (range                                   \
   9.258 +\                       (%u. (lfilter p (lfilter q u),          \
   9.259 +\                             lfilter (%x. p x & q x) u)))";
   9.260 +by (case_tac "l : Domain(findRel q)" 1);
   9.261 +by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   9.262 +by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
   9.263 +(*There are no qs in l: both lists are LNil*)
   9.264 +by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   9.265 +by (etac Domain_findRelE 1);
   9.266 +(*case q x*)
   9.267 +by (case_tac "p x" 1);
   9.268 +by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
   9.269 +                                     findRel_conj RS findRel_imp_lfilter]) 1);
   9.270 +by (Blast_tac 1);
   9.271 +(*case q x and ~(p x) *)
   9.272 +by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   9.273 +by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
   9.274 +(*subcase: there is no p&q in l' and therefore none in l*)
   9.275 +by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   9.276 +by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
   9.277 +by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
   9.278 +by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
   9.279 +(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
   9.280 +by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   9.281 +(*subcase: there is a p&q in l' and therefore also one in l*)
   9.282 +by (etac Domain_findRelE 1);
   9.283 +by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
   9.284 +by (blast_tac (!claset addIs [findRel_conj2]) 2);
   9.285 +by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
   9.286 +by (blast_tac (!claset addIs [findRel_conj_lfilter]) 2);
   9.287 +by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   9.288 +by (Blast_tac 1);
   9.289 +val lemma = result();
   9.290 +
   9.291 +
   9.292 +goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
   9.293 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.294 +by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   9.295 +by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
   9.296 +qed "lfilter_conj";
   9.297 +
   9.298 +
   9.299 +(*** Numerous lemmas required to prove ??:
   9.300 +     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
   9.301 + ***)
   9.302 +
   9.303 +goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
   9.304 +by (etac findRel.induct 1);
   9.305 +by (ALLGOALS Asm_full_simp_tac);
   9.306 +qed "findRel_lmap_Domain";
   9.307 +
   9.308 +
   9.309 +goal thy "!!p. lmap f l = LCons x l' -->     \
   9.310 +\              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
   9.311 +by (stac (lmap_def RS def_llist_corec) 1);
   9.312 +by (res_inst_tac [("l", "l")] llistE 1);
   9.313 +by (Auto_tac());
   9.314 +qed_spec_mp "lmap_eq_LCons";
   9.315 +
   9.316 +
   9.317 +goal thy "!!p. (lx,ly) : findRel p ==>  \
   9.318 +\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
   9.319 +\    (EX y l''. x = f y & l' = lmap f l'' &       \
   9.320 +\    (l, LCons y l'') : findRel(%x. p(f x)))";
   9.321 +by (etac findRel.induct 1);
   9.322 +by (ALLGOALS Asm_simp_tac);
   9.323 +by (safe_tac (!claset addSDs [lmap_eq_LCons]));
   9.324 +by (blast_tac (!claset addIs findRel.intrs) 1);
   9.325 +by (blast_tac (!claset addIs findRel.intrs) 1);
   9.326 +qed_spec_mp "lmap_LCons_findRel_lemma";
   9.327 +
   9.328 +val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
   9.329 +
   9.330 +goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
   9.331 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
   9.332 +by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
   9.333 +by (Step_tac 1);
   9.334 +by (Blast_tac 1);
   9.335 +by (case_tac "lmap f l : Domain (findRel p)" 1);
   9.336 +by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
   9.337 +by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
   9.338 +by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
   9.339 +by (etac Domain_findRelE 1);
   9.340 +by (forward_tac [lmap_LCons_findRel] 1);
   9.341 +by (Step_tac 1);
   9.342 +by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
   9.343 +by (Blast_tac 1);
   9.344 +qed "lfilter_lmap";
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Induct/LFilter.thy	Wed May 07 12:50:26 1997 +0200
    10.3 @@ -0,0 +1,29 @@
    10.4 +(*  Title:      HOL/LList.thy
    10.5 +    ID:         $Id$
    10.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    10.7 +    Copyright   1997  University of Cambridge
    10.8 +
    10.9 +The "filter" functional for coinductive lists
   10.10 +  --defined by a combination of induction and coinduction
   10.11 +*)
   10.12 +
   10.13 +LFilter = LList + Relation +
   10.14 +
   10.15 +consts
   10.16 +  findRel	:: "('a => bool) => ('a llist * 'a llist)set"
   10.17 +
   10.18 +inductive "findRel p"
   10.19 +  intrs
   10.20 +    found  "p x ==> (LCons x l, LCons x l) : findRel p"
   10.21 +    seek   "[| ~p x;  (l,l') : findRel p |] ==> (LCons x l, l') : findRel p"
   10.22 +
   10.23 +constdefs
   10.24 +  find		:: ['a => bool, 'a llist] => 'a llist
   10.25 +    "find p l == @l'. (l,l'): findRel p | (l' = LNil & l ~: Domain(findRel p))"
   10.26 +
   10.27 +  lfilter	:: ['a => bool, 'a llist] => 'a llist
   10.28 +    "lfilter p l == llist_corec l (%l. case find p l of
   10.29 +                                            LNil => Inl ()
   10.30 +                                          | LCons y z => Inr(y,z))"
   10.31 +
   10.32 +end
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Induct/LList.ML	Wed May 07 12:50:26 1997 +0200
    11.3 @@ -0,0 +1,886 @@
    11.4 +(*  Title:      HOL/ex/LList
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   1993  University of Cambridge
    11.8 +
    11.9 +SHOULD LListD_Fun_CONS_I, etc., be equations (for rewriting)?
   11.10 +*)
   11.11 +
   11.12 +open LList;
   11.13 +
   11.14 +(** Simplification **)
   11.15 +
   11.16 +simpset := !simpset setloop split_tac [expand_split, expand_sum_case];
   11.17 +
   11.18 +(*For adding _eqI rules to a simpset; we must remove Pair_eq because
   11.19 +  it may turn an instance of reflexivity into a conjunction!*)
   11.20 +fun add_eqI ss = ss addsimps [range_eqI, image_eqI] 
   11.21 +                    delsimps [Pair_eq];
   11.22 +
   11.23 +
   11.24 +(*This justifies using llist in other recursive type definitions*)
   11.25 +goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
   11.26 +by (rtac gfp_mono 1);
   11.27 +by (REPEAT (ares_tac basic_monos 1));
   11.28 +qed "llist_mono";
   11.29 +
   11.30 +
   11.31 +goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
   11.32 +let val rew = rewrite_rule [NIL_def, CONS_def] in  
   11.33 +by (fast_tac (!claset addSIs (equalityI :: map rew llist.intrs)
   11.34 +                      addEs [rew llist.elim]) 1)
   11.35 +end;
   11.36 +qed "llist_unfold";
   11.37 +
   11.38 +
   11.39 +(*** Type checking by coinduction, using list_Fun 
   11.40 +     THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
   11.41 +***)
   11.42 +
   11.43 +goalw LList.thy [list_Fun_def]
   11.44 +    "!!M. [| M : X;  X <= list_Fun A (X Un llist(A)) |] ==>  M : llist(A)";
   11.45 +by (etac llist.coinduct 1);
   11.46 +by (etac (subsetD RS CollectD) 1);
   11.47 +by (assume_tac 1);
   11.48 +qed "llist_coinduct";
   11.49 +
   11.50 +goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
   11.51 +by (Fast_tac 1);
   11.52 +qed "list_Fun_NIL_I";
   11.53 +
   11.54 +goalw LList.thy [list_Fun_def,CONS_def]
   11.55 +    "!!M N. [| M: A;  N: X |] ==> CONS M N : list_Fun A X";
   11.56 +by (Fast_tac 1);
   11.57 +qed "list_Fun_CONS_I";
   11.58 +
   11.59 +(*Utilise the "strong" part, i.e. gfp(f)*)
   11.60 +goalw LList.thy (llist.defs @ [list_Fun_def])
   11.61 +    "!!M N. M: llist(A) ==> M : list_Fun A (X Un llist(A))";
   11.62 +by (etac (llist.mono RS gfp_fun_UnI2) 1);
   11.63 +qed "list_Fun_llist_I";
   11.64 +
   11.65 +(*** LList_corec satisfies the desired recurion equation ***)
   11.66 +
   11.67 +(*A continuity result?*)
   11.68 +goalw LList.thy [CONS_def] "CONS M (UN x.f(x)) = (UN x. CONS M (f x))";
   11.69 +by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
   11.70 +qed "CONS_UN1";
   11.71 +
   11.72 +(*UNUSED; obsolete?
   11.73 +goal Prod.thy "split p (%x y.UN z.f x y z) = (UN z. split p (%x y.f x y z))";
   11.74 +by (simp_tac (!simpset setloop (split_tac [expand_split])) 1);
   11.75 +qed "split_UN1";
   11.76 +
   11.77 +goal Sum.thy "sum_case s f (%y.UN z.g y z) = (UN z.sum_case s f (%y.g y z))";
   11.78 +by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
   11.79 +qed "sum_case2_UN1";
   11.80 +*)
   11.81 +
   11.82 +val prems = goalw LList.thy [CONS_def]
   11.83 +    "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
   11.84 +by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
   11.85 +qed "CONS_mono";
   11.86 +
   11.87 +Addsimps [LList_corec_fun_def RS def_nat_rec_0,
   11.88 +          LList_corec_fun_def RS def_nat_rec_Suc];
   11.89 +
   11.90 +(** The directions of the equality are proved separately **)
   11.91 +
   11.92 +goalw LList.thy [LList_corec_def]
   11.93 +    "LList_corec a f <= sum_case (%u.NIL) \
   11.94 +\                          (split(%z w. CONS z (LList_corec w f))) (f a)";
   11.95 +by (rtac UN1_least 1);
   11.96 +by (res_inst_tac [("n","k")] natE 1);
   11.97 +by (ALLGOALS (Asm_simp_tac));
   11.98 +by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
   11.99 +qed "LList_corec_subset1";
  11.100 +
  11.101 +goalw LList.thy [LList_corec_def]
  11.102 +    "sum_case (%u.NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
  11.103 +\    LList_corec a f";
  11.104 +by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
  11.105 +by (safe_tac (!claset));
  11.106 +by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
  11.107 +qed "LList_corec_subset2";
  11.108 +
  11.109 +(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
  11.110 +goal LList.thy
  11.111 +    "LList_corec a f = sum_case (%u. NIL) \
  11.112 +\                           (split(%z w. CONS z (LList_corec w f))) (f a)";
  11.113 +by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
  11.114 +                         LList_corec_subset2] 1));
  11.115 +qed "LList_corec";
  11.116 +
  11.117 +(*definitional version of same*)
  11.118 +val [rew] = goal LList.thy
  11.119 +    "[| !!x. h(x) == LList_corec x f |] ==>     \
  11.120 +\    h(a) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f a)";
  11.121 +by (rewtac rew);
  11.122 +by (rtac LList_corec 1);
  11.123 +qed "def_LList_corec";
  11.124 +
  11.125 +(*A typical use of co-induction to show membership in the gfp. 
  11.126 +  Bisimulation is  range(%x. LList_corec x f) *)
  11.127 +goal LList.thy "LList_corec a f : llist({u.True})";
  11.128 +by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
  11.129 +by (rtac rangeI 1);
  11.130 +by (safe_tac (!claset));
  11.131 +by (stac LList_corec 1);
  11.132 +by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
  11.133 +                       |> add_eqI) 1);
  11.134 +qed "LList_corec_type";
  11.135 +
  11.136 +(*Lemma for the proof of llist_corec*)
  11.137 +goal LList.thy
  11.138 +   "LList_corec a (%z.sum_case Inl (split(%v w.Inr((Leaf(v),w)))) (f z)) : \
  11.139 +\   llist(range Leaf)";
  11.140 +by (res_inst_tac [("X", "range(%x.LList_corec x ?g)")] llist_coinduct 1);
  11.141 +by (rtac rangeI 1);
  11.142 +by (safe_tac (!claset));
  11.143 +by (stac LList_corec 1);
  11.144 +by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
  11.145 +by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
  11.146 +qed "LList_corec_type2";
  11.147 +
  11.148 +
  11.149 +(**** llist equality as a gfp; the bisimulation principle ****)
  11.150 +
  11.151 +(*This theorem is actually used, unlike the many similar ones in ZF*)
  11.152 +goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
  11.153 +let val rew = rewrite_rule [NIL_def, CONS_def] in  
  11.154 +by (fast_tac (!claset addSIs (equalityI :: map rew LListD.intrs)
  11.155 +                      addEs [rew LListD.elim]) 1)
  11.156 +end;
  11.157 +qed "LListD_unfold";
  11.158 +
  11.159 +goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
  11.160 +by (res_inst_tac [("n", "k")] less_induct 1);
  11.161 +by (safe_tac ((claset_of "Fun") delrules [equalityI]));
  11.162 +by (etac LListD.elim 1);
  11.163 +by (safe_tac (((claset_of "Prod") delrules [equalityI]) addSEs [diagE]));
  11.164 +by (res_inst_tac [("n", "n")] natE 1);
  11.165 +by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
  11.166 +by (rename_tac "n'" 1);
  11.167 +by (res_inst_tac [("n", "n'")] natE 1);
  11.168 +by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
  11.169 +by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
  11.170 +qed "LListD_implies_ntrunc_equality";
  11.171 +
  11.172 +(*The domain of the LListD relation*)
  11.173 +goalw LList.thy (llist.defs @ [NIL_def, CONS_def])
  11.174 +    "fst``LListD(diag(A)) <= llist(A)";
  11.175 +by (rtac gfp_upperbound 1);
  11.176 +(*avoids unfolding LListD on the rhs*)
  11.177 +by (res_inst_tac [("P", "%x. fst``x <= ?B")] (LListD_unfold RS ssubst) 1);
  11.178 +by (Simp_tac 1);
  11.179 +by (Fast_tac 1);
  11.180 +qed "fst_image_LListD";
  11.181 +
  11.182 +(*This inclusion justifies the use of coinduction to show M=N*)
  11.183 +goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
  11.184 +by (rtac subsetI 1);
  11.185 +by (res_inst_tac [("p","x")] PairE 1);
  11.186 +by (safe_tac (!claset));
  11.187 +by (rtac diag_eqI 1);
  11.188 +by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
  11.189 +          ntrunc_equality) 1);
  11.190 +by (assume_tac 1);
  11.191 +by (etac (fst_imageI RS (fst_image_LListD RS subsetD)) 1);
  11.192 +qed "LListD_subset_diag";
  11.193 +
  11.194 +
  11.195 +(** Coinduction, using LListD_Fun
  11.196 +    THE COINDUCTIVE DEFINITION PACKAGE COULD DO THIS!
  11.197 + **)
  11.198 +
  11.199 +goalw thy [LListD_Fun_def] "!!A B. A<=B ==> LListD_Fun r A <= LListD_Fun r B";
  11.200 +by (REPEAT (ares_tac basic_monos 1));
  11.201 +qed "LListD_Fun_mono";
  11.202 +
  11.203 +goalw LList.thy [LListD_Fun_def]
  11.204 +    "!!M. [| M : X;  X <= LListD_Fun r (X Un LListD(r)) |] ==>  M : LListD(r)";
  11.205 +by (etac LListD.coinduct 1);
  11.206 +by (etac (subsetD RS CollectD) 1);
  11.207 +by (assume_tac 1);
  11.208 +qed "LListD_coinduct";
  11.209 +
  11.210 +goalw LList.thy [LListD_Fun_def,NIL_def] "(NIL,NIL) : LListD_Fun r s";
  11.211 +by (Fast_tac 1);
  11.212 +qed "LListD_Fun_NIL_I";
  11.213 +
  11.214 +goalw LList.thy [LListD_Fun_def,CONS_def]
  11.215 + "!!x. [| x:A;  (M,N):s |] ==> (CONS x M, CONS x N) : LListD_Fun (diag A) s";
  11.216 +by (Fast_tac 1);
  11.217 +qed "LListD_Fun_CONS_I";
  11.218 +
  11.219 +(*Utilise the "strong" part, i.e. gfp(f)*)
  11.220 +goalw LList.thy (LListD.defs @ [LListD_Fun_def])
  11.221 +    "!!M N. M: LListD(r) ==> M : LListD_Fun r (X Un LListD(r))";
  11.222 +by (etac (LListD.mono RS gfp_fun_UnI2) 1);
  11.223 +qed "LListD_Fun_LListD_I";
  11.224 +
  11.225 +
  11.226 +(*This converse inclusion helps to strengthen LList_equalityI*)
  11.227 +goal LList.thy "diag(llist(A)) <= LListD(diag(A))";
  11.228 +by (rtac subsetI 1);
  11.229 +by (etac LListD_coinduct 1);
  11.230 +by (rtac subsetI 1);
  11.231 +by (etac diagE 1);
  11.232 +by (etac ssubst 1);
  11.233 +by (eresolve_tac [llist.elim] 1);
  11.234 +by (ALLGOALS
  11.235 +    (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I,
  11.236 +                                      LListD_Fun_CONS_I])));
  11.237 +qed "diag_subset_LListD";
  11.238 +
  11.239 +goal LList.thy "LListD(diag(A)) = diag(llist(A))";
  11.240 +by (REPEAT (resolve_tac [equalityI, LListD_subset_diag, 
  11.241 +                         diag_subset_LListD] 1));
  11.242 +qed "LListD_eq_diag";
  11.243 +
  11.244 +goal LList.thy 
  11.245 +    "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
  11.246 +by (rtac (LListD_eq_diag RS subst) 1);
  11.247 +by (rtac LListD_Fun_LListD_I 1);
  11.248 +by (asm_simp_tac (!simpset addsimps [LListD_eq_diag, diagI]) 1);
  11.249 +qed "LListD_Fun_diag_I";
  11.250 +
  11.251 +
  11.252 +(** To show two LLists are equal, exhibit a bisimulation! 
  11.253 +      [also admits true equality]
  11.254 +   Replace "A" by some particular set, like {x.True}??? *)
  11.255 +goal LList.thy 
  11.256 +    "!!r. [| (M,N) : r;  r <= LListD_Fun (diag A) (r Un diag(llist(A))) \
  11.257 +\         |] ==>  M=N";
  11.258 +by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
  11.259 +by (etac LListD_coinduct 1);
  11.260 +by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
  11.261 +by (safe_tac (!claset));
  11.262 +qed "LList_equalityI";
  11.263 +
  11.264 +
  11.265 +(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
  11.266 +
  11.267 +(*abstract proof using a bisimulation*)
  11.268 +val [prem1,prem2] = goal LList.thy
  11.269 + "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
  11.270 +\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
  11.271 +\ ==> h1=h2";
  11.272 +by (rtac ext 1);
  11.273 +(*next step avoids an unknown (and flexflex pair) in simplification*)
  11.274 +by (res_inst_tac [("A", "{u.True}"),
  11.275 +                  ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
  11.276 +by (rtac rangeI 1);
  11.277 +by (safe_tac (!claset));
  11.278 +by (stac prem1 1);
  11.279 +by (stac prem2 1);
  11.280 +by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
  11.281 +                                 CollectI RS LListD_Fun_CONS_I]
  11.282 +                       |> add_eqI) 1);
  11.283 +qed "LList_corec_unique";
  11.284 +
  11.285 +val [prem] = goal LList.thy
  11.286 + "[| !!x. h(x) = sum_case (%u.NIL) (split(%z w. CONS z (h w))) (f x) |] \
  11.287 +\ ==> h = (%x.LList_corec x f)";
  11.288 +by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
  11.289 +qed "equals_LList_corec";
  11.290 +
  11.291 +
  11.292 +(** Obsolete LList_corec_unique proof: complete induction, not coinduction **)
  11.293 +
  11.294 +goalw LList.thy [CONS_def] "ntrunc (Suc 0) (CONS M N) = {}";
  11.295 +by (rtac ntrunc_one_In1 1);
  11.296 +qed "ntrunc_one_CONS";
  11.297 +
  11.298 +goalw LList.thy [CONS_def]
  11.299 +    "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
  11.300 +by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1);
  11.301 +qed "ntrunc_CONS";
  11.302 +
  11.303 +val [prem1,prem2] = goal LList.thy
  11.304 + "[| !!x. h1(x) = sum_case (%u.NIL) (split(%z w. CONS z (h1 w))) (f x);  \
  11.305 +\    !!x. h2(x) = sum_case (%u.NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
  11.306 +\ ==> h1=h2";
  11.307 +by (rtac (ntrunc_equality RS ext) 1);
  11.308 +by (rename_tac "x k" 1);
  11.309 +by (res_inst_tac [("x", "x")] spec 1);
  11.310 +by (res_inst_tac [("n", "k")] less_induct 1);
  11.311 +by (rename_tac "n" 1);
  11.312 +by (rtac allI 1);
  11.313 +by (rename_tac "y" 1);
  11.314 +by (stac prem1 1);
  11.315 +by (stac prem2 1);
  11.316 +by (simp_tac (!simpset setloop (split_tac [expand_sum_case])) 1);
  11.317 +by (strip_tac 1);
  11.318 +by (res_inst_tac [("n", "n")] natE 1);
  11.319 +by (rename_tac "m" 2);
  11.320 +by (res_inst_tac [("n", "m")] natE 2);
  11.321 +by (ALLGOALS(asm_simp_tac(!simpset addsimps
  11.322 +            [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
  11.323 +result();
  11.324 +
  11.325 +
  11.326 +(*** Lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
  11.327 +
  11.328 +goal LList.thy "mono(CONS(M))";
  11.329 +by (REPEAT (ares_tac [monoI, subset_refl, CONS_mono] 1));
  11.330 +qed "Lconst_fun_mono";
  11.331 +
  11.332 +(* Lconst(M) = CONS M (Lconst M) *)
  11.333 +bind_thm ("Lconst", (Lconst_fun_mono RS (Lconst_def RS def_lfp_Tarski)));
  11.334 +
  11.335 +(*A typical use of co-induction to show membership in the gfp.
  11.336 +  The containing set is simply the singleton {Lconst(M)}. *)
  11.337 +goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
  11.338 +by (rtac (singletonI RS llist_coinduct) 1);
  11.339 +by (safe_tac (!claset));
  11.340 +by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
  11.341 +by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
  11.342 +qed "Lconst_type";
  11.343 +
  11.344 +goal LList.thy "Lconst(M) = LList_corec M (%x.Inr((x,x)))";
  11.345 +by (rtac (equals_LList_corec RS fun_cong) 1);
  11.346 +by (Simp_tac 1);
  11.347 +by (rtac Lconst 1);
  11.348 +qed "Lconst_eq_LList_corec";
  11.349 +
  11.350 +(*Thus we could have used gfp in the definition of Lconst*)
  11.351 +goal LList.thy "gfp(%N. CONS M N) = LList_corec M (%x.Inr((x,x)))";
  11.352 +by (rtac (equals_LList_corec RS fun_cong) 1);
  11.353 +by (Simp_tac 1);
  11.354 +by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
  11.355 +qed "gfp_Lconst_eq_LList_corec";
  11.356 +
  11.357 +
  11.358 +(*** Isomorphisms ***)
  11.359 +
  11.360 +goal LList.thy "inj(Rep_llist)";
  11.361 +by (rtac inj_inverseI 1);
  11.362 +by (rtac Rep_llist_inverse 1);
  11.363 +qed "inj_Rep_llist";
  11.364 +
  11.365 +goal LList.thy "inj_onto Abs_llist (llist(range Leaf))";
  11.366 +by (rtac inj_onto_inverseI 1);
  11.367 +by (etac Abs_llist_inverse 1);
  11.368 +qed "inj_onto_Abs_llist";
  11.369 +
  11.370 +(** Distinctness of constructors **)
  11.371 +
  11.372 +goalw LList.thy [LNil_def,LCons_def] "~ LCons x xs = LNil";
  11.373 +by (rtac (CONS_not_NIL RS (inj_onto_Abs_llist RS inj_onto_contraD)) 1);
  11.374 +by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
  11.375 +qed "LCons_not_LNil";
  11.376 +
  11.377 +bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
  11.378 +
  11.379 +AddIffs [LCons_not_LNil, LNil_not_LCons];
  11.380 +
  11.381 +
  11.382 +(** llist constructors **)
  11.383 +
  11.384 +goalw LList.thy [LNil_def]
  11.385 +    "Rep_llist(LNil) = NIL";
  11.386 +by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
  11.387 +qed "Rep_llist_LNil";
  11.388 +
  11.389 +goalw LList.thy [LCons_def]
  11.390 +    "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
  11.391 +by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
  11.392 +                         rangeI, Rep_llist] 1));
  11.393 +qed "Rep_llist_LCons";
  11.394 +
  11.395 +(** Injectiveness of CONS and LCons **)
  11.396 +
  11.397 +goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
  11.398 +by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
  11.399 +qed "CONS_CONS_eq2";
  11.400 +
  11.401 +bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
  11.402 +
  11.403 +
  11.404 +(*For reasoning about abstract llist constructors*)
  11.405 +
  11.406 +AddIs ([Rep_llist]@llist.intrs);
  11.407 +AddSDs [inj_onto_Abs_llist RS inj_ontoD,
  11.408 +        inj_Rep_llist RS injD, Leaf_inject];
  11.409 +
  11.410 +goalw LList.thy [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
  11.411 +by (Fast_tac 1);
  11.412 +qed "LCons_LCons_eq";
  11.413 +
  11.414 +AddIffs [LCons_LCons_eq];
  11.415 +
  11.416 +val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
  11.417 +by (rtac (major RS llist.elim) 1);
  11.418 +by (etac CONS_neq_NIL 1);
  11.419 +by (Fast_tac 1);
  11.420 +qed "CONS_D2";
  11.421 +
  11.422 +
  11.423 +(****** Reasoning about llist(A) ******)
  11.424 +
  11.425 +Addsimps [List_case_NIL, List_case_CONS];
  11.426 +
  11.427 +(*A special case of list_equality for functions over lazy lists*)
  11.428 +val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
  11.429 + "[| M: llist(A); g(NIL): llist(A);                             \
  11.430 +\    f(NIL)=g(NIL);                                             \
  11.431 +\    !!x l. [| x:A;  l: llist(A) |] ==>                         \
  11.432 +\           (f(CONS x l),g(CONS x l)) :                         \
  11.433 +\               LListD_Fun (diag A) ((%u.(f(u),g(u)))``llist(A) Un  \
  11.434 +\                                   diag(llist(A)))             \
  11.435 +\ |] ==> f(M) = g(M)";
  11.436 +by (rtac LList_equalityI 1);
  11.437 +by (rtac (Mlist RS imageI) 1);
  11.438 +by (rtac subsetI 1);
  11.439 +by (etac imageE 1);
  11.440 +by (etac ssubst 1);
  11.441 +by (etac llist.elim 1);
  11.442 +by (etac ssubst 1);
  11.443 +by (stac NILcase 1);
  11.444 +by (rtac (gMlist RS LListD_Fun_diag_I) 1);
  11.445 +by (etac ssubst 1);
  11.446 +by (REPEAT (ares_tac [CONScase] 1));
  11.447 +qed "LList_fun_equalityI";
  11.448 +
  11.449 +
  11.450 +(*** The functional "Lmap" ***)
  11.451 +
  11.452 +goal LList.thy "Lmap f NIL = NIL";
  11.453 +by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
  11.454 +by (Simp_tac 1);
  11.455 +qed "Lmap_NIL";
  11.456 +
  11.457 +goal LList.thy "Lmap f (CONS M N) = CONS (f M) (Lmap f N)";
  11.458 +by (rtac (Lmap_def RS def_LList_corec RS trans) 1);
  11.459 +by (Simp_tac 1);
  11.460 +qed "Lmap_CONS";
  11.461 +
  11.462 +(*Another type-checking proof by coinduction*)
  11.463 +val [major,minor] = goal LList.thy
  11.464 +    "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
  11.465 +by (rtac (major RS imageI RS llist_coinduct) 1);
  11.466 +by (safe_tac (!claset));
  11.467 +by (etac llist.elim 1);
  11.468 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  11.469 +by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
  11.470 +                      minor, imageI, UnI1] 1));
  11.471 +qed "Lmap_type";
  11.472 +
  11.473 +(*This type checking rule synthesises a sufficiently large set for f*)
  11.474 +val [major] = goal LList.thy  "M: llist(A) ==> Lmap f M: llist(f``A)";
  11.475 +by (rtac (major RS Lmap_type) 1);
  11.476 +by (etac imageI 1);
  11.477 +qed "Lmap_type2";
  11.478 +
  11.479 +(** Two easy results about Lmap **)
  11.480 +
  11.481 +val [prem] = goalw LList.thy [o_def]
  11.482 +    "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
  11.483 +by (rtac (prem RS imageI RS LList_equalityI) 1);
  11.484 +by (safe_tac (!claset));
  11.485 +by (etac llist.elim 1);
  11.486 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  11.487 +by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
  11.488 +                      rangeI RS LListD_Fun_CONS_I] 1));
  11.489 +qed "Lmap_compose";
  11.490 +
  11.491 +val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x.x) M = M";
  11.492 +by (rtac (prem RS imageI RS LList_equalityI) 1);
  11.493 +by (safe_tac (!claset));
  11.494 +by (etac llist.elim 1);
  11.495 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
  11.496 +by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
  11.497 +                      rangeI RS LListD_Fun_CONS_I] 1));
  11.498 +qed "Lmap_ident";
  11.499 +
  11.500 +
  11.501 +(*** Lappend -- its two arguments cause some complications! ***)
  11.502 +
  11.503 +goalw LList.thy [Lappend_def] "Lappend NIL NIL = NIL";
  11.504 +by (rtac (LList_corec RS trans) 1);
  11.505 +by (Simp_tac 1);
  11.506 +qed "Lappend_NIL_NIL";
  11.507 +
  11.508 +goalw LList.thy [Lappend_def]
  11.509 +    "Lappend NIL (CONS N N') = CONS N (Lappend NIL N')";
  11.510 +by (rtac (LList_corec RS trans) 1);
  11.511 +by (Simp_tac 1);
  11.512 +qed "Lappend_NIL_CONS";
  11.513 +
  11.514 +goalw LList.thy [Lappend_def]
  11.515 +    "Lappend (CONS M M') N = CONS M (Lappend M' N)";
  11.516 +by (rtac (LList_corec RS trans) 1);
  11.517 +by (Simp_tac 1);
  11.518 +qed "Lappend_CONS";
  11.519 +
  11.520 +Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
  11.521 +          Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
  11.522 +Delsimps [Pair_eq];
  11.523 +
  11.524 +goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
  11.525 +by (etac LList_fun_equalityI 1);
  11.526 +by (ALLGOALS Asm_simp_tac);
  11.527 +qed "Lappend_NIL";
  11.528 +
  11.529 +goal LList.thy "!!M. M: llist(A) ==> Lappend M NIL = M";
  11.530 +by (etac LList_fun_equalityI 1);
  11.531 +by (ALLGOALS Asm_simp_tac);
  11.532 +qed "Lappend_NIL2";
  11.533 +
  11.534 +(** Alternative type-checking proofs for Lappend **)
  11.535 +
  11.536 +(*weak co-induction: bisimulation and case analysis on both variables*)
  11.537 +goal LList.thy
  11.538 +    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
  11.539 +by (res_inst_tac
  11.540 +    [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
  11.541 +by (Fast_tac 1);
  11.542 +by (safe_tac (!claset));
  11.543 +by (eres_inst_tac [("a", "u")] llist.elim 1);
  11.544 +by (eres_inst_tac [("a", "v")] llist.elim 1);
  11.545 +by (ALLGOALS
  11.546 +    (Asm_simp_tac THEN'
  11.547 +     fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
  11.548 +qed "Lappend_type";
  11.549 +
  11.550 +(*strong co-induction: bisimulation and case analysis on one variable*)
  11.551 +goal LList.thy
  11.552 +    "!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
  11.553 +by (res_inst_tac [("X", "(%u.Lappend u N)``llist(A)")] llist_coinduct 1);
  11.554 +by (etac imageI 1);
  11.555 +by (rtac subsetI 1);
  11.556 +by (etac imageE 1);
  11.557 +by (eres_inst_tac [("a", "u")] llist.elim 1);
  11.558 +by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
  11.559 +by (Asm_simp_tac 1);
  11.560 +by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
  11.561 +qed "Lappend_type";
  11.562 +
  11.563 +(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
  11.564 +
  11.565 +(** llist_case: case analysis for 'a llist **)
  11.566 +
  11.567 +Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
  11.568 +           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
  11.569 +
  11.570 +goalw LList.thy [llist_case_def,LNil_def]  "llist_case c d LNil = c";
  11.571 +by (Simp_tac 1);
  11.572 +qed "llist_case_LNil";
  11.573 +
  11.574 +goalw LList.thy [llist_case_def,LCons_def]
  11.575 +    "llist_case c d (LCons M N) = d M N";
  11.576 +by (Simp_tac 1);
  11.577 +qed "llist_case_LCons";
  11.578 +
  11.579 +(*Elimination is case analysis, not induction.*)
  11.580 +val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
  11.581 +    "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P \
  11.582 +\    |] ==> P";
  11.583 +by (rtac (Rep_llist RS llist.elim) 1);
  11.584 +by (rtac (inj_Rep_llist RS injD RS prem1) 1);
  11.585 +by (stac Rep_llist_LNil 1);
  11.586 +by (assume_tac 1);
  11.587 +by (etac rangeE 1);
  11.588 +by (rtac (inj_Rep_llist RS injD RS prem2) 1);
  11.589 +by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
  11.590 +by (etac (Abs_llist_inverse RS ssubst) 1);
  11.591 +by (rtac refl 1);
  11.592 +qed "llistE";
  11.593 +
  11.594 +(** llist_corec: corecursion for 'a llist **)
  11.595 +
  11.596 +goalw LList.thy [llist_corec_def,LNil_def,LCons_def]
  11.597 +    "llist_corec a f = sum_case (%u. LNil) \
  11.598 +\                           (split(%z w. LCons z (llist_corec w f))) (f a)";
  11.599 +by (stac LList_corec 1);
  11.600 +by (res_inst_tac [("s","f(a)")] sumE 1);
  11.601 +by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
  11.602 +by (res_inst_tac [("p","y")] PairE 1);
  11.603 +by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
  11.604 +(*FIXME: correct case splits usd to be found automatically:
  11.605 +by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*)
  11.606 +qed "llist_corec";
  11.607 +
  11.608 +(*definitional version of same*)
  11.609 +val [rew] = goal LList.thy
  11.610 +    "[| !!x. h(x) == llist_corec x f |] ==>     \
  11.611 +\    h(a) = sum_case (%u.LNil) (split(%z w. LCons z (h w))) (f a)";
  11.612 +by (rewtac rew);
  11.613 +by (rtac llist_corec 1);
  11.614 +qed "def_llist_corec";
  11.615 +
  11.616 +(**** Proofs about type 'a llist functions ****)
  11.617 +
  11.618 +(*** Deriving llist_equalityI -- llist equality is a bisimulation ***)
  11.619 +
  11.620 +goalw LList.thy [LListD_Fun_def]
  11.621 +    "!!r A. r <= (llist A) Times (llist A) ==> \
  11.622 +\           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
  11.623 +by (stac llist_unfold 1);
  11.624 +by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
  11.625 +by (Fast_tac 1);
  11.626 +qed "LListD_Fun_subset_Sigma_llist";
  11.627 +
  11.628 +goal LList.thy
  11.629 +    "prod_fun Rep_llist Rep_llist `` r <= \
  11.630 +\    (llist(range Leaf)) Times (llist(range Leaf))";
  11.631 +by (fast_tac (!claset addIs [Rep_llist]) 1);
  11.632 +qed "subset_Sigma_llist";
  11.633 +
  11.634 +val [prem] = goal LList.thy
  11.635 +    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
  11.636 +\    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
  11.637 +by (safe_tac (!claset));
  11.638 +by (rtac (prem RS subsetD RS SigmaE2) 1);
  11.639 +by (assume_tac 1);
  11.640 +by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
  11.641 +qed "prod_fun_lemma";
  11.642 +
  11.643 +goal LList.thy
  11.644 +    "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
  11.645 +\    diag(llist(range Leaf))";
  11.646 +by (rtac equalityI 1);
  11.647 +by (fast_tac (!claset addIs [Rep_llist]) 1);
  11.648 +by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
  11.649 +qed "prod_fun_range_eq_diag";
  11.650 +
  11.651 +(*Surprisingly hard to prove.  Used with lfilter*)
  11.652 +goalw thy [llistD_Fun_def, prod_fun_def]
  11.653 +    "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
  11.654 +by (Auto_tac());
  11.655 +by (rtac image_eqI 1);
  11.656 +by (fast_tac (!claset addss (!simpset)) 1);
  11.657 +by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
  11.658 +qed "llistD_Fun_mono";
  11.659 +
  11.660 +(** To show two llists are equal, exhibit a bisimulation! 
  11.661 +      [also admits true equality] **)
  11.662 +val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
  11.663 +    "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
  11.664 +by (rtac (inj_Rep_llist RS injD) 1);
  11.665 +by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
  11.666 +                  ("A", "range(Leaf)")] 
  11.667 +        LList_equalityI 1);
  11.668 +by (rtac (prem1 RS prod_fun_imageI) 1);
  11.669 +by (rtac (prem2 RS image_mono RS subset_trans) 1);
  11.670 +by (rtac (image_compose RS subst) 1);
  11.671 +by (rtac (prod_fun_compose RS subst) 1);
  11.672 +by (stac image_Un 1);
  11.673 +by (stac prod_fun_range_eq_diag 1);
  11.674 +by (rtac (LListD_Fun_subset_Sigma_llist RS prod_fun_lemma) 1);
  11.675 +by (rtac (subset_Sigma_llist RS Un_least) 1);
  11.676 +by (rtac diag_subset_Sigma 1);
  11.677 +qed "llist_equalityI";
  11.678 +
  11.679 +(** Rules to prove the 2nd premise of llist_equalityI **)
  11.680 +goalw LList.thy [llistD_Fun_def,LNil_def] "(LNil,LNil) : llistD_Fun(r)";
  11.681 +by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
  11.682 +qed "llistD_Fun_LNil_I";
  11.683 +
  11.684 +val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
  11.685 +    "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
  11.686 +by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
  11.687 +by (rtac (prem RS prod_fun_imageI) 1);
  11.688 +qed "llistD_Fun_LCons_I";
  11.689 +
  11.690 +(*Utilise the "strong" part, i.e. gfp(f)*)
  11.691 +goalw LList.thy [llistD_Fun_def]
  11.692 +     "!!l. (l,l) : llistD_Fun(r Un range(%x.(x,x)))";
  11.693 +by (rtac (Rep_llist_inverse RS subst) 1);
  11.694 +by (rtac prod_fun_imageI 1);
  11.695 +by (stac image_Un 1);
  11.696 +by (stac prod_fun_range_eq_diag 1);
  11.697 +by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
  11.698 +qed "llistD_Fun_range_I";
  11.699 +
  11.700 +(*A special case of list_equality for functions over lazy lists*)
  11.701 +val [prem1,prem2] = goal LList.thy
  11.702 +    "[| f(LNil)=g(LNil);                                                \
  11.703 +\       !!x l. (f(LCons x l),g(LCons x l)) :                            \
  11.704 +\              llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
  11.705 +\    |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
  11.706 +by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
  11.707 +by (rtac rangeI 1);
  11.708 +by (rtac subsetI 1);
  11.709 +by (etac rangeE 1);
  11.710 +by (etac ssubst 1);
  11.711 +by (res_inst_tac [("l", "u")] llistE 1);
  11.712 +by (etac ssubst 1);
  11.713 +by (stac prem1 1);
  11.714 +by (rtac llistD_Fun_range_I 1);
  11.715 +by (etac ssubst 1);
  11.716 +by (rtac prem2 1);
  11.717 +qed "llist_fun_equalityI";
  11.718 +
  11.719 +(*simpset for llist bisimulations*)
  11.720 +Addsimps [llist_case_LNil, llist_case_LCons, 
  11.721 +          llistD_Fun_LNil_I, llistD_Fun_LCons_I];
  11.722 +
  11.723 +
  11.724 +(*** The functional "lmap" ***)
  11.725 +
  11.726 +goal LList.thy "lmap f LNil = LNil";
  11.727 +by (rtac (lmap_def RS def_llist_corec RS trans) 1);
  11.728 +by (Simp_tac 1);
  11.729 +qed "lmap_LNil";
  11.730 +
  11.731 +goal LList.thy "lmap f (LCons M N) = LCons (f M) (lmap f N)";
  11.732 +by (rtac (lmap_def RS def_llist_corec RS trans) 1);
  11.733 +by (Simp_tac 1);
  11.734 +qed "lmap_LCons";
  11.735 +
  11.736 +Addsimps [lmap_LNil, lmap_LCons];
  11.737 +
  11.738 +
  11.739 +(** Two easy results about lmap **)
  11.740 +
  11.741 +goal LList.thy "lmap (f o g) l = lmap f (lmap g l)";
  11.742 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  11.743 +by (ALLGOALS Simp_tac);
  11.744 +qed "lmap_compose";
  11.745 +
  11.746 +goal LList.thy "lmap (%x.x) l = l";
  11.747 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  11.748 +by (ALLGOALS Simp_tac);
  11.749 +qed "lmap_ident";
  11.750 +
  11.751 +
  11.752 +(*** iterates -- llist_fun_equalityI cannot be used! ***)
  11.753 +
  11.754 +goal LList.thy "iterates f x = LCons x (iterates f (f x))";
  11.755 +by (rtac (iterates_def RS def_llist_corec RS trans) 1);
  11.756 +by (Simp_tac 1);
  11.757 +qed "iterates";
  11.758 +
  11.759 +goal LList.thy "lmap f (iterates f x) = iterates f (f x)";
  11.760 +by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
  11.761 +    llist_equalityI 1);
  11.762 +by (rtac rangeI 1);
  11.763 +by (safe_tac (!claset));
  11.764 +by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
  11.765 +by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
  11.766 +by (Simp_tac 1);
  11.767 +qed "lmap_iterates";
  11.768 +
  11.769 +goal LList.thy "iterates f x = LCons x (lmap f (iterates f x))";
  11.770 +by (stac lmap_iterates 1);
  11.771 +by (rtac iterates 1);
  11.772 +qed "iterates_lmap";
  11.773 +
  11.774 +(*** A rather complex proof about iterates -- cf Andy Pitts ***)
  11.775 +
  11.776 +(** Two lemmas about natrec n x (%m.g), which is essentially (g^n)(x) **)
  11.777 +
  11.778 +goal LList.thy
  11.779 +    "nat_rec (LCons b l) (%m. lmap(f)) n =      \
  11.780 +\    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
  11.781 +by (nat_ind_tac "n" 1);
  11.782 +by (ALLGOALS Asm_simp_tac);
  11.783 +qed "fun_power_lmap";
  11.784 +
  11.785 +goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
  11.786 +by (nat_ind_tac "n" 1);
  11.787 +by (ALLGOALS Asm_simp_tac);
  11.788 +qed "fun_power_Suc";
  11.789 +
  11.790 +val Pair_cong = read_instantiate_sg (sign_of Prod.thy)
  11.791 + [("f","Pair")] (standard(refl RS cong RS cong));
  11.792 +
  11.793 +(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
  11.794 +  for all u and all n::nat.*)
  11.795 +val [prem] = goal LList.thy
  11.796 +    "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
  11.797 +by (rtac ext 1);
  11.798 +by (res_inst_tac [("r", 
  11.799 +   "UN u. range(%n. (nat_rec (h u) (%m y.lmap f y) n, \
  11.800 +\                    nat_rec (iterates f u) (%m y.lmap f y) n))")] 
  11.801 +    llist_equalityI 1);
  11.802 +by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
  11.803 +by (safe_tac (!claset));
  11.804 +by (stac iterates 1);
  11.805 +by (stac prem 1);
  11.806 +by (stac fun_power_lmap 1);
  11.807 +by (stac fun_power_lmap 1);
  11.808 +by (rtac llistD_Fun_LCons_I 1);
  11.809 +by (rtac (lmap_iterates RS subst) 1);
  11.810 +by (stac fun_power_Suc 1);
  11.811 +by (stac fun_power_Suc 1);
  11.812 +by (rtac (UN1_I RS UnI1) 1);
  11.813 +by (rtac rangeI 1);
  11.814 +qed "iterates_equality";
  11.815 +
  11.816 +
  11.817 +(*** lappend -- its two arguments cause some complications! ***)
  11.818 +
  11.819 +goalw LList.thy [lappend_def] "lappend LNil LNil = LNil";
  11.820 +by (rtac (llist_corec RS trans) 1);
  11.821 +by (Simp_tac 1);
  11.822 +qed "lappend_LNil_LNil";
  11.823 +
  11.824 +goalw LList.thy [lappend_def]
  11.825 +    "lappend LNil (LCons l l') = LCons l (lappend LNil l')";
  11.826 +by (rtac (llist_corec RS trans) 1);
  11.827 +by (Simp_tac 1);
  11.828 +qed "lappend_LNil_LCons";
  11.829 +
  11.830 +goalw LList.thy [lappend_def]
  11.831 +    "lappend (LCons l l') N = LCons l (lappend l' N)";
  11.832 +by (rtac (llist_corec RS trans) 1);
  11.833 +by (Simp_tac 1);
  11.834 +qed "lappend_LCons";
  11.835 +
  11.836 +Addsimps [lappend_LNil_LNil, lappend_LNil_LCons, lappend_LCons];
  11.837 +
  11.838 +goal LList.thy "lappend LNil l = l";
  11.839 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  11.840 +by (ALLGOALS Simp_tac);
  11.841 +qed "lappend_LNil";
  11.842 +
  11.843 +goal LList.thy "lappend l LNil = l";
  11.844 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  11.845 +by (ALLGOALS Simp_tac);
  11.846 +qed "lappend_LNil2";
  11.847 +
  11.848 +Addsimps [lappend_LNil, lappend_LNil2];
  11.849 +
  11.850 +(*The infinite first argument blocks the second*)
  11.851 +goal LList.thy "lappend (iterates f x) N = iterates f x";
  11.852 +by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
  11.853 +    llist_equalityI 1);
  11.854 +by (rtac rangeI 1);
  11.855 +by (safe_tac (!claset));
  11.856 +by (stac iterates 1);
  11.857 +by (Simp_tac 1);
  11.858 +qed "lappend_iterates";
  11.859 +
  11.860 +(** Two proofs that lmap distributes over lappend **)
  11.861 +
  11.862 +(*Long proof requiring case analysis on both both arguments*)
  11.863 +goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
  11.864 +by (res_inst_tac 
  11.865 +    [("r",  
  11.866 +      "UN n. range(%l.(lmap f (lappend l n),lappend (lmap f l) (lmap f n)))")] 
  11.867 +    llist_equalityI 1);
  11.868 +by (rtac UN1_I 1);
  11.869 +by (rtac rangeI 1);
  11.870 +by (safe_tac (!claset));
  11.871 +by (res_inst_tac [("l", "l")] llistE 1);
  11.872 +by (res_inst_tac [("l", "n")] llistE 1);
  11.873 +by (ALLGOALS Asm_simp_tac);
  11.874 +by (REPEAT_SOME (ares_tac [llistD_Fun_LCons_I, UN1_I RS UnI1, rangeI]));
  11.875 +qed "lmap_lappend_distrib";
  11.876 +
  11.877 +(*Shorter proof of theorem above using llist_equalityI as strong coinduction*)
  11.878 +goal LList.thy "lmap f (lappend l n) = lappend (lmap f l) (lmap f n)";
  11.879 +by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
  11.880 +by (Simp_tac 1);
  11.881 +by (Simp_tac 1);
  11.882 +qed "lmap_lappend_distrib";
  11.883 +
  11.884 +(*Without strong coinduction, three case analyses might be needed*)
  11.885 +goal LList.thy "lappend (lappend l1 l2) l3 = lappend l1 (lappend l2 l3)";
  11.886 +by (res_inst_tac [("l","l1")] llist_fun_equalityI 1);
  11.887 +by (Simp_tac 1);
  11.888 +by (Simp_tac 1);
  11.889 +qed "lappend_assoc";
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/HOL/Induct/LList.thy	Wed May 07 12:50:26 1997 +0200
    12.3 @@ -0,0 +1,153 @@
    12.4 +(*  Title:      HOL/LList.thy
    12.5 +    ID:         $Id$
    12.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.7 +    Copyright   1994  University of Cambridge
    12.8 +
    12.9 +Definition of type 'a llist by a greatest fixed point
   12.10 +
   12.11 +Shares NIL, CONS, List_case with List.thy
   12.12 +
   12.13 +Still needs filter and flatten functions -- hard because they need
   12.14 +bounds on the amount of lookahead required.
   12.15 +
   12.16 +Could try (but would it work for the gfp analogue of term?)
   12.17 +  LListD_Fun_def "LListD_Fun(A) == (%Z.diag({Numb(0)}) <++> diag(A) <**> Z)"
   12.18 +
   12.19 +A nice but complex example would be [ML for the Working Programmer, page 176]
   12.20 +  from(1) = enumerate (Lmap (Lmap(pack), makeqq(from(1),from(1))))
   12.21 +
   12.22 +Previous definition of llistD_Fun was explicit:
   12.23 +  llistD_Fun_def
   12.24 +   "llistD_Fun(r) ==    
   12.25 +       {(LNil,LNil)}  Un        
   12.26 +       (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
   12.27 +*)
   12.28 +
   12.29 +LList = Gfp + SList +
   12.30 +
   12.31 +types
   12.32 +  'a llist
   12.33 +
   12.34 +arities
   12.35 +   llist :: (term)term
   12.36 +
   12.37 +consts
   12.38 +  list_Fun   :: ['a item set, 'a item set] => 'a item set
   12.39 +  LListD_Fun :: 
   12.40 +      "[('a item * 'a item)set, ('a item * 'a item)set] => 
   12.41 +      ('a item * 'a item)set"
   12.42 +
   12.43 +  llist      :: 'a item set => 'a item set
   12.44 +  LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
   12.45 +  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
   12.46 +
   12.47 +  Rep_llist  :: 'a llist => 'a item
   12.48 +  Abs_llist  :: 'a item => 'a llist
   12.49 +  LNil       :: 'a llist
   12.50 +  LCons      :: ['a, 'a llist] => 'a llist
   12.51 +  
   12.52 +  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
   12.53 +
   12.54 +  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
   12.55 +  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
   12.56 +  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
   12.57 +
   12.58 +  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
   12.59 +  lmap       :: ('a=>'b) => ('a llist => 'b llist)
   12.60 +
   12.61 +  iterates   :: ['a => 'a, 'a] => 'a llist
   12.62 +
   12.63 +  Lconst     :: 'a item => 'a item
   12.64 +  Lappend    :: ['a item, 'a item] => 'a item
   12.65 +  lappend    :: ['a llist, 'a llist] => 'a llist
   12.66 +
   12.67 +
   12.68 +coinductive "llist(A)"
   12.69 +  intrs
   12.70 +    NIL_I  "NIL: llist(A)"
   12.71 +    CONS_I "[| a: A;  M: llist(A) |] ==> CONS a M : llist(A)"
   12.72 +
   12.73 +coinductive "LListD(r)"
   12.74 +  intrs
   12.75 +    NIL_I  "(NIL, NIL) : LListD(r)"
   12.76 +    CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
   12.77 +            |] ==> (CONS a M, CONS b N) : LListD(r)"
   12.78 +
   12.79 +translations
   12.80 +  "case p of LNil => a | LCons x l => b" == "llist_case a (%x l.b) p"
   12.81 +
   12.82 +
   12.83 +defs
   12.84 +  (*Now used exclusively for abbreviating the coinduction rule*)
   12.85 +  list_Fun_def   "list_Fun A X ==   
   12.86 +                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   12.87 +
   12.88 +  LListD_Fun_def "LListD_Fun r X ==   
   12.89 +                  {z. z = (NIL, NIL) |   
   12.90 +                      (? M N a b. z = (CONS a M, CONS b N) &   
   12.91 +                                  (a, b) : r & (M, N) : X)}"
   12.92 +
   12.93 +  (*defining the abstract constructors*)
   12.94 +  LNil_def      "LNil == Abs_llist(NIL)"
   12.95 +  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   12.96 +
   12.97 +  llist_case_def
   12.98 +   "llist_case c d l == 
   12.99 +       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
  12.100 +
  12.101 +  LList_corec_fun_def
  12.102 +    "LList_corec_fun k f == 
  12.103 +     nat_rec (%x. {})                         
  12.104 +             (%j r x. case f x of Inl u    => NIL
  12.105 +                                | Inr(z,w) => CONS z (r w)) 
  12.106 +             k"
  12.107 +
  12.108 +  LList_corec_def
  12.109 +    "LList_corec a f == UN k. LList_corec_fun k f a"
  12.110 +
  12.111 +  llist_corec_def
  12.112 +   "llist_corec a f == 
  12.113 +       Abs_llist(LList_corec a 
  12.114 +                 (%z.case f z of Inl x    => Inl(x)
  12.115 +                               | Inr(v,w) => Inr(Leaf(v), w)))"
  12.116 +
  12.117 +  llistD_Fun_def
  12.118 +   "llistD_Fun(r) ==    
  12.119 +        prod_fun Abs_llist Abs_llist ``         
  12.120 +                LListD_Fun (diag(range Leaf))   
  12.121 +                            (prod_fun Rep_llist Rep_llist `` r)"
  12.122 +
  12.123 +  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
  12.124 +
  12.125 +  Lmap_def
  12.126 +   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
  12.127 +
  12.128 +  lmap_def
  12.129 +   "lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
  12.130 +                                           | LCons y z => Inr(f(y), z))"
  12.131 +
  12.132 +  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
  12.133 +
  12.134 +(*Append generates its result by applying f, where
  12.135 +    f((NIL,NIL))          = Inl(())
  12.136 +    f((NIL, CONS N1 N2))  = Inr((N1, (NIL,N2))
  12.137 +    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
  12.138 +*)
  12.139 +
  12.140 +  Lappend_def
  12.141 +   "Lappend M N == LList_corec (M,N)                                         
  12.142 +     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
  12.143 +                      (%M1 M2 N. Inr((M1, (M2,N))))))"
  12.144 +
  12.145 +  lappend_def
  12.146 +   "lappend l n == llist_corec (l,n)                                         
  12.147 +   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
  12.148 +                     (%l1 l2 n. Inr((l1, (l2,n))))))"
  12.149 +
  12.150 +rules
  12.151 +    (*faking a type definition...*)
  12.152 +  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
  12.153 +  Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
  12.154 +  Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
  12.155 +
  12.156 +end
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Induct/Mutil.ML	Wed May 07 12:50:26 1997 +0200
    13.3 @@ -0,0 +1,172 @@
    13.4 +(*  Title:      HOL/ex/Mutil
    13.5 +    ID:         $Id$
    13.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    13.7 +    Copyright   1996  University of Cambridge
    13.8 +
    13.9 +The Mutilated Chess Board Problem, formalized inductively
   13.10 +*)
   13.11 +
   13.12 +open Mutil;
   13.13 +
   13.14 +Addsimps tiling.intrs;
   13.15 +
   13.16 +(** The union of two disjoint tilings is a tiling **)
   13.17 +
   13.18 +goal thy "!!t. t: tiling A ==> \
   13.19 +\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
   13.20 +by (etac tiling.induct 1);
   13.21 +by (Simp_tac 1);
   13.22 +by (simp_tac (!simpset addsimps [Un_assoc]) 1);
   13.23 +by (blast_tac (!claset addIs tiling.intrs) 1);
   13.24 +qed_spec_mp "tiling_UnI";
   13.25 +
   13.26 +
   13.27 +(*** Chess boards ***)
   13.28 +
   13.29 +val [below_0, below_Suc] = nat_recs below_def;
   13.30 +Addsimps [below_0, below_Suc];
   13.31 +
   13.32 +goal thy "ALL i. (i: below k) = (i<k)";
   13.33 +by (nat_ind_tac "k" 1);
   13.34 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
   13.35 +by (Blast_tac 1);
   13.36 +qed_spec_mp "below_less_iff";
   13.37 +
   13.38 +Addsimps [below_less_iff];
   13.39 +
   13.40 +goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
   13.41 +by (Simp_tac 1);
   13.42 +by (Blast_tac 1);
   13.43 +qed "Sigma_Suc1";
   13.44 +
   13.45 +goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
   13.46 +by (Simp_tac 1);
   13.47 +by (Blast_tac 1);
   13.48 +qed "Sigma_Suc2";
   13.49 +
   13.50 +(*Deletion is essential to allow use of Sigma_Suc1,2*)
   13.51 +Delsimps [below_Suc];
   13.52 +
   13.53 +goal thy "{i} Times below(n + n) : tiling domino";
   13.54 +by (nat_ind_tac "n" 1);
   13.55 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Un_assoc RS sym, Sigma_Suc2])));
   13.56 +by (resolve_tac tiling.intrs 1);
   13.57 +by (assume_tac 2);
   13.58 +by (subgoal_tac    (*seems the easiest way of turning one to the other*)
   13.59 +    "({i} Times {Suc(n+n)}) Un ({i} Times {n+n}) = \
   13.60 +\    {(i, n+n), (i, Suc(n+n))}" 1);
   13.61 +by (Blast_tac 2);
   13.62 +by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
   13.63 +by (blast_tac (!claset addEs  [less_irrefl, less_asym]
   13.64 +                       addSDs [below_less_iff RS iffD1]) 1);
   13.65 +qed "dominoes_tile_row";
   13.66 +
   13.67 +goal thy "(below m) Times below(n + n) : tiling domino";
   13.68 +by (nat_ind_tac "m" 1);
   13.69 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
   13.70 +by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
   13.71 +                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
   13.72 +qed "dominoes_tile_matrix";
   13.73 +
   13.74 +
   13.75 +(*** Basic properties of evnodd ***)
   13.76 +
   13.77 +goalw thy [evnodd_def] "(i,j): evnodd A b = ((i,j): A  &  (i+j) mod 2 = b)";
   13.78 +by (Simp_tac 1);
   13.79 +qed "evnodd_iff";
   13.80 +
   13.81 +goalw thy [evnodd_def] "evnodd A b <= A";
   13.82 +by (rtac Int_lower1 1);
   13.83 +qed "evnodd_subset";
   13.84 +
   13.85 +(* finite X ==> finite(evnodd X b) *)
   13.86 +bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
   13.87 +
   13.88 +goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
   13.89 +by (Blast_tac 1);
   13.90 +qed "evnodd_Un";
   13.91 +
   13.92 +goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
   13.93 +by (Blast_tac 1);
   13.94 +qed "evnodd_Diff";
   13.95 +
   13.96 +goalw thy [evnodd_def] "evnodd {} b = {}";
   13.97 +by (Simp_tac 1);
   13.98 +qed "evnodd_empty";
   13.99 +
  13.100 +goalw thy [evnodd_def]
  13.101 +    "evnodd (insert (i,j) C) b = \
  13.102 +\    (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
  13.103 +by (asm_full_simp_tac (!simpset addsimps [evnodd_def] 
  13.104 +             setloop (split_tac [expand_if] THEN' Step_tac)) 1);
  13.105 +qed "evnodd_insert";
  13.106 +
  13.107 +
  13.108 +(*** Dominoes ***)
  13.109 +
  13.110 +goal thy "!!d. [| d:domino; b<2 |] ==> EX i j. evnodd d b = {(i,j)}";
  13.111 +by (eresolve_tac [domino.elim] 1);
  13.112 +by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 2);
  13.113 +by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1);
  13.114 +by (REPEAT_FIRST assume_tac);
  13.115 +(*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*)
  13.116 +by (REPEAT (asm_full_simp_tac (!simpset addsimps
  13.117 +                          [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
  13.118 +                          setloop split_tac [expand_if]) 1
  13.119 +           THEN Blast_tac 1));
  13.120 +qed "domino_singleton";
  13.121 +
  13.122 +goal thy "!!d. d:domino ==> finite d";
  13.123 +by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
  13.124 +                      addSEs [domino.elim]) 1);
  13.125 +qed "domino_finite";
  13.126 +
  13.127 +
  13.128 +(*** Tilings of dominoes ***)
  13.129 +
  13.130 +goal thy "!!t. t:tiling domino ==> finite t";
  13.131 +by (eresolve_tac [tiling.induct] 1);
  13.132 +by (rtac finite_emptyI 1);
  13.133 +by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
  13.134 +qed "tiling_domino_finite";
  13.135 +
  13.136 +goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
  13.137 +by (eresolve_tac [tiling.induct] 1);
  13.138 +by (simp_tac (!simpset addsimps [evnodd_def]) 1);
  13.139 +by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1);
  13.140 +by (Simp_tac 2 THEN assume_tac 1);
  13.141 +by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
  13.142 +by (Simp_tac 2 THEN assume_tac 1);
  13.143 +by (Step_tac 1);
  13.144 +by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
  13.145 +by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
  13.146 +                                     tiling_domino_finite,
  13.147 +                                     evnodd_subset RS finite_subset,
  13.148 +                                     card_insert_disjoint]) 1);
  13.149 +by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
  13.150 +qed "tiling_domino_0_1";
  13.151 +
  13.152 +goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
  13.153 +\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
  13.154 +\                |] ==> t' ~: tiling domino";
  13.155 +by (rtac notI 1);
  13.156 +by (dtac tiling_domino_0_1 1);
  13.157 +by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
  13.158 +by (Asm_full_simp_tac 1);
  13.159 +by (subgoal_tac "t : tiling domino" 1);
  13.160 +(*Requires a small simpset that won't move the Suc applications*)
  13.161 +by (asm_simp_tac (HOL_ss addsimps [dominoes_tile_matrix]) 2);
  13.162 +by (subgoal_tac "(m+m)+(n+n) = (m+n)+(m+n)" 1);
  13.163 +by (asm_simp_tac (!simpset addsimps add_ac) 2);
  13.164 +by (asm_full_simp_tac 
  13.165 +    (!simpset addsimps [evnodd_Diff, evnodd_insert, evnodd_empty, 
  13.166 +                        mod_less, tiling_domino_0_1 RS sym]) 1);
  13.167 +by (rtac less_trans 1);
  13.168 +by (REPEAT
  13.169 +    (rtac card_Diff 1 
  13.170 +     THEN
  13.171 +     asm_simp_tac (!simpset addsimps [tiling_domino_finite, finite_evnodd]) 1 
  13.172 +     THEN
  13.173 +     asm_simp_tac (!simpset addsimps [mod_less, evnodd_iff]) 1));
  13.174 +qed "mutil_not_tiling";
  13.175 +
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Induct/Mutil.thy	Wed May 07 12:50:26 1997 +0200
    14.3 @@ -0,0 +1,32 @@
    14.4 +(*  Title:      HOL/ex/Mutil
    14.5 +    ID:         $Id$
    14.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    14.7 +    Copyright   1996  University of Cambridge
    14.8 +
    14.9 +The Mutilated Chess Board Problem, formalized inductively
   14.10 +  Originator is Max Black, according to J A Robinson.
   14.11 +  Popularized as the Mutilated Checkerboard Problem by J McCarthy
   14.12 +*)
   14.13 +
   14.14 +Mutil = Finite +
   14.15 +consts
   14.16 +  domino  :: "(nat*nat)set set"
   14.17 +  tiling  :: 'a set set => 'a set set
   14.18 +  below   :: nat => nat set
   14.19 +  evnodd  :: "[(nat*nat)set, nat] => (nat*nat)set"
   14.20 +
   14.21 +inductive domino
   14.22 +  intrs
   14.23 +    horiz  "{(i, j), (i, Suc j)} : domino"
   14.24 +    vertl  "{(i, j), (Suc i, j)} : domino"
   14.25 +
   14.26 +inductive "tiling A"
   14.27 +  intrs
   14.28 +    empty  "{} : tiling A"
   14.29 +    Un     "[| a: A;  t: tiling A;  a <= Compl t |] ==> a Un t : tiling A"
   14.30 +
   14.31 +defs
   14.32 +  below_def  "below n    == nat_rec {} insert n"
   14.33 +  evnodd_def "evnodd A b == A Int {(i,j). (i+j) mod 2 = b}"
   14.34 +
   14.35 +end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Induct/Perm.ML	Wed May 07 12:50:26 1997 +0200
    15.3 @@ -0,0 +1,98 @@
    15.4 +(*  Title:      HOL/ex/Perm.ML
    15.5 +    ID:         $Id$
    15.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7 +    Copyright   1995  University of Cambridge
    15.8 +
    15.9 +Permutations: example of an inductive definition
   15.10 +*)
   15.11 +
   15.12 +(*It would be nice to prove
   15.13 +    xs <~~> ys = (!x. count xs x = count ys x)
   15.14 +See mset on HOL/ex/Sorting.thy
   15.15 +*)
   15.16 +
   15.17 +open Perm;
   15.18 +
   15.19 +goal Perm.thy "l <~~> l";
   15.20 +by (list.induct_tac "l" 1);
   15.21 +by (REPEAT (ares_tac perm.intrs 1));
   15.22 +qed "perm_refl";
   15.23 +
   15.24 +
   15.25 +(** Some examples of rule induction on permutations **)
   15.26 +
   15.27 +(*The form of the premise lets the induction bind xs and ys.*)
   15.28 +goal Perm.thy "!!xs. xs <~~> ys ==> xs=[] --> ys=[]";
   15.29 +by (etac perm.induct 1);
   15.30 +by (ALLGOALS Asm_simp_tac);
   15.31 +qed "perm_Nil_lemma";
   15.32 +
   15.33 +(*A more general version is actually easier to understand!*)
   15.34 +goal Perm.thy "!!xs. xs <~~> ys ==> length(xs) = length(ys)";
   15.35 +by (etac perm.induct 1);
   15.36 +by (ALLGOALS Asm_simp_tac);
   15.37 +qed "perm_length";
   15.38 +
   15.39 +goal Perm.thy "!!xs. xs <~~> ys ==> ys <~~> xs";
   15.40 +by (etac perm.induct 1);
   15.41 +by (REPEAT (ares_tac perm.intrs 1));
   15.42 +qed "perm_sym";
   15.43 +
   15.44 +goal Perm.thy "!!xs. [| xs <~~> ys |] ==> x mem xs --> x mem ys";
   15.45 +by (etac perm.induct 1);
   15.46 +by (Fast_tac 4);
   15.47 +by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
   15.48 +val perm_mem_lemma = result();
   15.49 +
   15.50 +bind_thm ("perm_mem", perm_mem_lemma RS mp);
   15.51 +
   15.52 +(** Ways of making new permutations **)
   15.53 +
   15.54 +(*We can insert the head anywhere in the list*)
   15.55 +goal Perm.thy "a # xs @ ys <~~> xs @ a # ys";
   15.56 +by (list.induct_tac "xs" 1);
   15.57 +by (simp_tac (!simpset addsimps [perm_refl]) 1);
   15.58 +by (Simp_tac 1);
   15.59 +by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
   15.60 +qed "perm_append_Cons";
   15.61 +
   15.62 +(*single steps
   15.63 +by (rtac perm.trans 1);
   15.64 +by (rtac perm.swap 1);
   15.65 +by (rtac perm.Cons 1);
   15.66 +*)
   15.67 +
   15.68 +goal Perm.thy "xs@ys <~~> ys@xs";
   15.69 +by (list.induct_tac "xs" 1);
   15.70 +by (simp_tac (!simpset addsimps [perm_refl]) 1);
   15.71 +by (Simp_tac 1);
   15.72 +by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
   15.73 +qed "perm_append_swap";
   15.74 +
   15.75 +
   15.76 +goal Perm.thy "a # xs <~~> xs @ [a]";
   15.77 +by (rtac perm.trans 1);
   15.78 +by (rtac perm_append_swap 2);
   15.79 +by (simp_tac (!simpset addsimps [perm_refl]) 1);
   15.80 +qed "perm_append_single";
   15.81 +
   15.82 +goal Perm.thy "rev xs <~~> xs";
   15.83 +by (list.induct_tac "xs" 1);
   15.84 +by (simp_tac (!simpset addsimps [perm_refl]) 1);
   15.85 +by (Simp_tac 1);
   15.86 +by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
   15.87 +by (etac perm.Cons 1);
   15.88 +qed "perm_rev";
   15.89 +
   15.90 +goal Perm.thy "!!xs. xs <~~> ys ==> l@xs <~~> l@ys";
   15.91 +by (list.induct_tac "l" 1);
   15.92 +by (Simp_tac 1);
   15.93 +by (asm_simp_tac (!simpset addsimps [perm.Cons]) 1);
   15.94 +qed "perm_append1";
   15.95 +
   15.96 +goal Perm.thy "!!xs. xs <~~> ys ==> xs@l <~~> ys@l";
   15.97 +by (rtac (perm_append_swap RS perm.trans) 1);
   15.98 +by (etac (perm_append1 RS perm.trans) 1);
   15.99 +by (rtac perm_append_swap 1);
  15.100 +qed "perm_append2";
  15.101 +
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Induct/Perm.thy	Wed May 07 12:50:26 1997 +0200
    16.3 @@ -0,0 +1,24 @@
    16.4 +(*  Title:      HOL/ex/Perm.thy
    16.5 +    ID:         $Id$
    16.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    16.7 +    Copyright   1995  University of Cambridge
    16.8 +
    16.9 +Permutations: example of an inductive definition
   16.10 +*)
   16.11 +
   16.12 +Perm = List +
   16.13 +
   16.14 +consts  perm    :: "('a list * 'a list) set"   
   16.15 +syntax "@perm"  :: ['a list, 'a list] => bool ("_ <~~> _"  [50,50] 50)
   16.16 +
   16.17 +translations
   16.18 +    "x <~~> y" == "(x,y) : perm"
   16.19 +
   16.20 +inductive perm
   16.21 +  intrs
   16.22 +    Nil   "[] <~~> []"
   16.23 +    swap  "y#x#l <~~> x#y#l"
   16.24 +    Cons  "xs <~~> ys ==> z#xs <~~> z#ys"
   16.25 +    trans "[| xs <~~> ys;  ys <~~> zs |] ==> xs <~~> zs"
   16.26 +
   16.27 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Induct/PropLog.ML	Wed May 07 12:50:26 1997 +0200
    17.3 @@ -0,0 +1,229 @@
    17.4 +(*  Title:      HOL/ex/pl.ML
    17.5 +    ID:         $Id$
    17.6 +    Author:     Tobias Nipkow & Lawrence C Paulson
    17.7 +    Copyright   1994  TU Muenchen & University of Cambridge
    17.8 +
    17.9 +Soundness and completeness of propositional logic w.r.t. truth-tables.
   17.10 +
   17.11 +Prove: If H|=p then G|=p where G:Fin(H)
   17.12 +*)
   17.13 +
   17.14 +open PropLog;
   17.15 +
   17.16 +(** Monotonicity **)
   17.17 +goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
   17.18 +by (rtac lfp_mono 1);
   17.19 +by (REPEAT (ares_tac basic_monos 1));
   17.20 +qed "thms_mono";
   17.21 +
   17.22 +(*Rule is called I for Identity Combinator, not for Introduction*)
   17.23 +goal PropLog.thy "H |- p->p";
   17.24 +by (best_tac (!claset addIs [thms.K,thms.S,thms.MP]) 1);
   17.25 +qed "thms_I";
   17.26 +
   17.27 +(** Weakening, left and right **)
   17.28 +
   17.29 +(* "[| G<=H;  G |- p |] ==> H |- p"
   17.30 +   This order of premises is convenient with RS
   17.31 +*)
   17.32 +bind_thm ("weaken_left", (thms_mono RS subsetD));
   17.33 +
   17.34 +(* H |- p ==> insert(a,H) |- p *)
   17.35 +val weaken_left_insert = subset_insertI RS weaken_left;
   17.36 +
   17.37 +val weaken_left_Un1  =    Un_upper1 RS weaken_left;
   17.38 +val weaken_left_Un2  =    Un_upper2 RS weaken_left;
   17.39 +
   17.40 +goal PropLog.thy "!!H. H |- q ==> H |- p->q";
   17.41 +by (fast_tac (!claset addIs [thms.K,thms.MP]) 1);
   17.42 +qed "weaken_right";
   17.43 +
   17.44 +(*The deduction theorem*)
   17.45 +goal PropLog.thy "!!H. insert p H |- q  ==>  H |- p->q";
   17.46 +by (etac thms.induct 1);
   17.47 +by (ALLGOALS 
   17.48 +    (fast_tac (!claset addIs [thms_I, thms.H, thms.K, thms.S, thms.DN, 
   17.49 +                             thms.S RS thms.MP RS thms.MP, weaken_right])));
   17.50 +qed "deduction";
   17.51 +
   17.52 +
   17.53 +(* "[| insert p H |- q; H |- p |] ==> H |- q"
   17.54 +    The cut rule - not used
   17.55 +*)
   17.56 +val cut = deduction RS thms.MP;
   17.57 +
   17.58 +(* H |- false ==> H |- p *)
   17.59 +val thms_falseE = weaken_right RS (thms.DN RS thms.MP);
   17.60 +
   17.61 +(* [| H |- p->false;  H |- p;  q: pl |] ==> H |- q *)
   17.62 +bind_thm ("thms_notE", (thms.MP RS thms_falseE));
   17.63 +
   17.64 +(** The function eval **)
   17.65 +
   17.66 +goalw PropLog.thy [eval_def] "tt[false] = False";
   17.67 +by (Simp_tac 1);
   17.68 +qed "eval_false";
   17.69 +
   17.70 +goalw PropLog.thy [eval_def] "tt[#v] = (v:tt)";
   17.71 +by (Simp_tac 1);
   17.72 +qed "eval_var";
   17.73 +
   17.74 +goalw PropLog.thy [eval_def] "tt[p->q] = (tt[p]-->tt[q])";
   17.75 +by (Simp_tac 1);
   17.76 +qed "eval_imp";
   17.77 +
   17.78 +Addsimps [eval_false, eval_var, eval_imp];
   17.79 +
   17.80 +(*Soundness of the rules wrt truth-table semantics*)
   17.81 +goalw PropLog.thy [sat_def] "!!H. H |- p ==> H |= p";
   17.82 +by (etac thms.induct 1);
   17.83 +by (fast_tac (!claset addSDs [eval_imp RS iffD1 RS mp]) 5);
   17.84 +by (ALLGOALS Asm_simp_tac);
   17.85 +qed "soundness";
   17.86 +
   17.87 +(*** Towards the completeness proof ***)
   17.88 +
   17.89 +goal PropLog.thy "!!H. H |- p->false ==> H |- p->q";
   17.90 +by (rtac deduction 1);
   17.91 +by (etac (weaken_left_insert RS thms_notE) 1);
   17.92 +by (rtac thms.H 1);
   17.93 +by (rtac insertI1 1);
   17.94 +qed "false_imp";
   17.95 +
   17.96 +val [premp,premq] = goal PropLog.thy
   17.97 +    "[| H |- p;  H |- q->false |] ==> H |- (p->q)->false";
   17.98 +by (rtac deduction 1);
   17.99 +by (rtac (premq RS weaken_left_insert RS thms.MP) 1);
  17.100 +by (rtac (thms.H RS thms.MP) 1);
  17.101 +by (rtac insertI1 1);
  17.102 +by (rtac (premp RS weaken_left_insert) 1);
  17.103 +qed "imp_false";
  17.104 +
  17.105 +(*This formulation is required for strong induction hypotheses*)
  17.106 +goal PropLog.thy "hyps p tt |- (if tt[p] then p else p->false)";
  17.107 +by (rtac (expand_if RS iffD2) 1);
  17.108 +by (PropLog.pl.induct_tac "p" 1);
  17.109 +by (ALLGOALS (simp_tac (!simpset addsimps [thms_I, thms.H])));
  17.110 +by (fast_tac (!claset addIs [weaken_left_Un1, weaken_left_Un2, 
  17.111 +                           weaken_right, imp_false]
  17.112 +                    addSEs [false_imp]) 1);
  17.113 +qed "hyps_thms_if";
  17.114 +
  17.115 +(*Key lemma for completeness; yields a set of assumptions satisfying p*)
  17.116 +val [sat] = goalw PropLog.thy [sat_def] "{} |= p ==> hyps p tt |- p";
  17.117 +by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
  17.118 +    rtac hyps_thms_if 2);
  17.119 +by (Fast_tac 1);
  17.120 +qed "sat_thms_p";
  17.121 +
  17.122 +(*For proving certain theorems in our new propositional logic*)
  17.123 +
  17.124 +AddSIs [deduction];
  17.125 +AddIs [thms.H, thms.H RS thms.MP];
  17.126 +
  17.127 +(*The excluded middle in the form of an elimination rule*)
  17.128 +goal PropLog.thy "H |- (p->q) -> ((p->false)->q) -> q";
  17.129 +by (rtac (deduction RS deduction) 1);
  17.130 +by (rtac (thms.DN RS thms.MP) 1);
  17.131 +by (ALLGOALS (best_tac (!claset addSIs prems)));
  17.132 +qed "thms_excluded_middle";
  17.133 +
  17.134 +(*Hard to prove directly because it requires cuts*)
  17.135 +val prems = goal PropLog.thy
  17.136 +    "[| insert p H |- q;  insert (p->false) H |- q |] ==> H |- q";
  17.137 +by (rtac (thms_excluded_middle RS thms.MP RS thms.MP) 1);
  17.138 +by (REPEAT (resolve_tac (prems@[deduction]) 1));
  17.139 +qed "thms_excluded_middle_rule";
  17.140 +
  17.141 +(*** Completeness -- lemmas for reducing the set of assumptions ***)
  17.142 +
  17.143 +(*For the case hyps(p,t)-insert(#v,Y) |- p;
  17.144 +  we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
  17.145 +goal PropLog.thy "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
  17.146 +by (PropLog.pl.induct_tac "p" 1);
  17.147 +by (Simp_tac 1);
  17.148 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  17.149 +by (Simp_tac 1);
  17.150 +by (Fast_tac 1);
  17.151 +qed "hyps_Diff";
  17.152 +
  17.153 +(*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
  17.154 +  we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
  17.155 +goal PropLog.thy "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
  17.156 +by (PropLog.pl.induct_tac "p" 1);
  17.157 +by (Simp_tac 1);
  17.158 +by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
  17.159 +by (Simp_tac 1);
  17.160 +by (Fast_tac 1);
  17.161 +qed "hyps_insert";
  17.162 +
  17.163 +(** Two lemmas for use with weaken_left **)
  17.164 +
  17.165 +goal Set.thy "B-C <= insert a (B-insert a C)";
  17.166 +by (Fast_tac 1);
  17.167 +qed "insert_Diff_same";
  17.168 +
  17.169 +goal Set.thy "insert a (B-{c}) - D <= insert a (B-insert c D)";
  17.170 +by (Fast_tac 1);
  17.171 +qed "insert_Diff_subset2";
  17.172 +
  17.173 +(*The set hyps(p,t) is finite, and elements have the form #v or #v->false;
  17.174 + could probably prove the stronger hyps(p,t) : Fin(hyps(p,{}) Un hyps(p,nat))*)
  17.175 +goal PropLog.thy "hyps p t : Fin(UN v:{x.True}. {#v, #v->false})";
  17.176 +by (PropLog.pl.induct_tac "p" 1);
  17.177 +by (ALLGOALS (simp_tac (!simpset setloop (split_tac [expand_if]))));
  17.178 +by (ALLGOALS (fast_tac (!claset addSIs Fin.intrs@[Fin_UnI])));
  17.179 +qed "hyps_finite";
  17.180 +
  17.181 +val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
  17.182 +
  17.183 +(*Induction on the finite set of assumptions hyps(p,t0).
  17.184 +  We may repeatedly subtract assumptions until none are left!*)
  17.185 +val [sat] = goal PropLog.thy
  17.186 +    "{} |= p ==> !t. hyps p t - hyps p t0 |- p";
  17.187 +by (rtac (hyps_finite RS Fin_induct) 1);
  17.188 +by (simp_tac (!simpset addsimps [sat RS sat_thms_p]) 1);
  17.189 +by (safe_tac (!claset));
  17.190 +(*Case hyps(p,t)-insert(#v,Y) |- p *)
  17.191 +by (rtac thms_excluded_middle_rule 1);
  17.192 +by (rtac (insert_Diff_same RS weaken_left) 1);
  17.193 +by (etac spec 1);
  17.194 +by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  17.195 +by (rtac (hyps_Diff RS Diff_weaken_left) 1);
  17.196 +by (etac spec 1);
  17.197 +(*Case hyps(p,t)-insert(#v -> false,Y) |- p *)
  17.198 +by (rtac thms_excluded_middle_rule 1);
  17.199 +by (rtac (insert_Diff_same RS weaken_left) 2);
  17.200 +by (etac spec 2);
  17.201 +by (rtac (insert_Diff_subset2 RS weaken_left) 1);
  17.202 +by (rtac (hyps_insert RS Diff_weaken_left) 1);
  17.203 +by (etac spec 1);
  17.204 +qed "completeness_0_lemma";
  17.205 +
  17.206 +(*The base case for completeness*)
  17.207 +val [sat] = goal PropLog.thy "{} |= p ==> {} |- p";
  17.208 +by (rtac (Diff_cancel RS subst) 1);
  17.209 +by (rtac (sat RS (completeness_0_lemma RS spec)) 1);
  17.210 +qed "completeness_0";
  17.211 +
  17.212 +(*A semantic analogue of the Deduction Theorem*)
  17.213 +goalw PropLog.thy [sat_def] "!!p H. insert p H |= q ==> H |= p->q";
  17.214 +by (Simp_tac 1);
  17.215 +by (Fast_tac 1);
  17.216 +qed "sat_imp";
  17.217 +
  17.218 +val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> !p. H |= p --> H |- p";
  17.219 +by (rtac (finite RS Fin_induct) 1);
  17.220 +by (safe_tac ((claset_of "Fun") addSIs [completeness_0]));
  17.221 +by (rtac (weaken_left_insert RS thms.MP) 1);
  17.222 +by (fast_tac ((claset_of "Fun") addSIs [sat_imp]) 1);
  17.223 +by (Fast_tac 1);
  17.224 +qed "completeness_lemma";
  17.225 +
  17.226 +val completeness = completeness_lemma RS spec RS mp;
  17.227 +
  17.228 +val [finite] = goal PropLog.thy "H: Fin({p.True}) ==> (H |- p) = (H |= p)";
  17.229 +by (fast_tac (!claset addSEs [soundness, finite RS completeness]) 1);
  17.230 +qed "thms_iff";
  17.231 +
  17.232 +writeln"Reached end of file.";
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/src/HOL/Induct/PropLog.thy	Wed May 07 12:50:26 1997 +0200
    18.3 @@ -0,0 +1,46 @@
    18.4 +(*  Title:      HOL/ex/PropLog.thy
    18.5 +    ID:         $Id$
    18.6 +    Author:     Tobias Nipkow
    18.7 +    Copyright   1994  TU Muenchen
    18.8 +
    18.9 +Inductive definition of propositional logic.
   18.10 +*)
   18.11 +
   18.12 +PropLog = Finite +
   18.13 +datatype
   18.14 +    'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
   18.15 +consts
   18.16 +  thms :: 'a pl set => 'a pl set
   18.17 +  "|-"  :: ['a pl set, 'a pl] => bool   (infixl 50)
   18.18 +  "|="  :: ['a pl set, 'a pl] => bool   (infixl 50)
   18.19 +  eval2 :: ['a pl, 'a set] => bool
   18.20 +  eval  :: ['a set, 'a pl] => bool      ("_[_]" [100,0] 100)
   18.21 +  hyps  :: ['a pl, 'a set] => 'a pl set
   18.22 +
   18.23 +translations
   18.24 +  "H |- p" == "p : thms(H)"
   18.25 +
   18.26 +inductive "thms(H)"
   18.27 +  intrs
   18.28 +  H   "p:H ==> H |- p"
   18.29 +  K   "H |- p->q->p"
   18.30 +  S   "H |- (p->q->r) -> (p->q) -> p->r"
   18.31 +  DN  "H |- ((p->false) -> false) -> p"
   18.32 +  MP  "[| H |- p->q; H |- p |] ==> H |- q"
   18.33 +
   18.34 +defs
   18.35 +  sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
   18.36 +  eval_def "tt[p] == eval2 p tt"
   18.37 +
   18.38 +primrec eval2 pl
   18.39 +  "eval2(false) = (%x.False)"
   18.40 +  "eval2(#v) = (%tt.v:tt)"
   18.41 +  "eval2(p->q) = (%tt.eval2 p tt-->eval2 q tt)"
   18.42 +
   18.43 +primrec hyps pl
   18.44 +  "hyps(false) = (%tt.{})"
   18.45 +  "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
   18.46 +  "hyps(p->q) = (%tt.hyps p tt Un hyps q tt)"
   18.47 +
   18.48 +end
   18.49 +
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/Induct/ROOT.ML	Wed May 07 12:50:26 1997 +0200
    19.3 @@ -0,0 +1,22 @@
    19.4 +(*  Title:      HOL/Induct/ROOT
    19.5 +    ID:         $Id$
    19.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    19.7 +    Copyright   1997  University of Cambridge
    19.8 +
    19.9 +Exampled of Inductive Definitions
   19.10 +*)
   19.11 +
   19.12 +HOL_build_completed;    (*Make examples fail if HOL did*)
   19.13 +
   19.14 +writeln"Root file for HOL/Induct";
   19.15 +proof_timing := true;
   19.16 +time_use_thy "Perm";
   19.17 +time_use_thy "Comb";
   19.18 +time_use_thy "Mutil";
   19.19 +time_use_thy "Acc";
   19.20 +time_use_thy "PropLog";
   19.21 +time_use_thy "SList";
   19.22 +time_use_thy "LFilter";
   19.23 +time_use_thy "Term";
   19.24 +time_use_thy "Simult";
   19.25 +time_use_thy "Exp";
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/HOL/Induct/SList.ML	Wed May 07 12:50:26 1997 +0200
    20.3 @@ -0,0 +1,372 @@
    20.4 +(*  Title:      HOL/ex/SList.ML
    20.5 +    ID:         $Id$
    20.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    20.7 +    Copyright   1993  University of Cambridge
    20.8 +
    20.9 +Definition of type 'a list by a least fixed point
   20.10 +*)
   20.11 +
   20.12 +open SList;
   20.13 +
   20.14 +val list_con_defs = [NIL_def, CONS_def];
   20.15 +
   20.16 +goal SList.thy "list(A) = {Numb(0)} <+> (A <*> list(A))";
   20.17 +let val rew = rewrite_rule list_con_defs in  
   20.18 +by (fast_tac (!claset addSIs (equalityI :: map rew list.intrs)
   20.19 +                      addEs [rew list.elim]) 1)
   20.20 +end;
   20.21 +qed "list_unfold";
   20.22 +
   20.23 +(*This justifies using list in other recursive type definitions*)
   20.24 +goalw SList.thy list.defs "!!A B. A<=B ==> list(A) <= list(B)";
   20.25 +by (rtac lfp_mono 1);
   20.26 +by (REPEAT (ares_tac basic_monos 1));
   20.27 +qed "list_mono";
   20.28 +
   20.29 +(*Type checking -- list creates well-founded sets*)
   20.30 +goalw SList.thy (list_con_defs @ list.defs) "list(sexp) <= sexp";
   20.31 +by (rtac lfp_lowerbound 1);
   20.32 +by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
   20.33 +qed "list_sexp";
   20.34 +
   20.35 +(* A <= sexp ==> list(A) <= sexp *)
   20.36 +bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
   20.37 +
   20.38 +(*Induction for the type 'a list *)
   20.39 +val prems = goalw SList.thy [Nil_def,Cons_def]
   20.40 +    "[| P(Nil);   \
   20.41 +\       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
   20.42 +by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
   20.43 +by (rtac (Rep_list RS list.induct) 1);
   20.44 +by (REPEAT (ares_tac prems 1
   20.45 +     ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
   20.46 +qed "list_induct2";
   20.47 +
   20.48 +(*Perform induction on xs. *)
   20.49 +fun list_ind_tac a M = 
   20.50 +    EVERY [res_inst_tac [("l",a)] list_induct2 M,
   20.51 +           rename_last_tac a ["1"] (M+1)];
   20.52 +
   20.53 +(*** Isomorphisms ***)
   20.54 +
   20.55 +goal SList.thy "inj(Rep_list)";
   20.56 +by (rtac inj_inverseI 1);
   20.57 +by (rtac Rep_list_inverse 1);
   20.58 +qed "inj_Rep_list";
   20.59 +
   20.60 +goal SList.thy "inj_onto Abs_list (list(range Leaf))";
   20.61 +by (rtac inj_onto_inverseI 1);
   20.62 +by (etac Abs_list_inverse 1);
   20.63 +qed "inj_onto_Abs_list";
   20.64 +
   20.65 +(** Distinctness of constructors **)
   20.66 +
   20.67 +goalw SList.thy list_con_defs "CONS M N ~= NIL";
   20.68 +by (rtac In1_not_In0 1);
   20.69 +qed "CONS_not_NIL";
   20.70 +bind_thm ("NIL_not_CONS", (CONS_not_NIL RS not_sym));
   20.71 +
   20.72 +bind_thm ("CONS_neq_NIL", (CONS_not_NIL RS notE));
   20.73 +val NIL_neq_CONS = sym RS CONS_neq_NIL;
   20.74 +
   20.75 +goalw SList.thy [Nil_def,Cons_def] "x # xs ~= Nil";
   20.76 +by (rtac (CONS_not_NIL RS (inj_onto_Abs_list RS inj_onto_contraD)) 1);
   20.77 +by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
   20.78 +qed "Cons_not_Nil";
   20.79 +
   20.80 +bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
   20.81 +
   20.82 +(** Injectiveness of CONS and Cons **)
   20.83 +
   20.84 +goalw SList.thy [CONS_def] "(CONS K M=CONS L N) = (K=L & M=N)";
   20.85 +by (fast_tac (!claset addSEs [Scons_inject, make_elim In1_inject]) 1);
   20.86 +qed "CONS_CONS_eq";
   20.87 +
   20.88 +(*For reasoning about abstract list constructors*)
   20.89 +AddIs ([Rep_list] @ list.intrs);
   20.90 +
   20.91 +AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
   20.92 +
   20.93 +AddSDs [inj_onto_Abs_list RS inj_ontoD,
   20.94 +        inj_Rep_list RS injD, Leaf_inject];
   20.95 +
   20.96 +goalw SList.thy [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
   20.97 +by (Fast_tac 1);
   20.98 +qed "Cons_Cons_eq";
   20.99 +bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
  20.100 +
  20.101 +val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
  20.102 +by (rtac (major RS setup_induction) 1);
  20.103 +by (etac list.induct 1);
  20.104 +by (ALLGOALS (Fast_tac));
  20.105 +qed "CONS_D";
  20.106 +
  20.107 +val prems = goalw SList.thy [CONS_def,In1_def]
  20.108 +    "CONS M N: sexp ==> M: sexp & N: sexp";
  20.109 +by (cut_facts_tac prems 1);
  20.110 +by (fast_tac (!claset addSDs [Scons_D]) 1);
  20.111 +qed "sexp_CONS_D";
  20.112 +
  20.113 +
  20.114 +(*Reasoning about constructors and their freeness*)
  20.115 +Addsimps list.intrs;
  20.116 +
  20.117 +AddIffs [Cons_not_Nil, Nil_not_Cons, Cons_Cons_eq];
  20.118 +
  20.119 +goal SList.thy "!!N. N: list(A) ==> !M. N ~= CONS M N";
  20.120 +by (etac list.induct 1);
  20.121 +by (ALLGOALS Asm_simp_tac);
  20.122 +qed "not_CONS_self";
  20.123 +
  20.124 +goal SList.thy "!x. l ~= x#l";
  20.125 +by (list_ind_tac "l" 1);
  20.126 +by (ALLGOALS Asm_simp_tac);
  20.127 +qed "not_Cons_self2";
  20.128 +
  20.129 +
  20.130 +goal SList.thy "(xs ~= []) = (? y ys. xs = y#ys)";
  20.131 +by (list_ind_tac "xs" 1);
  20.132 +by (Simp_tac 1);
  20.133 +by (Asm_simp_tac 1);
  20.134 +by (REPEAT(resolve_tac [exI,refl,conjI] 1));
  20.135 +qed "neq_Nil_conv2";
  20.136 +
  20.137 +(** Conversion rules for List_case: case analysis operator **)
  20.138 +
  20.139 +goalw SList.thy [List_case_def,NIL_def] "List_case c h NIL = c";
  20.140 +by (rtac Case_In0 1);
  20.141 +qed "List_case_NIL";
  20.142 +
  20.143 +goalw SList.thy [List_case_def,CONS_def]  "List_case c h (CONS M N) = h M N";
  20.144 +by (simp_tac (!simpset addsimps [Split,Case_In1]) 1);
  20.145 +qed "List_case_CONS";
  20.146 +
  20.147 +(*** List_rec -- by wf recursion on pred_sexp ***)
  20.148 +
  20.149 +(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
  20.150 +   hold if pred_sexp^+ were changed to pred_sexp. *)
  20.151 +
  20.152 +goal SList.thy
  20.153 +   "(%M. List_rec M c d) = wfrec (trancl pred_sexp) \
  20.154 +                           \     (%g. List_case c (%x y. d x y (g y)))";
  20.155 +by (simp_tac (HOL_ss addsimps [List_rec_def]) 1);
  20.156 +val List_rec_unfold = standard 
  20.157 +  ((wf_pred_sexp RS wf_trancl) RS ((result() RS eq_reflection) RS def_wfrec));
  20.158 +
  20.159 +(*---------------------------------------------------------------------------
  20.160 + * Old:
  20.161 + * val List_rec_unfold = [List_rec_def,wf_pred_sexp RS wf_trancl] MRS def_wfrec
  20.162 + *                     |> standard;
  20.163 + *---------------------------------------------------------------------------*)
  20.164 +
  20.165 +(** pred_sexp lemmas **)
  20.166 +
  20.167 +goalw SList.thy [CONS_def,In1_def]
  20.168 +    "!!M. [| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+";
  20.169 +by (Asm_simp_tac 1);
  20.170 +qed "pred_sexp_CONS_I1";
  20.171 +
  20.172 +goalw SList.thy [CONS_def,In1_def]
  20.173 +    "!!M. [| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+";
  20.174 +by (Asm_simp_tac 1);
  20.175 +qed "pred_sexp_CONS_I2";
  20.176 +
  20.177 +val [prem] = goal SList.thy
  20.178 +    "(CONS M1 M2, N) : pred_sexp^+ ==> \
  20.179 +\    (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+";
  20.180 +by (rtac (prem RS (pred_sexp_subset_Sigma RS trancl_subset_Sigma RS 
  20.181 +                   subsetD RS SigmaE2)) 1);
  20.182 +by (etac (sexp_CONS_D RS conjE) 1);
  20.183 +by (REPEAT (ares_tac [conjI, pred_sexp_CONS_I1, pred_sexp_CONS_I2,
  20.184 +                      prem RSN (2, trans_trancl RS transD)] 1));
  20.185 +qed "pred_sexp_CONS_D";
  20.186 +
  20.187 +(** Conversion rules for List_rec **)
  20.188 +
  20.189 +goal SList.thy "List_rec NIL c h = c";
  20.190 +by (rtac (List_rec_unfold RS trans) 1);
  20.191 +by (simp_tac (!simpset addsimps [List_case_NIL]) 1);
  20.192 +qed "List_rec_NIL";
  20.193 +
  20.194 +goal SList.thy "!!M. [| M: sexp;  N: sexp |] ==> \
  20.195 +\    List_rec (CONS M N) c h = h M N (List_rec N c h)";
  20.196 +by (rtac (List_rec_unfold RS trans) 1);
  20.197 +by (asm_simp_tac (!simpset addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
  20.198 +qed "List_rec_CONS";
  20.199 +
  20.200 +(*** list_rec -- by List_rec ***)
  20.201 +
  20.202 +val Rep_list_in_sexp =
  20.203 +    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
  20.204 +
  20.205 +local
  20.206 +  val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
  20.207 +                        Abs_list_inverse, Rep_list_inverse,
  20.208 +                        Rep_list, rangeI, inj_Leaf, inv_f_f,
  20.209 +                        sexp.LeafI, Rep_list_in_sexp]
  20.210 +in
  20.211 +  val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
  20.212 +      "list_rec Nil c h = c"
  20.213 +   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
  20.214 +
  20.215 +  val list_rec_Cons = prove_goalw SList.thy [list_rec_def, Cons_def]
  20.216 +      "list_rec (a#l) c h = h a l (list_rec l c h)"
  20.217 +   (fn _=> [simp_tac (!simpset addsimps list_rec_simps) 1]);
  20.218 +end;
  20.219 +
  20.220 +Addsimps [List_rec_NIL, List_rec_CONS, list_rec_Nil, list_rec_Cons];
  20.221 +
  20.222 +
  20.223 +(*Type checking.  Useful?*)
  20.224 +val major::A_subset_sexp::prems = goal SList.thy
  20.225 +    "[| M: list(A);     \
  20.226 +\       A<=sexp;        \
  20.227 +\       c: C(NIL);      \
  20.228 +\       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
  20.229 +\    |] ==> List_rec M c h : C(M :: 'a item)";
  20.230 +val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
  20.231 +val sexp_A_I = A_subset_sexp RS subsetD;
  20.232 +by (rtac (major RS list.induct) 1);
  20.233 +by (ALLGOALS(asm_simp_tac (!simpset addsimps ([sexp_A_I,sexp_ListA_I]@prems))));
  20.234 +qed "List_rec_type";
  20.235 +
  20.236 +(** Generalized map functionals **)
  20.237 +
  20.238 +goalw SList.thy [Rep_map_def] "Rep_map f Nil = NIL";
  20.239 +by (rtac list_rec_Nil 1);
  20.240 +qed "Rep_map_Nil";
  20.241 +
  20.242 +goalw SList.thy [Rep_map_def]
  20.243 +    "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
  20.244 +by (rtac list_rec_Cons 1);
  20.245 +qed "Rep_map_Cons";
  20.246 +
  20.247 +goalw SList.thy [Rep_map_def] "!!f. (!!x. f(x): A) ==> Rep_map f xs: list(A)";
  20.248 +by (rtac list_induct2 1);
  20.249 +by (ALLGOALS Asm_simp_tac);
  20.250 +qed "Rep_map_type";
  20.251 +
  20.252 +goalw SList.thy [Abs_map_def] "Abs_map g NIL = Nil";
  20.253 +by (rtac List_rec_NIL 1);
  20.254 +qed "Abs_map_NIL";
  20.255 +
  20.256 +val prems = goalw SList.thy [Abs_map_def]
  20.257 +    "[| M: sexp;  N: sexp |] ==> \
  20.258 +\    Abs_map g (CONS M N) = g(M) # Abs_map g N";
  20.259 +by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
  20.260 +qed "Abs_map_CONS";
  20.261 +
  20.262 +(*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
  20.263 +val [rew] = goal SList.thy
  20.264 +    "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
  20.265 +by (rewtac rew);
  20.266 +by (rtac list_rec_Nil 1);
  20.267 +qed "def_list_rec_Nil";
  20.268 +
  20.269 +val [rew] = goal SList.thy
  20.270 +    "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
  20.271 +by (rewtac rew);
  20.272 +by (rtac list_rec_Cons 1);
  20.273 +qed "def_list_rec_Cons";
  20.274 +
  20.275 +fun list_recs def =
  20.276 +      [standard (def RS def_list_rec_Nil),
  20.277 +       standard (def RS def_list_rec_Cons)];
  20.278 +
  20.279 +(*** Unfolding the basic combinators ***)
  20.280 +
  20.281 +val [null_Nil, null_Cons]               = list_recs null_def;
  20.282 +val [_, hd_Cons]                        = list_recs hd_def;
  20.283 +val [_, tl_Cons]                        = list_recs tl_def;
  20.284 +val [ttl_Nil, ttl_Cons]                 = list_recs ttl_def;
  20.285 +val [append_Nil3, append_Cons]          = list_recs append_def;
  20.286 +val [mem_Nil, mem_Cons]                 = list_recs mem_def;
  20.287 +val [set_of_list_Nil, set_of_list_Cons] = list_recs set_of_list_def;
  20.288 +val [map_Nil, map_Cons]                 = list_recs map_def;
  20.289 +val [list_case_Nil, list_case_Cons]     = list_recs list_case_def;
  20.290 +val [filter_Nil, filter_Cons]           = list_recs filter_def;
  20.291 +
  20.292 +Addsimps
  20.293 +  [null_Nil, ttl_Nil,
  20.294 +   mem_Nil, mem_Cons,
  20.295 +   list_case_Nil, list_case_Cons,
  20.296 +   append_Nil3, append_Cons,
  20.297 +   set_of_list_Nil, set_of_list_Cons, 
  20.298 +   map_Nil, map_Cons,
  20.299 +   filter_Nil, filter_Cons];
  20.300 +
  20.301 +
  20.302 +(** @ - append **)
  20.303 +
  20.304 +goal SList.thy "(xs@ys)@zs = xs@(ys@zs)";
  20.305 +by (list_ind_tac "xs" 1);
  20.306 +by (ALLGOALS Asm_simp_tac);
  20.307 +qed "append_assoc2";
  20.308 +
  20.309 +goal SList.thy "xs @ [] = xs";
  20.310 +by (list_ind_tac "xs" 1);
  20.311 +by (ALLGOALS Asm_simp_tac);
  20.312 +qed "append_Nil4";
  20.313 +
  20.314 +(** mem **)
  20.315 +
  20.316 +goal SList.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
  20.317 +by (list_ind_tac "xs" 1);
  20.318 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
  20.319 +qed "mem_append2";
  20.320 +
  20.321 +goal SList.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
  20.322 +by (list_ind_tac "xs" 1);
  20.323 +by (ALLGOALS(asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
  20.324 +qed "mem_filter2";
  20.325 +
  20.326 +
  20.327 +(** The functional "map" **)
  20.328 +
  20.329 +Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
  20.330 +
  20.331 +val [major,A_subset_sexp,minor] = goal SList.thy 
  20.332 +    "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
  20.333 +\    ==> Rep_map f (Abs_map g M) = M";
  20.334 +by (rtac (major RS list.induct) 1);
  20.335 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [sexp_A_I,sexp_ListA_I,minor])));
  20.336 +qed "Abs_map_inverse";
  20.337 +
  20.338 +(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
  20.339 +
  20.340 +(** list_case **)
  20.341 +
  20.342 +goal SList.thy
  20.343 + "P(list_case a f xs) = ((xs=[] --> P(a)) & \
  20.344 +\                        (!y ys. xs=y#ys --> P(f y ys)))";
  20.345 +by (list_ind_tac "xs" 1);
  20.346 +by (ALLGOALS Asm_simp_tac);
  20.347 +by (Fast_tac 1);
  20.348 +qed "expand_list_case2";
  20.349 +
  20.350 +
  20.351 +(** Additional mapping lemmas **)
  20.352 +
  20.353 +goal SList.thy "map (%x.x) xs = xs";
  20.354 +by (list_ind_tac "xs" 1);
  20.355 +by (ALLGOALS Asm_simp_tac);
  20.356 +qed "map_ident2";
  20.357 +
  20.358 +goal SList.thy "map f (xs@ys) = map f xs @ map f ys";
  20.359 +by (list_ind_tac "xs" 1);
  20.360 +by (ALLGOALS Asm_simp_tac);
  20.361 +qed "map_append2";
  20.362 +
  20.363 +goalw SList.thy [o_def] "map (f o g) xs = map f (map g xs)";
  20.364 +by (list_ind_tac "xs" 1);
  20.365 +by (ALLGOALS Asm_simp_tac);
  20.366 +qed "map_compose2";
  20.367 +
  20.368 +goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
  20.369 +\       Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
  20.370 +by (list_ind_tac "xs" 1);
  20.371 +by (ALLGOALS(asm_simp_tac(!simpset addsimps
  20.372 +       [Rep_map_type,list_sexp RS subsetD])));
  20.373 +qed "Abs_Rep_map";
  20.374 +
  20.375 +Addsimps [append_Nil4, map_ident2];
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/src/HOL/Induct/SList.thy	Wed May 07 12:50:26 1997 +0200
    21.3 @@ -0,0 +1,119 @@
    21.4 +(*  Title:      HOL/ex/SList.thy
    21.5 +    ID:         $Id$
    21.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    21.7 +    Copyright   1993  University of Cambridge
    21.8 +
    21.9 +Definition of type 'a list (strict lists) by a least fixed point
   21.10 +
   21.11 +We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
   21.12 +and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)
   21.13 +so that list can serve as a "functor" for defining other recursive types
   21.14 +*)
   21.15 +
   21.16 +SList = Sexp +
   21.17 +
   21.18 +types
   21.19 +  'a list
   21.20 +
   21.21 +arities
   21.22 +  list :: (term) term
   21.23 +
   21.24 +
   21.25 +consts
   21.26 +
   21.27 +  list        :: 'a item set => 'a item set
   21.28 +  Rep_list    :: 'a list => 'a item
   21.29 +  Abs_list    :: 'a item => 'a list
   21.30 +  NIL         :: 'a item
   21.31 +  CONS        :: ['a item, 'a item] => 'a item
   21.32 +  Nil         :: 'a list
   21.33 +  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
   21.34 +  List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
   21.35 +  List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
   21.36 +  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
   21.37 +  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
   21.38 +  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
   21.39 +  Abs_map     :: ('a item => 'b) => 'a item => 'b list
   21.40 +  null        :: 'a list => bool
   21.41 +  hd          :: 'a list => 'a
   21.42 +  tl,ttl      :: 'a list => 'a list
   21.43 +  set_of_list :: ('a list => 'a set)
   21.44 +  mem         :: ['a, 'a list] => bool                            (infixl 55)
   21.45 +  map         :: ('a=>'b) => ('a list => 'b list)
   21.46 +  "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
   21.47 +  filter      :: ['a => bool, 'a list] => 'a list
   21.48 +
   21.49 +  (* list Enumeration *)
   21.50 +
   21.51 +  "[]"        :: 'a list                              ("[]")
   21.52 +  "@list"     :: args => 'a list                      ("[(_)]")
   21.53 +
   21.54 +  (* Special syntax for filter *)
   21.55 +  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
   21.56 +
   21.57 +translations
   21.58 +  "[x, xs]"     == "x#[xs]"
   21.59 +  "[x]"         == "x#[]"
   21.60 +  "[]"          == "Nil"
   21.61 +
   21.62 +  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys.b) xs"
   21.63 +
   21.64 +  "[x:xs . P]"  == "filter (%x.P) xs"
   21.65 +
   21.66 +defs
   21.67 +  (* Defining the Concrete Constructors *)
   21.68 +  NIL_def       "NIL == In0(Numb(0))"
   21.69 +  CONS_def      "CONS M N == In1(M $ N)"
   21.70 +
   21.71 +inductive "list(A)"
   21.72 +  intrs
   21.73 +    NIL_I  "NIL: list(A)"
   21.74 +    CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
   21.75 +
   21.76 +rules
   21.77 +  (* Faking a Type Definition ... *)
   21.78 +  Rep_list          "Rep_list(xs): list(range(Leaf))"
   21.79 +  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
   21.80 +  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
   21.81 +
   21.82 +
   21.83 +defs
   21.84 +  (* Defining the Abstract Constructors *)
   21.85 +  Nil_def       "Nil == Abs_list(NIL)"
   21.86 +  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
   21.87 +
   21.88 +  List_case_def "List_case c d == Case (%x.c) (Split d)"
   21.89 +
   21.90 +  (* list Recursion -- the trancl is Essential; see list.ML *)
   21.91 +
   21.92 +  List_rec_def
   21.93 +   "List_rec M c d == wfrec (trancl pred_sexp)
   21.94 +                            (%g. List_case c (%x y. d x y (g y))) M"
   21.95 +
   21.96 +  list_rec_def
   21.97 +   "list_rec l c d == 
   21.98 +   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
   21.99 +
  21.100 +  (* Generalized Map Functionals *)
  21.101 +
  21.102 +  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
  21.103 +  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
  21.104 +
  21.105 +  null_def      "null(xs)            == list_rec xs True (%x xs r.False)"
  21.106 +  hd_def        "hd(xs)              == list_rec xs (@x.True) (%x xs r.x)"
  21.107 +  tl_def        "tl(xs)              == list_rec xs (@xs.True) (%x xs r.xs)"
  21.108 +  (* a total version of tl: *)
  21.109 +  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r.xs)"
  21.110 +
  21.111 +  set_of_list_def "set_of_list xs    == list_rec xs {} (%x l r. insert x r)"
  21.112 +
  21.113 +  mem_def       "x mem xs            == 
  21.114 +                   list_rec xs False (%y ys r. if y=x then True else r)"
  21.115 +  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
  21.116 +  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
  21.117 +  filter_def    "filter P xs         == 
  21.118 +                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
  21.119 +
  21.120 +  list_case_def  "list_case a f xs == list_rec xs a (%x xs r.f x xs)"
  21.121 +
  21.122 +end
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/src/HOL/Induct/Simult.ML	Wed May 07 12:50:26 1997 +0200
    22.3 @@ -0,0 +1,298 @@
    22.4 +(*  Title:      HOL/ex/Simult.ML
    22.5 +    ID:         $Id$
    22.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    22.7 +    Copyright   1993  University of Cambridge
    22.8 +
    22.9 +Primitives for simultaneous recursive type definitions
   22.10 +  includes worked example of trees & forests
   22.11 +
   22.12 +This is essentially the same data structure that on ex/term.ML, which is
   22.13 +simpler because it uses list as a new type former.  The approach in this
   22.14 +file may be superior for other simultaneous recursions.
   22.15 +*)
   22.16 +
   22.17 +open Simult;
   22.18 +
   22.19 +(*** Monotonicity and unfolding of the function ***)
   22.20 +
   22.21 +goal Simult.thy "mono(%Z.  A <*> Part Z In1 \
   22.22 +\                      <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))";
   22.23 +by (REPEAT (ares_tac [monoI, subset_refl, usum_mono, uprod_mono,
   22.24 +                      Part_mono] 1));
   22.25 +qed "TF_fun_mono";
   22.26 +
   22.27 +val TF_unfold = TF_fun_mono RS (TF_def RS def_lfp_Tarski);
   22.28 +
   22.29 +goalw Simult.thy [TF_def] "!!A B. A<=B ==> TF(A) <= TF(B)";
   22.30 +by (REPEAT (ares_tac [lfp_mono, subset_refl, usum_mono, uprod_mono] 1));
   22.31 +qed "TF_mono";
   22.32 +
   22.33 +goalw Simult.thy [TF_def] "TF(sexp) <= sexp";
   22.34 +by (rtac lfp_lowerbound 1);
   22.35 +by (blast_tac (!claset addIs  sexp.intrs@[sexp_In0I, sexp_In1I]
   22.36 +                      addSEs [PartE]) 1);
   22.37 +qed "TF_sexp";
   22.38 +
   22.39 +(* A <= sexp ==> TF(A) <= sexp *)
   22.40 +val TF_subset_sexp = standard
   22.41 +    (TF_mono RS (TF_sexp RSN (2,subset_trans)));
   22.42 +
   22.43 +
   22.44 +(** Elimination -- structural induction on the set TF **)
   22.45 +
   22.46 +val TF_Rep_defs = [TCONS_def,FNIL_def,FCONS_def,NIL_def,CONS_def];
   22.47 +
   22.48 +val major::prems = goalw Simult.thy TF_Rep_defs
   22.49 + "[| i: TF(A);  \
   22.50 +\    !!M N. [| M: A;  N: Part (TF A) In1;  R(N) |] ==> R(TCONS M N);    \
   22.51 +\    R(FNIL);                   \
   22.52 +\    !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  R(M);  R(N) \
   22.53 +\            |] ==> R(FCONS M N)    \
   22.54 +\    |] ==> R(i)";
   22.55 +by (rtac ([TF_def, TF_fun_mono, major] MRS def_induct) 1);
   22.56 +by (blast_tac (!claset addIs (prems@[PartI])
   22.57 +                       addEs [usumE, uprodE, PartE]) 1);
   22.58 +qed "TF_induct";
   22.59 +
   22.60 +(*This lemma replaces a use of subgoal_tac to prove tree_forest_induct*)
   22.61 +goalw Simult.thy [Part_def]
   22.62 + "!!A.  ! M: TF(A). (M: Part (TF A) In0 --> P(M)) & \
   22.63 +\                   (M: Part (TF A) In1 --> Q(M)) \
   22.64 +\  ==> (! M: Part (TF A) In0. P(M)) & (! M: Part (TF A) In1. Q(M))";
   22.65 +by (Blast_tac 1);
   22.66 +qed "TF_induct_lemma";
   22.67 +
   22.68 +(*Could prove  ~ TCONS M N : Part (TF A) In1  etc. *)
   22.69 +
   22.70 +(*Induction on TF with separate predicates P, Q*)
   22.71 +val prems = goalw Simult.thy TF_Rep_defs
   22.72 +    "[| !!M N. [| M: A;  N: Part (TF A) In1;  Q(N) |] ==> P(TCONS M N); \
   22.73 +\       Q(FNIL);        \
   22.74 +\       !!M N. [| M:  Part (TF A) In0;  N: Part (TF A) In1;  P(M);  Q(N) \
   22.75 +\               |] ==> Q(FCONS M N)     \
   22.76 +\    |] ==> (! M: Part (TF A) In0. P(M)) & (! N: Part (TF A) In1. Q(N))";
   22.77 +by (rtac (ballI RS TF_induct_lemma) 1);
   22.78 +by (etac TF_induct 1);
   22.79 +by (rewrite_goals_tac TF_Rep_defs);
   22.80 +	(*Blast_tac needs this type instantiation in order to preserve the
   22.81 +          right overloading of equality.  The injectiveness properties for
   22.82 +          type 'a item hold only for set types.*)
   22.83 +val PartE' = read_instantiate [("'a", "?'c set")] PartE;
   22.84 +by (ALLGOALS (blast_tac (!claset addSEs [PartE'] addIs prems)));
   22.85 +qed "Tree_Forest_induct";
   22.86 +
   22.87 +(*Induction for the abstract types 'a tree, 'a forest*)
   22.88 +val prems = goalw Simult.thy [Tcons_def,Fnil_def,Fcons_def]
   22.89 +    "[| !!x ts. Q(ts) ==> P(Tcons x ts);     \
   22.90 +\       Q(Fnil);        \
   22.91 +\       !!t ts. [| P(t);  Q(ts) |] ==> Q(Fcons t ts)    \
   22.92 +\    |] ==> (! t. P(t)) & (! ts. Q(ts))";
   22.93 +by (res_inst_tac [("P1","%z.P(Abs_Tree(z))"),
   22.94 +                  ("Q1","%z.Q(Abs_Forest(z))")] 
   22.95 +    (Tree_Forest_induct RS conjE) 1);
   22.96 +(*Instantiates ?A1 to range(Leaf). *)
   22.97 +by (fast_tac (!claset addSEs [Rep_Tree_inverse RS subst, 
   22.98 +			      Rep_Forest_inverse RS subst] 
   22.99 +                       addSIs [Rep_Tree,Rep_Forest]) 4);
  22.100 +(*Cannot use simplifier: the rewrites work in the wrong direction!*)
  22.101 +by (ALLGOALS (fast_tac (!claset addSEs [Abs_Tree_inverse RS subst,
  22.102 +					Abs_Forest_inverse RS subst] 
  22.103 +                                addSIs prems)));
  22.104 +qed "tree_forest_induct";
  22.105 +
  22.106 +
  22.107 +
  22.108 +(*** Isomorphisms ***)
  22.109 +
  22.110 +goal Simult.thy "inj(Rep_Tree)";
  22.111 +by (rtac inj_inverseI 1);
  22.112 +by (rtac Rep_Tree_inverse 1);
  22.113 +qed "inj_Rep_Tree";
  22.114 +
  22.115 +goal Simult.thy "inj_onto Abs_Tree (Part (TF(range Leaf)) In0)";
  22.116 +by (rtac inj_onto_inverseI 1);
  22.117 +by (etac Abs_Tree_inverse 1);
  22.118 +qed "inj_onto_Abs_Tree";
  22.119 +
  22.120 +goal Simult.thy "inj(Rep_Forest)";
  22.121 +by (rtac inj_inverseI 1);
  22.122 +by (rtac Rep_Forest_inverse 1);
  22.123 +qed "inj_Rep_Forest";
  22.124 +
  22.125 +goal Simult.thy "inj_onto Abs_Forest (Part (TF(range Leaf)) In1)";
  22.126 +by (rtac inj_onto_inverseI 1);
  22.127 +by (etac Abs_Forest_inverse 1);
  22.128 +qed "inj_onto_Abs_Forest";
  22.129 +
  22.130 +(** Introduction rules for constructors **)
  22.131 +
  22.132 +(* c : A <*> Part (TF A) In1 
  22.133 +        <+> {Numb(0)} <+> Part (TF A) In0 <*> Part (TF A) In1 ==> c : TF(A) *)
  22.134 +val TF_I = TF_unfold RS equalityD2 RS subsetD;
  22.135 +
  22.136 +(*For reasoning about the representation*)
  22.137 +AddIs [TF_I, uprodI, usum_In0I, usum_In1I];
  22.138 +AddSEs [Scons_inject];
  22.139 +
  22.140 +goalw Simult.thy TF_Rep_defs
  22.141 +    "!!A. [| a: A;  M: Part (TF A) In1 |] ==> TCONS a M : Part (TF A) In0";
  22.142 +by (Blast_tac 1);
  22.143 +qed "TCONS_I";
  22.144 +
  22.145 +(* FNIL is a TF(A) -- this also justifies the type definition*)
  22.146 +goalw Simult.thy TF_Rep_defs "FNIL: Part (TF A) In1";
  22.147 +by (Blast_tac 1);
  22.148 +qed "FNIL_I";
  22.149 +
  22.150 +goalw Simult.thy TF_Rep_defs
  22.151 +    "!!A. [| M: Part (TF A) In0;  N: Part (TF A) In1 |] ==> \
  22.152 +\         FCONS M N : Part (TF A) In1";
  22.153 +by (Blast_tac 1);
  22.154 +qed "FCONS_I";
  22.155 +
  22.156 +(** Injectiveness of TCONS and FCONS **)
  22.157 +
  22.158 +goalw Simult.thy TF_Rep_defs "(TCONS K M=TCONS L N) = (K=L & M=N)";
  22.159 +by (Blast_tac 1);
  22.160 +qed "TCONS_TCONS_eq";
  22.161 +bind_thm ("TCONS_inject", (TCONS_TCONS_eq RS iffD1 RS conjE));
  22.162 +
  22.163 +goalw Simult.thy TF_Rep_defs "(FCONS K M=FCONS L N) = (K=L & M=N)";
  22.164 +by (Blast_tac 1);
  22.165 +qed "FCONS_FCONS_eq";
  22.166 +bind_thm ("FCONS_inject", (FCONS_FCONS_eq RS iffD1 RS conjE));
  22.167 +
  22.168 +(** Distinctness of TCONS, FNIL and FCONS **)
  22.169 +
  22.170 +goalw Simult.thy TF_Rep_defs "TCONS M N ~= FNIL";
  22.171 +by (Blast_tac 1);
  22.172 +qed "TCONS_not_FNIL";
  22.173 +bind_thm ("FNIL_not_TCONS", (TCONS_not_FNIL RS not_sym));
  22.174 +
  22.175 +bind_thm ("TCONS_neq_FNIL", (TCONS_not_FNIL RS notE));
  22.176 +val FNIL_neq_TCONS = sym RS TCONS_neq_FNIL;
  22.177 +
  22.178 +goalw Simult.thy TF_Rep_defs "FCONS M N ~= FNIL";
  22.179 +by (Blast_tac 1);
  22.180 +qed "FCONS_not_FNIL";
  22.181 +bind_thm ("FNIL_not_FCONS", (FCONS_not_FNIL RS not_sym));
  22.182 +
  22.183 +bind_thm ("FCONS_neq_FNIL", (FCONS_not_FNIL RS notE));
  22.184 +val FNIL_neq_FCONS = sym RS FCONS_neq_FNIL;
  22.185 +
  22.186 +goalw Simult.thy TF_Rep_defs "TCONS M N ~= FCONS K L";
  22.187 +by (Blast_tac 1);
  22.188 +qed "TCONS_not_FCONS";
  22.189 +bind_thm ("FCONS_not_TCONS", (TCONS_not_FCONS RS not_sym));
  22.190 +
  22.191 +bind_thm ("TCONS_neq_FCONS", (TCONS_not_FCONS RS notE));
  22.192 +val FCONS_neq_TCONS = sym RS TCONS_neq_FCONS;
  22.193 +
  22.194 +(*???? Too many derived rules ????
  22.195 +  Automatically generate symmetric forms?  Always expand TF_Rep_defs? *)
  22.196 +
  22.197 +(** Injectiveness of Tcons and Fcons **)
  22.198 +
  22.199 +(*For reasoning about abstract constructors*)
  22.200 +AddSIs [Rep_Tree, Rep_Forest, TCONS_I, FNIL_I, FCONS_I];
  22.201 +AddSEs [TCONS_inject, FCONS_inject,
  22.202 +                           TCONS_neq_FNIL, FNIL_neq_TCONS,
  22.203 +                           FCONS_neq_FNIL, FNIL_neq_FCONS,
  22.204 +                           TCONS_neq_FCONS, FCONS_neq_TCONS];
  22.205 +AddSDs [inj_onto_Abs_Tree RS inj_ontoD,
  22.206 +                           inj_onto_Abs_Forest RS inj_ontoD,
  22.207 +                           inj_Rep_Tree RS injD, inj_Rep_Forest RS injD,
  22.208 +                           Leaf_inject];
  22.209 +
  22.210 +goalw Simult.thy [Tcons_def] "(Tcons x xs=Tcons y ys) = (x=y & xs=ys)";
  22.211 +by (Blast_tac 1);
  22.212 +qed "Tcons_Tcons_eq";
  22.213 +bind_thm ("Tcons_inject", (Tcons_Tcons_eq RS iffD1 RS conjE));
  22.214 +
  22.215 +goalw Simult.thy [Fcons_def,Fnil_def] "Fcons x xs ~= Fnil";
  22.216 +by (Blast_tac 1);
  22.217 +qed "Fcons_not_Fnil";
  22.218 +
  22.219 +bind_thm ("Fcons_neq_Fnil", Fcons_not_Fnil RS notE);
  22.220 +val Fnil_neq_Fcons = sym RS Fcons_neq_Fnil;
  22.221 +
  22.222 +
  22.223 +(** Injectiveness of Fcons **)
  22.224 +
  22.225 +goalw Simult.thy [Fcons_def] "(Fcons x xs=Fcons y ys) = (x=y & xs=ys)";
  22.226 +by (Blast_tac 1);
  22.227 +qed "Fcons_Fcons_eq";
  22.228 +bind_thm ("Fcons_inject", Fcons_Fcons_eq RS iffD1 RS conjE);
  22.229 +
  22.230 +
  22.231 +(*** TF_rec -- by wf recursion on pred_sexp ***)
  22.232 +
  22.233 +goal Simult.thy
  22.234 +   "(%M. TF_rec M b c d) = wfrec (trancl pred_sexp) \
  22.235 +                         \       (%g. Case (Split(%x y. b x y (g y))) \
  22.236 +                         \           (List_case c (%x y. d x y (g x) (g y))))";
  22.237 +by (simp_tac (HOL_ss addsimps [TF_rec_def]) 1);
  22.238 +val TF_rec_unfold = (wf_pred_sexp RS wf_trancl) RS 
  22.239 +                    ((result() RS eq_reflection) RS def_wfrec);
  22.240 +
  22.241 +(*---------------------------------------------------------------------------
  22.242 + * Old: 
  22.243 + * val TF_rec_unfold =
  22.244 + *   wf_pred_sexp RS wf_trancl RS (TF_rec_def RS def_wfrec);
  22.245 + *---------------------------------------------------------------------------*)
  22.246 +
  22.247 +(** conversion rules for TF_rec **)
  22.248 +
  22.249 +goalw Simult.thy [TCONS_def]
  22.250 +    "!!M N. [| M: sexp;  N: sexp |] ==>         \
  22.251 +\           TF_rec (TCONS M N) b c d = b M N (TF_rec N b c d)";
  22.252 +by (rtac (TF_rec_unfold RS trans) 1);
  22.253 +by (simp_tac (!simpset addsimps [Case_In0, Split]) 1);
  22.254 +by (asm_simp_tac (!simpset addsimps [In0_def]) 1);
  22.255 +qed "TF_rec_TCONS";
  22.256 +
  22.257 +goalw Simult.thy [FNIL_def] "TF_rec FNIL b c d = c";
  22.258 +by (rtac (TF_rec_unfold RS trans) 1);
  22.259 +by (simp_tac (HOL_ss addsimps [Case_In1, List_case_NIL]) 1);
  22.260 +qed "TF_rec_FNIL";
  22.261 +
  22.262 +goalw Simult.thy [FCONS_def]
  22.263 + "!!M N. [| M: sexp;  N: sexp |] ==>    \
  22.264 +\        TF_rec (FCONS M N) b c d = d M N (TF_rec M b c d) (TF_rec N b c d)";
  22.265 +by (rtac (TF_rec_unfold RS trans) 1);
  22.266 +by (simp_tac (HOL_ss addsimps [Case_In1, List_case_CONS]) 1);
  22.267 +by (asm_simp_tac (!simpset addsimps [CONS_def,In1_def]) 1);
  22.268 +qed "TF_rec_FCONS";
  22.269 +
  22.270 +
  22.271 +(*** tree_rec, forest_rec -- by TF_rec ***)
  22.272 +
  22.273 +val Rep_Tree_in_sexp =
  22.274 +    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
  22.275 +     Rep_Tree] MRS subsetD;
  22.276 +val Rep_Forest_in_sexp =
  22.277 +    [range_Leaf_subset_sexp RS TF_subset_sexp RS (Part_subset RS subset_trans),
  22.278 +     Rep_Forest] MRS subsetD;
  22.279 +
  22.280 +val tf_rec_ss = HOL_ss addsimps
  22.281 +  [TF_rec_TCONS, TF_rec_FNIL, TF_rec_FCONS,
  22.282 +   TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
  22.283 +   Rep_Tree_inverse, Rep_Forest_inverse,
  22.284 +   Abs_Tree_inverse, Abs_Forest_inverse,
  22.285 +   inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
  22.286 +   Rep_Tree_in_sexp, Rep_Forest_in_sexp];
  22.287 +
  22.288 +goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
  22.289 +    "tree_rec (Tcons a tf) b c d = b a tf (forest_rec tf b c d)";
  22.290 +by (simp_tac tf_rec_ss 1);
  22.291 +qed "tree_rec_Tcons";
  22.292 +
  22.293 +goalw Simult.thy [forest_rec_def, Fnil_def] "forest_rec Fnil b c d = c";
  22.294 +by (simp_tac tf_rec_ss 1);
  22.295 +qed "forest_rec_Fnil";
  22.296 +
  22.297 +goalw Simult.thy [tree_rec_def, forest_rec_def, Fcons_def]
  22.298 +    "forest_rec (Fcons t tf) b c d = \
  22.299 +\    d t tf (tree_rec t b c d) (forest_rec tf b c d)";
  22.300 +by (simp_tac tf_rec_ss 1);
  22.301 +qed "forest_rec_Cons";
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/src/HOL/Induct/Simult.thy	Wed May 07 12:50:26 1997 +0200
    23.3 @@ -0,0 +1,82 @@
    23.4 +(*  Title:      HOL/ex/Simult
    23.5 +    ID:         $Id$
    23.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    23.7 +    Copyright   1993  University of Cambridge
    23.8 +
    23.9 +A simultaneous recursive type definition: trees & forests
   23.10 +
   23.11 +This is essentially the same data structure that on ex/term.ML, which is
   23.12 +simpler because it uses list as a new type former.  The approach in this
   23.13 +file may be superior for other simultaneous recursions.
   23.14 +
   23.15 +The inductive definition package does not help defining this sort of mutually
   23.16 +recursive data structure because it uses Inl, Inr instead of In0, In1.
   23.17 +*)
   23.18 +
   23.19 +Simult = SList +
   23.20 +
   23.21 +types    'a tree
   23.22 +         'a forest
   23.23 +
   23.24 +arities  tree,forest :: (term)term
   23.25 +
   23.26 +consts
   23.27 +  TF          :: 'a item set => 'a item set
   23.28 +  FNIL        :: 'a item
   23.29 +  TCONS,FCONS :: ['a item, 'a item] => 'a item
   23.30 +  Rep_Tree    :: 'a tree => 'a item
   23.31 +  Abs_Tree    :: 'a item => 'a tree
   23.32 +  Rep_Forest  :: 'a forest => 'a item
   23.33 +  Abs_Forest  :: 'a item => 'a forest
   23.34 +  Tcons       :: ['a, 'a forest] => 'a tree
   23.35 +  Fcons       :: ['a tree, 'a forest] => 'a forest
   23.36 +  Fnil        :: 'a forest
   23.37 +  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
   23.38 +                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
   23.39 +  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
   23.40 +                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
   23.41 +  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
   23.42 +                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
   23.43 +
   23.44 +defs
   23.45 +     (*the concrete constants*)
   23.46 +  TCONS_def     "TCONS M N == In0(M $ N)"
   23.47 +  FNIL_def      "FNIL      == In1(NIL)"
   23.48 +  FCONS_def     "FCONS M N == In1(CONS M N)"
   23.49 +     (*the abstract constants*)
   23.50 +  Tcons_def     "Tcons a ts == Abs_Tree(TCONS (Leaf a) (Rep_Forest ts))"
   23.51 +  Fnil_def      "Fnil       == Abs_Forest(FNIL)"
   23.52 +  Fcons_def     "Fcons t ts == Abs_Forest(FCONS (Rep_Tree t) (Rep_Forest ts))"
   23.53 +
   23.54 +  TF_def        "TF(A) == lfp(%Z. A <*> Part Z In1 
   23.55 +                           <+> ({Numb(0)} <+> Part Z In0 <*> Part Z In1))"
   23.56 +
   23.57 +rules
   23.58 +  (*faking a type definition for tree...*)
   23.59 +  Rep_Tree         "Rep_Tree(n): Part (TF(range Leaf)) In0"
   23.60 +  Rep_Tree_inverse "Abs_Tree(Rep_Tree(t)) = t"
   23.61 +  Abs_Tree_inverse "z: Part (TF(range Leaf)) In0 ==> Rep_Tree(Abs_Tree(z)) = z"
   23.62 +    (*faking a type definition for forest...*)
   23.63 +  Rep_Forest         "Rep_Forest(n): Part (TF(range Leaf)) In1"
   23.64 +  Rep_Forest_inverse "Abs_Forest(Rep_Forest(ts)) = ts"
   23.65 +  Abs_Forest_inverse 
   23.66 +        "z: Part (TF(range Leaf)) In1 ==> Rep_Forest(Abs_Forest(z)) = z"
   23.67 +
   23.68 +
   23.69 +defs
   23.70 +     (*recursion*)
   23.71 +  TF_rec_def    
   23.72 +   "TF_rec M b c d == wfrec (trancl pred_sexp)
   23.73 +               (%g. Case (Split(%x y. b x y (g y))) 
   23.74 +                      (List_case c (%x y. d x y (g x) (g y)))) M"
   23.75 +
   23.76 +  tree_rec_def
   23.77 +   "tree_rec t b c d == 
   23.78 +   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
   23.79 +          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   23.80 +
   23.81 +  forest_rec_def
   23.82 +   "forest_rec tf b c d == 
   23.83 +   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
   23.84 +          c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
   23.85 +end
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/src/HOL/Induct/Term.ML	Wed May 07 12:50:26 1997 +0200
    24.3 @@ -0,0 +1,172 @@
    24.4 +(*  Title:      HOL/ex/Term
    24.5 +    ID:         $Id$
    24.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    24.7 +    Copyright   1992  University of Cambridge
    24.8 +
    24.9 +Terms over a given alphabet -- function applications; illustrates list functor
   24.10 +  (essentially the same type as in Trees & Forests)
   24.11 +*)
   24.12 +
   24.13 +open Term;
   24.14 +
   24.15 +(*** Monotonicity and unfolding of the function ***)
   24.16 +
   24.17 +goal Term.thy "term(A) = A <*> list(term(A))";
   24.18 +by (fast_tac (!claset addSIs (equalityI :: term.intrs)
   24.19 +                      addEs [term.elim]) 1);
   24.20 +qed "term_unfold";
   24.21 +
   24.22 +(*This justifies using term in other recursive type definitions*)
   24.23 +goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
   24.24 +by (REPEAT (ares_tac ([lfp_mono, list_mono] @ basic_monos) 1));
   24.25 +qed "term_mono";
   24.26 +
   24.27 +(** Type checking -- term creates well-founded sets **)
   24.28 +
   24.29 +goalw Term.thy term.defs "term(sexp) <= sexp";
   24.30 +by (rtac lfp_lowerbound 1);
   24.31 +by (fast_tac (!claset addIs [sexp.SconsI, list_sexp RS subsetD]) 1);
   24.32 +qed "term_sexp";
   24.33 +
   24.34 +(* A <= sexp ==> term(A) <= sexp *)
   24.35 +bind_thm ("term_subset_sexp", ([term_mono, term_sexp] MRS subset_trans));
   24.36 +
   24.37 +
   24.38 +(** Elimination -- structural induction on the set term(A) **)
   24.39 +
   24.40 +(*Induction for the set term(A) *)
   24.41 +val [major,minor] = goal Term.thy 
   24.42 +    "[| M: term(A);  \
   24.43 +\       !!x zs. [| x: A;  zs: list(term(A));  zs: list({x.R(x)}) \
   24.44 +\               |] ==> R(x$zs)  \
   24.45 +\    |] ==> R(M)";
   24.46 +by (rtac (major RS term.induct) 1);
   24.47 +by (REPEAT (eresolve_tac ([minor] @
   24.48 +                ([Int_lower1,Int_lower2] RL [list_mono RS subsetD])) 1));
   24.49 +(*Proof could also use  mono_Int RS subsetD RS IntE *)
   24.50 +qed "Term_induct";
   24.51 +
   24.52 +(*Induction on term(A) followed by induction on list *)
   24.53 +val major::prems = goal Term.thy
   24.54 +    "[| M: term(A);  \
   24.55 +\       !!x.      [| x: A |] ==> R(x$NIL);  \
   24.56 +\       !!x z zs. [| x: A;  z: term(A);  zs: list(term(A));  R(x$zs)  \
   24.57 +\                 |] ==> R(x $ CONS z zs)  \
   24.58 +\    |] ==> R(M)";
   24.59 +by (rtac (major RS Term_induct) 1);
   24.60 +by (etac list.induct 1);
   24.61 +by (REPEAT (ares_tac prems 1));
   24.62 +qed "Term_induct2";
   24.63 +
   24.64 +(*** Structural Induction on the abstract type 'a term ***)
   24.65 +
   24.66 +val Rep_term_in_sexp =
   24.67 +    Rep_term RS (range_Leaf_subset_sexp RS term_subset_sexp RS subsetD);
   24.68 +
   24.69 +(*Induction for the abstract type 'a term*)
   24.70 +val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
   24.71 +    "[| !!x ts. (ALL t: set_of_list ts. R t) ==> R(App x ts)  \
   24.72 +\    |] ==> R(t)";
   24.73 +by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
   24.74 +by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
   24.75 +by (rtac (Rep_term RS Term_induct) 1);
   24.76 +by (REPEAT (ares_tac [conjI, sexp.SconsI, term_subset_sexp RS 
   24.77 +    list_subset_sexp, range_Leaf_subset_sexp] 1
   24.78 +     ORELSE etac rev_subsetD 1));
   24.79 +by (eres_inst_tac [("A1","term(?u)"), ("f1","Rep_term"), ("g1","Abs_term")]
   24.80 +        (Abs_map_inverse RS subst) 1);
   24.81 +by (rtac (range_Leaf_subset_sexp RS term_subset_sexp) 1);
   24.82 +by (etac Abs_term_inverse 1);
   24.83 +by (etac rangeE 1);
   24.84 +by (hyp_subst_tac 1);
   24.85 +by (resolve_tac prems 1);
   24.86 +by (etac list.induct 1);
   24.87 +by (etac CollectE 2);
   24.88 +by (stac Abs_map_CONS 2);
   24.89 +by (etac conjunct1 2);
   24.90 +by (etac rev_subsetD 2);
   24.91 +by (rtac list_subset_sexp 2);
   24.92 +by (ALLGOALS Asm_simp_tac);
   24.93 +by (ALLGOALS Fast_tac);
   24.94 +qed "term_induct";
   24.95 +
   24.96 +(*Induction for the abstract type 'a term*)
   24.97 +val prems = goal Term.thy 
   24.98 +    "[| !!x. R(App x Nil);  \
   24.99 +\       !!x t ts. R(App x ts) ==> R(App x (t#ts))  \
  24.100 +\    |] ==> R(t)";
  24.101 +by (rtac term_induct 1);  (*types force good instantiation*)
  24.102 +by (etac rev_mp 1);
  24.103 +by (rtac list_induct2 1);  (*types force good instantiation*)
  24.104 +by (ALLGOALS (asm_simp_tac (!simpset addsimps prems)));
  24.105 +qed "term_induct2";
  24.106 +
  24.107 +(*Perform induction on xs. *)
  24.108 +fun term_ind2_tac a i = 
  24.109 +    EVERY [res_inst_tac [("t",a)] term_induct2 i,
  24.110 +           rename_last_tac a ["1","s"] (i+1)];
  24.111 +
  24.112 +
  24.113 +
  24.114 +(*** Term_rec -- by wf recursion on pred_sexp ***)
  24.115 +
  24.116 +goal Term.thy
  24.117 +   "(%M. Term_rec M d) = wfrec (trancl pred_sexp) \
  24.118 +                             \ (%g. Split(%x y. d x y (Abs_map g y)))";
  24.119 +by (simp_tac (HOL_ss addsimps [Term_rec_def]) 1);
  24.120 +bind_thm("Term_rec_unfold", (wf_pred_sexp RS wf_trancl) RS 
  24.121 +                            ((result() RS eq_reflection) RS def_wfrec));
  24.122 +
  24.123 +(*---------------------------------------------------------------------------
  24.124 + * Old:
  24.125 + * val Term_rec_unfold =
  24.126 + *     wf_pred_sexp RS wf_trancl RS (Term_rec_def RS def_wfrec);
  24.127 + *---------------------------------------------------------------------------*)
  24.128 +
  24.129 +(** conversion rules **)
  24.130 +
  24.131 +val [prem] = goal Term.thy
  24.132 +    "N: list(term(A)) ==>  \
  24.133 +\    !M. (N,M): pred_sexp^+ --> \
  24.134 +\        Abs_map (cut h (pred_sexp^+) M) N = \
  24.135 +\        Abs_map h N";
  24.136 +by (rtac (prem RS list.induct) 1);
  24.137 +by (Simp_tac 1);
  24.138 +by (strip_tac 1);
  24.139 +by (etac (pred_sexp_CONS_D RS conjE) 1);
  24.140 +by (asm_simp_tac (!simpset addsimps [trancl_pred_sexpD1]) 1);
  24.141 +qed "Abs_map_lemma";
  24.142 +
  24.143 +val [prem1,prem2,A_subset_sexp] = goal Term.thy
  24.144 +    "[| M: sexp;  N: list(term(A));  A<=sexp |] ==> \
  24.145 +\    Term_rec (M$N) d = d M N (Abs_map (%Z. Term_rec Z d) N)";
  24.146 +by (rtac (Term_rec_unfold RS trans) 1);
  24.147 +by (simp_tac (HOL_ss addsimps
  24.148 +      [Split,
  24.149 +       prem2 RS Abs_map_lemma RS spec RS mp, pred_sexpI2 RS r_into_trancl,
  24.150 +       prem1, prem2 RS rev_subsetD, list_subset_sexp,
  24.151 +       term_subset_sexp, A_subset_sexp]) 1);
  24.152 +qed "Term_rec";
  24.153 +
  24.154 +(*** term_rec -- by Term_rec ***)
  24.155 +
  24.156 +local
  24.157 +  val Rep_map_type1 = read_instantiate_sg (sign_of Term.thy)
  24.158 +                        [("f","Rep_term")] Rep_map_type;
  24.159 +  val Rep_Tlist = Rep_term RS Rep_map_type1;
  24.160 +  val Rep_Term_rec = range_Leaf_subset_sexp RSN (2,Rep_Tlist RSN(2,Term_rec));
  24.161 +
  24.162 +  (*Now avoids conditional rewriting with the premise N: list(term(A)),
  24.163 +    since A will be uninstantiated and will cause rewriting to fail. *)
  24.164 +  val term_rec_ss = HOL_ss
  24.165 +      addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
  24.166 +                Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
  24.167 +                inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
  24.168 +in
  24.169 +
  24.170 +val term_rec = prove_goalw Term.thy
  24.171 +         [term_rec_def, App_def, Rep_Tlist_def, Abs_Tlist_def]
  24.172 +    "term_rec (App f ts) d = d f ts (map (%t. term_rec t d) ts)"
  24.173 + (fn _ => [simp_tac term_rec_ss 1])
  24.174 +
  24.175 +end;
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/src/HOL/Induct/Term.thy	Wed May 07 12:50:26 1997 +0200
    25.3 @@ -0,0 +1,55 @@
    25.4 +(*  Title:      HOL/ex/Term
    25.5 +    ID:         $Id$
    25.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    25.7 +    Copyright   1992  University of Cambridge
    25.8 +
    25.9 +Terms over a given alphabet -- function applications; illustrates list functor
   25.10 +  (essentially the same type as in Trees & Forests)
   25.11 +
   25.12 +There is no constructor APP because it is simply cons ($) 
   25.13 +*)
   25.14 +
   25.15 +Term = SList +
   25.16 +
   25.17 +types   'a term
   25.18 +
   25.19 +arities term :: (term)term
   25.20 +
   25.21 +consts
   25.22 +  term          :: 'a item set => 'a item set
   25.23 +  Rep_term      :: 'a term => 'a item
   25.24 +  Abs_term      :: 'a item => 'a term
   25.25 +  Rep_Tlist     :: 'a term list => 'a item
   25.26 +  Abs_Tlist     :: 'a item => 'a term list
   25.27 +  App           :: ['a, ('a term)list] => 'a term
   25.28 +  Term_rec      :: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
   25.29 +  term_rec      :: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
   25.30 +
   25.31 +inductive "term(A)"
   25.32 +  intrs
   25.33 +    APP_I "[| M: A;  N : list(term(A)) |] ==> M$N : term(A)"
   25.34 +  monos   "[list_mono]"
   25.35 +
   25.36 +defs
   25.37 +  (*defining abstraction/representation functions for term list...*)
   25.38 +  Rep_Tlist_def "Rep_Tlist == Rep_map(Rep_term)"
   25.39 +  Abs_Tlist_def "Abs_Tlist == Abs_map(Abs_term)"
   25.40 +
   25.41 +  (*defining the abstract constants*)
   25.42 +  App_def       "App a ts == Abs_term(Leaf(a) $ Rep_Tlist(ts))"
   25.43 +
   25.44 +  (*list recursion*)
   25.45 +  Term_rec_def  
   25.46 +   "Term_rec M d == wfrec (trancl pred_sexp)
   25.47 +           (%g. Split(%x y. d x y (Abs_map g y))) M"
   25.48 +
   25.49 +  term_rec_def
   25.50 +   "term_rec t d == 
   25.51 +   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
   25.52 +
   25.53 +rules
   25.54 +    (*faking a type definition for term...*)
   25.55 +  Rep_term              "Rep_term(n): term(range(Leaf))"
   25.56 +  Rep_term_inverse      "Abs_term(Rep_term(t)) = t"
   25.57 +  Abs_term_inverse      "M: term(range(Leaf)) ==> Rep_term(Abs_term(M)) = M"
   25.58 +end