# HG changeset patch # User lcp # Date 775472985 -7200 # Node ID 3fc829fa81d299ab2f27838d17fb237ad63a21f9 # Parent 612888a078894c265e26f5b765d86434d67f21c3 Inductive defs need no longer mention SigmaI/E2 diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/IMP/Evala.ML --- a/src/ZF/IMP/Evala.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/IMP/Evala.ML Fri Jul 29 11:09:45 1994 +0200 @@ -21,6 +21,6 @@ val monos = []; val con_defs = []; - val type_intrs = Aexp.intrs@[SigmaI,apply_funtype]; - val type_elims = [SigmaE2] + val type_intrs = Aexp.intrs@[apply_funtype]; + val type_elims = [] ); diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/IMP/Evalb.ML --- a/src/ZF/IMP/Evalb.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/IMP/Evalb.ML Fri Jul 29 11:09:45 1994 +0200 @@ -25,7 +25,7 @@ val monos = []; val con_defs = []; - val type_intrs = Bexp.intrs@[SigmaI,apply_funtype,and_type,or_type, + val type_intrs = Bexp.intrs@[apply_funtype,and_type,or_type, bool_1I,bool_0I,not_type]; - val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD) ]; + val type_elims = [make_elim(Evala.dom_subset RS subsetD) ]; ); diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/IMP/Evalc.ML --- a/src/ZF/IMP/Evalc.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/IMP/Evalc.ML Fri Jul 29 11:09:45 1994 +0200 @@ -28,6 +28,6 @@ val monos = []; val con_defs = [assign_def]; - val type_intrs = Bexp.intrs@Com.intrs@[SigmaI,if_type,lam_type,apply_type]; - val type_elims = [SigmaE2,make_elim(Evala.dom_subset RS subsetD), - make_elim(Evalb.dom_subset RS subsetD) ]); + val type_intrs = Bexp.intrs@Com.intrs@[if_type,lam_type,apply_type]; + val type_elims = [make_elim(Evala.dom_subset RS subsetD), + make_elim(Evalb.dom_subset RS subsetD) ]); diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/ex/Contract0.ML --- a/src/ZF/ex/Contract0.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/ex/Contract0.ML Fri Jul 29 11:09:45 1994 +0200 @@ -9,18 +9,18 @@ open Contract0; structure Contract = Inductive_Fun - (val thy = Contract0.thy; - val thy_name = "Contract"; - val rec_doms = [("contract","comb*comb")]; - val sintrs = + (val thy = Contract0.thy; + val thy_name = "Contract"; + val rec_doms = [("contract","comb*comb")]; + val sintrs = ["[| p:comb; q:comb |] ==> K#p#q -1-> p", "[| p:comb; q:comb; r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)", "[| p-1->q; r:comb |] ==> p#r -1-> q#r", "[| p-1->q; r:comb |] ==> r#p -1-> r#q"]; - val monos = []; - val con_defs = []; - val type_intrs = Comb.intrs@[SigmaI]; - val type_elims = [SigmaE2]); + val monos = []; + val con_defs = []; + val type_intrs = Comb.intrs; + val type_elims = []); val [K_contract,S_contract,Ap_contract1,Ap_contract2] = Contract.intrs; diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/ex/LList_Eq.ML --- a/src/ZF/ex/LList_Eq.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/ex/LList_Eq.ML Fri Jul 29 11:09:45 1994 +0200 @@ -11,16 +11,16 @@ a q/Q to the Sigma, Pair and converse rules.*) structure LList_Eq = CoInductive_Fun - (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)] - val thy_name = "LList_Eq" + (val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)] + val thy_name = "LList_Eq" 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 @ [SigmaI] - val type_elims = [SigmaE2]); + val type_intrs = LList.intrs + val type_elims = []); (** Alternatives for above: val con_defs = LList.con_defs diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/ex/ListN.ML --- a/src/ZF/ex/ListN.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/ex/ListN.ML Fri Jul 29 11:09:45 1994 +0200 @@ -18,8 +18,8 @@ "[| a: A; : listn(A) |] ==> : listn(A)"] val monos = [] val con_defs = [] - val type_intrs = nat_typechecks @ List.intrs @ [SigmaI] - val type_elims = [SigmaE2]); + val type_intrs = nat_typechecks @ List.intrs + val type_elims = []); val listn_induct = standard (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp)); diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/ex/ParContract.ML --- a/src/ZF/ex/ParContract.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/ex/ParContract.ML Fri Jul 29 11:09:45 1994 +0200 @@ -10,18 +10,18 @@ *) structure ParContract = Inductive_Fun - (val thy = Contract.thy; - val thy_name = "ParContract"; - val rec_doms = [("parcontract","comb*comb")]; - val sintrs = + (val thy = Contract.thy; + val thy_name = "ParContract"; + val rec_doms = [("parcontract","comb*comb")]; + val sintrs = ["[| p:comb |] ==> p =1=> p", "[| p:comb; q:comb |] ==> K#p#q =1=> p", "[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)", "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"]; - val monos = []; - val con_defs = []; - val type_intrs = Comb.intrs@[SigmaI]; - val type_elims = [SigmaE2]); + val monos = []; + val con_defs = []; + val type_intrs = Comb.intrs; + val type_elims = []); val [parcontract_refl,K_parcontract,S_parcontract,Ap_parcontract] = ParContract.intrs; diff -r 612888a07889 -r 3fc829fa81d2 src/ZF/ex/Rmap.ML --- a/src/ZF/ex/Rmap.ML Fri Jul 29 11:03:23 1994 +0200 +++ b/src/ZF/ex/Rmap.ML Fri Jul 29 11:09:45 1994 +0200 @@ -7,18 +7,18 @@ *) structure Rmap = Inductive_Fun - (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)]; - val thy_name = "Rmap"; - val rec_doms = [("rmap", "list(domain(r))*list(range(r))")]; - val sintrs = + (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)]; + val thy_name = "Rmap"; + val rec_doms = [("rmap", "list(domain(r))*list(range(r))")]; + val sintrs = [" : rmap(r)", "[| : r; : rmap(r) |] ==> \ \ : rmap(r)"]; - val monos = []; - val con_defs = []; - val type_intrs = [domainI,rangeI] @ List.intrs @ [SigmaI] - val type_elims = [SigmaE2]); + val monos = []; + val con_defs = []; + val type_intrs = [domainI,rangeI] @ List.intrs + val type_elims = []); goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)"; by (rtac lfp_mono 1);