--- a/src/ZF/Induct/Acc.ML Thu Dec 20 15:00:02 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 \\<in> field(r)
- Otherwise acc(r) would be a proper class! *)
-
-(*The intended introduction rule*)
-val prems = goal Acc.thy
- "[| !!b. <b,a>:r ==> b \\<in> acc(r); a \\<in> field(r) |] ==> a \\<in> acc(r)";
-by (fast_tac (claset() addIs prems@acc.intrs) 1);
-qed "accI";
-
-Goal "[| b \\<in> acc(r); <a,b>: r |] ==> a \\<in> acc(r)";
-by (etac acc.elim 1);
-by (Fast_tac 1);
-qed "acc_downward";
-
-val [major,indhyp] = goal Acc.thy
- "[| a \\<in> acc(r); \
-\ !!x. [| x \\<in> acc(r); \\<forall>y. <y,x>: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) \\<subseteq> 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) \\<subseteq> 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) \\<subseteq> acc(r)";
-by (EVERY1 [rtac iffI, etac acc_wfD, etac acc_wfI]);
-qed "wf_acc_iff";
--- a/src/ZF/Induct/Acc.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Acc.thy Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Acc.thy
+(* Title: ZF/Induct/Acc.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
@@ -9,15 +9,52 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-Acc = Main +
+theory Acc = Main:
consts
- acc :: i=>i
+ acc :: "i=>i"
inductive
domains "acc(r)" <= "field(r)"
- intrs
- vimage "[| r-``{a}: Pow(acc(r)); a \\<in> field(r) |] ==> a \\<in> acc(r)"
+ intros
+ vimage: "[| r-``{a}: Pow(acc(r)); a \<in> field(r) |] ==> a \<in> acc(r)"
monos Pow_mono
+
+(*The introduction rule must require a \<in> field(r)
+ Otherwise acc(r) would be a proper class! *)
+
+(*The intended introduction rule*)
+lemma accI: "[| !!b. <b,a>:r ==> b \<in> acc(r); a \<in> field(r) |] ==> a \<in> acc(r)"
+by (blast intro: acc.intros)
+
+lemma acc_downward: "[| b \<in> acc(r); <a,b>: r |] ==> a \<in> acc(r)"
+by (erule acc.cases, blast)
+
+lemma acc_induct:
+ "[| a \<in> acc(r);
+ !!x. [| x \<in> acc(r); \<forall>y. <y,x>:r --> P(y) |] ==> P(x)
+ |] ==> P(a)"
+apply (erule acc.induct)
+apply (blast intro: acc.intros)
+done
+
+lemma wf_on_acc: "wf[acc(r)](r)"
+apply (rule wf_onI2)
+apply (erule acc_induct)
+apply fast
+done
+
+(* field(r) \<subseteq> acc(r) ==> wf(r) *)
+lemmas acc_wfI = wf_on_acc [THEN wf_on_subset_A, THEN wf_on_field_imp_wf]
+
+lemma acc_wfD: "wf(r) ==> field(r) \<subseteq> acc(r)"
+apply (rule subsetI)
+apply (erule wf_induct2, assumption)
+apply (blast intro: accI)+
+done
+
+lemma wf_acc_iff: "wf(r) <-> field(r) \<subseteq> acc(r)"
+by (rule iffI, erule acc_wfD, erule acc_wfI)
+
end
--- a/src/ZF/Induct/Comb.ML Thu Dec 20 15:00:02 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); <x,y>:r^+ |] ==> \
-\ \\<forall>y'. <x,y'>:r --> (\\<exists>z. <y',z>: r^+ & <y,z>: 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 \\<in> comb";
-
-AddSIs comb.intrs;
-
-
-(*** Results about Contraction ***)
-
-(*For type checking: replaces a-1->b by a,b \\<in> 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 \\<in> comb ==> I#p ---> p";
-by (blast_tac (claset() addIs reduction_rls) 1);
-qed "reduce_I";
-
-Goalw [I_def] "I \\<in> 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 ==> (\\<exists>q. r = K#q & p -1-> q)";
-by Auto_tac;
-qed "K1_contractD";
-
-Goal "[| p ---> q; r \\<in> 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 \\<in> 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 \\<in> 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 ==> (\\<exists>p'. r = K#p' & p =1=> p')";
-by Auto_tac;
-qed "K1_parcontractD";
-AddSDs [K1_parcontractD];
-
-Goal "S#p =1=> r ==> (\\<exists>p'. r = S#p' & p =1=> p')";
-by Auto_tac;
-qed "S1_parcontractD";
-AddSDs [S1_parcontractD];
-
-Goal "S#p#q =1=> r ==> (\\<exists>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.";
--- a/src/ZF/Induct/Comb.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Comb.thy Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Comb.thy
+(* Title: ZF/Induct/Comb.thy
ID: $Id$
Author: Lawrence C Paulson
Copyright 1994 University of Cambridge
@@ -10,60 +10,63 @@
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
*)
-Comb = Main +
+theory Comb = Main:
(** Datatype definition of combinators S and K, with infixed application **)
consts comb :: i
datatype
"comb" = K
| S
- | "#" ("p \\<in> comb", "q \\<in> comb") (infixl 90)
+ | "#" ("p \<in> comb", "q \<in> 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)
+ contract :: "i"
+ "-1->" :: "[i,i] => o" (infixl 50)
+ "--->" :: "[i,i] => o" (infixl 50)
translations
- "p -1-> q" == "<p,q> \\<in> contract"
- "p ---> q" == "<p,q> \\<in> contract^*"
+ "p -1-> q" == "<p,q> \<in> contract"
+ "p ---> q" == "<p,q> \<in> contract^*"
inductive
domains "contract" <= "comb*comb"
- intrs
- K "[| p \\<in> comb; q \\<in> comb |] ==> K#p#q -1-> p"
- S "[| p \\<in> comb; q \\<in> comb; r \\<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
- Ap1 "[| p-1->q; r \\<in> comb |] ==> p#r -1-> q#r"
- Ap2 "[| p-1->q; r \\<in> comb |] ==> r#p -1-> r#q"
- type_intrs "comb.intrs"
+ intros
+ K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q -1-> p"
+ S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+ Ap1: "[| p-1->q; r \<in> comb |] ==> p#r -1-> q#r"
+ Ap2: "[| p-1->q; r \<in> comb |] ==> r#p -1-> r#q"
+ type_intros "comb.intros"
(** 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)
+ parcontract :: "i"
+ "=1=>" :: "[i,i] => o" (infixl 50)
+ "===>" :: "[i,i] => o" (infixl 50)
translations
- "p =1=> q" == "<p,q> \\<in> parcontract"
- "p ===> q" == "<p,q> \\<in> parcontract^+"
+ "p =1=> q" == "<p,q> \<in> parcontract"
+ "p ===> q" == "<p,q> \<in> parcontract^+"
inductive
domains "parcontract" <= "comb*comb"
- intrs
- refl "[| p \\<in> comb |] ==> p =1=> p"
- K "[| p \\<in> comb; q \\<in> comb |] ==> K#p#q =1=> p"
- S "[| p \\<in> comb; q \\<in> comb; r \\<in> 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"
+ intros
+ refl: "[| p \<in> comb |] ==> p =1=> p"
+ K: "[| p \<in> comb; q \<in> comb |] ==> K#p#q =1=> p"
+ S: "[| p \<in> comb; q \<in> comb; r \<in> comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+ Ap: "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"
+ type_intros "comb.intros"
(*Misc definitions*)
@@ -71,9 +74,197 @@
I :: i
"I == S#K#K"
- diamond :: i => o
- "diamond(r) == \\<forall>x y. <x,y>:r -->
- (\\<forall>y'. <x,y'>:r -->
- (\\<exists>z. <y,z>:r & <y',z> \\<in> r))"
+ diamond :: "i => o"
+ "diamond(r) == \<forall>x y. <x,y>\<in>r -->
+ (\<forall>y'. <x,y'>\<in>r -->
+ (\<exists>z. <y,z>\<in>r & <y',z> \<in> r))"
+
+
+
+(*** Transitive closure preserves the Church-Rosser property ***)
+
+lemma diamond_strip_lemmaD [rule_format]:
+ "[| diamond(r); <x,y>:r^+ |] ==>
+ \<forall>y'. <x,y'>:r --> (\<exists>z. <y',z>: r^+ & <y,z>: r)"
+apply (unfold diamond_def)
+apply (erule trancl_induct)
+apply (blast intro: r_into_trancl)
+apply clarify
+apply (drule spec [THEN mp], assumption)
+apply (blast intro: r_into_trancl trans_trancl [THEN transD])
+done
+
+
+lemma diamond_trancl: "diamond(r) ==> diamond(r^+)"
+apply (simp (no_asm_simp) add: diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule trancl_induct)
+apply (auto );
+apply (best intro: r_into_trancl trans_trancl [THEN transD]
+ dest: diamond_strip_lemmaD)+
+done
+
+
+inductive_cases Ap_E [elim!]: "p#q \<in> comb"
+
+declare comb.intros [intro!]
+
+
+(*** Results about Contraction ***)
+
+(*For type checking: replaces a-1->b by a,b \<in> comb *)
+lemmas contract_combE2 = contract.dom_subset [THEN subsetD, THEN SigmaE2]
+lemmas contract_combD1 = contract.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas contract_combD2 = contract.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemma field_contract_eq: "field(contract) = comb"
+by (blast intro: contract.K elim!: contract_combE2)
+
+lemmas reduction_refl =
+ field_contract_eq [THEN equalityD2, THEN subsetD, THEN rtrancl_refl]
+
+lemmas rtrancl_into_rtrancl2 =
+ r_into_rtrancl [THEN trans_rtrancl [THEN transD]]
+
+declare reduction_refl [intro!] contract.K [intro!] contract.S [intro!]
+
+lemmas reduction_rls = contract.K [THEN rtrancl_into_rtrancl2]
+ contract.S [THEN rtrancl_into_rtrancl2]
+ contract.Ap1 [THEN rtrancl_into_rtrancl2]
+ contract.Ap2 [THEN rtrancl_into_rtrancl2]
+
+(*Example only: not used*)
+lemma reduce_I: "p \<in> comb ==> I#p ---> p"
+by (unfold I_def, blast intro: reduction_rls)
+
+lemma comb_I: "I \<in> comb"
+by (unfold I_def, blast)
+
+(** Non-contraction results **)
+
+(*Derive a case for each combinator constructor*)
+inductive_cases K_contractE [elim!]: "K -1-> r"
+inductive_cases S_contractE [elim!]: "S -1-> r"
+inductive_cases Ap_contractE [elim!]: "p#q -1-> r"
+
+declare contract.Ap1 [intro] contract.Ap2 [intro]
+
+lemma I_contract_E: "I -1-> r ==> P"
+by (auto simp add: I_def)
+
+lemma K1_contractD: "K#p -1-> r ==> (\<exists>q. r = K#q & p -1-> q)"
+by auto
+
+lemma Ap_reduce1: "[| p ---> q; r \<in> comb |] ==> p#r ---> q#r"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: reduction_rls)
+apply (erule trans_rtrancl [THEN transD])
+apply (blast intro: contract_combD2 reduction_rls)
+done
+
+lemma Ap_reduce2: "[| p ---> q; r \<in> comb |] ==> r#p ---> r#q"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+apply (blast intro: reduction_rls)
+apply (erule trans_rtrancl [THEN transD])
+apply (blast intro: contract_combD2 reduction_rls)
+done
+
+(** Counterexample to the diamond property for -1-> **)
+
+lemma KIII_contract1: "K#I#(I#I) -1-> I"
+by (blast intro: comb.intros contract.K comb_I)
+
+lemma KIII_contract2: "K#I#(I#I) -1-> K#I#((K#I)#(K#I))"
+by (unfold I_def, blast intro: comb.intros contract.intros)
+
+
+lemma KIII_contract3: "K#I#((K#I)#(K#I)) -1-> I"
+by (blast intro: comb.intros contract.K comb_I)
+
+lemma not_diamond_contract: "~ diamond(contract)"
+apply (unfold diamond_def)
+apply (blast intro: KIII_contract1 KIII_contract2 KIII_contract3
+ elim!: I_contract_E)
+done
+
+
+
+(*** Results about Parallel Contraction ***)
+
+(*For type checking: replaces a=1=>b by a,b \<in> comb *)
+lemmas parcontract_combE2 = parcontract.dom_subset [THEN subsetD, THEN SigmaE2]
+lemmas parcontract_combD1 = parcontract.dom_subset [THEN subsetD, THEN SigmaD1]
+lemmas parcontract_combD2 = parcontract.dom_subset [THEN subsetD, THEN SigmaD2]
+
+lemma field_parcontract_eq: "field(parcontract) = comb"
+by (blast intro: parcontract.K elim!: parcontract_combE2)
+
+(*Derive a case for each combinator constructor*)
+inductive_cases K_parcontractE [elim!]: "K =1=> r"
+inductive_cases S_parcontractE [elim!]: "S =1=> r"
+inductive_cases Ap_parcontractE [elim!]: "p#q =1=> r"
+
+declare parcontract.intros [intro]
+
+
+(*** Basic properties of parallel contraction ***)
+
+lemma K1_parcontractD [dest!]: "K#p =1=> r ==> (\<exists>p'. r = K#p' & p =1=> p')"
+by auto
+
+lemma S1_parcontractD [dest!]: "S#p =1=> r ==> (\<exists>p'. r = S#p' & p =1=> p')"
+by auto
+
+lemma S2_parcontractD [dest!]:
+ "S#p#q =1=> r ==> (\<exists>p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')"
+by auto
+
+
+(*Church-Rosser property for parallel contraction*)
+lemma diamond_parcontract: "diamond(parcontract)"
+apply (unfold diamond_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule parcontract.induct)
+apply (blast elim!: comb.free_elims intro: parcontract_combD2)+
+done
+
+(*** Equivalence of p--->q and p===>q ***)
+
+lemma contract_imp_parcontract: "p-1->q ==> p=1=>q"
+by (erule contract.induct, auto)
+
+lemma reduce_imp_parreduce: "p--->q ==> p===>q"
+apply (frule rtrancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_contract_eq [THEN equalityD1, THEN subsetD])
+apply (erule rtrancl_induct)
+ apply (blast intro: r_into_trancl)
+apply (blast intro: contract_imp_parcontract r_into_trancl
+ trans_trancl [THEN transD])
+done
+
+
+lemma parcontract_imp_reduce: "p=1=>q ==> p--->q"
+apply (erule parcontract.induct)
+ apply (blast intro: reduction_rls)
+ apply (blast intro: reduction_rls)
+ apply (blast intro: reduction_rls)
+apply (blast intro: trans_rtrancl [THEN transD]
+ Ap_reduce1 Ap_reduce2 parcontract_combD1 parcontract_combD2)
+done
+
+lemma parreduce_imp_reduce: "p===>q ==> p--->q"
+apply (frule trancl_type [THEN subsetD, THEN SigmaD1])
+apply (drule field_parcontract_eq [THEN equalityD1, THEN subsetD])
+apply (erule trancl_induct, erule parcontract_imp_reduce)
+apply (erule trans_rtrancl [THEN transD])
+apply (erule parcontract_imp_reduce)
+done
+
+lemma parreduce_iff_reduce: "p===>q <-> p--->q"
+by (blast intro: parreduce_imp_reduce reduce_imp_parreduce)
end
--- a/src/ZF/Induct/ListN.ML Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* 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 \\<in> list(A) ==> <length(l),l> \\<in> listn(A)";
-by (etac list.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (REPEAT (ares_tac listn.intrs 1));
-qed "list_into_listn";
-
-Goal "<n,l> \\<in> listn(A) <-> l \\<in> 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 \\<in> 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 \\<subseteq> B ==> listn(A) \\<subseteq> 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 "[| <n,l> \\<in> listn(A); <n',l'> \\<in> listn(A) |] ==> <n#+n', l@l'> \\<in> 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 "<i,Nil> \\<in> listn(A)"
-and Cons_listn_case = listn.mk_cases "<i,Cons(x,l)> \\<in> listn(A)";
-
-val zero_listn_case = listn.mk_cases "<0,l> \\<in> listn(A)"
-and succ_listn_case = listn.mk_cases "<succ(i),l> \\<in> listn(A)";
--- a/src/ZF/Induct/ListN.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/ListN.thy Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/ListN
+(* Title: ZF/Induct/ListN
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
@@ -9,14 +9,50 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-ListN = Main +
+theory ListN = Main:
-consts listn ::i=>i
+consts listn :: "i=>i"
inductive
domains "listn(A)" <= "nat*list(A)"
- intrs
- NilI "<0,Nil> \\<in> listn(A)"
- ConsI "[| a \\<in> A; <n,l> \\<in> listn(A) |] ==> <succ(n), Cons(a,l)> \\<in> listn(A)"
- type_intrs "nat_typechecks @ list.intrs"
+ intros
+ NilI: "<0,Nil> \<in> listn(A)"
+ ConsI: "[| a \<in> A; <n,l> \<in> listn(A) |] ==> <succ(n), Cons(a,l)> \<in> listn(A)"
+ type_intros nat_typechecks list.intros
+
+
+lemma list_into_listn: "l \<in> list(A) ==> <length(l),l> \<in> listn(A)"
+by (erule list.induct, simp_all add: listn.intros)
+
+lemma listn_iff: "<n,l> \<in> listn(A) <-> l \<in> list(A) & length(l)=n"
+apply (rule iffI)
+apply (erule listn.induct)
+apply auto
+apply (blast intro: list_into_listn)
+done
+
+lemma listn_image_eq: "listn(A)``{n} = {l \<in> list(A). length(l)=n}"
+apply (rule equality_iffI)
+apply (simp (no_asm) add: listn_iff separation image_singleton_iff)
+done
+
+lemma listn_mono: "A \<subseteq> B ==> listn(A) \<subseteq> listn(B)"
+apply (unfold listn.defs )
+apply (rule lfp_mono)
+apply (rule listn.bnd_mono)+
+apply (assumption | rule univ_mono Sigma_mono list_mono basic_monos)+
+done
+
+lemma listn_append:
+ "[| <n,l> \<in> listn(A); <n',l'> \<in> listn(A) |] ==> <n#+n', l@l'> \<in> listn(A)"
+apply (erule listn.induct)
+apply (frule listn.dom_subset [THEN subsetD])
+apply (simp_all add: listn.intros)
+done
+
+inductive_cases Nil_listn_case: "<i,Nil> \<in> listn(A)"
+inductive_cases Cons_listn_case: "<i,Cons(x,l)> \<in> listn(A)"
+
+inductive_cases zero_listn_case: "<0,l> \<in> listn(A)"
+inductive_cases succ_listn_case: "<succ(i),l> \<in> listn(A)"
end
--- a/src/ZF/Induct/Multiset.ML Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Multiset.ML Thu Dec 20 15:17:48 2001 +0100
@@ -884,7 +884,7 @@
Goal "acc(0)=0";
by (auto_tac (claset() addSIs [equalityI]
- addDs [acc.dom_subset RS subsetD], simpset()));
+ addDs [thm "acc.dom_subset" RS subsetD], simpset()));
qed "acc_0";
Goal "[| ALL b:A. <b,a>:r --> \
@@ -893,10 +893,10 @@
\ ALL M. <M,M0> : multirel1(A, r) --> M +# {#a#} : acc(multirel1(A, r)) |] \
\ ==> M0 +# {#a#} : acc(multirel1(A, r))";
by (subgoal_tac "multiset[A](M0)" 1);
-by (etac acc.elim 2);
+by (etac (thm "acc.cases") 2);
by (etac fieldE 2);
by (REPEAT(blast_tac (claset() addDs [multirel1D]) 2));
-by (rtac accI 1);
+by (rtac (thm "accI") 1);
by (rename_tac "N" 1);
by (dtac less_munion 1);
by (Blast_tac 1);
@@ -926,13 +926,12 @@
Goal "[| ALL b:A. <b,a>:r \
\ --> (ALL M : acc(multirel1(A, r)). M +# {#b#} :acc(multirel1(A, r))); \
\ M:acc(multirel1(A, r)); a:A|] ==> M +# {#a#} : acc(multirel1(A, r))";
-by (etac acc_induct 1);
+by (etac (thm "acc_induct") 1);
by (blast_tac (claset() addIs [lemma1]) 1);
qed "lemma2";
-Goal
- "[| wf[A](r); a:A |] ==> \
-\ ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
+Goal "[| wf[A](r); a:A |] \
+\ ==> ALL M:acc(multirel1(A, r)). M +# {#a#} : acc(multirel1(A, r))";
by (eres_inst_tac [("a","a")] wf_on_induct 1);
by (Blast_tac 1);
by (blast_tac (claset() addIs [lemma2]) 1);
@@ -943,7 +942,7 @@
by (etac multiset_induct 1);
by (ALLGOALS(Clarify_tac));
(* proving the base case *)
-by (rtac accI 1);
+by (rtac (thm "accI") 1);
by (cut_inst_tac [("M", "b"), ("r", "r")] not_less_0 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() addsimps [multirel1_def]) 1);
@@ -974,7 +973,7 @@
by (rtac wf_on_field_imp_wf 1);
by (asm_simp_tac (simpset() addsimps [wf_on_0]) 1);
by (res_inst_tac [("A", "acc(multirel1(A,r))")] wf_on_subset_A 1);
-by (rtac wf_on_acc 1);
+by (rtac (thm "wf_on_acc") 1);
by (Clarify_tac 1);
by (full_simp_tac (simpset() addsimps [FiniteFun_iff_multiset_on]) 1);
by (blast_tac (claset() addIs [all_accessible]) 1);
@@ -1031,8 +1030,7 @@
by (auto_tac (claset() addDs [domain_type], simpset() addsimps [lemma]));
qed "mdiff_union_single_conv";
-Goal
-"[| n le m; m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
+Goal "[| n le m; m:nat; n:nat; k:nat |] ==> m #- n #+ k = m #+ k #- n";
by (auto_tac (claset(), simpset() addsimps
[le_iff, diff_self_eq_0, less_iff_succ_add]));
qed "diff_add_commute";
@@ -1105,9 +1103,8 @@
qed "melem_imp_eq_diff_union";
Addsimps [melem_imp_eq_diff_union];
-Goal
-"[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
-\ ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
+Goal "[| msize(M)=$# succ(n); multiset[A](M); n:nat |] \
+\ ==> EX a N. M = N +# {#a#} & multiset[A](N) & a:A";
by (dtac msize_eq_succ_imp_elem 1);
by Auto_tac;
by (res_inst_tac [("x", "a")] exI 1);
@@ -1372,8 +1369,7 @@
AddSEs [mless_irrefl];
(*transitivity*)
-Goalw [mless_def]
- "[| K <# M; M <# N |] ==> K <# N";
+Goalw [mless_def] "[| K <# M; M <# N |] ==> K <# N";
by (Clarify_tac 1);
by (res_inst_tac [("x", "i Un ia")] exI 1);
by (blast_tac (claset() addDs
@@ -1459,13 +1455,11 @@
(* <#= *)
-Goalw [mle_def]
- "M <#= N ==> omultiset(M) & omultiset(N)";
+Goalw [mle_def] "M <#= N ==> omultiset(M) & omultiset(N)";
by (auto_tac (claset(), simpset() addsimps [mless_imp_omultiset]));
qed "mle_imp_omultiset";
-Goal
- "[| M <#= K; N <#= L |] ==> M +# N <#= K +# L";
+Goal "[| M <#= K; N <#= L |] ==> M +# N <#= K +# L";
by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1);
by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1);
by (rewtac mle_def);
@@ -1483,8 +1477,7 @@
qed "omultiset_0";
AddIffs [omultiset_0];
-Goalw [mle_def, mless_def]
- "omultiset(M) ==> 0 <#= M";
+Goalw [mle_def, mless_def] "omultiset(M) ==> 0 <#= M";
by (subgoal_tac "EX i. Ord(i) & multiset[field(Memrel(i))](M)" 1);
by (asm_full_simp_tac (simpset() addsimps [omultiset_def]) 2);
by (case_tac "M=0" 1);
--- a/src/ZF/Induct/Primrec.ML Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,297 +0,0 @@
-(* 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 \\<in> prim_rec ==> c \\<in> list(nat) -> nat *)
-val prim_rec_into_fun = prim_rec.dom_subset RS subsetD;
-
-AddTCs ([prim_rec_into_fun] @ prim_rec.intrs);
-
-Goal "i \\<in> 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 \\<in> nat; j \\<in> nat |] ==> ack(i,j): nat";
-by Auto_tac;
-qed "ack_type";
-AddTCs [ack_type];
-
-(** Ackermann's function cases **)
-
-(*PROPERTY A 1*)
-Goal "j \\<in> 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 \\<in> nat; j \\<in> 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 \\<in> nat ==> \\<forall>j \\<in> 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 \\<in> nat; j \\<in> 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<k; i \\<in> nat; k \\<in> 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 \\<in> nat; k \\<in> 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 \\<in> nat; j \\<in> 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 \\<in> nat; j \\<in> 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<j; j \\<in> nat; k \\<in> 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 \\<in> nat; k \\<in> 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 \\<in> 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 \\<in> 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 \\<in> nat; i2 \\<in> nat; j \\<in> 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 \\<in> nat; i2 \\<in> nat; j \\<in> 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 \\<exists>k'. \\<forall>i,j... *)
-Goal "[| i < ack(k,j); j \\<in> nat; k \\<in> 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 \\<in> 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 \\<in> nat; j \\<in> 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 \\<in> list(nat); k \\<in> 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 \\<in> list(nat) ==> \\<forall>i \\<in> 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 \\<in> list({f \\<in> prim_rec . \
-\ \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat). \
-\ f`l < ack(kf, list_add(l))}) \
-\ ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> 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; \
-\ \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l)); \
-\ fs \\<in> list({f \\<in> prim_rec . \
-\ \\<exists>kf \\<in> nat. \\<forall>l \\<in> list(nat). \
-\ f`l < ack(kf, list_add(l))}) \
-\ |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> 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]
- "[| \\<forall>l \\<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
-\ \\<forall>l \\<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
-\ f \\<in> prim_rec; kf: nat; \
-\ g \\<in> prim_rec; kg: nat; \
-\ l \\<in> 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 \\<in> prim_rec; kf: nat; \
-\ g \\<in> prim_rec; kg: nat; \
-\ \\<forall>l \\<in> list(nat). f`l < ack(kf, list_add(l)); \
-\ \\<forall>l \\<in> list(nat). g`l < ack(kg, list_add(l)) \
-\ |] ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> 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 \\<in> prim_rec ==> \\<exists>k \\<in> nat. \\<forall>l \\<in> 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 "~ (\\<lambda>l \\<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \\<in> 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";
-
--- a/src/ZF/Induct/Primrec.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Primrec.thy Thu Dec 20 15:17:48 2001 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Primrec.thy
+(* Title: ZF/Induct/Primrec.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
@@ -14,22 +14,357 @@
(Van Nostrand, 1964), page 250, exercise 11.
*)
-Primrec = Primrec_defs +
+theory Primrec = Main:
+
+constdefs
+ SC :: "i"
+ "SC == \<lambda>l \<in> list(nat). list_case(0, %x xs. succ(x), l)"
+
+ CONST :: "i=>i"
+ "CONST(k) == \<lambda>l \<in> list(nat). k"
+
+ PROJ :: "i=>i"
+ "PROJ(i) == \<lambda>l \<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
+
+ COMP :: "[i,i]=>i"
+ "COMP(g,fs) == \<lambda>l \<in> list(nat). g ` List.map(%f. f`l, fs)"
+
+ PREC :: "[i,i]=>i"
+ (*Note that g is applied first to PREC(f,g)`y and then to y!*)
+ "PREC(f,g) ==
+ \<lambda>l \<in> list(nat). list_case(0,
+ %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+
consts
- prim_rec :: i
+ ACK :: "i=>i"
+
+primrec
+ ACK_0: "ACK(0) = SC"
+ ACK_succ: "ACK(succ(i)) = PREC (CONST (ACK(i) ` [1]),
+ COMP(ACK(i), [PROJ(0)]))"
+
+syntax
+ ack :: "[i,i]=>i"
+
+translations
+ "ack(x,y)" == "ACK(x) ` [y]"
+
+
+
+(** Useful special cases of evaluation ***)
+
+lemma SC: "[| x \<in> nat; l \<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)"
+by (simp add: SC_def)
+
+lemma CONST: "l \<in> list(nat) ==> CONST(k) ` l = k"
+by (simp add: CONST_def)
+
+lemma PROJ_0: "[| x \<in> nat; l \<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x"
+by (simp add: PROJ_def)
+
+lemma COMP_1: "l \<in> list(nat) ==> COMP(g,[f]) ` l = g` [f`l]"
+by (simp add: COMP_def)
+
+lemma PREC_0: "l \<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l"
+by (simp add: PREC_def)
+
+lemma PREC_succ:
+ "[| x \<in> nat; l \<in> list(nat) |]
+ ==> PREC(f,g) ` (Cons(succ(x),l)) =
+ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))"
+by (simp add: PREC_def)
+
+
+consts
+ prim_rec :: "i"
inductive
domains "prim_rec" <= "list(nat)->nat"
- intrs
- SC "SC \\<in> prim_rec"
- CONST "k \\<in> nat ==> CONST(k) \\<in> prim_rec"
- PROJ "i \\<in> nat ==> PROJ(i) \\<in> prim_rec"
- COMP "[| g \\<in> prim_rec; fs: list(prim_rec) |] ==> COMP(g,fs): prim_rec"
- PREC "[| f \\<in> prim_rec; g \\<in> 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]"
+ intros
+ "SC \<in> prim_rec"
+ "k \<in> nat ==> CONST(k) \<in> prim_rec"
+ "i \<in> nat ==> PROJ(i) \<in> prim_rec"
+ "[| g \<in> prim_rec; fs\<in>list(prim_rec) |] ==> COMP(g,fs): prim_rec"
+ "[| f \<in> prim_rec; g \<in> prim_rec |] ==> PREC(f,g): prim_rec"
+ monos list_mono
+ con_defs SC_def CONST_def PROJ_def COMP_def PREC_def
+ type_intros nat_typechecks list.intros
+ lam_type list_case_type drop_type List.map_type
+ apply_type rec_type
+
+
+(*** Inductive definition of the PR functions ***)
+
+(* c \<in> prim_rec ==> c \<in> list(nat) -> nat *)
+lemmas prim_rec_into_fun [TC] = subsetD [OF prim_rec.dom_subset]
+lemmas [TC] = apply_type [OF prim_rec_into_fun]
+
+declare prim_rec.intros [TC]
+declare nat_into_Ord [TC]
+declare rec_type [TC]
+
+lemma ACK_in_prim_rec [TC]: "i \<in> nat ==> ACK(i): prim_rec"
+by (induct_tac "i", simp_all)
+
+lemma ack_type [TC]: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j): nat"
+by auto
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+lemma ack_0: "j \<in> nat ==> ack(0,j) = succ(j)"
+by (simp add: SC)
+
+(*PROPERTY A 2*)
+lemma ack_succ_0: "ack(succ(i), 0) = ack(i,1)"
+by (simp add: CONST PREC_0)
+
+(*PROPERTY A 3*)
+lemma ack_succ_succ:
+ "[| i\<in>nat; j\<in>nat |] ==> ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))"
+by (simp add: CONST PREC_succ COMP_1 PROJ_0)
+
+declare ack_0 [simp] ack_succ_0 [simp] ack_succ_succ [simp] ack_type [simp]
+declare ACK_0 [simp del] ACK_succ [simp del]
+
+
+(*PROPERTY A 4*)
+lemma lt_ack2 [rule_format]: "i \<in> nat ==> \<forall>j \<in> nat. j < ack(i,j)"
+apply (induct_tac "i")
+apply simp
+apply (rule ballI)
+apply (induct_tac "j")
+apply (erule_tac [2] succ_leI [THEN lt_trans1])
+apply (rule nat_0I [THEN nat_0_le, THEN lt_trans])
+apply auto
+done
+
+(*PROPERTY A 5-, the single-step lemma*)
+lemma ack_lt_ack_succ2: "[|i\<in>nat; j\<in>nat|] ==> ack(i,j) < ack(i, succ(j))"
+by (induct_tac "i", simp_all add: lt_ack2)
+
+(*PROPERTY A 5, monotonicity for < *)
+lemma ack_lt_mono2: "[| j<k; i \<in> nat; k \<in> nat |] ==> ack(i,j) < ack(i,k)"
+apply (frule lt_nat_in_nat , assumption)
+apply (erule succ_lt_induct)
+apply assumption
+apply (rule_tac [2] lt_trans)
+apply (auto intro: ack_lt_ack_succ2)
+done
+
+(*PROPERTY A 5', monotonicity for\<le>*)
+lemma ack_le_mono2: "[|j\<le>k; i\<in>nat; k\<in>nat|] ==> ack(i,j) \<le> ack(i,k)"
+apply (rule_tac f = "%j. ack (i,j) " in Ord_lt_mono_imp_le_mono)
+apply (assumption | rule ack_lt_mono2 ack_type [THEN nat_into_Ord])+;
+done
+
+(*PROPERTY A 6*)
+lemma ack2_le_ack1:
+ "[| i\<in>nat; j\<in>nat |] ==> ack(i, succ(j)) \<le> ack(succ(i), j)"
+apply (induct_tac "j")
+apply (simp_all)
+apply (rule ack_le_mono2)
+apply (rule lt_ack2 [THEN succ_leI, THEN le_trans])
+apply auto
+done
+
+(*PROPERTY A 7-, the single-step lemma*)
+lemma ack_lt_ack_succ1: "[| i \<in> nat; j \<in> nat |] ==> ack(i,j) < ack(succ(i),j)"
+apply (rule ack_lt_mono2 [THEN lt_trans2])
+apply (rule_tac [4] ack2_le_ack1)
+apply auto
+done
+
+(*PROPERTY A 7, monotonicity for < *)
+lemma ack_lt_mono1: "[| i<j; j \<in> nat; k \<in> nat |] ==> ack(i,k) < ack(j,k)"
+apply (frule lt_nat_in_nat , assumption)
+apply (erule succ_lt_induct)
+apply assumption
+apply (rule_tac [2] lt_trans)
+apply (auto intro: ack_lt_ack_succ1)
+done
+
+(*PROPERTY A 7', monotonicity for\<le>*)
+lemma ack_le_mono1: "[| i\<le>j; j \<in> nat; k \<in> nat |] ==> ack(i,k) \<le> ack(j,k)"
+apply (rule_tac f = "%j. ack (j,k) " in Ord_lt_mono_imp_le_mono)
+apply (assumption | rule ack_lt_mono1 ack_type [THEN nat_into_Ord])+;
+done
+
+(*PROPERTY A 8*)
+lemma ack_1: "j \<in> nat ==> ack(1,j) = succ(succ(j))"
+by (induct_tac "j", simp_all)
+
+(*PROPERTY A 9*)
+lemma ack_2: "j \<in> nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))"
+by (induct_tac "j", simp_all add: ack_1)
+
+(*PROPERTY A 10*)
+lemma ack_nest_bound:
+ "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
+ ==> ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)"
+apply (rule lt_trans2 [OF _ ack2_le_ack1])
+apply simp
+apply (rule add_le_self [THEN ack_le_mono1, THEN lt_trans1])
+apply auto
+apply (force intro: add_le_self2 [THEN ack_lt_mono1, THEN ack_lt_mono2])
+done
+
+(*PROPERTY A 11*)
+lemma ack_add_bound:
+ "[| i1 \<in> nat; i2 \<in> nat; j \<in> nat |]
+ ==> ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)"
+apply (rule_tac j = "ack (succ (1) , ack (i1 #+ i2, j))" in lt_trans)
+apply (simp add: ack_2)
+apply (rule_tac [2] ack_nest_bound [THEN lt_trans2])
+apply (rule add_le_mono [THEN leI, THEN leI])
+apply (auto intro: add_le_self add_le_self2 ack_le_mono1)
+done
+
+(*PROPERTY A 12. Article uses existential quantifier but the ALF proof
+ used k#+4. Quantified version must be nested \<exists>k'. \<forall>i,j... *)
+lemma ack_add_bound2:
+ "[| i < ack(k,j); j \<in> nat; k \<in> nat |]
+ ==> i#+j < ack(succ(succ(succ(succ(k)))), j)"
+apply (rule_tac j = "ack (k,j) #+ ack (0,j) " in lt_trans)
+apply (rule_tac [2] ack_add_bound [THEN lt_trans2])
+apply (rule add_lt_mono)
+apply auto
+done
+
+(*** MAIN RESULT ***)
+
+declare list_add_type [simp]
+
+lemma SC_case: "l \<in> list(nat) ==> SC ` l < ack(1, list_add(l))"
+apply (unfold SC_def)
+apply (erule list.cases)
+apply (simp add: succ_iff)
+apply (simp add: ack_1 add_le_self)
+done
+
+(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
+lemma lt_ack1: "[| i \<in> nat; j \<in> nat |] ==> i < ack(i,j)"
+apply (induct_tac "i")
+apply (simp add: nat_0_le)
+apply (erule lt_trans1 [OF succ_leI ack_lt_ack_succ1])
+apply auto
+done
+
+lemma CONST_case:
+ "[| l \<in> list(nat); k \<in> nat |] ==> CONST(k) ` l < ack(k, list_add(l))"
+by (simp add: CONST_def lt_ack1)
+
+lemma PROJ_case [rule_format]:
+ "l \<in> list(nat) ==> \<forall>i \<in> nat. PROJ(i) ` l < ack(0, list_add(l))"
+apply (unfold PROJ_def)
+apply simp
+apply (erule list.induct)
+apply (simp add: nat_0_le)
+apply simp
+apply (rule ballI)
+apply (erule_tac n = "x" in natE)
+apply (simp add: add_le_self)
+apply simp
+apply (erule bspec [THEN lt_trans2])
+apply (rule_tac [2] add_le_self2 [THEN succ_leI])
+apply auto
+done
+
+(** COMP case **)
+
+lemma COMP_map_lemma:
+ "fs \<in> list({f \<in> prim_rec .
+ \<exists>kf \<in> nat. \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l))})
+ ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat).
+ list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))"
+apply (erule list.induct)
+apply (rule_tac x = "0" in bexI)
+apply (simp_all add: lt_ack1 nat_0_le)
+apply clarify
+apply (rule ballI [THEN bexI])
+apply (rule add_lt_mono [THEN lt_trans])
+apply (rule_tac [5] ack_add_bound)
+apply blast
+apply auto
+done
+
+lemma COMP_case:
+ "[| kg\<in>nat;
+ \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l));
+ fs \<in> list({f \<in> prim_rec .
+ \<exists>kf \<in> nat. \<forall>l \<in> list(nat).
+ f`l < ack(kf, list_add(l))}) |]
+ ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). COMP(g,fs)`l < ack(k, list_add(l))"
+apply (simp add: COMP_def)
+apply (frule list_CollectD)
+apply (erule COMP_map_lemma [THEN bexE])
+apply (rule ballI [THEN bexI])
+apply (erule bspec [THEN lt_trans])
+apply (rule_tac [2] lt_trans)
+apply (rule_tac [3] ack_nest_bound)
+apply (erule_tac [2] bspec [THEN ack_lt_mono2])
+apply auto
+done
+
+(** PREC case **)
+
+lemma PREC_case_lemma:
+ "[| \<forall>l \<in> list(nat). f`l #+ list_add(l) < ack(kf, list_add(l));
+ \<forall>l \<in> list(nat). g`l #+ list_add(l) < ack(kg, list_add(l));
+ f \<in> prim_rec; kf\<in>nat;
+ g \<in> prim_rec; kg\<in>nat;
+ l \<in> list(nat) |]
+ ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))"
+apply (unfold PREC_def)
+apply (erule list.cases)
+apply (simp add: lt_trans [OF nat_le_refl lt_ack2])
+apply simp
+apply (erule ssubst) (*get rid of the needless assumption*)
+apply (induct_tac "a")
+apply simp_all
+(*base case*)
+apply (rule lt_trans, erule bspec, assumption);
+apply (simp add: add_le_self [THEN ack_lt_mono1])
+(*ind step*)
+apply (rule succ_leI [THEN lt_trans1])
+apply (rule_tac j = "g ` ?ll #+ ?mm" in lt_trans1)
+apply (erule_tac [2] bspec)
+apply (rule nat_le_refl [THEN add_le_mono])
+apply typecheck
+apply (simp add: add_le_self2)
+(*final part of the simplification*)
+apply simp
+apply (rule add_le_self2 [THEN ack_le_mono1, THEN lt_trans1])
+apply (erule_tac [4] ack_lt_mono2)
+apply auto
+done
+
+lemma PREC_case:
+ "[| f \<in> prim_rec; kf\<in>nat;
+ g \<in> prim_rec; kg\<in>nat;
+ \<forall>l \<in> list(nat). f`l < ack(kf, list_add(l));
+ \<forall>l \<in> list(nat). g`l < ack(kg, list_add(l)) |]
+ ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). PREC(f,g)`l< ack(k, list_add(l))"
+apply (rule ballI [THEN bexI])
+apply (rule lt_trans1 [OF add_le_self PREC_case_lemma])
+apply typecheck
+apply (blast intro: ack_add_bound2 list_add_type)+
+done
+
+lemma ack_bounds_prim_rec:
+ "f \<in> prim_rec ==> \<exists>k \<in> nat. \<forall>l \<in> list(nat). f`l < ack(k, list_add(l))"
+apply (erule prim_rec.induct)
+apply (auto intro: SC_case CONST_case PROJ_case COMP_case PREC_case)
+done
+
+lemma ack_not_prim_rec:
+ "~ (\<lambda>l \<in> list(nat). list_case(0, %x xs. ack(x,x), l)) \<in> prim_rec"
+apply (rule notI)
+apply (drule ack_bounds_prim_rec)
+apply force
+done
end
+
+
+
--- a/src/ZF/Induct/Primrec_defs.ML Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,40 +0,0 @@
-(* 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 \\<in> nat; l \\<in> list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
-by (Asm_simp_tac 1);
-qed "SC";
-
-Goalw [CONST_def] "[| l \\<in> list(nat) |] ==> CONST(k) ` l = k";
-by (Asm_simp_tac 1);
-qed "CONST";
-
-Goalw [PROJ_def] "[| x \\<in> nat; l \\<in> list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
-by (Asm_simp_tac 1);
-qed "PROJ_0";
-
-Goalw [COMP_def] "[| l \\<in> list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
-by (Asm_simp_tac 1);
-qed "COMP_1";
-
-Goalw [PREC_def] "l \\<in> list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
-by (Asm_simp_tac 1);
-qed "PREC_0";
-
-Goalw [PREC_def]
- "[| x \\<in> nat; l \\<in> 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";
-
--- a/src/ZF/Induct/Primrec_defs.thy Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(* 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 == \\<lambda>l \\<in> list(nat).list_case(0, %x xs. succ(x), l)"
-
- CONST_def "CONST(k) == \\<lambda>l \\<in> list(nat).k"
-
- PROJ_def "PROJ(i) == \\<lambda>l \\<in> list(nat). list_case(0, %x xs. x, drop(i,l))"
-
- COMP_def "COMP(g,fs) == \\<lambda>l \\<in> 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) ==
- \\<lambda>l \\<in> 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
--- a/src/ZF/Induct/PropLog.ML Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,249 +0,0 @@
-(* 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 \\<in> 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 \\<in> 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 \\<subseteq> H ==> thms(G) \\<subseteq> 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 \\<in> 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 \\<in> 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 \\<subseteq> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> 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 \\<in> prop; q \\<in> 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 \\<in> 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} \\<subseteq> hyps(p, t-{v}) *)
-Goal "p \\<in> prop ==> hyps(p, t-{v}) \\<subseteq> 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} \\<subseteq> hyps(p, cons(v,t)) *)
-Goal "p \\<in> prop ==> hyps(p, cons(v,t)) \\<subseteq> 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 \\<subseteq> cons(a, B-cons(a,C))";
-by (Fast_tac 1);
-qed "cons_Diff_same";
-
-Goal "cons(a, B-{c}) - D \\<subseteq> 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) \\<in> Fin(hyps(p,0) Un hyps(p,nat))*)
-Goal "p \\<in> prop ==> hyps(p,t) \\<in> Fin(\\<Union>v \\<in> 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 \\<in> prop; 0 |= p |] ==> \\<forall>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 \\<in> 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 \\<in> Fin(prop) ==> \\<forall>p \\<in> 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 \\<in> Fin(prop) ==> H |- p <-> H |= p & p \\<in> prop";
-by (fast_tac (claset() addSEs [soundness, finite RS completeness,
- thms_in_pl]) 1);
-qed "thms_iff";
-
-writeln"Reached end of file.";
--- a/src/ZF/Induct/PropLog.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/PropLog.thy Thu Dec 20 15:17:48 2001 +0100
@@ -1,68 +1,297 @@
-(* Title: ZF/ex/PropLog.thy
+(* Title: ZF/Induct/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.
+
+Inductive definition of propositional logic.
+Soundness and completeness w.r.t. truth-tables.
+
+Prove: If H|=p then G|=p where G \<in> Fin(H)
*)
-PropLog = Main +
+theory PropLog = Main:
(** The datatype of propositions; note mixfix syntax **)
consts
- prop :: i
+ propn :: "i"
datatype
- "prop" = Fls
- | Var ("n \\<in> nat") ("#_" [100] 100)
- | "=>" ("p \\<in> prop", "q \\<in> prop") (infixr 90)
+ "propn" = Fls
+ | Var ("n \<in> nat") ("#_" [100] 100)
+ | "=>" ("p \<in> propn", "q \<in> propn") (infixr 90)
(** The proof system **)
consts
- thms :: i => i
+ thms :: "i => i"
syntax
- "|-" :: [i,i] => o (infixl 50)
+ "|-" :: "[i,i] => o" (infixl 50)
translations
- "H |- p" == "p \\<in> thms(H)"
+ "H |- p" == "p \<in> thms(H)"
inductive
- domains "thms(H)" <= "prop"
- intrs
- H "[| p \\<in> H; p \\<in> prop |] ==> H |- p"
- K "[| p \\<in> prop; q \\<in> prop |] ==> H |- p=>q=>p"
- S "[| p \\<in> prop; q \\<in> prop; r \\<in> prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
- DN "p \\<in> prop ==> H |- ((p=>Fls) => Fls) => p"
- MP "[| H |- p=>q; H |- p; p \\<in> prop; q \\<in> prop |] ==> H |- q"
- type_intrs "prop.intrs"
+ domains "thms(H)" <= "propn"
+ intros
+ H: "[| p \<in> H; p \<in> propn |] ==> H |- p"
+ K: "[| p \<in> propn; q \<in> propn |] ==> H |- p=>q=>p"
+ S: "[| p \<in> propn; q \<in> propn; r \<in> propn |]
+ ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+ DN: "p \<in> propn ==> H |- ((p=>Fls) => Fls) => p"
+ MP: "[| H |- p=>q; H |- p; p \<in> propn; q \<in> propn |] ==> H |- q"
+ type_intros "propn.intros"
(** The semantics **)
consts
- "|=" :: [i,i] => o (infixl 50)
- hyps :: [i,i] => i
- is_true_fun :: [i,i] => i
+ "|=" :: "[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 :: "[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 == \\<forall>t. (\\<forall>q \\<in> H. is_true(q,t)) --> is_true(p,t)"
+ logcon_def: "H |= p == \<forall>t. (\<forall>q \<in> 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 \\<in> t then {#v} else {#v=>Fls})"
+ "hyps(Var(v), t) = (if v \<in> 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 \\<in> t then 1 else 0)"
+ "is_true_fun(Var(v), t) = (if v \<in> 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)"
+declare propn.intros [simp]
+
+(*** Semantics of propositional logic ***)
+
+(** The function is_true **)
+
+lemma is_true_Fls [simp]: "is_true(Fls,t) <-> False"
+by (simp add: is_true_def)
+
+lemma is_true_Var [simp]: "is_true(#v,t) <-> v \<in> t"
+by (simp add: is_true_def)
+
+lemma is_true_Imp [simp]: "is_true(p=>q,t) <-> (is_true(p,t)-->is_true(q,t))"
+by (simp add: is_true_def)
+
+
+(*** Proof theory of propositional logic ***)
+
+lemma thms_mono: "G \<subseteq> H ==> thms(G) \<subseteq> thms(H)"
+apply (unfold thms.defs )
+apply (rule lfp_mono)
+apply (rule thms.bnd_mono)+
+apply (assumption | rule univ_mono basic_monos)+
+done
+
+lemmas thms_in_pl = thms.dom_subset [THEN subsetD]
+
+inductive_cases ImpE: "p=>q \<in> propn"
+
+(*Stronger Modus Ponens rule: no typechecking!*)
+lemma thms_MP: "[| H |- p=>q; H |- p |] ==> H |- q"
+apply (rule thms.MP)
+apply (erule asm_rl thms_in_pl thms_in_pl [THEN ImpE])+
+done
+
+(*Rule is called I for Identity Combinator, not for Introduction*)
+lemma thms_I: "p \<in> propn ==> H |- p=>p"
+apply (rule thms.S [THEN thms_MP, THEN thms_MP])
+apply (rule_tac [5] thms.K)
+apply (rule_tac [4] thms.K)
+apply (simp_all add: propn.intros )
+done
+
+(** Weakening, left and right **)
+
+(* [| G \<subseteq> H; G|-p |] ==> H|-p Order of premises is convenient with RS*)
+lemmas weaken_left = thms_mono [THEN subsetD, standard]
+
+(* H |- p ==> cons(a,H) |- p *)
+lemmas weaken_left_cons = subset_consI [THEN weaken_left]
+
+lemmas weaken_left_Un1 = Un_upper1 [THEN weaken_left]
+lemmas weaken_left_Un2 = Un_upper2 [THEN weaken_left]
+
+lemma weaken_right: "[| H |- q; p \<in> propn |] ==> H |- p=>q"
+by (simp_all add: thms.K [THEN thms_MP] thms_in_pl)
+
+
+(*The deduction theorem*)
+lemma deduction: "[| cons(p,H) |- q; p \<in> propn |] ==> H |- p=>q"
+apply (erule thms.induct)
+ apply (blast intro: thms_I thms.H [THEN weaken_right])
+ apply (blast intro: thms.K [THEN weaken_right])
+ apply (blast intro: thms.S [THEN weaken_right])
+ apply (blast intro: thms.DN [THEN weaken_right])
+apply (blast intro: thms.S [THEN thms_MP [THEN thms_MP]])
+done
+
+
+(*The cut rule*)
+lemma cut: "[| H|-p; cons(p,H) |- q |] ==> H |- q"
+apply (rule deduction [THEN thms_MP])
+apply (simp_all add: thms_in_pl)
+done
+
+lemma thms_FlsE: "[| H |- Fls; p \<in> propn |] ==> H |- p"
+apply (rule thms.DN [THEN thms_MP])
+apply (rule_tac [2] weaken_right)
+apply (simp_all add: propn.intros)
+done
+
+(* [| H |- p=>Fls; H |- p; q \<in> propn |] ==> H |- q *)
+lemmas thms_notE = thms_MP [THEN thms_FlsE, standard]
+
+(*Soundness of the rules wrt truth-table semantics*)
+lemma soundness: "H |- p ==> H |= p"
+apply (unfold logcon_def)
+apply (erule thms.induct)
+apply auto
+done
+
+(*** Towards the completeness proof ***)
+
+lemma Fls_Imp: "[| H |- p=>Fls; q \<in> propn |] ==> H |- p=>q"
+apply (frule thms_in_pl)
+apply (rule deduction)
+apply (rule weaken_left_cons [THEN thms_notE])
+apply (blast intro: thms.H elim: ImpE)+
+done
+
+lemma Imp_Fls: "[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls"
+apply (frule thms_in_pl)
+apply (frule thms_in_pl [of concl: "q=>Fls"])
+apply (rule deduction)
+apply (erule weaken_left_cons [THEN thms_MP])
+apply (rule consI1 [THEN thms.H, THEN thms_MP])
+apply (blast intro: weaken_left_cons elim: ImpE)+
+done
+
+(*Typical example of strengthening the induction formula*)
+lemma hyps_thms_if:
+ "p \<in> propn ==> hyps(p,t) |- (if is_true(p,t) then p else p=>Fls)"
+apply (simp (no_asm))
+apply (induct_tac "p")
+apply (simp_all (no_asm_simp) add: thms_I thms.H)
+apply (safe elim!: Fls_Imp [THEN weaken_left_Un1]
+ Fls_Imp [THEN weaken_left_Un2])
+apply (blast intro: weaken_left_Un1 weaken_left_Un2 weaken_right Imp_Fls)+
+done
+
+(*Key lemma for completeness; yields a set of assumptions satisfying p*)
+lemma logcon_thms_p: "[| p \<in> propn; 0 |= p |] ==> hyps(p,t) |- p"
+apply (unfold logcon_def)
+apply (drule hyps_thms_if)
+apply simp
+done
+
+
+(*For proving certain theorems in our new propositional logic*)
+lemmas propn_SIs = propn.intros deduction
+lemmas propn_Is = thms_in_pl thms.H thms.H [THEN thms_MP]
+
+
+(*The excluded middle in the form of an elimination rule*)
+lemma thms_excluded_middle:
+ "[| p \<in> propn; q \<in> propn |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q"
+apply (rule deduction [THEN deduction])
+apply (rule thms.DN [THEN thms_MP])
+apply (best intro!: propn_SIs intro: propn_Is)+
+done
+
+(*Hard to prove directly because it requires cuts*)
+lemma thms_excluded_middle_rule:
+ "[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p \<in> propn |] ==> H |- q"
+apply (rule thms_excluded_middle [THEN thms_MP, THEN thms_MP])
+apply (blast intro!: propn_SIs intro: propn_Is)+
+done
+
+
+(*** 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} \<subseteq> hyps(p, t-{v}) *)
+lemma hyps_Diff:
+ "p \<in> propn ==> hyps(p, t-{v}) \<subseteq> cons(#v=>Fls, hyps(p,t)-{#v})"
+by (induct_tac "p", auto)
+
+(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p
+ we also have hyps(p,t)-{#v=>Fls} \<subseteq> hyps(p, cons(v,t)) *)
+lemma hyps_cons:
+ "p \<in> propn ==> hyps(p, cons(v,t)) \<subseteq> cons(#v, hyps(p,t)-{#v=>Fls})"
+by (induct_tac "p", auto)
+
+(** Two lemmas for use with weaken_left **)
+
+lemma cons_Diff_same: "B-C \<subseteq> cons(a, B-cons(a,C))"
+by blast
+
+lemma cons_Diff_subset2: "cons(a, B-{c}) - D \<subseteq> cons(a, B-cons(c,D))"
+by blast
+
+(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls
+ could probably prove the stronger hyps(p,t) \<in> Fin(hyps(p,0) Un hyps(p,nat))*)
+lemma hyps_finite: "p \<in> propn ==> hyps(p,t) \<in> Fin(\<Union>v \<in> nat. {#v, #v=>Fls})"
+by (induct_tac "p", auto)
+
+lemmas Diff_weaken_left = Diff_mono [OF _ subset_refl, THEN weaken_left]
+
+(*Induction on the finite set of assumptions hyps(p,t0).
+ We may repeatedly subtract assumptions until none are left!*)
+lemma completeness_0_lemma [rule_format]:
+ "[| p \<in> propn; 0 |= p |] ==> \<forall>t. hyps(p,t) - hyps(p,t0) |- p"
+apply (frule hyps_finite)
+apply (erule Fin_induct)
+apply (simp add: logcon_thms_p Diff_0)
+(*inductive step*)
+apply safe
+(*Case hyps(p,t)-cons(#v,Y) |- p *)
+ apply (rule thms_excluded_middle_rule)
+ apply (erule_tac [3] propn.intros)
+ apply (blast intro: cons_Diff_same [THEN weaken_left])
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
+ hyps_Diff [THEN Diff_weaken_left])
+(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
+apply (rule thms_excluded_middle_rule)
+ apply (erule_tac [3] propn.intros)
+ apply (blast intro: cons_Diff_subset2 [THEN weaken_left]
+ hyps_cons [THEN Diff_weaken_left])
+apply (blast intro: cons_Diff_same [THEN weaken_left])
+done
+
+(*The base case for completeness*)
+lemma completeness_0: "[| p \<in> propn; 0 |= p |] ==> 0 |- p"
+apply (rule Diff_cancel [THEN subst])
+apply (blast intro: completeness_0_lemma)
+done
+
+(*A semantic analogue of the Deduction Theorem*)
+lemma logcon_Imp: "[| cons(p,H) |= q |] ==> H |= p=>q"
+by (simp add: logcon_def)
+
+lemma completeness [rule_format]:
+ "H \<in> Fin(propn) ==> \<forall>p \<in> propn. H |= p --> H |- p"
+apply (erule Fin_induct)
+apply (safe intro!: completeness_0)
+apply (rule weaken_left_cons [THEN thms_MP])
+ apply (blast intro!: logcon_Imp propn.intros)
+apply (blast intro: propn_Is)
+done
+
+lemma thms_iff: "H \<in> Fin(propn) ==> H |- p <-> H |= p & p \<in> propn"
+by (blast intro: soundness completeness thms_in_pl)
+
end
--- a/src/ZF/Induct/Rmap.ML Thu Dec 20 15:00:02 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-(* 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 \\<subseteq> s ==> rmap(r) \\<subseteq> 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 "<Nil,zs> \\<in> rmap(r)"
-and Cons_rmap_case = rmap.mk_cases "<Cons(x,xs),zs> \\<in> rmap(r)";
-
-AddIs rmap.intrs;
-AddSEs [Nil_rmap_case, Cons_rmap_case];
-
-Goal "r \\<subseteq> A*B ==> rmap(r) \\<subseteq> 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 \\<subseteq> domain(r) ==> list(A) \\<subseteq> 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 \\<in> 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 \\<in> A->B; x \\<in> 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";
--- a/src/ZF/Induct/Rmap.thy Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/Induct/Rmap.thy Thu Dec 20 15:17:48 2001 +0100
@@ -6,20 +6,66 @@
Inductive definition of an operator to "map" a relation over a list
*)
-Rmap = Main +
+theory Rmap = Main:
consts
- rmap :: i=>i
+ rmap :: "i=>i"
inductive
domains "rmap(r)" <= "list(domain(r))*list(range(r))"
- intrs
- NilI "<Nil,Nil> \\<in> rmap(r)"
+ intros
+ NilI: "<Nil,Nil> \<in> rmap(r)"
+
+ ConsI: "[| <x,y>: r; <xs,ys> \<in> rmap(r) |]
+ ==> <Cons(x,xs), Cons(y,ys)> \<in> rmap(r)"
+
+ type_intros domainI rangeI list.intros
+
+lemma rmap_mono: "r \<subseteq> s ==> rmap(r) \<subseteq> rmap(s)"
+apply (unfold rmap.defs )
+apply (rule lfp_mono)
+apply (rule rmap.bnd_mono)+
+apply (assumption |
+ rule Sigma_mono list_mono domain_mono range_mono basic_monos)+
+done
+
+inductive_cases Nil_rmap_case [elim!]: "<Nil,zs> \<in> rmap(r)"
+inductive_cases Cons_rmap_case [elim!]: "<Cons(x,xs),zs> \<in> rmap(r)"
+
+declare rmap.intros [intro]
+
+lemma rmap_rel_type: "r \<subseteq> A*B ==> rmap(r) \<subseteq> list(A)*list(B)"
+apply (rule rmap.dom_subset [THEN subset_trans])
+apply (assumption |
+ rule domain_rel_subset range_rel_subset Sigma_mono list_mono)+
+done
- ConsI "[| <x,y>: r; <xs,ys> \\<in> rmap(r) |] ==>
- <Cons(x,xs), Cons(y,ys)> \\<in> rmap(r)"
+lemma rmap_total: "A \<subseteq> domain(r) ==> list(A) \<subseteq> domain(rmap(r))"
+apply (rule subsetI)
+apply (erule list.induct)
+apply blast+
+done
+
+lemma rmap_functional: "function(r) ==> function(rmap(r))"
+apply (unfold function_def)
+apply (rule impI [THEN allI, THEN allI])
+apply (erule rmap.induct)
+apply blast+
+done
- type_intrs "[domainI,rangeI] @ list.intrs"
+
+(** If f is a function then rmap(f) behaves as expected. **)
+
+lemma rmap_fun_type: "f \<in> A->B ==> rmap(f): list(A)->list(B)"
+by (simp add: Pi_iff rmap_rel_type rmap_functional rmap_total)
+
+lemma rmap_Nil: "rmap(f)`Nil = Nil"
+by (unfold apply_def, blast)
+
+lemma rmap_Cons: "[| f \<in> A->B; x \<in> A; xs: list(A) |]
+ ==> rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)"
+by (blast intro: apply_equality apply_Pair rmap_fun_type rmap.intros)
+
end
--- a/src/ZF/IsaMakefile Thu Dec 20 15:00:02 2001 +0100
+++ b/src/ZF/IsaMakefile Thu Dec 20 15:17:48 2001 +0100
@@ -122,13 +122,11 @@
ZF-Induct: ZF $(LOG)/ZF-Induct.gz
-$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
- Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.ML Induct/Comb.thy \
- Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML \
+$(LOG)/ZF-Induct.gz: $(OUT)/ZF Induct/ROOT.ML Induct/Acc.thy \
+ Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.thy \
+ Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy \
Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
- Induct/Ntree.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 \
+ Induct/Ntree.thy Induct/Primrec.thy Induct/PropLog.thy Induct/Rmap.thy \
Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
@$(ISATOOL) usedir $(OUT)/ZF Induct