# HG changeset patch # User paulson # Date 1005132547 -3600 # Node ID 6f463d16cbd0e5c5ad53dfd7869df227bb3447d9 # Parent b38cfbabfda4da51845db9fbe2e02e52500b6274 reorganization of the ZF examples diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Acc.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Acc.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,58 @@ +(* Title: ZF/ex/acc + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +(*The introduction rule must require a \\ field(r) + Otherwise acc(r) would be a proper class! *) + +(*The intended introduction rule*) +val prems = goal Acc.thy + "[| !!b. :r ==> b \\ acc(r); a \\ field(r) |] ==> a \\ acc(r)"; +by (fast_tac (claset() addIs prems@acc.intrs) 1); +qed "accI"; + +Goal "[| b \\ acc(r); : r |] ==> a \\ acc(r)"; +by (etac acc.elim 1); +by (Fast_tac 1); +qed "acc_downward"; + +val [major,indhyp] = goal Acc.thy + "[| a \\ acc(r); \ +\ !!x. [| x \\ acc(r); \\y. :r --> P(y) |] ==> P(x) \ +\ |] ==> P(a)"; +by (rtac (major RS acc.induct) 1); +by (rtac indhyp 1); +by (Fast_tac 2); +by (resolve_tac acc.intrs 1); +by (assume_tac 2); +by (etac (Collect_subset RS Pow_mono RS subsetD) 1); +qed "acc_induct"; + +Goal "wf[acc(r)](r)"; +by (rtac wf_onI2 1); +by (etac acc_induct 1); +by (Fast_tac 1); +qed "wf_on_acc"; + +(* field(r) \\ acc(r) ==> wf(r) *) +val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf; + +val [major] = goal Acc.thy "wf(r) ==> field(r) \\ acc(r)"; +by (rtac subsetI 1); +by (etac (major RS wf_induct2) 1); +by (rtac subset_refl 1); +by (rtac accI 1); +by (assume_tac 2); +by (Fast_tac 1); +qed "acc_wfD"; + +Goal "wf(r) <-> field(r) \\ acc(r)"; +by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); +qed "wf_acc_iff"; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Acc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Acc.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,23 @@ +(* Title: ZF/ex/Acc.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of acc(r) + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +Acc = Main + + +consts + acc :: i=>i + +inductive + domains "acc(r)" <= "field(r)" + intrs + vimage "[| r-``{a}: Pow(acc(r)); a \\ field(r) |] ==> a \\ acc(r)" + monos Pow_mono + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Comb.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Comb.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,222 @@ +(* Title: ZF/ex/comb.ML + ID: $Id$ + Author: Lawrence C Paulson + Copyright 1993 University of Cambridge + +Combinatory Logic example: the Church-Rosser Theorem +Curiously, combinators do not include free variables. + +Example taken from + J. Camilleri and T. F. Melham. + Reasoning with Inductively Defined Relations in the HOL Theorem Prover. + Report 265, University of Cambridge Computer Laboratory, 1992. + +HOL system proofs may be found in +/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml +*) + +(*** Transitive closure preserves the Church-Rosser property ***) + +Goalw [diamond_def] + "!!x y r. [| diamond(r); :r^+ |] ==> \ +\ \\y'. :r --> (\\z. : r^+ & : r)"; +by (etac trancl_induct 1); +by (blast_tac (claset() addIs [r_into_trancl]) 1); +by (slow_best_tac (claset() addSDs [spec RS mp] + addIs [r_into_trancl, trans_trancl RS transD]) 1); +val diamond_strip_lemmaE = result() RS spec RS mp RS exE; + +val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)"; +by (rewtac diamond_def); (*unfold only in goal, not in premise!*) +by (rtac (impI RS allI RS allI) 1); +by (etac trancl_induct 1); +by (ALLGOALS (*Seems to be a brittle, undirected search*) + (slow_best_tac (claset() addIs [r_into_trancl, trans_trancl RS transD] + addEs [major RS diamond_strip_lemmaE]))); +qed "diamond_trancl"; + + +val [_,_,comb_Ap] = comb.intrs; +val Ap_E = comb.mk_cases "p#q \\ comb"; + +AddSIs comb.intrs; + + +(*** Results about Contraction ***) + +(*For type checking: replaces a-1->b by a,b \\ comb *) +val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2; +val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1; +val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2; + +Goal "field(contract) = comb"; +by (blast_tac (claset() addIs [contract.K] addSEs [contract_combE2]) 1); +qed "field_contract_eq"; + +bind_thm ("reduction_refl", + (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl)); + +bind_thm ("rtrancl_into_rtrancl2", + (r_into_rtrancl RS (trans_rtrancl RS transD))); + +AddSIs [reduction_refl, contract.K, contract.S]; + +val reduction_rls = [contract.K RS rtrancl_into_rtrancl2, + contract.S RS rtrancl_into_rtrancl2, + contract.Ap1 RS rtrancl_into_rtrancl2, + contract.Ap2 RS rtrancl_into_rtrancl2]; + +(*Example only: not used*) +Goalw [I_def] "p \\ comb ==> I#p ---> p"; +by (blast_tac (claset() addIs reduction_rls) 1); +qed "reduce_I"; + +Goalw [I_def] "I \\ comb"; +by (Blast_tac 1); +qed "comb_I"; + +(** Non-contraction results **) + +(*Derive a case for each combinator constructor*) +val K_contractE = contract.mk_cases "K -1-> r"; +val S_contractE = contract.mk_cases "S -1-> r"; +val Ap_contractE = contract.mk_cases "p#q -1-> r"; + +AddIs [contract.Ap1, contract.Ap2]; +AddSEs [K_contractE, S_contractE, Ap_contractE]; + +Goalw [I_def] "I -1-> r ==> P"; +by Auto_tac; +qed "I_contract_E"; + +Goal "K#p -1-> r ==> (\\q. r = K#q & p -1-> q)"; +by Auto_tac; +qed "K1_contractD"; + +Goal "[| p ---> q; r \\ comb |] ==> p#r ---> q#r"; +by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); +by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); +by (etac rtrancl_induct 1); +by (blast_tac (claset() addIs reduction_rls) 1); +by (etac (trans_rtrancl RS transD) 1); +by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1); +qed "Ap_reduce1"; + +Goal "[| p ---> q; r \\ comb |] ==> r#p ---> r#q"; +by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); +by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); +by (etac rtrancl_induct 1); +by (blast_tac (claset() addIs reduction_rls) 1); +by (etac (trans_rtrancl RS transD) 1); +by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1); +qed "Ap_reduce2"; + +(** Counterexample to the diamond property for -1-> **) + +Goal "K#I#(I#I) -1-> I"; +by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1)); +qed "KIII_contract1"; + +Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"; +by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1)); +qed "KIII_contract2"; + +Goal "K#I#((K#I)#(K#I)) -1-> I"; +by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1)); +qed "KIII_contract3"; + +Goalw [diamond_def] "~ diamond(contract)"; +by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3] + addSEs [I_contract_E]) 1); +qed "not_diamond_contract"; + + + +(*** Results about Parallel Contraction ***) + +(*For type checking: replaces a=1=>b by a,b \\ comb *) +val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2; +val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1; +val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2; + +Goal "field(parcontract) = comb"; +by (blast_tac (claset() addIs [parcontract.K] + addSEs [parcontract_combE2]) 1); +qed "field_parcontract_eq"; + +(*Derive a case for each combinator constructor*) +val K_parcontractE = parcontract.mk_cases "K =1=> r"; +val S_parcontractE = parcontract.mk_cases "S =1=> r"; +val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r"; + +AddIs parcontract.intrs; +AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE]; + +(*** Basic properties of parallel contraction ***) + +Goal "K#p =1=> r ==> (\\p'. r = K#p' & p =1=> p')"; +by Auto_tac; +qed "K1_parcontractD"; +AddSDs [K1_parcontractD]; + +Goal "S#p =1=> r ==> (\\p'. r = S#p' & p =1=> p')"; +by Auto_tac; +qed "S1_parcontractD"; +AddSDs [S1_parcontractD]; + +Goal "S#p#q =1=> r ==> (\\p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"; +by Auto_tac; +qed "S2_parcontractD"; +AddSDs [S2_parcontractD]; + +(*Church-Rosser property for parallel contraction*) +Goalw [diamond_def] "diamond(parcontract)"; +by (rtac (impI RS allI RS allI) 1); +by (etac parcontract.induct 1); +by (ALLGOALS + (blast_tac (claset() addSEs comb.free_SEs + addIs [parcontract_combD2]))); +qed "diamond_parcontract"; + +(*** Equivalence of p--->q and p===>q ***) + +Goal "p-1->q ==> p=1=>q"; +by (etac contract.induct 1); +by Auto_tac; +qed "contract_imp_parcontract"; + +Goal "p--->q ==> p===>q"; +by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); +by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); +by (etac rtrancl_induct 1); +by (blast_tac (claset() addIs [r_into_trancl]) 1); +by (blast_tac (claset() addIs [contract_imp_parcontract, + r_into_trancl, trans_trancl RS transD]) 1); +qed "reduce_imp_parreduce"; + + +Goal "p=1=>q ==> p--->q"; +by (etac parcontract.induct 1); +by (blast_tac (claset() addIs reduction_rls) 1); +by (blast_tac (claset() addIs reduction_rls) 1); +by (blast_tac (claset() addIs reduction_rls) 1); +by (blast_tac + (claset() addIs [trans_rtrancl RS transD, + Ap_reduce1, Ap_reduce2, parcontract_combD1, + parcontract_combD2]) 1); +qed "parcontract_imp_reduce"; + +Goal "p===>q ==> p--->q"; +by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1); +by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1); +by (etac trancl_induct 1); +by (etac parcontract_imp_reduce 1); +by (etac (trans_rtrancl RS transD) 1); +by (etac parcontract_imp_reduce 1); +qed "parreduce_imp_reduce"; + +Goal "p===>q <-> p--->q"; +by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1); +qed "parreduce_iff_reduce"; + +writeln"Reached end of file."; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Comb.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Comb.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,79 @@ +(* Title: ZF/ex/Comb.thy + ID: $Id$ + Author: Lawrence C Paulson + Copyright 1994 University of Cambridge + +Combinatory Logic example: the Church-Rosser Theorem +Curiously, combinators do not include free variables. + +Example taken from + J. Camilleri and T. F. Melham. + Reasoning with Inductively Defined Relations in the HOL Theorem Prover. + Report 265, University of Cambridge Computer Laboratory, 1992. +*) + + +Comb = Main + + +(** Datatype definition of combinators S and K, with infixed application **) +consts comb :: i +datatype + "comb" = K + | S + | "#" ("p \\ comb", "q \\ comb") (infixl 90) + +(** Inductive definition of contractions, -1-> + and (multi-step) reductions, ---> +**) +consts + contract :: i + "-1->" :: [i,i] => o (infixl 50) + "--->" :: [i,i] => o (infixl 50) + +translations + "p -1-> q" == " \\ contract" + "p ---> q" == " \\ contract^*" + +inductive + domains "contract" <= "comb*comb" + intrs + K "[| p \\ comb; q \\ comb |] ==> K#p#q -1-> p" + S "[| p \\ comb; q \\ comb; r \\ comb |] ==> S#p#q#r -1-> (p#r)#(q#r)" + Ap1 "[| p-1->q; r \\ comb |] ==> p#r -1-> q#r" + Ap2 "[| p-1->q; r \\ comb |] ==> r#p -1-> r#q" + type_intrs "comb.intrs" + + +(** Inductive definition of parallel contractions, =1=> + and (multi-step) parallel reductions, ===> +**) +consts + parcontract :: i + "=1=>" :: [i,i] => o (infixl 50) + "===>" :: [i,i] => o (infixl 50) + +translations + "p =1=> q" == " \\ parcontract" + "p ===> q" == " \\ parcontract^+" + +inductive + domains "parcontract" <= "comb*comb" + intrs + refl "[| p \\ comb |] ==> p =1=> p" + K "[| p \\ comb; q \\ comb |] ==> K#p#q =1=> p" + S "[| p \\ comb; q \\ comb; r \\ comb |] ==> S#p#q#r =1=> (p#r)#(q#r)" + Ap "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s" + type_intrs "comb.intrs" + + +(*Misc definitions*) +constdefs + I :: i + "I == S#K#K" + + diamond :: i => o + "diamond(r) == \\x y. :r --> + (\\y'. :r --> + (\\z. :r & \\ r))" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/ListN.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/ListN.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,46 @@ +(* Title: ZF/ex/ListN + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Inductive definition of lists of n elements + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +Goal "l \\ list(A) ==> \\ listn(A)"; +by (etac list.induct 1); +by (ALLGOALS Asm_simp_tac); +by (REPEAT (ares_tac listn.intrs 1)); +qed "list_into_listn"; + +Goal " \\ listn(A) <-> l \\ list(A) & length(l)=n"; +by (rtac iffI 1); +by (blast_tac (claset() addIs [list_into_listn]) 2); +by (etac listn.induct 1); +by Auto_tac; +qed "listn_iff"; + +Goal "listn(A)``{n} = {l \\ list(A). length(l)=n}"; +by (rtac equality_iffI 1); +by (simp_tac (simpset() addsimps [listn_iff,separation,image_singleton_iff]) 1); +qed "listn_image_eq"; + +Goalw listn.defs "A \\ B ==> listn(A) \\ listn(B)"; +by (rtac lfp_mono 1); +by (REPEAT (rtac listn.bnd_mono 1)); +by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1)); +qed "listn_mono"; + +Goal "[| \\ listn(A); \\ listn(A) |] ==> \\ listn(A)"; +by (etac listn.induct 1); +by (ftac (impOfSubs listn.dom_subset) 1); +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps listn.intrs))); +qed "listn_append"; + +val Nil_listn_case = listn.mk_cases " \\ listn(A)" +and Cons_listn_case = listn.mk_cases " \\ listn(A)"; + +val zero_listn_case = listn.mk_cases "<0,l> \\ listn(A)" +and succ_listn_case = listn.mk_cases " \\ listn(A)"; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/ListN.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/ListN.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,22 @@ +(* Title: ZF/ex/ListN + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of lists of n elements + +See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. +Research Report 92-49, LIP, ENS Lyon. Dec 1992. +*) + +ListN = Main + + +consts listn ::i=>i +inductive + domains "listn(A)" <= "nat*list(A)" + intrs + NilI "<0,Nil> \\ listn(A)" + ConsI "[| a \\ A; \\ listn(A) |] ==> \\ listn(A)" + type_intrs "nat_typechecks @ list.intrs" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Mutil.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Mutil.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,147 @@ +(* Title: ZF/ex/Mutil + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +The Mutilated Checkerboard Problem, formalized inductively +*) + +open Mutil; + + +(** Basic properties of evnodd **) + +Goalw [evnodd_def] ": evnodd(A,b) <-> : A & (i#+j) mod 2 = b"; +by (Blast_tac 1); +qed "evnodd_iff"; + +Goalw [evnodd_def] "evnodd(A, b) \\ A"; +by (Blast_tac 1); +qed "evnodd_subset"; + +(* Finite(X) ==> Finite(evnodd(X,b)) *) +bind_thm("Finite_evnodd", evnodd_subset RS subset_imp_lepoll RS lepoll_Finite); + +Goalw [evnodd_def] "evnodd(A Un B, b) = evnodd(A,b) Un evnodd(B,b)"; +by (simp_tac (simpset() addsimps [Collect_Un]) 1); +qed "evnodd_Un"; + +Goalw [evnodd_def] "evnodd(A - B, b) = evnodd(A,b) - evnodd(B,b)"; +by (simp_tac (simpset() addsimps [Collect_Diff]) 1); +qed "evnodd_Diff"; + +Goalw [evnodd_def] + "evnodd(cons(,C), b) = \ +\ (if (i#+j) mod 2 = b then cons(, evnodd(C,b)) else evnodd(C,b))"; +by (asm_simp_tac (simpset() addsimps [evnodd_def, Collect_cons]) 1); +qed "evnodd_cons"; + +Goalw [evnodd_def] "evnodd(0, b) = 0"; +by (simp_tac (simpset() addsimps [evnodd_def]) 1); +qed "evnodd_0"; + +Addsimps [evnodd_cons, evnodd_0]; + +(*** Dominoes ***) + +Goal "d \\ domino ==> Finite(d)"; +by (blast_tac (claset() addSIs [Finite_cons, Finite_0] addEs [domino.elim]) 1); +qed "domino_Finite"; + +Goal "[| d \\ domino; b<2 |] ==> \\i' j'. evnodd(d,b) = {}"; +by (eresolve_tac [domino.elim] 1); +by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 2); +by (res_inst_tac [("k1", "i#+j")] (mod2_cases RS disjE) 1); +by (REPEAT_FIRST (ares_tac [add_type])); +(*Four similar cases: case (i#+j) mod 2 = b, 2#-b, ...*) +by (REPEAT (asm_simp_tac (simpset() addsimps [mod_succ, succ_neq_self]) 1 + THEN blast_tac (claset() addDs [ltD]) 1)); +qed "domino_singleton"; + + +(*** Tilings ***) + +(** The union of two disjoint tilings is a tiling **) + +Goal "t \\ tiling(A) ==> \ +\ u \\ tiling(A) --> t Int u = 0 --> t Un u \\ tiling(A)"; +by (etac tiling.induct 1); +by (simp_tac (simpset() addsimps tiling.intrs) 1); +by (asm_full_simp_tac (simpset() addsimps [Un_assoc, + subset_empty_iff RS iff_sym]) 1); +by (blast_tac (claset() addIs tiling.intrs) 1); +qed_spec_mp "tiling_UnI"; + +Goal "t \\ tiling(domino) ==> Finite(t)"; +by (eresolve_tac [tiling.induct] 1); +by (rtac Finite_0 1); +by (blast_tac (claset() addSIs [Finite_Un] addIs [domino_Finite]) 1); +qed "tiling_domino_Finite"; + +Goal "t \\ tiling(domino) ==> |evnodd(t,0)| = |evnodd(t,1)|"; +by (eresolve_tac [tiling.induct] 1); +by (simp_tac (simpset() addsimps [evnodd_def]) 1); +by (res_inst_tac [("b1","0")] (domino_singleton RS exE) 1); +by (Simp_tac 2 THEN assume_tac 1); +by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1); +by (Simp_tac 2 THEN assume_tac 1); +by Safe_tac; +by (subgoal_tac "\\p b. p \\ evnodd(a,b) --> p\\evnodd(t,b)" 1); +by (asm_simp_tac + (simpset() addsimps [evnodd_Un, Un_cons, tiling_domino_Finite, + evnodd_subset RS subset_Finite, + Finite_imp_cardinal_cons]) 1); +by (blast_tac (claset() addSDs [evnodd_subset RS subsetD] + addEs [equalityE]) 1); +qed "tiling_domino_0_1"; + +Goal "[| i \\ nat; n \\ nat |] ==> {i} * (n #+ n) \\ tiling(domino)"; +by (induct_tac "n" 1); +by (simp_tac (simpset() addsimps tiling.intrs) 1); +by (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_succ2]) 1); +by (resolve_tac tiling.intrs 1); +by (assume_tac 2); +by (rename_tac "n'" 1); +by (subgoal_tac (*seems the easiest way of turning one to the other*) + "{i}*{succ(n'#+n')} Un {i}*{n'#+n'} = {, }" 1); +by (Blast_tac 2); +by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1); +by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 1); +qed "dominoes_tile_row"; + +Goal "[| m \\ nat; n \\ nat |] ==> m * (n #+ n) \\ tiling(domino)"; +by (induct_tac "m" 1); +by (simp_tac (simpset() addsimps tiling.intrs) 1); +by (asm_simp_tac (simpset() addsimps [Sigma_succ1]) 1); +by (blast_tac (claset() addIs [tiling_UnI, dominoes_tile_row] + addEs [mem_irrefl]) 1); +qed "dominoes_tile_matrix"; + +Goal "[| x=y; x P"; +by Auto_tac; +qed "eq_lt_E"; + +Goal "[| m \\ nat; n \\ nat; \ +\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \ +\ t' = t - {<0,0>} - {} |] \ +\ ==> t' \\ tiling(domino)"; +by (rtac notI 1); +by (dtac tiling_domino_0_1 1); +by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1); +by (subgoal_tac "t \\ tiling(domino)" 1); +(*Requires a small simpset that won't move the succ applications*) +by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type, + dominoes_tile_matrix]) 2); +by (asm_full_simp_tac + (simpset() addsimps [evnodd_Diff, mod2_add_self, + mod2_succ_succ, tiling_domino_0_1 RS sym]) 1); +by (rtac lt_trans 1); +by (REPEAT + (rtac Finite_imp_cardinal_Diff 1 + THEN + asm_simp_tac (simpset() addsimps [tiling_domino_Finite, Finite_evnodd, + Finite_Diff]) 1 + THEN + asm_simp_tac (simpset() addsimps [evnodd_iff, nat_0_le RS ltD, + mod2_add_self]) 1)); +qed "mutil_not_tiling"; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Mutil.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Mutil.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,36 @@ +(* Title: ZF/ex/Mutil + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +The Mutilated Chess Board Problem, formalized inductively + Originator is Max Black, according to J A Robinson. + Popularized as the Mutilated Checkerboard Problem by J McCarthy +*) + +Mutil = Main + +consts + domino :: i + tiling :: i=>i + +inductive + domains "domino" <= "Pow(nat*nat)" + intrs + horiz "[| i \\ nat; j \\ nat |] ==> {, } \\ domino" + vertl "[| i \\ nat; j \\ nat |] ==> {, } \\ domino" + type_intrs empty_subsetI, cons_subsetI, PowI, SigmaI, nat_succI + + +inductive + domains "tiling(A)" <= "Pow(Union(A))" + intrs + empty "0 \\ tiling(A)" + Un "[| a \\ A; t \\ tiling(A); a Int t = 0 |] ==> a Un t \\ tiling(A)" + type_intrs empty_subsetI, Union_upper, Un_least, PowI + type_elims "[make_elim PowD]" + +constdefs + evnodd :: [i,i]=>i + "evnodd(A,b) == {z \\ A. \\i j. z= & (i#+j) mod 2 = b}" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Primrec.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Primrec.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,297 @@ +(* Title: ZF/ex/Primrec + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions + +Proof adopted from +Nora Szasz, +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. + +See also E. Mendelson, Introduction to Mathematical Logic. +(Van Nostrand, 1964), page 250, exercise 11. +*) + +(*** Inductive definition of the PR functions ***) + +(* c \\ prim_rec ==> c \\ list(nat) -> nat *) +val prim_rec_into_fun = prim_rec.dom_subset RS subsetD; + +AddTCs ([prim_rec_into_fun] @ prim_rec.intrs); + +Goal "i \\ nat ==> ACK(i): prim_rec"; +by (induct_tac "i" 1); +by (ALLGOALS Asm_simp_tac); +qed "ACK_in_prim_rec"; + +AddTCs [ACK_in_prim_rec, prim_rec_into_fun RS apply_type, + list_add_type, nat_into_Ord, rec_type]; + +Goal "[| i \\ nat; j \\ nat |] ==> ack(i,j): nat"; +by Auto_tac; +qed "ack_type"; +AddTCs [ack_type]; + +(** Ackermann's function cases **) + +(*PROPERTY A 1*) +Goal "j \\ nat ==> ack(0,j) = succ(j)"; +by (asm_simp_tac (simpset() addsimps [SC]) 1); +qed "ack_0"; + +(*PROPERTY A 2*) +Goal "ack(succ(i), 0) = ack(i,1)"; +by (asm_simp_tac (simpset() addsimps [CONST,PREC_0]) 1); +qed "ack_succ_0"; + +(*PROPERTY A 3*) +Goal "[| i \\ nat; j \\ nat |] \ +\ ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"; +by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1); +qed "ack_succ_succ"; + +Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type]; +Delsimps [ACK_0, ACK_succ]; + + +(*PROPERTY A 4*) +Goal "i \\ nat ==> \\j \\ nat. j < ack(i,j)"; +by (induct_tac "i" 1); +by (Asm_simp_tac 1); +by (rtac ballI 1); +by (induct_tac "j" 1); +by (etac (succ_leI RS lt_trans1) 2); +by (rtac (nat_0I RS nat_0_le RS lt_trans) 1); +by Auto_tac; +qed_spec_mp "lt_ack2"; + +(*PROPERTY A 5-, the single-step lemma*) +Goal "[| i \\ nat; j \\ nat |] ==> ack(i,j) < ack(i, succ(j))"; +by (induct_tac "i" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack2]))); +qed "ack_lt_ack_succ2"; + +(*PROPERTY A 5, monotonicity for < *) +Goal "[| j nat; k \\ nat |] ==> ack(i,j) < ack(i,k)"; +by (ftac lt_nat_in_nat 1 THEN assume_tac 1); +by (etac succ_lt_induct 1); +by (assume_tac 1); +by (rtac lt_trans 2); +by (auto_tac (claset() addIs [ack_lt_ack_succ2], simpset())); +qed "ack_lt_mono2"; + +(*PROPERTY A 5', monotonicity for le *) +Goal "[| j le k; i \\ nat; k \\ nat |] ==> ack(i,j) le ack(i,k)"; +by (res_inst_tac [("f", "%j. ack(i,j)")] Ord_lt_mono_imp_le_mono 1); +by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1)); +qed "ack_le_mono2"; + +(*PROPERTY A 6*) +Goal "[| i \\ nat; j \\ nat |] ==> ack(i, succ(j)) le ack(succ(i), j)"; +by (induct_tac "j" 1); +by (ALLGOALS Asm_simp_tac); +by (rtac ack_le_mono2 1); +by (rtac (lt_ack2 RS succ_leI RS le_trans) 1); +by Auto_tac; +qed "ack2_le_ack1"; + +(*PROPERTY A 7-, the single-step lemma*) +Goal "[| i \\ nat; j \\ nat |] ==> ack(i,j) < ack(succ(i),j)"; +by (rtac (ack_lt_mono2 RS lt_trans2) 1); +by (rtac ack2_le_ack1 4); +by Auto_tac; +qed "ack_lt_ack_succ1"; + +(*PROPERTY A 7, monotonicity for < *) +Goal "[| i nat; k \\ nat |] ==> ack(i,k) < ack(j,k)"; +by (ftac lt_nat_in_nat 1 THEN assume_tac 1); +by (etac succ_lt_induct 1); +by (assume_tac 1); +by (rtac lt_trans 2); +by (auto_tac (claset() addIs [ack_lt_ack_succ1], simpset())); +qed "ack_lt_mono1"; + +(*PROPERTY A 7', monotonicity for le *) +Goal "[| i le j; j \\ nat; k \\ nat |] ==> ack(i,k) le ack(j,k)"; +by (res_inst_tac [("f", "%j. ack(j,k)")] Ord_lt_mono_imp_le_mono 1); +by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1)); +qed "ack_le_mono1"; + +(*PROPERTY A 8*) +Goal "j \\ nat ==> ack(1,j) = succ(succ(j))"; +by (induct_tac "j" 1); +by (ALLGOALS Asm_simp_tac); +qed "ack_1"; + +(*PROPERTY A 9*) +Goal "j \\ nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"; +by (induct_tac "j" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [ack_1, add_succ_right]))); +qed "ack_2"; + +(*PROPERTY A 10*) +Goal "[| i1 \\ nat; i2 \\ nat; j \\ nat |] ==> \ +\ ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"; +by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1); +by (Asm_simp_tac 1); +by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1); +by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 4); +by Auto_tac; +qed "ack_nest_bound"; + +(*PROPERTY A 11*) +Goal "[| i1 \\ nat; i2 \\ nat; j \\ nat |] ==> \ +\ ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"; +by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1); +by (asm_simp_tac (simpset() addsimps [ack_2]) 1); +by (rtac (ack_nest_bound RS lt_trans2) 2); +by (Asm_simp_tac 5); +by (rtac (add_le_mono RS leI RS leI) 1); +by (auto_tac (claset() addIs [add_le_self, add_le_self2, ack_le_mono1], + simpset())); +qed "ack_add_bound"; + +(*PROPERTY A 12. Article uses existential quantifier but the ALF proof + used k#+4. Quantified version must be nested \\k'. \\i,j... *) +Goal "[| i < ack(k,j); j \\ nat; k \\ nat |] ==> \ +\ i#+j < ack(succ(succ(succ(succ(k)))), j)"; +by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1); +by (rtac (ack_add_bound RS lt_trans2) 2); +by (rtac add_lt_mono 1); +by Auto_tac; +qed "ack_add_bound2"; + +(*** MAIN RESULT ***) + +Addsimps [list_add_type]; + +Goalw [SC_def] "l \\ list(nat) ==> SC ` l < ack(1, list_add(l))"; +by (exhaust_tac "l" 1); +by (asm_simp_tac (simpset() addsimps [succ_iff]) 1); +by (asm_simp_tac (simpset() addsimps [ack_1, add_le_self]) 1); +qed "SC_case"; + +(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*) +Goal "[| i \\ nat; j \\ nat |] ==> i < ack(i,j)"; +by (induct_tac "i" 1); +by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1); +by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1); +by Auto_tac; +qed "lt_ack1"; + +Goalw [CONST_def] + "[| l \\ list(nat); k \\ nat |] ==> CONST(k) ` l < ack(k, list_add(l))"; +by (asm_simp_tac (simpset() addsimps [lt_ack1]) 1); +qed "CONST_case"; + +Goalw [PROJ_def] + "l \\ list(nat) ==> \\i \\ nat. PROJ(i) ` l < ack(0, list_add(l))"; +by (Asm_simp_tac 1); +by (etac list.induct 1); +by (asm_simp_tac (simpset() addsimps [nat_0_le]) 1); +by (Asm_simp_tac 1); +by (rtac ballI 1); +by (eres_inst_tac [("n","x")] natE 1); +by (asm_simp_tac (simpset() addsimps [add_le_self]) 1); +by (Asm_simp_tac 1); +by (etac (bspec RS lt_trans2) 1); +by (rtac (add_le_self2 RS succ_leI) 2); +by Auto_tac; +qed_spec_mp "PROJ_case"; + +(** COMP case **) + +Goal "fs \\ list({f \\ prim_rec . \ +\ \\kf \\ nat. \\l \\ list(nat). \ +\ f`l < ack(kf, list_add(l))}) \ +\ ==> \\k \\ nat. \\l \\ list(nat). \ +\ list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))"; +by (etac list.induct 1); +by (res_inst_tac [("x","0")] bexI 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_ack1, nat_0_le]))); +by (Clarify_tac 1); +by (rtac (ballI RS bexI) 1); +by (rtac (add_lt_mono RS lt_trans) 1); +by (REPEAT (FIRSTGOAL (etac bspec))); +by (rtac ack_add_bound 5); +by Auto_tac; +qed "COMP_map_lemma"; + +Goalw [COMP_def] + "[| kg: nat; \ +\ \\l \\ list(nat). g`l < ack(kg, list_add(l)); \ +\ fs \\ list({f \\ prim_rec . \ +\ \\kf \\ nat. \\l \\ list(nat). \ +\ f`l < ack(kf, list_add(l))}) \ +\ |] ==> \\k \\ nat. \\l \\ list(nat). COMP(g,fs)`l < ack(k, list_add(l))"; +by (Asm_simp_tac 1); +by (ftac list_CollectD 1); +by (etac (COMP_map_lemma RS bexE) 1); +by (rtac (ballI RS bexI) 1); +by (etac (bspec RS lt_trans) 1); +by (rtac lt_trans 2); +by (rtac ack_nest_bound 3); +by (etac (bspec RS ack_lt_mono2) 2); +by Auto_tac; +qed "COMP_case"; + +(** PREC case **) + +Goalw [PREC_def] + "[| \\l \\ list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \ +\ \\l \\ list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \ +\ f \\ prim_rec; kf: nat; \ +\ g \\ prim_rec; kg: nat; \ +\ l \\ list(nat) \ +\ |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"; +by (exhaust_tac "l" 1); +by (asm_simp_tac (simpset() addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1); +by (Asm_simp_tac 1); +by (etac ssubst 1); (*get rid of the needless assumption*) +by (induct_tac "a" 1); +(*base case*) +by (EVERY1 [Asm_simp_tac, rtac lt_trans, etac bspec, + assume_tac, rtac (add_le_self RS ack_lt_mono1)]); +by (ALLGOALS Asm_simp_tac); +(*ind step*) +by (rtac (succ_leI RS lt_trans1) 1); +by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1); +by (etac bspec 2); +by (rtac (nat_le_refl RS add_le_mono) 1); +by Typecheck_tac; +by (asm_simp_tac (simpset() addsimps [add_le_self2]) 1); +(*final part of the simplification*) +by (Asm_simp_tac 1); +by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1); +by (etac ack_lt_mono2 4); +by Auto_tac; +qed "PREC_case_lemma"; + +Goal "[| f \\ prim_rec; kf: nat; \ +\ g \\ prim_rec; kg: nat; \ +\ \\l \\ list(nat). f`l < ack(kf, list_add(l)); \ +\ \\l \\ list(nat). g`l < ack(kg, list_add(l)) \ +\ |] ==> \\k \\ nat. \\l \\ list(nat). PREC(f,g)`l< ack(k, list_add(l))"; +by (rtac (ballI RS bexI) 1); +by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1); +by (REPEAT_FIRST (rtac (ack_add_bound2 RS ballI) THEN' etac bspec)); +by Typecheck_tac; +qed "PREC_case"; + +Goal "f \\ prim_rec ==> \\k \\ nat. \\l \\ list(nat). f`l < ack(k, list_add(l))"; +by (etac prim_rec.induct 1); +by (auto_tac (claset() addIs [SC_case, CONST_case, PROJ_case, COMP_case, + PREC_case], + simpset())); +qed "ack_bounds_prim_rec"; + +Goal "~ (\\l \\ list(nat). list_case(0, %x xs. ack(x,x), l)) \\ prim_rec"; +by (rtac notI 1); +by (etac (ack_bounds_prim_rec RS bexE) 1); +by (rtac lt_irrefl 1); +by (dres_inst_tac [("x", "[x]")] bspec 1); +by Auto_tac; +qed "ack_not_prim_rec"; + diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Primrec.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Primrec.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,35 @@ +(* Title: ZF/ex/Primrec.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions: the inductive definition + +Proof adopted from +Nora Szasz, +A Machine Checked Proof that Ackermann's Function is not Primitive Recursive, +In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338. + +See also E. Mendelson, Introduction to Mathematical Logic. +(Van Nostrand, 1964), page 250, exercise 11. +*) + +Primrec = Primrec_defs + +consts + prim_rec :: i + +inductive + domains "prim_rec" <= "list(nat)->nat" + intrs + SC "SC \\ prim_rec" + CONST "k \\ nat ==> CONST(k) \\ prim_rec" + PROJ "i \\ nat ==> PROJ(i) \\ prim_rec" + COMP "[| g \\ prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec" + PREC "[| f \\ prim_rec; g \\ prim_rec |] ==> PREC(f,g): prim_rec" + monos list_mono + con_defs SC_def, CONST_def, PROJ_def, COMP_def, PREC_def + type_intrs "nat_typechecks @ list.intrs @ + [lam_type, list_case_type, drop_type, map_type, + apply_type, rec_type]" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Primrec_defs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Primrec_defs.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,40 @@ +(* Title: ZF/ex/Primrec + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions: preliminary definitions +*) + +(*Theory TF redeclares map_type*) +val map_type = thm "List.map_type"; + +(** Useful special cases of evaluation ***) + +Goalw [SC_def] "[| x \\ nat; l \\ list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"; +by (Asm_simp_tac 1); +qed "SC"; + +Goalw [CONST_def] "[| l \\ list(nat) |] ==> CONST(k) ` l = k"; +by (Asm_simp_tac 1); +qed "CONST"; + +Goalw [PROJ_def] "[| x \\ nat; l \\ list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"; +by (Asm_simp_tac 1); +qed "PROJ_0"; + +Goalw [COMP_def] "[| l \\ list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]"; +by (Asm_simp_tac 1); +qed "COMP_1"; + +Goalw [PREC_def] "l \\ list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"; +by (Asm_simp_tac 1); +qed "PREC_0"; + +Goalw [PREC_def] + "[| x \\ nat; l \\ list(nat) |] ==> \ +\ PREC(f,g) ` (Cons(succ(x),l)) = \ +\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"; +by (Asm_simp_tac 1); +qed "PREC_succ"; + diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Primrec_defs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Primrec_defs.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,46 @@ +(* Title: ZF/ex/Primrec_defs.thy + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Primitive Recursive Functions: preliminary definitions of the constructors + +[These must reside in a separate theory in order to be visible in the + con_defs part of prim_rec's inductive definition.] +*) + +Primrec_defs = Main + + +consts + SC :: i + CONST :: i=>i + PROJ :: i=>i + COMP :: [i,i]=>i + PREC :: [i,i]=>i + ACK :: i=>i + ack :: [i,i]=>i + +translations + "ack(x,y)" == "ACK(x) ` [y]" + +defs + + SC_def "SC == \\l \\ list(nat).list_case(0, %x xs. succ(x), l)" + + CONST_def "CONST(k) == \\l \\ list(nat).k" + + PROJ_def "PROJ(i) == \\l \\ list(nat). list_case(0, %x xs. x, drop(i,l))" + + COMP_def "COMP(g,fs) == \\l \\ list(nat). g ` List.map(%f. f`l, fs)" + + (*Note that g is applied first to PREC(f,g)`y and then to y!*) + PREC_def "PREC(f,g) == + \\l \\ list(nat). list_case(0, + %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)" + +primrec + ACK_0 "ACK(0) = SC" + ACK_succ "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]), + COMP(ACK(i), [PROJ(0)]))" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/PropLog.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/PropLog.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,249 @@ +(* Title: ZF/ex/prop-log.ML + ID: $Id$ + Author: Tobias Nipkow & Lawrence C Paulson + Copyright 1992 University of Cambridge + +Inductive definition of propositional logic. +Soundness and completeness w.r.t. truth-tables. + +Prove: If H|=p then G|=p where G \\ Fin(H) +*) + +Addsimps prop.intrs; + +(*** Semantics of propositional logic ***) + +(** The function is_true **) + +Goalw [is_true_def] "is_true(Fls,t) <-> False"; +by (Simp_tac 1); +qed "is_true_Fls"; + +Goalw [is_true_def] "is_true(#v,t) <-> v \\ t"; +by (Simp_tac 1); +qed "is_true_Var"; + +Goalw [is_true_def] "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"; +by (Simp_tac 1); +qed "is_true_Imp"; + +Addsimps [is_true_Fls, is_true_Var, is_true_Imp]; + + +(*** Proof theory of propositional logic ***) + +Goalw thms.defs "G \\ H ==> thms(G) \\ thms(H)"; +by (rtac lfp_mono 1); +by (REPEAT (rtac thms.bnd_mono 1)); +by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); +qed "thms_mono"; + +val thms_in_pl = thms.dom_subset RS subsetD; + +val ImpE = prop.mk_cases "p=>q \\ prop"; + +(*Stronger Modus Ponens rule: no typechecking!*) +Goal "[| H |- p=>q; H |- p |] ==> H |- q"; +by (rtac thms.MP 1); +by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1)); +qed "thms_MP"; + +(*Rule is called I for Identity Combinator, not for Introduction*) +Goal "p \\ prop ==> H |- p=>p"; +by (rtac (thms.S RS thms_MP RS thms_MP) 1); +by (rtac thms.K 5); +by (rtac thms.K 4); +by (REPEAT (ares_tac prop.intrs 1)); +qed "thms_I"; + +(** Weakening, left and right **) + +(* [| G \\ H; G|-p |] ==> H|-p Order of premises is convenient with RS*) +bind_thm ("weaken_left", (thms_mono RS subsetD)); + +(* H |- p ==> cons(a,H) |- p *) +val weaken_left_cons = subset_consI RS weaken_left; + +val weaken_left_Un1 = Un_upper1 RS weaken_left; +val weaken_left_Un2 = Un_upper2 RS weaken_left; + +Goal "[| H |- q; p \\ prop |] ==> H |- p=>q"; +by (rtac (thms.K RS thms_MP) 1); +by (REPEAT (ares_tac [thms_in_pl] 1)); +qed "weaken_right"; + +(*The deduction theorem*) +Goal "[| cons(p,H) |- q; p \\ prop |] ==> H |- p=>q"; +by (etac thms.induct 1); +by (blast_tac (claset() addIs [thms_I, thms.H RS weaken_right]) 1); +by (blast_tac (claset() addIs [thms.K RS weaken_right]) 1); +by (blast_tac (claset() addIs [thms.S RS weaken_right]) 1); +by (blast_tac (claset() addIs [thms.DN RS weaken_right]) 1); +by (blast_tac (claset() addIs [thms.S RS thms_MP RS thms_MP]) 1); +qed "deduction"; + + +(*The cut rule*) +Goal "[| H|-p; cons(p,H) |- q |] ==> H |- q"; +by (rtac (deduction RS thms_MP) 1); +by (REPEAT (ares_tac [thms_in_pl] 1)); +qed "cut"; + +Goal "[| H |- Fls; p \\ prop |] ==> H |- p"; +by (rtac (thms.DN RS thms_MP) 1); +by (rtac weaken_right 2); +by (REPEAT (ares_tac (prop.intrs@[consI1]) 1)); +qed "thms_FlsE"; + +(* [| H |- p=>Fls; H |- p; q \\ prop |] ==> H |- q *) +bind_thm ("thms_notE", (thms_MP RS thms_FlsE)); + +(*Soundness of the rules wrt truth-table semantics*) +Goalw [logcon_def] "H |- p ==> H |= p"; +by (etac thms.induct 1); +by Auto_tac; +qed "soundness"; + +(*** Towards the completeness proof ***) + +val [premf,premq] = goal PropLog.thy + "[| H |- p=>Fls; q \\ prop |] ==> H |- p=>q"; +by (rtac (premf RS thms_in_pl RS ImpE) 1); +by (rtac deduction 1); +by (rtac (premf RS weaken_left_cons RS thms_notE) 1); +by (REPEAT (ares_tac [premq, consI1, thms.H] 1)); +qed "Fls_Imp"; + +val [premp,premq] = goal PropLog.thy + "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls"; +by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1); +by (etac ImpE 1); +by (rtac deduction 1); +by (rtac (premq RS weaken_left_cons RS thms_MP) 1); +by (rtac (consI1 RS thms.H RS thms_MP) 1); +by (rtac (premp RS weaken_left_cons) 2); +by (REPEAT (ares_tac prop.intrs 1)); +qed "Imp_Fls"; + +(*Typical example of strengthening the induction formula*) +Goal "p \\ prop ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"; +by (Simp_tac 1); +by (induct_tac "p" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [thms_I, thms.H]))); +by (safe_tac (claset() addSEs [Fls_Imp RS weaken_left_Un1, + Fls_Imp RS weaken_left_Un2])); +by (ALLGOALS (blast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, + weaken_right, Imp_Fls]))); +qed "hyps_thms_if"; + +(*Key lemma for completeness; yields a set of assumptions satisfying p*) +Goalw [logcon_def] "[| p \\ prop; 0 |= p |] ==> hyps(p,t) |- p"; +by (dtac hyps_thms_if 1); +by (Asm_full_simp_tac 1); +qed "logcon_thms_p"; + +(*For proving certain theorems in our new propositional logic*) +val thms_cs = + ZF_cs addSIs (prop.intrs @ [deduction]) + addIs [thms_in_pl, thms.H, thms.H RS thms_MP]; + +(*The excluded middle in the form of an elimination rule*) +Goal "[| p \\ prop; q \\ prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"; +by (rtac (deduction RS deduction) 1); +by (rtac (thms.DN RS thms_MP) 1); +by (ALLGOALS (blast_tac thms_cs)); +qed "thms_excluded_middle"; + +(*Hard to prove directly because it requires cuts*) +Goal "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \\ prop |] ==> H |- q"; +by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1); +by (REPEAT (ares_tac (prop.intrs@[deduction,thms_in_pl]) 1)); +qed "thms_excluded_middle_rule"; + +(*** Completeness -- lemmas for reducing the set of assumptions ***) + +(*For the case hyps(p,t)-cons(#v,Y) |- p; + we also have hyps(p,t)-{#v} \\ hyps(p, t-{v}) *) +Goal "p \\ prop ==> hyps(p, t-{v}) \\ cons(#v=>Fls, hyps(p,t)-{#v})"; +by (induct_tac "p" 1); +by Auto_tac; +qed "hyps_Diff"; + +(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p; + we also have hyps(p,t)-{#v=>Fls} \\ hyps(p, cons(v,t)) *) +Goal "p \\ prop ==> hyps(p, cons(v,t)) \\ cons(#v, hyps(p,t)-{#v=>Fls})"; +by (induct_tac "p" 1); +by Auto_tac; +qed "hyps_cons"; + +(** Two lemmas for use with weaken_left **) + +Goal "B-C \\ cons(a, B-cons(a,C))"; +by (Fast_tac 1); +qed "cons_Diff_same"; + +Goal "cons(a, B-{c}) - D \\ cons(a, B-cons(c,D))"; +by (Fast_tac 1); +qed "cons_Diff_subset2"; + +(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls; + could probably prove the stronger hyps(p,t) \\ Fin(hyps(p,0) Un hyps(p,nat))*) +Goal "p \\ prop ==> hyps(p,t) \\ Fin(\\v \\ nat. {#v, #v=>Fls})"; +by (induct_tac "p" 1); +by Auto_tac; +qed "hyps_finite"; + +val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left; + +(*Induction on the finite set of assumptions hyps(p,t0). + We may repeatedly subtract assumptions until none are left!*) +val [premp,sat] = goal PropLog.thy + "[| p \\ prop; 0 |= p |] ==> \\t. hyps(p,t) - hyps(p,t0) |- p"; +by (rtac (premp RS hyps_finite RS Fin_induct) 1); +by (simp_tac (simpset() addsimps [premp, sat, logcon_thms_p, Diff_0]) 1); +by Safe_tac; +(*Case hyps(p,t)-cons(#v,Y) |- p *) +by (rtac thms_excluded_middle_rule 1); +by (etac prop.Var_I 3); +by (rtac (cons_Diff_same RS weaken_left) 1); +by (etac spec 1); +by (rtac (cons_Diff_subset2 RS weaken_left) 1); +by (rtac (premp RS hyps_Diff RS Diff_weaken_left) 1); +by (etac spec 1); +(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *) +by (rtac thms_excluded_middle_rule 1); +by (etac prop.Var_I 3); +by (rtac (cons_Diff_same RS weaken_left) 2); +by (etac spec 2); +by (rtac (cons_Diff_subset2 RS weaken_left) 1); +by (rtac (premp RS hyps_cons RS Diff_weaken_left) 1); +by (etac spec 1); +qed "completeness_0_lemma"; + +(*The base case for completeness*) +val [premp,sat] = goal PropLog.thy "[| p \\ prop; 0 |= p |] ==> 0 |- p"; +by (rtac (Diff_cancel RS subst) 1); +by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1); +qed "completeness_0"; + +(*A semantic analogue of the Deduction Theorem*) +Goalw [logcon_def] "[| cons(p,H) |= q |] ==> H |= p=>q"; +by Auto_tac; +qed "logcon_Imp"; + +Goal "H \\ Fin(prop) ==> \\p \\ prop. H |= p --> H |- p"; +by (etac Fin_induct 1); +by (safe_tac (claset() addSIs [completeness_0])); +by (rtac (weaken_left_cons RS thms_MP) 1); +by (blast_tac (claset() addSIs (logcon_Imp::prop.intrs)) 1); +by (blast_tac thms_cs 1); +qed "completeness_lemma"; + +val completeness = completeness_lemma RS bspec RS mp; + +val [finite] = goal PropLog.thy "H \\ Fin(prop) ==> H |- p <-> H |= p & p \\ prop"; +by (fast_tac (claset() addSEs [soundness, finite RS completeness, + thms_in_pl]) 1); +qed "thms_iff"; + +writeln"Reached end of file."; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/PropLog.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/PropLog.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,68 @@ +(* Title: ZF/ex/PropLog.thy + ID: $Id$ + Author: Tobias Nipkow & Lawrence C Paulson + Copyright 1993 University of Cambridge + +Datatype definition of propositional logic formulae and inductive definition +of the propositional tautologies. +*) + +PropLog = Main + + +(** The datatype of propositions; note mixfix syntax **) +consts + prop :: i + +datatype + "prop" = Fls + | Var ("n \\ nat") ("#_" [100] 100) + | "=>" ("p \\ prop", "q \\ prop") (infixr 90) + +(** The proof system **) +consts + thms :: i => i + +syntax + "|-" :: [i,i] => o (infixl 50) + +translations + "H |- p" == "p \\ thms(H)" + +inductive + domains "thms(H)" <= "prop" + intrs + H "[| p \\ H; p \\ prop |] ==> H |- p" + K "[| p \\ prop; q \\ prop |] ==> H |- p=>q=>p" + S "[| p \\ prop; q \\ prop; r \\ prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r" + DN "p \\ prop ==> H |- ((p=>Fls) => Fls) => p" + MP "[| H |- p=>q; H |- p; p \\ prop; q \\ prop |] ==> H |- q" + type_intrs "prop.intrs" + + +(** The semantics **) +consts + "|=" :: [i,i] => o (infixl 50) + hyps :: [i,i] => i + is_true_fun :: [i,i] => i + +constdefs (*this definitionis necessary since predicates can't be recursive*) + is_true :: [i,i] => o + "is_true(p,t) == is_true_fun(p,t)=1" + +defs + (*Logical consequence: for every valuation, if all elements of H are true + then so is p*) + logcon_def "H |= p == \\t. (\\q \\ H. is_true(q,t)) --> is_true(p,t)" + +primrec (** A finite set of hypotheses from t and the Vars in p **) + "hyps(Fls, t) = 0" + "hyps(Var(v), t) = (if v \\ t then {#v} else {#v=>Fls})" + "hyps(p=>q, t) = hyps(p,t) Un hyps(q,t)" + +primrec (** Semantics of propositional logic **) + "is_true_fun(Fls, t) = 0" + "is_true_fun(Var(v), t) = (if v \\ t then 1 else 0)" + "is_true_fun(p=>q, t) = (if is_true_fun(p,t)=1 then is_true_fun(q,t) + else 1)" + +end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Rmap.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Rmap.ML Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,56 @@ +(* Title: ZF/ex/Rmap + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of an operator to "map" a relation over a list +*) + +Goalw rmap.defs "r \\ s ==> rmap(r) \\ rmap(s)"; +by (rtac lfp_mono 1); +by (REPEAT (rtac rmap.bnd_mono 1)); +by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @ + basic_monos) 1)); +qed "rmap_mono"; + +val Nil_rmap_case = rmap.mk_cases " \\ rmap(r)" +and Cons_rmap_case = rmap.mk_cases " \\ rmap(r)"; + +AddIs rmap.intrs; +AddSEs [Nil_rmap_case, Cons_rmap_case]; + +Goal "r \\ A*B ==> rmap(r) \\ list(A)*list(B)"; +by (rtac (rmap.dom_subset RS subset_trans) 1); +by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset, + Sigma_mono, list_mono] 1)); +qed "rmap_rel_type"; + +Goal "A \\ domain(r) ==> list(A) \\ domain(rmap(r))"; +by (rtac subsetI 1); +by (etac list.induct 1); +by (ALLGOALS Fast_tac); +qed "rmap_total"; + +Goalw [function_def] "function(r) ==> function(rmap(r))"; +by (rtac (impI RS allI RS allI) 1); +by (etac rmap.induct 1); +by (ALLGOALS Fast_tac); +qed "rmap_functional"; + + +(** If f is a function then rmap(f) behaves as expected. **) + +Goal "f \\ A->B ==> rmap(f): list(A)->list(B)"; +by (asm_full_simp_tac (simpset() addsimps [Pi_iff, rmap_rel_type, + rmap_functional, rmap_total]) 1); +qed "rmap_fun_type"; + +Goalw [apply_def] "rmap(f)`Nil = Nil"; +by (Blast_tac 1); +qed "rmap_Nil"; + +Goal "[| f \\ A->B; x \\ A; xs: list(A) |] \ +\ ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"; +by (rtac apply_equality 1); +by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1)); +qed "rmap_Cons"; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/Induct/Rmap.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/Induct/Rmap.thy Wed Nov 07 12:29:07 2001 +0100 @@ -0,0 +1,25 @@ +(* Title: ZF/ex/Rmap + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1994 University of Cambridge + +Inductive definition of an operator to "map" a relation over a list +*) + +Rmap = Main + + +consts + rmap :: i=>i + +inductive + domains "rmap(r)" <= "list(domain(r))*list(range(r))" + intrs + NilI " \\ rmap(r)" + + ConsI "[| : r; \\ rmap(r) |] ==> + \\ rmap(r)" + + type_intrs "[domainI,rangeI] @ list.intrs" + +end + diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Wed Nov 07 00:16:19 2001 +0100 +++ b/src/ZF/IsaMakefile Wed Nov 07 12:29:07 2001 +0100 @@ -10,7 +10,7 @@ images: ZF #Note: keep targets sorted -test: ZF-AC ZF-Coind ZF-ex ZF-IMP ZF-Resid ZF-UNITY +test: ZF-AC ZF-Coind ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex all: images test @@ -84,24 +84,6 @@ @$(ISATOOL) usedir $(OUT)/ZF Coind -## ZF-ex - -ZF-ex: ZF $(LOG)/ZF-ex.gz - -$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ - ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ - ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \ - ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ - ex/LList.ML ex/LList.thy \ - ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ - ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ - ex/NatSum.ML ex/NatSum.thy ex/Primrec_defs.ML ex/Primrec_defs.thy \ - ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ - ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ - ex/Term.ML ex/Term.thy ex/misc.thy - @$(ISATOOL) usedir $(OUT)/ZF ex - - ## ZF-IMP ZF-IMP: ZF $(LOG)/ZF-IMP.gz @@ -138,6 +120,34 @@ @$(ISATOOL) usedir $(OUT)/ZF UNITY +## ZF-Induct + +ZF-Induct: ZF $(LOG)/ZF-Induct.gz + +$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \ + Induct/Comb.ML Induct/Comb.thy \ + Induct/ListN.ML Induct/ListN.thy Induct/Mutil.ML Induct/Mutil.thy\ + Induct/Primrec_defs.ML Induct/Primrec_defs.thy\ + Induct/Primrec.ML Induct/Primrec.thy\ + Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy + @$(ISATOOL) usedir $(OUT)/ZF Induct + +## ZF-ex + +ZF-ex: ZF $(LOG)/ZF-ex.gz + +$(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML ex/BT.ML ex/BT.thy \ + ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ + ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \ + ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ + ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy\ + ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy\ + ex/NatSum.ML ex/NatSum.thy \ + ex/Ramsey.ML ex/Ramsey.thy ex/TF.ML ex/TF.thy \ + ex/Term.ML ex/Term.thy ex/misc.thy + @$(ISATOOL) usedir $(OUT)/ZF ex + + ## clean clean: diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/ex/Acc.ML --- a/src/ZF/ex/Acc.ML Wed Nov 07 00:16:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,58 +0,0 @@ -(* Title: ZF/ex/acc - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Inductive definition of acc(r) - -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. -Research Report 92-49, LIP, ENS Lyon. Dec 1992. -*) - -(*The introduction rule must require a \\ field(r) - Otherwise acc(r) would be a proper class! *) - -(*The intended introduction rule*) -val prems = goal Acc.thy - "[| !!b. :r ==> b \\ acc(r); a \\ field(r) |] ==> a \\ acc(r)"; -by (fast_tac (claset() addIs prems@acc.intrs) 1); -qed "accI"; - -Goal "[| b \\ acc(r); : r |] ==> a \\ acc(r)"; -by (etac acc.elim 1); -by (Fast_tac 1); -qed "acc_downward"; - -val [major,indhyp] = goal Acc.thy - "[| a \\ acc(r); \ -\ !!x. [| x \\ acc(r); \\y. :r --> P(y) |] ==> P(x) \ -\ |] ==> P(a)"; -by (rtac (major RS acc.induct) 1); -by (rtac indhyp 1); -by (Fast_tac 2); -by (resolve_tac acc.intrs 1); -by (assume_tac 2); -by (etac (Collect_subset RS Pow_mono RS subsetD) 1); -qed "acc_induct"; - -Goal "wf[acc(r)](r)"; -by (rtac wf_onI2 1); -by (etac acc_induct 1); -by (Fast_tac 1); -qed "wf_on_acc"; - -(* field(r) \\ acc(r) ==> wf(r) *) -val acc_wfI = wf_on_acc RS wf_on_subset_A RS wf_on_field_imp_wf; - -val [major] = goal Acc.thy "wf(r) ==> field(r) \\ acc(r)"; -by (rtac subsetI 1); -by (etac (major RS wf_induct2) 1); -by (rtac subset_refl 1); -by (rtac accI 1); -by (assume_tac 2); -by (Fast_tac 1); -qed "acc_wfD"; - -Goal "wf(r) <-> field(r) \\ acc(r)"; -by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]); -qed "wf_acc_iff"; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/ex/Acc.thy --- a/src/ZF/ex/Acc.thy Wed Nov 07 00:16:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,23 +0,0 @@ -(* Title: ZF/ex/Acc.thy - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1994 University of Cambridge - -Inductive definition of acc(r) - -See Ch. Paulin-Mohring, Inductive Definitions in the System Coq. -Research Report 92-49, LIP, ENS Lyon. Dec 1992. -*) - -Acc = Main + - -consts - acc :: i=>i - -inductive - domains "acc(r)" <= "field(r)" - intrs - vimage "[| r-``{a}: Pow(acc(r)); a \\ field(r) |] ==> a \\ acc(r)" - monos Pow_mono - -end diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/ex/Comb.ML --- a/src/ZF/ex/Comb.ML Wed Nov 07 00:16:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,222 +0,0 @@ -(* Title: ZF/ex/comb.ML - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1993 University of Cambridge - -Combinatory Logic example: the Church-Rosser Theorem -Curiously, combinators do not include free variables. - -Example taken from - J. Camilleri and T. F. Melham. - Reasoning with Inductively Defined Relations in the HOL Theorem Prover. - Report 265, University of Cambridge Computer Laboratory, 1992. - -HOL system proofs may be found in -/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml -*) - -(*** Transitive closure preserves the Church-Rosser property ***) - -Goalw [diamond_def] - "!!x y r. [| diamond(r); :r^+ |] ==> \ -\ \\y'. :r --> (\\z. : r^+ & : r)"; -by (etac trancl_induct 1); -by (blast_tac (claset() addIs [r_into_trancl]) 1); -by (slow_best_tac (claset() addSDs [spec RS mp] - addIs [r_into_trancl, trans_trancl RS transD]) 1); -val diamond_strip_lemmaE = result() RS spec RS mp RS exE; - -val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)"; -by (rewtac diamond_def); (*unfold only in goal, not in premise!*) -by (rtac (impI RS allI RS allI) 1); -by (etac trancl_induct 1); -by (ALLGOALS (*Seems to be a brittle, undirected search*) - (slow_best_tac (claset() addIs [r_into_trancl, trans_trancl RS transD] - addEs [major RS diamond_strip_lemmaE]))); -qed "diamond_trancl"; - - -val [_,_,comb_Ap] = comb.intrs; -val Ap_E = comb.mk_cases "p#q \\ comb"; - -AddSIs comb.intrs; - - -(*** Results about Contraction ***) - -(*For type checking: replaces a-1->b by a,b \\ comb *) -val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2; -val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1; -val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2; - -Goal "field(contract) = comb"; -by (blast_tac (claset() addIs [contract.K] addSEs [contract_combE2]) 1); -qed "field_contract_eq"; - -bind_thm ("reduction_refl", - (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl)); - -bind_thm ("rtrancl_into_rtrancl2", - (r_into_rtrancl RS (trans_rtrancl RS transD))); - -AddSIs [reduction_refl, contract.K, contract.S]; - -val reduction_rls = [contract.K RS rtrancl_into_rtrancl2, - contract.S RS rtrancl_into_rtrancl2, - contract.Ap1 RS rtrancl_into_rtrancl2, - contract.Ap2 RS rtrancl_into_rtrancl2]; - -(*Example only: not used*) -Goalw [I_def] "p \\ comb ==> I#p ---> p"; -by (blast_tac (claset() addIs reduction_rls) 1); -qed "reduce_I"; - -Goalw [I_def] "I \\ comb"; -by (Blast_tac 1); -qed "comb_I"; - -(** Non-contraction results **) - -(*Derive a case for each combinator constructor*) -val K_contractE = contract.mk_cases "K -1-> r"; -val S_contractE = contract.mk_cases "S -1-> r"; -val Ap_contractE = contract.mk_cases "p#q -1-> r"; - -AddIs [contract.Ap1, contract.Ap2]; -AddSEs [K_contractE, S_contractE, Ap_contractE]; - -Goalw [I_def] "I -1-> r ==> P"; -by Auto_tac; -qed "I_contract_E"; - -Goal "K#p -1-> r ==> (\\q. r = K#q & p -1-> q)"; -by Auto_tac; -qed "K1_contractD"; - -Goal "[| p ---> q; r \\ comb |] ==> p#r ---> q#r"; -by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); -by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); -by (etac rtrancl_induct 1); -by (blast_tac (claset() addIs reduction_rls) 1); -by (etac (trans_rtrancl RS transD) 1); -by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1); -qed "Ap_reduce1"; - -Goal "[| p ---> q; r \\ comb |] ==> r#p ---> r#q"; -by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); -by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); -by (etac rtrancl_induct 1); -by (blast_tac (claset() addIs reduction_rls) 1); -by (etac (trans_rtrancl RS transD) 1); -by (blast_tac (claset() addIs (contract_combD2::reduction_rls)) 1); -qed "Ap_reduce2"; - -(** Counterexample to the diamond property for -1-> **) - -Goal "K#I#(I#I) -1-> I"; -by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1)); -qed "KIII_contract1"; - -Goalw [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"; -by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1)); -qed "KIII_contract2"; - -Goal "K#I#((K#I)#(K#I)) -1-> I"; -by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1)); -qed "KIII_contract3"; - -Goalw [diamond_def] "~ diamond(contract)"; -by (blast_tac (claset() addIs [KIII_contract1,KIII_contract2,KIII_contract3] - addSEs [I_contract_E]) 1); -qed "not_diamond_contract"; - - - -(*** Results about Parallel Contraction ***) - -(*For type checking: replaces a=1=>b by a,b \\ comb *) -val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2; -val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1; -val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2; - -Goal "field(parcontract) = comb"; -by (blast_tac (claset() addIs [parcontract.K] - addSEs [parcontract_combE2]) 1); -qed "field_parcontract_eq"; - -(*Derive a case for each combinator constructor*) -val K_parcontractE = parcontract.mk_cases "K =1=> r"; -val S_parcontractE = parcontract.mk_cases "S =1=> r"; -val Ap_parcontractE = parcontract.mk_cases "p#q =1=> r"; - -AddIs parcontract.intrs; -AddSEs [Ap_E, K_parcontractE, S_parcontractE, Ap_parcontractE]; - -(*** Basic properties of parallel contraction ***) - -Goal "K#p =1=> r ==> (\\p'. r = K#p' & p =1=> p')"; -by Auto_tac; -qed "K1_parcontractD"; -AddSDs [K1_parcontractD]; - -Goal "S#p =1=> r ==> (\\p'. r = S#p' & p =1=> p')"; -by Auto_tac; -qed "S1_parcontractD"; -AddSDs [S1_parcontractD]; - -Goal "S#p#q =1=> r ==> (\\p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"; -by Auto_tac; -qed "S2_parcontractD"; -AddSDs [S2_parcontractD]; - -(*Church-Rosser property for parallel contraction*) -Goalw [diamond_def] "diamond(parcontract)"; -by (rtac (impI RS allI RS allI) 1); -by (etac parcontract.induct 1); -by (ALLGOALS - (blast_tac (claset() addSEs comb.free_SEs - addIs [parcontract_combD2]))); -qed "diamond_parcontract"; - -(*** Equivalence of p--->q and p===>q ***) - -Goal "p-1->q ==> p=1=>q"; -by (etac contract.induct 1); -by Auto_tac; -qed "contract_imp_parcontract"; - -Goal "p--->q ==> p===>q"; -by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1); -by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1); -by (etac rtrancl_induct 1); -by (blast_tac (claset() addIs [r_into_trancl]) 1); -by (blast_tac (claset() addIs [contract_imp_parcontract, - r_into_trancl, trans_trancl RS transD]) 1); -qed "reduce_imp_parreduce"; - - -Goal "p=1=>q ==> p--->q"; -by (etac parcontract.induct 1); -by (blast_tac (claset() addIs reduction_rls) 1); -by (blast_tac (claset() addIs reduction_rls) 1); -by (blast_tac (claset() addIs reduction_rls) 1); -by (blast_tac - (claset() addIs [trans_rtrancl RS transD, - Ap_reduce1, Ap_reduce2, parcontract_combD1, - parcontract_combD2]) 1); -qed "parcontract_imp_reduce"; - -Goal "p===>q ==> p--->q"; -by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1); -by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1); -by (etac trancl_induct 1); -by (etac parcontract_imp_reduce 1); -by (etac (trans_rtrancl RS transD) 1); -by (etac parcontract_imp_reduce 1); -qed "parreduce_imp_reduce"; - -Goal "p===>q <-> p--->q"; -by (blast_tac (claset() addIs [parreduce_imp_reduce, reduce_imp_parreduce]) 1); -qed "parreduce_iff_reduce"; - -writeln"Reached end of file."; diff -r b38cfbabfda4 -r 6f463d16cbd0 src/ZF/ex/Comb.thy --- a/src/ZF/ex/Comb.thy Wed Nov 07 00:16:19 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,79 +0,0 @@ -(* Title: ZF/ex/Comb.thy - ID: $Id$ - Author: Lawrence C Paulson - Copyright 1994 University of Cambridge - -Combinatory Logic example: the Church-Rosser Theorem -Curiously, combinators do not include free variables. - -Example taken from - J. Camilleri and T. F. Melham. - Reasoning with Inductively Defined Relations in the HOL Theorem Prover. - Report 265, University of Cambridge Computer Laboratory, 1992. -*) - - -Comb = Main + - -(** Datatype definition of combinators S and K, with infixed application **) -consts comb :: i -datatype - "comb" = K - | S - | "#" ("p \\ comb", "q \\ comb") (infixl 90) - -(** Inductive definition of contractions, -1-> - and (multi-step) reductions, ---> -**) -consts - contract :: i - "-1->" :: [i,i] => o (infixl 50) - "--->" :: [i,i] => o (infixl 50) - -translations - "p -1-> q" == " \\ contract" - "p ---> q" == " \\ contract^*" - -inductive - domains "contract" <= "comb*comb" - intrs - K "[| p \\ comb; q \\ comb |] ==> K#p#q -1-> p" - S "[| p \\ comb; q \\ comb; r \\ comb |] ==> S#p#q#r -1-> (p#r)#(q#r)" - Ap1 "[| p-1->q; r \\ comb |] ==> p#r -1-> q#r" - Ap2 "[| p-1->q; r \\ comb |] ==> r#p -1-> r#q" - type_intrs "comb.intrs" - - -(** Inductive definition of parallel contractions, =1=> - and (multi-step) parallel reductions, ===> -**) -consts - parcontract :: i - "=1=>" :: [i,i] => o (infixl 50) - "===>" :: [i,i] => o (infixl 50) - -translations - "p =1=> q" == " \\ parcontract" - "p ===> q" == " \\ parcontract^+" - -inductive - domains "parcontract" <= "comb*comb" - intrs - refl "[| p \\ comb |] ==> p =1=> p" - K "[| p \\ comb; q \\ comb |] ==> K#p#q =1=> p" - S "[| p \\ comb; q \\ comb; r \\ comb |] ==> S#p#q#r =1=> (p#r)#(q#r)" - Ap "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s" - type_intrs "comb.intrs" - - -(*Misc definitions*) -constdefs - I :: i - "I == S#K#K" - - diamond :: i => o - "diamond(r) == \\x y. :r --> - (\\y'. :r --> - (\\z. :r &