comp -> rel_comp
authornipkow
Thu Dec 13 16:47:35 2001 +0100 (2001-12-13)
changeset 12487bbd564190c9b
parent 12486 0ed8bdd883e0
child 12488 83acab8042ad
comp -> rel_comp
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Relation.ML
src/HOL/Relation.thy
src/HOL/Relation_Power.ML
src/HOL/Transitive_Closure_lemmas.ML
     1.1 --- a/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 15:45:03 2001 +0100
     1.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Thu Dec 13 16:47:35 2001 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4   "([False],[False]) : steps (atom a) w = (w = [])";
     1.5  by (induct_tac "w" 1);
     1.6   by (Simp_tac 1);
     1.7 -by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
     1.8 +by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
     1.9  qed "False_False_in_steps_atom";
    1.10  
    1.11  Goal
    1.12 @@ -34,7 +34,7 @@
    1.13  by (induct_tac "w" 1);
    1.14   by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
    1.15  by (asm_full_simp_tac (simpset()
    1.16 -     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    1.17 +     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
    1.18  qed "start_fin_in_steps_atom";
    1.19  
    1.20  Goal
     2.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Thu Dec 13 15:45:03 2001 +0100
     2.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Thu Dec 13 16:47:35 2001 +0100
     2.3 @@ -33,14 +33,14 @@
     2.4  Goal "([False],[False]) : steps (atom a) w = (w = [])";
     2.5  by (induct_tac "w" 1);
     2.6   by (Simp_tac 1);
     2.7 -by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
     2.8 +by (asm_simp_tac (simpset() addsimps [rel_comp_def]) 1);
     2.9  qed "False_False_in_steps_atom";
    2.10  
    2.11  Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    2.12  by (induct_tac "w" 1);
    2.13   by (asm_simp_tac (simpset() addsimps [start_atom,thm"rtrancl_empty"]) 1);
    2.14  by (asm_full_simp_tac (simpset()
    2.15 -     addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    2.16 +     addsimps [False_False_in_steps_atom,rel_comp_def,start_atom]) 1);
    2.17  qed "start_fin_in_steps_atom";
    2.18  
    2.19  Goal "accepts (atom a) w = (w = [a])";
     3.1 --- a/src/HOL/Relation.ML	Thu Dec 13 15:45:03 2001 +0100
     3.2 +++ b/src/HOL/Relation.ML	Thu Dec 13 16:47:35 2001 +0100
     3.3 @@ -71,31 +71,31 @@
     3.4  
     3.5  (** Composition of two relations **)
     3.6  
     3.7 -Goalw [comp_def]
     3.8 +Goalw [rel_comp_def]
     3.9      "[| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    3.10  by (Blast_tac 1);
    3.11 -qed "compI";
    3.12 +qed "rel_compI";
    3.13  
    3.14  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    3.15 -val prems = Goalw [comp_def]
    3.16 +val prems = Goalw [rel_comp_def]
    3.17      "[| xz : r O s;  \
    3.18  \       !!x y z. [| xz = (x,z);  (x,y):s;  (y,z):r |] ==> P \
    3.19  \    |] ==> P";
    3.20  by (cut_facts_tac prems 1);
    3.21  by (REPEAT (eresolve_tac [CollectE, splitE, exE, conjE] 1 
    3.22       ORELSE ares_tac prems 1));
    3.23 -qed "compE";
    3.24 +qed "rel_compE";
    3.25  
    3.26  val prems = Goal
    3.27      "[| (a,c) : r O s;  \
    3.28  \       !!y. [| (a,y):s;  (y,c):r |] ==> P \
    3.29  \    |] ==> P";
    3.30 -by (rtac compE 1);
    3.31 +by (rtac rel_compE 1);
    3.32  by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [Pair_inject,ssubst] 1));
    3.33 -qed "compEpair";
    3.34 +qed "rel_compEpair";
    3.35  
    3.36 -AddIs [compI, IdI];
    3.37 -AddSEs [compE, IdE];
    3.38 +AddIs [rel_compI, IdI];
    3.39 +AddSEs [rel_compE, IdE];
    3.40  
    3.41  Goal "R O Id = R";
    3.42  by (Fast_tac 1);
    3.43 @@ -117,11 +117,11 @@
    3.44  
    3.45  Goal "[| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    3.46  by (Blast_tac 1);
    3.47 -qed "comp_mono";
    3.48 +qed "rel_comp_mono";
    3.49  
    3.50  Goal "[| s <= A <*> B;  r <= B <*> C |] ==> (r O s) <= A <*> C";
    3.51  by (Blast_tac 1);
    3.52 -qed "comp_subset_Sigma";
    3.53 +qed "rel_comp_subset_Sigma";
    3.54  
    3.55  (** Natural deduction for refl(r) **)
    3.56  
    3.57 @@ -191,7 +191,7 @@
    3.58  
    3.59  Goal "(r O s)^-1 = s^-1 O r^-1";
    3.60  by (Blast_tac 1);
    3.61 -qed "converse_comp";
    3.62 +qed "converse_rel_comp";
    3.63  
    3.64  Goal "Id^-1 = Id";
    3.65  by (Blast_tac 1);
     4.1 --- a/src/HOL/Relation.thy	Thu Dec 13 15:45:03 2001 +0100
     4.2 +++ b/src/HOL/Relation.thy	Thu Dec 13 16:47:35 2001 +0100
     4.3 @@ -13,7 +13,7 @@
     4.4    converse :: "('a * 'b) set => ('b * 'a) set"    ("(_\\<inverse>)" [1000] 999)
     4.5  
     4.6  constdefs
     4.7 -  comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     4.8 +  rel_comp  :: "[('b * 'c) set, ('a * 'b) set] => ('a * 'c) set"  (infixr "O" 60)
     4.9      "r O s == {(x,z). ? y. (x,y):s & (y,z):r}"
    4.10  
    4.11    Image :: "[('a * 'b) set, 'a set] => 'b set"                (infixl "``" 90)
     5.1 --- a/src/HOL/Relation_Power.ML	Thu Dec 13 15:45:03 2001 +0100
     5.2 +++ b/src/HOL/Relation_Power.ML	Thu Dec 13 16:47:35 2001 +0100
     5.3 @@ -44,7 +44,7 @@
     5.4  by (case_tac "n" 1);
     5.5  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
     5.6  by (Asm_full_simp_tac 1);
     5.7 -by (etac compEpair 1);
     5.8 +by (etac rel_compEpair 1);
     5.9  by (REPEAT(ares_tac [p3] 1));
    5.10  qed "rel_pow_E";
    5.11  
    5.12 @@ -71,7 +71,7 @@
    5.13  by (case_tac "n" 1);
    5.14  by (asm_full_simp_tac (simpset() addsimps [p2]) 1);
    5.15  by (Asm_full_simp_tac 1);
    5.16 -by (etac compEpair 1);
    5.17 +by (etac rel_compEpair 1);
    5.18  by (dtac (conjI RS rel_pow_Suc_D2') 1);
    5.19  by (assume_tac 1);
    5.20  by (etac exE 1);
     6.1 --- a/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 15:45:03 2001 +0100
     6.2 +++ b/src/HOL/Transitive_Closure_lemmas.ML	Thu Dec 13 16:47:35 2001 +0100
     6.3 @@ -184,7 +184,7 @@
     6.4  Goalw [trancl_def]
     6.5      "!!p. p : r^+ ==> p : r^*";
     6.6  by (split_all_tac 1);
     6.7 -by (etac compEpair 1);
     6.8 +by (etac rel_compEpair 1);
     6.9  by (REPEAT (ares_tac [rtrancl_into_rtrancl] 1));
    6.10  qed "trancl_into_rtrancl";
    6.11  
    6.12 @@ -192,7 +192,7 @@
    6.13  Goalw [trancl_def]
    6.14     "!!p. p : r ==> p : r^+";
    6.15  by (split_all_tac 1);
    6.16 -by (REPEAT (ares_tac [prem,compI,rtrancl_refl] 1));
    6.17 +by (REPEAT (ares_tac [prem,rel_compI,rtrancl_refl] 1));
    6.18  qed "r_into_trancl";
    6.19  AddIs [r_into_trancl];
    6.20  
    6.21 @@ -215,7 +215,7 @@
    6.22  \     !!y.  [| (a,y) : r |] ==> P(y);                   \
    6.23  \     !!y z.[| (a,y) : r^+;  (y,z) : r;  P(y) |] ==> P(z)       \
    6.24  \  |] ==> P(b)";
    6.25 -by (rtac (rewrite_rule [trancl_def] major  RS  compEpair) 1);
    6.26 +by (rtac (rewrite_rule [trancl_def] major  RS  rel_compEpair) 1);
    6.27  (*by induction on this formula*)
    6.28  by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
    6.29  (*now solve first subgoal: this formula is sufficient*)
    6.30 @@ -241,7 +241,7 @@
    6.31  \    |] ==> P";
    6.32  by (subgoal_tac "(a::'a,b) : r | (? y. (a,y) : r^+  &  (y,b) : r)" 1);
    6.33  by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
    6.34 -by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
    6.35 +by (rtac (rewrite_rule [trancl_def] major RS rel_compEpair) 1);
    6.36  by (etac rtranclE 1);
    6.37  by (Blast_tac 1);
    6.38  by (blast_tac (claset() addSIs [rtrancl_into_trancl1]) 1);
    6.39 @@ -251,8 +251,8 @@
    6.40    Proved by unfolding since it uses transitivity of rtrancl. *)
    6.41  Goalw [trancl_def] "trans(r^+)";
    6.42  by (rtac transI 1);
    6.43 -by (REPEAT (etac compEpair 1));
    6.44 -by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS compI)) 1);
    6.45 +by (REPEAT (etac rel_compEpair 1));
    6.46 +by (rtac (rtrancl_into_rtrancl RS (rtrancl_trans RS rel_compI)) 1);
    6.47  by (REPEAT (assume_tac 1));
    6.48  qed "trans_trancl";
    6.49  
    6.50 @@ -281,7 +281,7 @@
    6.51  qed "trancl_insert";
    6.52  
    6.53  Goalw [trancl_def] "(r^-1)^+ = (r^+)^-1";
    6.54 -by (simp_tac (simpset() addsimps [rtrancl_converse,converse_comp]) 1);
    6.55 +by (simp_tac (simpset() addsimps [rtrancl_converse,converse_rel_comp]) 1);
    6.56  by (simp_tac (simpset() addsimps [rtrancl_converse RS sym,
    6.57  				  r_comp_rtrancl_eq]) 1);
    6.58  qed "trancl_converse";