# HG changeset patch # User slotosch # Date 856173840 -3600 # Node ID 3c3a84cc85a90c0e11eb71ad4f1eeba77750d432 # Parent 533a84b3bedd288d97648bea5c3a07db07206170 Examples are adopted to the changes from HOLCF. Classlib is reduced. Classlib still uses arities, Classlib will change completely to new classes of ADTs diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Classlib.ML --- a/src/HOLCF/ex/Classlib.ML Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Classlib.ML Mon Feb 17 11:04:00 1997 +0100 @@ -1,196 +1,2 @@ open Classlib; -qed_goal "strict_qless" Classlib.thy "(UU .< x) = UU & (x .< UU) = UU" - (fn prems => - [ - (simp_tac (HOLCF_ss addsimps [strict_qpo,qless_def,strict_per]) 1) - ]); - -qed_goal "total_qless" Classlib.thy "[|x ~= UU; y ~= UU|] ==> (x .< y) ~= UU" - (fn prems => - [ - (cut_facts_tac prems 1), - (asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1), - (res_inst_tac [("p","x .= y")] trE 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1), - (res_inst_tac [("P","x .= y = UU")] notE 1), - (etac total_per 1), - (atac 1), - (atac 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_qpo,total_qpo,strict_per,total_per]) 1) - ]); - -qed_goal "irrefl_qless" Classlib.thy "[|x ~= UU|] ==> (x .< x)=FF" - (fn prems => - [ - (cut_facts_tac prems 1), - (asm_simp_tac (HOLCF_ss addsimps [total_per,qless_def,refl_per]) 1) - ]); - -qed_goal "asym_qless" Classlib.thy "~((x .< y)=TT & (y .< x)=TT)" - (fn prems => - [ - (case_tac "x ~= UU & y ~= UU" 1), - (etac conjE 1), - (asm_simp_tac (HOLCF_ss addsimps [qless_def]) 1), - (res_inst_tac [("p","x .= y")] trE 1), - (asm_simp_tac HOLCF_ss 1), - (asm_simp_tac HOLCF_ss 1), - (asm_simp_tac HOLCF_ss 1), - (rtac (sym_per RS subst) 1), - (asm_simp_tac HOLCF_ss 1), - (rtac (de_Morgan_conj RS iffD1) 1), - (res_inst_tac [("Pa","(x .= y)=TT")] classical2 1), - (asm_simp_tac (HOLCF_ss addsimps []) 1), - (etac conjE 1), - (rtac antisym_qpo 1), - (atac 1), - (atac 1), - (subgoal_tac "x=UU Á y=UU" 1), - (etac disjE 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_qless]) 1), - (fast_tac HOL_cs 1) - ]); - - -qed_goal "qless_iff" Classlib.thy "((x .< y)=TT) = ((x.=y)=FF & (x .<= y)=TT)" - (fn prems => - [ - (rtac iffI 1), - (asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1), - (res_inst_tac [("p","x .= y")] trE 1), - (res_inst_tac [("P","TT=UU")] notE 1), - (simp_tac (HOLCF_ss addsimps []) 1), - (rtac trans 1), - (etac sym 1), - (asm_simp_tac (HOLCF_ss addsimps []) 1), - (res_inst_tac [("P","TT=FF")] notE 1), - (simp_tac (HOLCF_ss addsimps []) 1), - (rtac trans 1), - (etac sym 1), - (asm_full_simp_tac (HOLCF_ss addsimps []) 1), - (rtac conjI 1), - (atac 1), - (rtac trans 1), - (atac 2), - (asm_full_simp_tac (HOLCF_ss addsimps []) 1), - (asm_full_simp_tac (HOLCF_ss addsimps [qless_def]) 1) - ]); - -qed_goal "trans_qless" Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT" - (fn prems => - [ - (cut_facts_tac prems 1), - (rtac (qless_iff RS iffD2) 1), - (rtac conjI 1), - (dtac (qless_iff RS iffD1) 1), - (dtac (qless_iff RS iffD1) 1), - (REPEAT (etac conjE 1)), - (case_tac "x~=UU & z~=UU" 1), - (REPEAT (etac conjE 1)), - (res_inst_tac [("p","x .= z")] trE 1), - (res_inst_tac [("P","x .= z = UU")] notE 1), - (rtac total_per 1), - (atac 1), - (atac 1), - (atac 1), - (res_inst_tac [("P","TT = FF")] notE 1), - (simp_tac (HOLCF_ss addsimps []) 1), - (subgoal_tac "(y.=z)=TT" 1), - (rtac trans 1), - (etac sym 1), - (atac 1), - (rtac antisym_qpo 1), - (atac 1), - (rtac trans_qpo 1), - (atac 2), - (etac (antisym_qpo_rev RS conjunct2) 1), - (atac 1), - (dtac (de_Morgan_conj RS iffD1) 1), - (etac disjE 1), - (dtac notnotD 1), - (res_inst_tac [("P","FF=UU")] notE 1), - (simp_tac (HOLCF_ss addsimps []) 1), - (rtac trans 1), - (etac sym 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1), - (dtac notnotD 1), - (res_inst_tac [("P","FF=UU")] notE 1), - (simp_tac (HOLCF_ss addsimps []) 1), - (rtac trans 1), - (etac sym 1), - (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1), - (dtac (qless_iff RS iffD1) 1), - (dtac (qless_iff RS iffD1) 1), - (REPEAT (etac conjE 1)), - (rtac trans_qpo 1), - (atac 1), - (atac 1) - ]); - -(* - -proof for transitivity depends on property antisym_qpo_rev -the proof is a bit lengthy - -val prems = goal Classlib.thy "[|(x .< y)=TT; (y .< z)=TT |] ==> (x .< z)=TT"; -by (cut_facts_tac prems 1); -by (rtac (qless_iff RS iffD2) 1); -by (rtac conjI 1); - -by (dtac (qless_iff RS iffD1) 1); -by (dtac (qless_iff RS iffD1) 1); -by (REPEAT (etac conjE 1)); -by (case_tac "x~=UU & z~=UU" 1); -by (REPEAT (etac conjE 1)); -by (res_inst_tac [("p","x .= z")] trE 1); -by (res_inst_tac [("P","x .= z = UU")] notE 1); - -by (rtac total_per 1); -by (atac 1); -by (atac 1); -by (atac 1); - -by (res_inst_tac [("P","TT = FF")] notE 1); -by (simp_tac (HOLCF_ss addsimps []) 1); -by (subgoal_tac "(y.=z)=TT" 1); -by (rtac trans 1); -by (etac sym 1); -back(); -back(); -back(); -by (atac 1); -by (rtac antisym_qpo 1); -by (atac 1); -by (rtac trans_qpo 1); -by (atac 2); -by (etac (antisym_qpo_rev RS conjunct2) 1); -by (atac 1); - -by (dtac (de_Morgan_conj RS iffD1) 1); -by (etac disjE 1); -by (dtac notnotD 1); -by (res_inst_tac [("P","FF=UU")] notE 1); -by (simp_tac (HOLCF_ss addsimps []) 1); -by (rtac trans 1); -by (etac sym 1); -by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1); - -by (dtac notnotD 1); -by (res_inst_tac [("P","FF=UU")] notE 1); -by (simp_tac (HOLCF_ss addsimps []) 1); -by (rtac trans 1); -by (etac sym 1); -back(); -by (asm_simp_tac (HOLCF_ss addsimps [strict_per]) 1); - -by (dtac (qless_iff RS iffD1) 1); -by (dtac (qless_iff RS iffD1) 1); -by (REPEAT (etac conjE 1)); -by (rtac trans_qpo 1); -by (atac 1); -by (atac 1); -val trans_qless = result(); -*) diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Classlib.thy --- a/src/HOLCF/ex/Classlib.thy Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Classlib.thy Mon Feb 17 11:04:00 1997 +0100 @@ -5,13 +5,14 @@ Introduce various type classes -The 8bit package is needed for this theory - -The type void of HOLCF/Void.thy is a witness for all the introduced classes. +The type void of HOLCF/One.thy is a witness for all the introduced classes. Inspect theory Witness.thy for all the proofs. -the trivial instance for ++ -- ** // is LAM x y.(UU::void) -the trivial instance for .= and .<= is LAM x y.(UU::tr) +!!! Witness and Claslib have to be adapted to axclasses !!! +------------------------------------------------------------ + +the trivial instance for ++ -- ** // is circ +the trivial instance for .= and .<= is bullet the class hierarchy is as follows @@ -42,7 +43,7 @@ classes cplus < pcpo -arities void :: cplus +arities lift :: (term)cplus ops curried "++" :: "'a::cplus -> 'a -> 'a" (cinfixl 65) @@ -56,7 +57,7 @@ classes cminus < pcpo -arities void :: cminus +arities lift :: (term)cminus ops curried "--" :: "'a::cminus -> 'a -> 'a" (cinfixl 65) @@ -69,7 +70,7 @@ classes ctimes < pcpo -arities void :: ctimes +arities lift :: (term)ctimes ops curried "**" :: "'a::ctimes -> 'a -> 'a" (cinfixl 70) @@ -82,7 +83,7 @@ classes cdiv < pcpo -arities void :: cdiv +arities lift :: (term)cdiv ops curried "//" :: "'a::cdiv -> 'a -> 'a" (cinfixl 70) @@ -95,7 +96,7 @@ classes per < pcpo -arities void :: per +arities lift :: (term)per ops curried ".=" :: "'a::per -> 'a -> tr" (cinfixl 55) @@ -106,7 +107,7 @@ strict_per "(UU .= x) = UU & (x .= UU) = UU" total_per "[|x ~= UU; y ~= UU|] ==> (x .= y) ~= UU" -flat_per "flat (UU::'a::per)" +flat_per "flat (x::'a::per)" sym_per "(x .= y) = (y .= x)" trans_per "[| (x .= y)=TT; (y .= z)=TT |] ==> (x .= z)=TT" @@ -118,7 +119,7 @@ classes equiv < per -arities void :: equiv +arities lift :: (term)equiv rules @@ -131,65 +132,11 @@ classes eq < equiv -arities void :: eq +arities lift :: (term)eq rules weq "[| (x::'a::eq) ~= UU; y ~= UU |] ==> (x = y --> (x .=y) = TT) & (x ~= y --> (x .= y)=FF)" -(* -------------------------------------------------------------------- *) - -(* -------------------------------------------------------------------- *) -(* class qpo with characteristic constant .<= *) -(* .<= is a partial order wrt an equivalence *) - -classes qpo < equiv - -arities void :: qpo - -ops curried - ".<=" :: "'a::qpo -> 'a -> tr" (cinfixl 55) -syntax (symbols) - "op .<=":: "'a::qpo => 'a => tr" (infixl "\\" 55) -rules - -strict_qpo "(UU .<= x) = UU & (x .<= UU) = UU" -total_qpo "[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU" - -refl_qpo "[|x ~= UU|] ==> (x .<= x)=TT" -antisym_qpo "[| (x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT" -trans_qpo "[| (x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT" - -antisym_qpo_rev "(x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" - -(* -------------------------------------------------------------------- *) - -(* -------------------------------------------------------------------- *) -(* irreflexive part .< defined via .<= *) - -ops curried - ".<" :: "'a::qpo -> 'a -> tr" (cinfixl 55) -syntax (symbols) - "op .<" :: "'a::qpo => 'a => tr" (infixl "\\" 55) - -defs - -qless_def "(op .<) Ú LAM x y.If x .= y then FF else x .<= y fi" - -(* -------------------------------------------------------------------- *) - -(* -------------------------------------------------------------------- *) -(* class qlinear is a refinement of of class qpo *) - -classes qlinear < qpo - -arities void :: qlinear - -rules - -qlinear "[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT Á (y .<= x)=TT " - -(* -------------------------------------------------------------------- *) - end diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Hoare.ML --- a/src/HOLCF/ex/Hoare.ML Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Hoare.ML Mon Feb 17 11:04:00 1997 +0100 @@ -95,7 +95,7 @@ (fn prems => [ (cut_facts_tac prems 1), - (etac (flat_tr RS flat_codom RS disjE) 1), + (etac (flat_flat RS flat_codom RS disjE) 1), (atac 1), (etac spec 1) ]); @@ -323,7 +323,7 @@ (fn prems => [ (cut_facts_tac prems 1), - (rtac (flat_tr RS flat_codom) 1), + (rtac (flat_flat RS flat_codom) 1), (res_inst_tac [("t","x1")] (iterate_0 RS subst) 1), (etac spec 1) ]); diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Loop.ML --- a/src/HOLCF/ex/Loop.ML Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Loop.ML Mon Feb 17 11:04:00 1997 +0100 @@ -57,7 +57,7 @@ (asm_simp_tac HOLCF_ss 1), (stac while_unfold 1), (res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1), - (etac (flat_tr RS flat_codom RS disjE) 1), + (etac (flat_flat RS flat_codom RS disjE) 1), (atac 1), (etac spec 1), (simp_tac HOLCF_ss 1), @@ -92,7 +92,7 @@ (rtac step_def2 1), (asm_simp_tac HOLCF_ss 1), (etac exE 1), - (etac (flat_tr RS flat_codom RS disjE) 1), + (etac (flat_flat RS flat_codom RS disjE) 1), (asm_simp_tac HOLCF_ss 1), (asm_simp_tac HOLCF_ss 1) ]); diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Loop.thy --- a/src/HOLCF/ex/Loop.thy Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Loop.thy Mon Feb 17 11:04:00 1997 +0100 @@ -6,10 +6,9 @@ Theory for a loop primitive like while *) -Loop = Tr2 + +Loop = Tr + consts - step :: "('a -> tr)->('a -> 'a)->'a->'a" while :: "('a -> tr)->('a -> 'a)->'a->'a" diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Witness.ML --- a/src/HOLCF/ex/Witness.ML Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Witness.ML Mon Feb 17 11:04:00 1997 +0100 @@ -4,7 +4,7 @@ (* classes cplus, cminus, ctimes, cdiv introduce characteristic constants o+ o- o* o/ - "bullet":: "void -> void -> void" + "circ":: "one -> one -> one" is the witness for o+ o- o* o/ @@ -18,9 +18,9 @@ The witness for these is - "cric" :: "void -> void -> tr" (cinfixl 55) + "bullet":: "one -> one -> tr" (cinfixl 55) - the classes equiv, eq, qlinear impose additional axioms + the classes equiv, eq, impose additional axioms *) (* -------------------------------------------------------------------- *) @@ -45,88 +45,85 @@ characteristic axioms of class eq: -weq "[|(x::'a::eq) ~= UU; y ~= UU|] ==> (x = y --> (x .= y)=TT) & (x ~= y --> Çx .= yÈ)" +weq "[|(x::'a::eq)~=UU; y~=UU|] ==> (x=y --> (x.=y)=TT) & (x~=y --> Çx.=yÈ)" -------------------------------------------------------------------- -characteristic axioms of class qpo: - -strict_qpo "(UU .<= x) = UU & (x .<= UU) = UU" -total_qpo "[|x ~= UU; y ~= UU|] ==> (x .<= y) ~= UU" - -refl_qpo "[|x ~= UU|] ==> (x .<= x)=TT" -antisym_qpo "[|(x .<= y)=TT; (y .<= x)=TT |] ==> (x .= y)=TT" -trans_qpo "[|(x .<= y)=TT; (y .<= z)=TT |] ==> (x .<= z)=TT" -antisym_qpo_rev " (x .= y)=TT ==> (x .<= y)=TT & (y .<= x)=TT" - - -------------------------------------------------------------------- - -characteristic axioms of class qlinear: - -qlinear "[|(x::'a::qlinear) ~= UU; y ~= UU|] ==> (x .<= y)=TT | (y .<= x)=TT " - *) (* strict_per, strict_qpo *) -val prems = goal thy "(UU circ x) = UU & (x circ UU) = UU"; -by (simp_tac (HOLCF_ss addsimps [circ_def]) 1); +goalw thy [bullet_def] "(UU bullet x) = UU & (x bullet UU) = UU"; +by (simp_tac (!simpset addsimps [flift1_def,flift2_def,o_def]) 1); +by (lift.induct_tac "x" 1); +auto(); result(); (* total_per, total_qpo *) -val prems = goal thy "[|x ~= UU; y ~= UU|] ==> (x circ y) ~= UU"; +val prems = goal thy "[|x~=UU; y~=UU|] ==> (x bullet y) ~= UU"; +by (subgoal_tac "x~=UU&y~=UU-->(x bullet y) ~= UU" 1); by (cut_facts_tac prems 1); -by (etac notE 1); -by (rtac unique_void2 1); +by (fast_tac HOL_cs 1); +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); +by (lift.induct_tac "x" 1); +by (fast_tac HOL_cs 1); +by (lift.induct_tac "y" 1); +auto(); result(); (* flat_per *) -val prems = goal thy "flat (UU::void)"; -by (rtac flat_void 1); +goal thy "flat (x::one)"; +by (rtac flat_flat 1); result(); (* sym_per *) -val prems = goal thy "(x circ y) = (y circ x)"; -by (simp_tac (HOLCF_ss addsimps [circ_def]) 1); +goalw thy [bullet_def] "(x bullet y) = (y bullet x)"; +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); +by (lift.induct_tac "x" 1); +by (lift.induct_tac "y" 2); +by (lift.induct_tac "y" 1); +auto(); result(); (* trans_per, trans_qpo *) -val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT |] ==> (x bullet z)=TT"; +val prems = goal thy "[|(x bullet y)=TT; (y bullet z)=TT|] ==>(x bullet z)=TT"; +by (subgoal_tac "(x bullet y)=TT&(y bullet z)=TT-->(x bullet z)=TT" 1); by (cut_facts_tac prems 1); -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1); +by (fast_tac HOL_cs 1); +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); +by (lift.induct_tac "x" 1); +by (lift.induct_tac "y" 2); +by (lift.induct_tac "y" 1); +by (lift.induct_tac "z" 4); +by (lift.induct_tac "z" 3); +by (lift.induct_tac "z" 2); +by (lift.induct_tac "z" 1); +auto(); result(); (* refl_per *) -val prems = goal thy "[|(x::void) ~= UU|] ==> (x bullet x)=TT"; +val prems = goal thy "x ~= UU ==> (x bullet x)=TT"; +by (subgoal_tac "x ~= UU --> (x bullet x)=TT" 1); by (cut_facts_tac prems 1); -by (etac notE 1); -by (rtac unique_void2 1); -result(); +by (fast_tac HOL_cs 1); +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); +by (lift.induct_tac "x" 1); +auto(); +qed "refl_per_one"; (* weq *) val prems = goal thy - "[|(x::void) ~= UU; y ~= UU|] ==> (x = y --> (x bullet y)=TT) & (x ~= y --> (x bullet y)=FF)"; + "[|x~=UU; y~=UU|]==>(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"; +by(subgoal_tac"x~=UU&y~=UU-->(x=y-->(x bullet y)=TT)&(x~=y-->(x bullet y)=FF)"1); by (cut_facts_tac prems 1); -by (etac notE 1); -by (rtac unique_void2 1); -result(); - -(* antisym_qpo *) -val prems = goal thy "[|(x bullet y)=TT; (y bullet x)=TT |] ==> (x bullet y)=TT"; -by (cut_facts_tac prems 1); -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1); +by (fast_tac HOL_cs 1); +by (lift.induct_tac "x" 1); +by (lift.induct_tac "y" 2); +by (lift.induct_tac "y" 1); +auto(); +br refl_per_one 1; +auto(); +by (simp_tac (!simpset addsimps [bullet_def,flift1_def,flift2_def,o_def]) 1); result(); -(* antisym_qpo_rev *) -val prems = goal thy "(x bullet y)=TT ==> (x bullet y)=TT & (y bullet x)=TT"; -by (cut_facts_tac prems 1); -by (asm_full_simp_tac (HOLCF_ss addsimps [bullet_def]) 1); - -(* qlinear *) -val prems = goal thy - "[|(x::void) ~= UU; y ~= UU|] ==> (x bullet y)=TT | (y bullet x)=TT "; -by (cut_facts_tac prems 1); -by (etac notE 1); -by (rtac unique_void2 1); -result(); diff -r 533a84b3bedd -r 3c3a84cc85a9 src/HOLCF/ex/Witness.thy --- a/src/HOLCF/ex/Witness.thy Mon Feb 17 11:01:10 1997 +0100 +++ b/src/HOLCF/ex/Witness.thy Mon Feb 17 11:04:00 1997 +0100 @@ -1,29 +1,24 @@ (* Title: FOCUS/Witness.thy - ID: $ $ + ID: $Id$ Author: Franz Regensburger Copyright 1995 Technical University Munich Witnesses for introduction of type cleasse in theory Classlib -The 8bit package is needed for this theory +The type one of HOLCF/One.thy is a witness for all the introduced classes. -The type void of HOLCF/Void.thy is a witness for all the introduced classes. - -the trivial instance for ++ -- ** // is LAM x y.(UU::void) -the trivial instance for .= and .<= is LAM x y.(UU::tr) +the trivial instance for ++ -- ** // is circ +the trivial instance for .= and .<= is bullet *) Witness = HOLCF + ops curried - "circ" :: "void -> void -> void" (cinfixl 65) - "bullet":: "void -> void -> tr" (cinfixl 55) + "bullet":: "one -> one -> tr" (cinfixl 55) defs -circ_def "(op circ) Ú (LAM x y.UU)" - -bullet_def "(op bullet) Ú (LAM x y.UU)" +bullet_def "(op bullet) Ú flift1(flift2 o (op =))" end