--- a/src/HOLCF/IOA/ABP/Lemmas.ML Mon Dec 13 18:41:49 2004 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Tue Dec 14 10:40:07 2004 +0100
@@ -5,19 +5,19 @@
(* Logic *)
-goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
+Goal "(~(A&B)) = ((~A)&B| ~B)";
by (Fast_tac 1);
-val and_de_morgan_and_absorbe = result();
+qed "and_de_morgan_and_absorbe";
-goal HOL.thy "(if C then A else B) --> (A|B)";
+Goal "(if C then A else B) --> (A|B)";
by (stac split_if 1);
by (Fast_tac 1);
-val bool_if_impl_or = result();
+qed "bool_if_impl_or";
(* Sets *)
val set_lemmas =
- map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
+ map (fn s => prove_goal Main.thy s (fn _ => [Fast_tac 1]))
["f(x) : (UN x. {f(x)})",
"f x y : (UN x y. {f x y})",
"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
@@ -25,14 +25,14 @@
(* 2 Lemmas to add to set_lemmas ... , used also for action handling,
namely for Intersections and the empty list (compatibility of IOA!) *)
-goal Set.thy "(UN b.{x. x=f(b)})= (UN b.{f(b)})";
+Goal "(UN b.{x. x=f(b)})= (UN b.{f(b)})";
by (rtac set_ext 1);
by (Fast_tac 1);
-val singleton_set =result();
+qed "singleton_set";
-goal HOL.thy "((A|B)=False) = ((~A)&(~B))";
+Goal "((A|B)=False) = ((~A)&(~B))";
by (Fast_tac 1);
-val de_morgan = result();
+qed "de_morgan";
(* Lists *)
@@ -40,7 +40,7 @@
by (induct_tac "l" 1);
by (Simp_tac 1);
by (Simp_tac 1);
-val hd_append =result();
+qed "hd_append";
Goal "l ~= [] --> (? x xs. l = (x#xs))";
by (induct_tac "l" 1);
--- a/src/HOLCF/IOA/NTP/Impl.ML Mon Dec 13 18:41:49 2004 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Tue Dec 14 10:40:07 2004 +0100
@@ -72,7 +72,7 @@
Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
by (simp_tac (simpset() delsimps [trans_of_par4]
- addsimps [fork_lemma,inv1_def]) 1);
+ addsimps [imp_conjR,inv1_def]) 1);
(* Split proof in two *)
by (rtac conjI 1);
@@ -242,7 +242,7 @@
by (asm_full_simp_tac ss 1);
by (simp_tac (simpset() addsimps [inv3_def]) 1);
by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (rtac (imp_or_lem RS iffD2) 1);
+ by (rtac (imp_disjL RS iffD1) 1);
by (rtac impI 1);
by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
@@ -263,7 +263,7 @@
(* 1 *)
by (tac3 1);
by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (rtac (imp_or_lem RS iffD2) 1);
+ by (rtac (imp_disjL RS iffD1) 1);
by (rtac impI 1);
by (forward_tac [rewrite_rule [Impl.inv2_def] (inv2 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Mon Dec 13 18:41:49 2004 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Tue Dec 14 10:40:07 2004 +0100
@@ -5,22 +5,14 @@
(* Logic *)
-goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
- by (Fast_tac 1);
-qed "fork_lemma";
-
-goal HOL.thy "((A --> B) & (C --> B)) = ((A | C) --> B)";
- by (Fast_tac 1);
-qed "imp_or_lem";
-
-goal HOL.thy "(X = (~ Y)) = ((~X) = Y)";
+Goal "(X = (~ Y)) = ((~X) = Y)";
by (Fast_tac 1);
qed "neg_flip";
(* Sets *)
val set_lemmas =
- map (fn s => prove_goal Set.thy s (fn _ => [Fast_tac 1]))
+ map (fn s => prove_goal Main.thy s (fn _ => [Fast_tac 1]))
["f(x) : (UN x. {f(x)})",
"f x y : (UN x y. {f x y})",
"!!a. (!x. a ~= f(x)) ==> a ~: (UN x. {f(x)})",
@@ -29,7 +21,7 @@
(* Arithmetic *)
-goal NatArith.thy "!!x. 0<x ==> (x - 1 = y) = (x = Suc(y))";
+Goal "0<x ==> (x - 1 = y) = (x = Suc(y))";
by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
qed "pred_suc";
--- a/src/HOLCF/IOA/meta_theory/IOA.ML Mon Dec 13 18:41:49 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-(* Title: HOLCF/IOA/meta_theory/IOA.thy
- ID: $Id$
- Author: Olaf Müller
-
-The theory of I/O automata in HOLCF.
-*)
-
-
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by (fast_tac (claset() addDs prems) 1);
-qed "imp_conj_lemma";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Dec 13 18:41:49 2004 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Tue Dec 14 10:40:07 2004 +0100
@@ -59,9 +59,9 @@
qed"weak_ref_map2ref_map";
-val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
+val prems = Goal "(P ==> Q-->R) ==> P&Q --> R";
by (fast_tac (claset() addDs prems) 1);
-val lemma = result();
+qed "imp_conj_lemma";
Delsplits [split_if]; Delcongs [if_weak_cong];
@@ -73,7 +73,7 @@
by (asm_full_simp_tac (simpset() addsimps [rename_def,rename_set_def,starts_of_def]) 1);
(* 2: reachable transitions *)
by (REPEAT (rtac allI 1));
-by (rtac lemma 1);
+by (rtac imp_conj_lemma 1);
by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
asig_outputs_def,asig_of_def,trans_of_def]) 1);
--- a/src/HOLCF/IsaMakefile Mon Dec 13 18:41:49 2004 +0100
+++ b/src/HOLCF/IsaMakefile Tue Dec 14 10:40:07 2004 +0100
@@ -88,7 +88,7 @@
IOA/meta_theory/Automata.thy IOA/meta_theory/Traces.ML \
IOA/meta_theory/Seq.ML IOA/meta_theory/RefMappings.ML \
IOA/meta_theory/ShortExecutions.thy IOA/meta_theory/ShortExecutions.ML \
- IOA/meta_theory/IOA.thy IOA/meta_theory/IOA.ML \
+ IOA/meta_theory/IOA.thy \
IOA/meta_theory/Sequence.thy IOA/meta_theory/Automata.ML \
IOA/meta_theory/CompoExecs.thy IOA/meta_theory/RefMappings.thy \
IOA/meta_theory/RefCorrectness.ML IOA/meta_theory/Compositionality.ML \