# HG changeset patch
# User wenzelm
# Date 1148757531 -7200
# Node ID 6b38551d0798ce279cbc405bb2f6d45ce5d19747
# Parent  c58ef2aa5430072ecb01d298f37e2a65174c2bf8
removed legacy ML scripts;

diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/Storage/Action.thy
--- a/src/HOLCF/IOA/Storage/Action.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/Storage/Action.thy	Sat May 27 21:18:51 2006 +0200
@@ -14,6 +14,4 @@
 lemma [cong]: "!!x. x = y ==> action_case a b c x = action_case a b c y"
   by simp
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/Storage/Correctness.ML
--- a/src/HOLCF/IOA/Storage/Correctness.ML	Sat May 27 21:00:31 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,68 +0,0 @@
-(*  Title:      HOL/IOA/example/Correctness.ML
-    ID:         $Id$
-    Author:     Olaf Mueller
-*)
-
-
-Addsimps [split_paired_All];
-Delsimps [split_paired_Ex];
-
-
-(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
-         simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans
-   Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
-         as this can be done globally *)
-
-Goal
-      "is_simulation sim_relation impl_ioa spec_ioa";
-by (simp_tac (simpset() addsimps [is_simulation_def]) 1);
-by (rtac conjI 1);
-(* --------------  start states ----------------- *)
-by (SELECT_GOAL (safe_tac set_cs) 1);
-by (res_inst_tac [("x","({},False)")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [sim_relation_def,starts_of_def,
-        thm "Spec.ioa_def", thm "Impl.ioa_def"]) 1);
-(* ---------------- main-part ------------------- *)
-
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (rename_tac "k b used c k' b' a" 1);
-by (induct_tac "a" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
-      thm"Impl.ioa_def",thm "Impl.trans_def",trans_of_def])));
-by (safe_tac set_cs);
-(* NEW *)
-by (res_inst_tac [("x","(used,True)")] exI 1);
-by (Asm_full_simp_tac 1);
-by (rtac transition_is_ex 1);
-by (simp_tac (simpset() addsimps [
-      thm "Spec.ioa_def", thm "Spec.trans_def",trans_of_def])1);
-(* LOC *)
-by (res_inst_tac [("x","(used Un {k},False)")] exI 1);
-by (asm_full_simp_tac (simpset() addsimps [less_SucI]) 1);
-by (rtac transition_is_ex 1);
-by (simp_tac (simpset() addsimps [
-      thm "Spec.ioa_def", thm "Spec.trans_def",trans_of_def])1);
-by (Fast_tac 1);
-(* FREE *)
-by (res_inst_tac [("x","(used - {nat},c)")] exI 1);
-by (Asm_full_simp_tac 1);
-by (rtac transition_is_ex 1);
-by (simp_tac (simpset() addsimps [
-      thm "Spec.ioa_def",thm "Spec.trans_def",trans_of_def])1);
-qed"issimulation";
-
-
-
-Goalw [ioa_implements_def]
-"impl_ioa =<| spec_ioa";
-by (rtac conjI 1);
-by (simp_tac (simpset() addsimps [thm "Impl.sig_def",thm "Spec.sig_def",
-    thm "Impl.ioa_def",thm "Spec.ioa_def", asig_outputs_def,asig_of_def,
-    asig_inputs_def]) 1);
-by (rtac trace_inclusion_for_simulations 1);
-by (simp_tac (simpset() addsimps [thm "Impl.sig_def",thm "Spec.sig_def",
-    thm "Impl.ioa_def",thm "Spec.ioa_def", externals_def,asig_outputs_def,asig_of_def,
-    asig_inputs_def]) 1);
-by (rtac issimulation 1);
-qed"implementation";
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOLCF/IOA/Storage/Correctness.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.thy	Sat May 27 21:18:51 2006 +0200
@@ -19,6 +19,59 @@
                          in
                          (! l:used. l < k) & b=c }"
 
-ML {* use_legacy_bindings (the_context ()) *}
+declare split_paired_All [simp]
+declare split_paired_Ex [simp del]
+
+
+(* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive
+         simple lemmas asig_of impl_ioa = impl_sig, trans_of impl_ioa = impl_trans
+   Idea: ?ex. move .. should be generally replaced by a step via a subst tac if desired,
+         as this can be done globally *)
+
+lemma issimulation:
+      "is_simulation sim_relation impl_ioa spec_ioa"
+apply (simp (no_asm) add: is_simulation_def)
+apply (rule conjI)
+txt {* start states *}
+apply (tactic "SELECT_GOAL (safe_tac set_cs) 1")
+apply (rule_tac x = " ({},False) " in exI)
+apply (simp add: sim_relation_def starts_of_def Spec.ioa_def Impl.ioa_def)
+txt {* main-part *}
+apply (rule allI)+
+apply (rule imp_conj_lemma)
+apply (rename_tac k b used c k' b' a)
+apply (induct_tac "a")
+apply (simp_all (no_asm) add: sim_relation_def Impl.ioa_def Impl.trans_def trans_of_def)
+apply (tactic "safe_tac set_cs")
+txt {* NEW *}
+apply (rule_tac x = "(used,True)" in exI)
+apply simp
+apply (rule transition_is_ex)
+apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
+txt {* LOC *}
+apply (rule_tac x = " (used Un {k},False) " in exI)
+apply (simp add: less_SucI)
+apply (rule transition_is_ex)
+apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
+apply fast
+txt {* FREE *}
+apply (rule_tac x = " (used - {nat},c) " in exI)
+apply simp
+apply (rule transition_is_ex)
+apply (simp (no_asm) add: Spec.ioa_def Spec.trans_def trans_of_def)
+done
+
+
+lemma implementation:
+"impl_ioa =<| spec_ioa"
+apply (unfold ioa_implements_def)
+apply (rule conjI)
+apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def
+  asig_outputs_def asig_of_def asig_inputs_def)
+apply (rule trace_inclusion_for_simulations)
+apply (simp (no_asm) add: Impl.sig_def Spec.sig_def Impl.ioa_def Spec.ioa_def
+  externals_def asig_outputs_def asig_of_def asig_inputs_def)
+apply (rule issimulation)
+done
 
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOLCF/IOA/Storage/Impl.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/Storage/Impl.thy	Sat May 27 21:18:51 2006 +0200
@@ -39,6 +39,4 @@
     Free l : actions(impl_sig) "
   by (simp add: Impl.sig_def actions_def asig_projections)
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOLCF/IOA/Storage/Spec.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/Storage/Spec.thy	Sat May 27 21:18:51 2006 +0200
@@ -33,6 +33,4 @@
 
 ioa_def: "spec_ioa == (spec_sig, {({},False)}, spec_trans,{},{})"
 
-ML {* use_legacy_bindings (the_context ()) *}
-
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/ex/ROOT.ML
--- a/src/HOLCF/IOA/ex/ROOT.ML	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/ex/ROOT.ML	Sat May 27 21:18:51 2006 +0200
@@ -1,12 +1,7 @@
 (*  Title:      HOL/IOA/ex/ROOT.ML
     ID:         $Id$
     Author:     Olaf Mueller
-
-This is the ROOT file for the formalization of a semantic model of
-I/O-Automata.  See the README.html file for details.
 *)
 
-goals_limit := 1;
-
 time_use_thy "TrivEx";
 time_use_thy "TrivEx2";
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/ex/TrivEx.ML
--- a/src/HOLCF/IOA/ex/TrivEx.ML	Sat May 27 21:00:31 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(*  Title:      HOLCF/IOA/TrivEx.thy
-    ID:         $Id$
-    Author:     Olaf Mueller
-
-Trivial Abstraction Example.
-*)
-
-Goalw [is_abstraction_def] 
-"is_abstraction h_abs C_ioa A_ioa";
-by (rtac conjI 1);
-(* ------------- start states ------------ *)
-by (simp_tac (simpset() addsimps 
-    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
-(* -------------- step case ---------------- *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (simp_tac (simpset() addsimps [trans_of_def,
-        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
-by (induct_tac "a" 1);
-by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-qed"h_abs_is_abstraction";
-
-
-Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
-by (rtac AbsRuleT1 1);
-by (rtac h_abs_is_abstraction 1);
-by (rtac MC_result 1);
-by (abstraction_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
-qed"TrivEx_abstraction";
-
-
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOLCF/IOA/ex/TrivEx.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx.thy	Sat May 27 21:18:51 2006 +0200
@@ -59,6 +59,26 @@
 MC_result:
   "validIOA A_ioa (<>[] <%(b,a,c). b>)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemma h_abs_is_abstraction:
+  "is_abstraction h_abs C_ioa A_ioa"
+apply (unfold is_abstraction_def)
+apply (rule conjI)
+txt {* start states *}
+apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
+txt {* step case *}
+apply (rule allI)+
+apply (rule imp_conj_lemma)
+apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
+apply (induct_tac "a")
+apply (simp add: h_abs_def)
+done
+
+lemma TrivEx_abstraction: "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"
+apply (rule AbsRuleT1)
+apply (rule h_abs_is_abstraction)
+apply (rule MC_result)
+apply (tactic "abstraction_tac 1")
+apply (simp add: h_abs_def)
+done
 
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/ex/TrivEx2.ML
--- a/src/HOLCF/IOA/ex/TrivEx2.ML	Sat May 27 21:00:31 2006 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      HOLCF/IOA/TrivEx.thy
-    ID:         $Id$
-    Author:     Olaf Mueller
-
-Trivial Abstraction Example.
-*)
-
-Goalw [is_abstraction_def] 
-"is_abstraction h_abs C_ioa A_ioa";
-by (rtac conjI 1);
-(* ------------- start states ------------ *)
-by (simp_tac (simpset() addsimps 
-    [h_abs_def,starts_of_def,C_ioa_def,A_ioa_def]) 1);
-(* -------------- step case ---------------- *)
-by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (simp_tac (simpset() addsimps [trans_of_def,
-        C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
-by (induct_tac "a" 1);
-by (simp_tac (simpset() addsimps [h_abs_def]) 1);
-qed"h_abs_is_abstraction";
-
-
-(*
-Goalw [xt2_def,plift,option_lift]
-  "(xt2 (plift afun)) (s,a,t) = (afun a)";
-(* !!!!!!!!!!!!! Occurs check !!!! *)
-by (induct_tac "a" 1);
-
-*)
-
-Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
-           C_trans_def,trans_of_def] 
-"!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
-by Auto_tac;
-qed"Enabled_implication";
-
-
-Goalw [is_live_abstraction_def]
-"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
-by Auto_tac;
-(* is_abstraction *)
-by (rtac h_abs_is_abstraction 1);
-(* temp_weakening *)
-by (abstraction_tac 1);
-by (etac Enabled_implication 1);
-qed"h_abs_is_liveabstraction";
-
-
-Goalw [C_live_ioa_def]
-"validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
-by (rtac AbsRuleT2 1);
-by (rtac h_abs_is_liveabstraction 1);
-by (rtac MC_result 1);
-by (abstraction_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
-qed"TrivEx2_abstraction";
-
-
-(*
-Goal "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) 
-IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))";
-
-*)
-
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOLCF/IOA/ex/TrivEx2.thy	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy	Sat May 27 21:18:51 2006 +0200
@@ -68,6 +68,50 @@
 MC_result:
   "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+lemma h_abs_is_abstraction:
+"is_abstraction h_abs C_ioa A_ioa"
+apply (unfold is_abstraction_def)
+apply (rule conjI)
+txt {* start states *}
+apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
+txt {* step case *}
+apply (rule allI)+
+apply (rule imp_conj_lemma)
+apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
+apply (induct_tac "a")
+apply (simp (no_asm) add: h_abs_def)
+done
+
+
+lemma Enabled_implication:
+    "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s"
+  apply (unfold Enabled_def enabled_def h_abs_def A_ioa_def C_ioa_def A_trans_def
+    C_trans_def trans_of_def)
+  apply auto
+  done
+
+
+lemma h_abs_is_liveabstraction:
+"is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
+apply (unfold is_live_abstraction_def)
+apply auto
+txt {* is_abstraction *}
+apply (rule h_abs_is_abstraction)
+txt {* temp_weakening *}
+apply (tactic "abstraction_tac 1")
+apply (erule Enabled_implication)
+done
+
+
+lemma TrivEx2_abstraction:
+  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
+apply (unfold C_live_ioa_def)
+apply (rule AbsRuleT2)
+apply (rule h_abs_is_liveabstraction)
+apply (rule MC_result)
+apply (tactic "abstraction_tac 1")
+apply (simp add: h_abs_def)
+done
 
 end
diff -r c58ef2aa5430 -r 6b38551d0798 src/HOLCF/IsaMakefile
--- a/src/HOLCF/IsaMakefile	Sat May 27 21:00:31 2006 +0200
+++ b/src/HOLCF/IsaMakefile	Sat May 27 21:18:51 2006 +0200
@@ -139,7 +139,7 @@
 
 IOA-Storage: IOA $(LOG)/IOA-Storage.gz
 
-$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy IOA/Storage/Correctness.ML \
+$(LOG)/IOA-Storage.gz: $(OUT)/IOA IOA/Storage/Action.thy \
   IOA/Storage/Correctness.thy IOA/Storage/Impl.thy \
   IOA/Storage/ROOT.ML IOA/Storage/Spec.thy
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA Storage
@@ -149,9 +149,7 @@
 
 IOA-ex: IOA $(LOG)/IOA-ex.gz
 
-$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML \
-  IOA/ex/TrivEx.thy IOA/ex/TrivEx.ML \
-  IOA/ex/TrivEx2.thy IOA/ex/TrivEx2.ML 
+$(LOG)/IOA-ex.gz: $(OUT)/IOA IOA/ex/ROOT.ML IOA/ex/TrivEx.thy IOA/ex/TrivEx2.thy
 	@cd IOA; $(ISATOOL) usedir $(OUT)/IOA ex