# HG changeset patch # User clasohm # Date 749915104 -3600 # Node ID 747f1aad03cf0a284732fe395f0ab89cf202d181 # Parent ab5ed678130d65bfa68336a5e4edf28e038a5a55 changed filenames to lower case name of theory the file contains (only one theory per file, therefore llist.ML has been split) diff -r ab5ed678130d -r 747f1aad03cf src/ZF/ex/LList.ML --- a/src/ZF/ex/LList.ML Wed Oct 06 14:21:36 1993 +0100 +++ b/src/ZF/ex/LList.ML Wed Oct 06 14:45:04 1993 +0100 @@ -75,76 +75,5 @@ val llist_subset_quniv = standard (llist_mono RS (llist_quniv RSN (2,subset_trans))); -(*** Equality for llist(A) as a greatest fixed point ***) - -structure LList_Eq = Co_Inductive_Fun - (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; - val rec_doms = [("lleq","llist(A) <*> llist(A)")]; - val sintrs = - [" : lleq(A)", - "[| a:A; : lleq(A) |] ==> : lleq(A)"]; - val monos = []; - val con_defs = []; - val type_intrs = LList.intrs@[QSigmaI]; - val type_elims = [QSigmaE2]); - -(** Alternatives for above: - val con_defs = LList.con_defs - val type_intrs = co_data_typechecks - val type_elims = [quniv_QPair_E] -**) - -val lleq_cs = subset_cs - addSIs [succI1, Int_Vset_0_subset, - QPair_Int_Vset_succ_subset_trans, - QPair_Int_Vset_subset_trans]; - -(*Keep unfolding the lazy list until the induction hypothesis applies*) -goal LList_Eq.thy - "!!i. Ord(i) ==> ALL l l'. : lleq(A) --> l Int Vset(i) <= l'"; -by (etac trans_induct 1); -by (safe_tac subset_cs); -by (etac LList_Eq.elim 1); -by (safe_tac (subset_cs addSEs [QPair_inject])); -by (rewrite_goals_tac LList.con_defs); -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); -(*0 case*) -by (fast_tac lleq_cs 1); -(*succ(j) case*) -by (rewtac QInr_def); -by (fast_tac lleq_cs 1); -(*Limit(i) case*) -by (etac (Limit_Vfrom_eq RS ssubst) 1); -by (rtac (Int_UN_distrib RS ssubst) 1); -by (fast_tac lleq_cs 1); -val lleq_Int_Vset_subset_lemma = result(); - -val lleq_Int_Vset_subset = standard - (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); - - -(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) -val [prem] = goal LList_Eq.thy " : lleq(A) ==> : lleq(A)"; -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); -by (safe_tac qconverse_cs); -by (etac LList_Eq.elim 1); -by (ALLGOALS (fast_tac qconverse_cs)); -val lleq_symmetric = result(); - -goal LList_Eq.thy "!!l l'. : lleq(A) ==> l=l'"; -by (rtac equalityI 1); -by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 - ORELSE etac lleq_symmetric 1)); -val lleq_implies_equal = result(); - -val [eqprem,lprem] = goal LList_Eq.thy - "[| l=l'; l: llist(A) |] ==> : lleq(A)"; -by (res_inst_tac [("X", "{. l: llist(A)}")] LList_Eq.co_induct 1); -by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); -by (safe_tac qpair_cs); -by (etac LList.elim 1); -by (ALLGOALS (fast_tac qpair_cs)); -val equal_llist_implies_leq = result(); - - +(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow + automatic association between theory name and filename. *) diff -r ab5ed678130d -r 747f1aad03cf src/ZF/ex/LList_Eq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/LList_Eq.ML Wed Oct 06 14:45:04 1993 +0100 @@ -0,0 +1,81 @@ +(* Title: ZF/ex/llist_eq.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Former part of llist.ML, contains definition and use of LList_Eq +*) + +(*** Equality for llist(A) as a greatest fixed point ***) + +structure LList_Eq = Co_Inductive_Fun + (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; + val rec_doms = [("lleq","llist(A) <*> llist(A)")]; + val sintrs = + [" : lleq(A)", + "[| a:A; : lleq(A) |] ==> : lleq(A)"]; + val monos = []; + val con_defs = []; + val type_intrs = LList.intrs@[QSigmaI]; + val type_elims = [QSigmaE2]); + +(** Alternatives for above: + val con_defs = LList.con_defs + val type_intrs = co_data_typechecks + val type_elims = [quniv_QPair_E] +**) + +val lleq_cs = subset_cs + addSIs [succI1, Int_Vset_0_subset, + QPair_Int_Vset_succ_subset_trans, + QPair_Int_Vset_subset_trans]; + +(*Keep unfolding the lazy list until the induction hypothesis applies*) +goal LList_Eq.thy + "!!i. Ord(i) ==> ALL l l'. : lleq(A) --> l Int Vset(i) <= l'"; +by (etac trans_induct 1); +by (safe_tac subset_cs); +by (etac LList_Eq.elim 1); +by (safe_tac (subset_cs addSEs [QPair_inject])); +by (rewrite_goals_tac LList.con_defs); +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); +(*0 case*) +by (fast_tac lleq_cs 1); +(*succ(j) case*) +by (rewtac QInr_def); +by (fast_tac lleq_cs 1); +(*Limit(i) case*) +by (etac (Limit_Vfrom_eq RS ssubst) 1); +by (rtac (Int_UN_distrib RS ssubst) 1); +by (fast_tac lleq_cs 1); +val lleq_Int_Vset_subset_lemma = result(); + +val lleq_Int_Vset_subset = standard + (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); + + +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) +val [prem] = goal LList_Eq.thy " : lleq(A) ==> : lleq(A)"; +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); +by (safe_tac qconverse_cs); +by (etac LList_Eq.elim 1); +by (ALLGOALS (fast_tac qconverse_cs)); +val lleq_symmetric = result(); + +goal LList_Eq.thy "!!l l'. : lleq(A) ==> l=l'"; +by (rtac equalityI 1); +by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 + ORELSE etac lleq_symmetric 1)); +val lleq_implies_equal = result(); + +val [eqprem,lprem] = goal LList_Eq.thy + "[| l=l'; l: llist(A) |] ==> : lleq(A)"; +by (res_inst_tac [("X", "{. l: llist(A)}")] LList_Eq.co_induct 1); +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); +by (safe_tac qpair_cs); +by (etac LList.elim 1); +by (ALLGOALS (fast_tac qpair_cs)); +val equal_llist_implies_leq = result(); + + diff -r ab5ed678130d -r 747f1aad03cf src/ZF/ex/ROOT.ML --- a/src/ZF/ex/ROOT.ML Wed Oct 06 14:21:36 1993 +0100 +++ b/src/ZF/ex/ROOT.ML Wed Oct 06 14:45:04 1993 +0100 @@ -20,18 +20,18 @@ (*Binary integer arithmetic*) use "ex/twos-compl.ML"; time_use "ex/bin.ML"; -time_use_thy "ex/bin-fn"; +time_use_thy "ex/binfn"; (** Datatypes **) (*binary trees*) time_use "ex/bt.ML"; -time_use_thy "ex/bt-fn"; +time_use_thy "ex/bt_fn"; (*terms: recursion over the list functor*) time_use "ex/term.ML"; -time_use_thy "ex/term-fn"; +time_use_thy "ex/termfn"; (*trees/forests: mutual recursion*) time_use "ex/tf.ML"; -time_use_thy "ex/tf-fn"; +time_use_thy "ex/tf_fn"; (*Enormous enumeration type -- could be even bigger?*) time_use "ex/enum.ML"; @@ -40,7 +40,7 @@ time_use "ex/rmap.ML"; (*completeness of propositional logic*) time_use "ex/prop.ML"; -time_use_thy "ex/prop-log"; +time_use_thy "ex/propthms"; (*two Coq examples by Ch. Paulin-Mohring*) time_use "ex/listn.ML"; time_use "ex/acc.ML"; @@ -52,7 +52,8 @@ (** Co-Datatypes **) time_use "ex/llist.ML"; -time_use_thy "ex/llist-fn"; +time_use "ex/llist_eq.ML"; +time_use_thy "ex/llistfn"; maketest"END: Root file for ZF Set Theory examples"; diff -r ab5ed678130d -r 747f1aad03cf src/ZF/ex/llist.ML --- a/src/ZF/ex/llist.ML Wed Oct 06 14:21:36 1993 +0100 +++ b/src/ZF/ex/llist.ML Wed Oct 06 14:45:04 1993 +0100 @@ -75,76 +75,5 @@ val llist_subset_quniv = standard (llist_mono RS (llist_quniv RSN (2,subset_trans))); -(*** Equality for llist(A) as a greatest fixed point ***) - -structure LList_Eq = Co_Inductive_Fun - (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; - val rec_doms = [("lleq","llist(A) <*> llist(A)")]; - val sintrs = - [" : lleq(A)", - "[| a:A; : lleq(A) |] ==> : lleq(A)"]; - val monos = []; - val con_defs = []; - val type_intrs = LList.intrs@[QSigmaI]; - val type_elims = [QSigmaE2]); - -(** Alternatives for above: - val con_defs = LList.con_defs - val type_intrs = co_data_typechecks - val type_elims = [quniv_QPair_E] -**) - -val lleq_cs = subset_cs - addSIs [succI1, Int_Vset_0_subset, - QPair_Int_Vset_succ_subset_trans, - QPair_Int_Vset_subset_trans]; - -(*Keep unfolding the lazy list until the induction hypothesis applies*) -goal LList_Eq.thy - "!!i. Ord(i) ==> ALL l l'. : lleq(A) --> l Int Vset(i) <= l'"; -by (etac trans_induct 1); -by (safe_tac subset_cs); -by (etac LList_Eq.elim 1); -by (safe_tac (subset_cs addSEs [QPair_inject])); -by (rewrite_goals_tac LList.con_defs); -by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); -(*0 case*) -by (fast_tac lleq_cs 1); -(*succ(j) case*) -by (rewtac QInr_def); -by (fast_tac lleq_cs 1); -(*Limit(i) case*) -by (etac (Limit_Vfrom_eq RS ssubst) 1); -by (rtac (Int_UN_distrib RS ssubst) 1); -by (fast_tac lleq_cs 1); -val lleq_Int_Vset_subset_lemma = result(); - -val lleq_Int_Vset_subset = standard - (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); - - -(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) -val [prem] = goal LList_Eq.thy " : lleq(A) ==> : lleq(A)"; -by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); -by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); -by (safe_tac qconverse_cs); -by (etac LList_Eq.elim 1); -by (ALLGOALS (fast_tac qconverse_cs)); -val lleq_symmetric = result(); - -goal LList_Eq.thy "!!l l'. : lleq(A) ==> l=l'"; -by (rtac equalityI 1); -by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 - ORELSE etac lleq_symmetric 1)); -val lleq_implies_equal = result(); - -val [eqprem,lprem] = goal LList_Eq.thy - "[| l=l'; l: llist(A) |] ==> : lleq(A)"; -by (res_inst_tac [("X", "{. l: llist(A)}")] LList_Eq.co_induct 1); -by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); -by (safe_tac qpair_cs); -by (etac LList.elim 1); -by (ALLGOALS (fast_tac qpair_cs)); -val equal_llist_implies_leq = result(); - - +(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow + automatic association between theory name and filename. *) diff -r ab5ed678130d -r 747f1aad03cf src/ZF/ex/llist_eq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/ZF/ex/llist_eq.ML Wed Oct 06 14:45:04 1993 +0100 @@ -0,0 +1,81 @@ +(* Title: ZF/ex/llist_eq.ML + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1993 University of Cambridge + +Former part of llist.ML, contains definition and use of LList_Eq +*) + +(*** Equality for llist(A) as a greatest fixed point ***) + +structure LList_Eq = Co_Inductive_Fun + (val thy = LList.thy addconsts [(["lleq"],"i=>i")]; + val rec_doms = [("lleq","llist(A) <*> llist(A)")]; + val sintrs = + [" : lleq(A)", + "[| a:A; : lleq(A) |] ==> : lleq(A)"]; + val monos = []; + val con_defs = []; + val type_intrs = LList.intrs@[QSigmaI]; + val type_elims = [QSigmaE2]); + +(** Alternatives for above: + val con_defs = LList.con_defs + val type_intrs = co_data_typechecks + val type_elims = [quniv_QPair_E] +**) + +val lleq_cs = subset_cs + addSIs [succI1, Int_Vset_0_subset, + QPair_Int_Vset_succ_subset_trans, + QPair_Int_Vset_subset_trans]; + +(*Keep unfolding the lazy list until the induction hypothesis applies*) +goal LList_Eq.thy + "!!i. Ord(i) ==> ALL l l'. : lleq(A) --> l Int Vset(i) <= l'"; +by (etac trans_induct 1); +by (safe_tac subset_cs); +by (etac LList_Eq.elim 1); +by (safe_tac (subset_cs addSEs [QPair_inject])); +by (rewrite_goals_tac LList.con_defs); +by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac); +(*0 case*) +by (fast_tac lleq_cs 1); +(*succ(j) case*) +by (rewtac QInr_def); +by (fast_tac lleq_cs 1); +(*Limit(i) case*) +by (etac (Limit_Vfrom_eq RS ssubst) 1); +by (rtac (Int_UN_distrib RS ssubst) 1); +by (fast_tac lleq_cs 1); +val lleq_Int_Vset_subset_lemma = result(); + +val lleq_Int_Vset_subset = standard + (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp); + + +(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*) +val [prem] = goal LList_Eq.thy " : lleq(A) ==> : lleq(A)"; +by (rtac (prem RS qconverseI RS LList_Eq.co_induct) 1); +by (rtac (LList_Eq.dom_subset RS qconverse_type) 1); +by (safe_tac qconverse_cs); +by (etac LList_Eq.elim 1); +by (ALLGOALS (fast_tac qconverse_cs)); +val lleq_symmetric = result(); + +goal LList_Eq.thy "!!l l'. : lleq(A) ==> l=l'"; +by (rtac equalityI 1); +by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1 + ORELSE etac lleq_symmetric 1)); +val lleq_implies_equal = result(); + +val [eqprem,lprem] = goal LList_Eq.thy + "[| l=l'; l: llist(A) |] ==> : lleq(A)"; +by (res_inst_tac [("X", "{. l: llist(A)}")] LList_Eq.co_induct 1); +by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1); +by (safe_tac qpair_cs); +by (etac LList.elim 1); +by (ALLGOALS (fast_tac qpair_cs)); +val equal_llist_implies_leq = result(); + +