# HG changeset patch
# User paulson
# Date 1103017207 -3600
# Node ID 6001135caa918b4e374138de1ee046c6afbf468d
# Parent  9e85d2b04867d40f41630047288ed9cf6a426469
tidied; removed references to HOL theories

diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IOA/ABP/Lemmas.ML
--- 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);
diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IOA/NTP/Impl.ML
--- 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);
diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IOA/NTP/Lemmas.ML
--- 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";
 
diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IOA/meta_theory/IOA.ML
--- 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";
diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- 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);
diff -r 9e85d2b04867 -r 6001135caa91 src/HOLCF/IsaMakefile
--- 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 \