--- a/src/HOL/Modelcheck/CTL.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/CTL.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,18 +4,19 @@
Copyright 1997 TU Muenchen
*)
-CTL = MuCalculus +
-
+theory CTL
+imports MuCalculus
+begin
types
'a trans = "('a * 'a) set"
-consts
- CEX ::"['a trans,'a pred, 'a]=>bool"
- EG ::"['a trans,'a pred]=> 'a pred"
+constdefs
+ CEX ::"['a trans,'a pred, 'a]=>bool"
+ "CEX N f u == (? v. (f v & (u,v):N))"
+ EG ::"['a trans,'a pred]=> 'a pred"
+ "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
-defs
- CEX_def "CEX N f u == (? v. (f v & (u,v):N))"
- EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/Modelcheck/EindhovenExample.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/Modelcheck/EindhovenExample.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-val reach_rws = [reach_def,INIT_def,N_def];
-
-
-Goal "reach (True,True,True)";
-by (simp_tac (Eindhoven_ss addsimps reach_rws) 1);
-
-(*show the current proof state using the model checker syntax*)
-setmp print_mode ["Eindhoven"] pr ();
-
-(* actually invoke the model checker *)
-(* try out after installing the model checker: see the README file *)
-
-(* by (mc_eindhoven_tac 1); *)
-
-(*qed "reach_ex_thm";*)
-
-
-
-(* just to make a proof in this file :-) *)
-Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
-by (Simp_tac 1);
-qed"init_state";
--- a/src/HOL/Modelcheck/EindhovenExample.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenExample.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,28 +4,39 @@
Copyright 1997 TU Muenchen
*)
-EindhovenExample = CTL + EindhovenSyn +
-
+theory EindhovenExample
+imports EindhovenSyn CTL
+begin
types
- state = "bool * bool * bool"
+ state = "bool * bool * bool"
-consts
+constdefs
+ INIT :: "state pred"
+ "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
- INIT :: "state pred"
- N :: "[state,state] => bool"
+ N :: "[state,state] => bool"
+ "N == % (x1,x2,x3) (y1,y2,y3).
+ (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) |
+ ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) |
+ ( x1 & ~x2 & ~x3 & y1 & y2 & y3)"
+
reach:: "state pred"
+ "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
-defs
-
- INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
+ by (simp add: INIT_def)
+
+
+lemmas reach_rws = reach_def INIT_def N_def
- N_def "N == % (x1,x2,x3) (y1,y2,y3).
- (~x1 & ~x2 & ~x3 & y1 & ~y2 & ~y3) |
- ( x1 & ~x2 & ~x3 & ~y1 & ~y2 & ~y3) |
- ( x1 & ~x2 & ~x3 & y1 & y2 & y3) "
-
- reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
-
+lemma reach_ex: "reach (True, True, True)"
+ apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
+ txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
+ pr (Eindhoven)
+ txt {* actually invoke the model checker, try out after installing
+ the model checker: see the README file *}
+ apply (tactic {* mc_eindhoven_tac 1 *})
+ done
end
--- a/src/HOL/Modelcheck/EindhovenSyn.ML Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML Tue Sep 06 16:24:53 2005 +0200
@@ -4,19 +4,11 @@
Copyright 1997 TU Muenchen
*)
-fun mc_eindhoven_tac i state =
-let val sign = #sign (rep_thm state)
-in
-case Library.drop(i-1,prems_of state) of
- [] => Seq.empty |
- subgoal::_ =>
- let val concl = Logic.strip_imp_concl subgoal;
- val OraAss = invoke_oracle EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn concl);
- in
- ((cut_facts_tac [OraAss] i) THEN (atac i)) state
- end
-end;
-
+fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
+ let
+ val thy = Thm.theory_of_thm state;
+ val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
+ in cut_facts_tac [assertion] i THEN atac i end) i state;
Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
by (rtac ext 1);
@@ -25,7 +17,7 @@
qed "pair_eta_expand";
val pair_eta_expand_proc =
- Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
+ Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
(fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
val Eindhoven_ss =
--- a/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,74 +4,59 @@
Copyright 1997 TU Muenchen
*)
-EindhovenSyn = MuCalculus +
-
+theory EindhovenSyn
+imports MuCalculus
+begin
syntax (Eindhoven output)
+ True :: bool ("TRUE")
+ False :: bool ("FALSE")
- True :: bool ("TRUE")
- False :: bool ("FALSE")
+ Not :: "bool => bool" ("NOT _" [40] 40)
+ "op &" :: "[bool, bool] => bool" (infixr "AND" 35)
+ "op |" :: "[bool, bool] => bool" (infixr "OR" 30)
- Not :: bool => bool ("NOT _" [40] 40)
- "op &" :: [bool, bool] => bool (infixr "AND" 35)
- "op |" :: [bool, bool] => bool (infixr "OR" 30)
+ "ALL " :: "[idts, bool] => bool" ("'((3A _./ _)')" [0, 10] 10)
+ "EX " :: "[idts, bool] => bool" ("'((3E _./ _)')" [0, 10] 10)
+ "_lambda" :: "[pttrns, 'a] => 'b" ("(3L _./ _)" 10)
+
+ "_idts" :: "[idt, idts] => idts" ("_,/_" [1, 0] 0)
+ "_pattern" :: "[pttrn, patterns] => pttrn" ("_,/_" [1, 0] 0)
+
+ "Mu " :: "[idts, 'a pred] => 'a pred" ("(3[mu _./ _])" 1000)
+ "Nu " :: "[idts, 'a pred] => 'a pred" ("(3[nu _./ _])" 1000)
+
+ML {*
+ val trace_eindhoven = ref false;
+*}
- "! " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
- "? " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
- "ALL " :: [idts, bool] => bool ("'((3A _./ _)')" [0, 10] 10)
- "EX " :: [idts, bool] => bool ("'((3E _./ _)')" [0, 10] 10)
- "_lambda" :: [pttrns, 'a] => 'b ("(3L _./ _)" 10)
+oracle mc_eindhoven_oracle ("term") =
+{*
+let
+ val eindhoven_term =
+ setmp print_mode ["Eindhoven"] o Sign.string_of_term;
- "_idts" :: [idt, idts] => idts ("_,/_" [1, 0] 0)
- "_pattern" :: [pttrn, patterns] => pttrn ("_,/_" [1, 0] 0)
-
- "Mu " :: [idts, 'a pred] => 'a pred ("(3[mu _./ _])" 1000)
- "Nu " :: [idts, 'a pred] => 'a pred ("(3[nu _./ _])" 1000)
-
-oracle
- eindhoven_mc = mk_eindhoven_mc_oracle
+ fun call_mc s =
+ let
+ val eindhoven_home = getenv "EINDHOVEN_HOME";
+ val pmu =
+ if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
+ else eindhoven_home ^ "/pmu";
+ in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
+in
+ fn thy => fn goal =>
+ let
+ val s = eindhoven_term thy goal;
+ val debug = tracing ("MC debugger: " ^ s);
+ val result = call_mc s;
+ in
+ if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
+ (case result of
+ "TRUE\n" => goal |
+ "FALSE\n" => error "MC oracle yields FALSE" |
+ _ => error ("MC syntax error: " ^ result))
+ end
+end
+*}
end
-
-
-
-ML
-
-
-exception EindhovenOracleExn of term;
-
-
-val trace_mc = ref false;
-
-local
-
-fun termtext sign term =
- setmp print_mode ["Eindhoven"]
- (Sign.string_of_term sign) term;
-
-fun call_mc s =
- let
- val eindhoven_home = getenv "EINDHOVEN_HOME";
- val pmu =
- if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
- else eindhoven_home ^ "/pmu";
- in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
-
-in
-
-fun mk_eindhoven_mc_oracle (sign, EindhovenOracleExn trm) =
- let
- val tmtext = termtext sign trm;
- val debug = writeln ("MC debugger: " ^ tmtext);
- val result = call_mc tmtext;
- in
- if ! trace_mc then
- (writeln tmtext; writeln("----"); writeln result)
- else ();
- (case result of
- "TRUE\n" => trm |
- "FALSE\n" => (error "MC oracle yields FALSE") |
- _ => (error ("MC syntax error: " ^ result)))
- end;
-
-end;
--- a/src/HOL/Modelcheck/MuCalculus.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(* Title: HOL/Modelcheck/MuCalculus.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-exception MCOracleExn of term;
-exception MCFailureExn of string;
-
-
-val trace_mc = ref false;
-
-local
-
-fun termtext sign term =
- setmp print_mode ["Eindhoven"] (Sign.string_of_term sign) term;
-
-fun call_mc s =
- execute ( "echo \"" ^ s ^ "\" | pmu -w" );
-
-in
-
-fun mk_mc_oracle (sign, MCOracleExn trm) =
- let
- val tmtext = termtext sign trm;
- val debug = writeln ("MC debugger: " ^ tmtext);
- val result = call_mc tmtext;
- in
- if ! trace_mc then
- (writeln tmtext; writeln("----"); writeln result)
- else ();
- (case result of
- "TRUE\n" => trm |
- "FALSE\n" => (error "MC oracle yields FALSE") |
- _ => (error ("MC syntax error: " ^ result)))
- end;
-
-end;
--- a/src/HOL/Modelcheck/MuCalculus.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,23 +4,26 @@
Copyright 1997 TU Muenchen
*)
-MuCalculus = Main +
+theory MuCalculus
+imports Main
+begin
types
'a pred = "'a=>bool"
-consts
-
+constdefs
Charfun :: "'a set => 'a pred"
- mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
- nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
+ "Charfun == (% A.% x. x:A)"
+
monoP :: "('a pred => 'a pred) => bool"
+ "monoP f == mono(Collect o f o Charfun)"
-defs
+ mu :: "('a pred => 'a pred) => 'a pred" (binder "Mu " 10)
+ "mu f == Charfun(lfp(Collect o f o Charfun))"
-Charfun_def "Charfun == (% A.% x. x:A)"
-monoP_def "monoP f == mono(Collect o f o Charfun)"
-mu_def "mu f == Charfun(lfp(Collect o f o Charfun))"
-nu_def "nu f == Charfun(gfp(Collect o f o Charfun))"
+ nu :: "('a pred => 'a pred) => 'a pred" (binder "Nu " 10)
+ "nu f == Charfun(gfp(Collect o f o Charfun))"
+
+ML {* use_legacy_bindings (the_context ()) *}
end
--- a/src/HOL/Modelcheck/MuckeExample1.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(* Title: HOL/Modelcheck/MuckeExample1.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-val reach_rws = [INIT_def,N_def,reach_def];
-
-Goal "reach (True,True,True)";
-by (simp_tac (Mucke_ss addsimps reach_rws) 1);
-by (mc_mucke_tac [] 1);
-qed "reach_ex_thm1";
-
-(*alternative*)
-Goal "reach (True,True,True)";
-by (mc_mucke_tac reach_rws 1);
-qed "reach_ex_thm1'";
--- a/src/HOL/Modelcheck/MuckeExample1.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample1.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,31 +4,34 @@
Copyright 1997 TU Muenchen
*)
-MuckeExample1 = MuckeSyn +
-
-
+theory MuckeExample1
+imports MuckeSyn
+begin
types
- state = "bool * bool * bool"
-
-consts
-
- INIT :: "state pred"
- N :: "[state,state] => bool"
- reach:: "state pred"
+ state = "bool * bool * bool"
-defs
-
- INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+constdefs
+ INIT :: "state pred"
+ "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+ N :: "[state,state] => bool"
+ "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
+ y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
+ in (~x1&~x2&~x3 & y1&~y2&~y3) |
+ (x1&~x2&~x3 & ~y1&~y2&~y3) |
+ (x1&~x2&~x3 & y1&y2&y3)"
+ reach:: "state pred"
+ "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
- N_def "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
- y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
- in (~x1&~x2&~x3 & y1&~y2&~y3) |
- (x1&~x2&~x3 & ~y1&~y2&~y3) |
- (x1&~x2&~x3 & y1&y2&y3) "
-
- reach_def "reach == mu (%Q x. INIT x | (? y. Q y & N y x))"
-
+lemmas reach_rws = INIT_def N_def reach_def
+
+lemma reach_ex1: "reach (True,True,True)"
+ apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
+ apply (tactic {* mc_mucke_tac [] 1 *})
+ done
+
+(*alternative*)
+lemma reach_ex' "reach (True,True,True)"
+ by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
end
-
--- a/src/HOL/Modelcheck/MuckeExample2.ML Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: HOL/Modelcheck/MuckeExample2.ML
- ID: $Id$
- Author: Olaf Mueller, Jan Philipps, Robert Sandner
- Copyright 1997 TU Muenchen
-*)
-
-
-(* prints the mucke output on the screen *)
-(* trace_mc := true; *)
-val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
-
-Goal "Reach2 True";
-by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
-by (mc_mucke_tac [] 1);
-qed "Reach_thm";
-
-(*alternative:*)
-goal thy "Reach2 True";
-by (mc_mucke_tac Reach_rws 1);
-qed "Reach_thm'";
--- a/src/HOL/Modelcheck/MuckeExample2.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample2.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,24 +4,29 @@
Copyright 1997 TU Muenchen
*)
-
-MuckeExample2 = MuckeSyn +
-
-consts
-
- Init :: "bool pred"
- R :: "[bool,bool] => bool"
- Reach :: "bool pred"
- Reach2:: "bool pred"
+theory MuckeExample2
+imports MuckeSyn
+begin
-defs
-
- Init_def " Init x == x"
-
- R_def "R x y == (x & ~y) | (~x & y)"
+constdefs
+ Init :: "bool pred"
+ "Init x == x"
+ R :: "[bool,bool] => bool"
+ "R x y == (x & ~y) | (~x & y)"
+ Reach :: "bool pred"
+ "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+ Reach2:: "bool pred"
+ "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
- Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
- Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
+lemma Reach: "Reach2 True"
+ apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
+ apply (tactic {* mc_mucke_tac [] 1 *})
+ done
-end
\ No newline at end of file
+(*alternative:*)
+lemma Reach': "Reach2 True"
+ by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
+
+end
--- a/src/HOL/Modelcheck/MuckeSyn.ML Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML Tue Sep 06 16:24:53 2005 +0200
@@ -49,7 +49,7 @@
local
- val move_thm = prove_goal MuckeSyn.thy "[| a = b ==> P a; a = b |] ==> P b"
+ val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
REPEAT (resolve_tac prems 1)]);
@@ -86,9 +86,9 @@
(* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *)
(* Normally t can be user-instantiated by the value thy of the Isabelle context *)
fun call_mucke_tac i state =
-let val sign = #sign (rep_thm state);
+let val thy = Thm.theory_of_thm state;
val (subgoal::_) = Library.drop(i-1,prems_of state);
- val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal));
+ val OraAss = mc_mucke_oracle thy subgoal;
in
(cut_facts_tac [OraAss] i) state
end;
--- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Tue Sep 06 16:24:53 2005 +0200
@@ -4,76 +4,73 @@
Copyright 1999 TU Muenchen
*)
+theory MuckeSyn
+imports MuCalculus
+uses "mucke_oracle.ML"
+begin
-MuckeSyn = MuCalculus +
-
-(* extended with some operators and case treatment (which requires postprocessing with
+(* extended with some operators and case treatment (which requires postprocessing with
transform_case (from MuCalculus) (TH) *)
-types
- mutype
+nonterminals
+ mutype
decl decls
- cases_syn case_syn
+ cases_syn case_syn
syntax (Mucke output)
- True :: bool ("true")
- False :: bool ("false")
- Not :: bool => bool ("! _" [40] 40)
- If :: [bool, 'a, 'a] => 'a ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
-
- "op &" :: [bool, bool] => bool (infixr "&" 35)
- "op |" :: [bool, bool] => bool (infixr "|" 30)
- "op -->" :: [bool, bool] => bool (infixr "->" 25)
- "op =" :: ['a, 'a] => bool ("(_ =/ _)" [51, 51] 50)
- "_not_equal" :: ['a, 'a] => bool ("(_ !=/ _)" [51, 51] 50)
+ True :: bool ("true")
+ False :: bool ("false")
+ Not :: "bool => bool" ("! _" [40] 40)
+ If :: "[bool, 'a, 'a] => 'a" ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
- "! " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10)
- "? " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10)
- "ALL " :: [idts, bool] => bool ("'((3forall _./ _)')" [0, 10] 10)
- "EX " :: [idts, bool] => bool ("'((3exists _./ _)')" [0, 10] 10)
+ "op &" :: "[bool, bool] => bool" (infixr "&" 35)
+ "op |" :: "[bool, bool] => bool" (infixr "|" 30)
+ "op -->" :: "[bool, bool] => bool" (infixr "->" 25)
+ "op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50)
+ "_not_equal" :: "['a, 'a] => bool" ("(_ !=/ _)" [51, 51] 50)
- "_lambda" :: [idts, 'a] => 'b ("(3L _./ _)" 10)
- "_applC" :: [('b => 'a), cargs] => aprop ("(1_/ '(_'))" [1000,1000] 999)
- "_cargs" :: ['a, cargs] => cargs ("_,/ _" [1000,1000] 1000)
+ "ALL " :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10)
+ "EX " :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10)
- "_idts" :: [idt, idts] => idts ("_,/ _" [1, 0] 0)
+ "_lambda" :: "[idts, 'a] => 'b" ("(3L _./ _)" 10)
+ "_applC" :: "[('b => 'a), cargs] => aprop" ("(1_/ '(_'))" [1000,1000] 999)
+ "_cargs" :: "['a, cargs] => cargs" ("_,/ _" [1000,1000] 1000)
+
+ "_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0)
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)")
-(* "@pttrn" :: [pttrn, pttrns] => pttrn ("_,/ _" [1, 0] 0)
- "_pattern" :: [pttrn, patterns] => pttrn ("_,/ _" [1, 0] 0) *)
-
+(* "@pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0)
+ "_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *)
- "_decl" :: [mutype,pttrn] => decl ("_ _")
- "_decls" :: [decl,decls] => decls ("_,/ _")
- "" :: decl => decls ("_")
- "_mu" :: [decl,decls,'a pred] => 'a pred ("mu _ '(_') _ ;")
- "_mudec" :: [decl,decls] => 'a pred ("mu _ '(_') ;")
- "_nu" :: [decl,decls,'a pred] => 'a pred ("nu _ '(_') _ ;")
- "_nudec" :: [decl,decls] => 'a pred ("nu _ '(_') ;")
- "_fun" :: [decl,decls,'a pred] => 'a pred ("_ '(_') _ ;")
- "_dec" :: [decl,decls] => 'a pred ("_ '(_') ;")
+ "_decl" :: "[mutype,pttrn] => decl" ("_ _")
+ "_decls" :: "[decl,decls] => decls" ("_,/ _")
+ "" :: "decl => decls" ("_")
+ "_mu" :: "[decl,decls,'a pred] => 'a pred" ("mu _ '(_') _ ;")
+ "_mudec" :: "[decl,decls] => 'a pred" ("mu _ '(_') ;")
+ "_nu" :: "[decl,decls,'a pred] => 'a pred" ("nu _ '(_') _ ;")
+ "_nudec" :: "[decl,decls] => 'a pred" ("nu _ '(_') ;")
+ "_fun" :: "[decl,decls,'a pred] => 'a pred" ("_ '(_') _ ;")
+ "_dec" :: "[decl,decls] => 'a pred" ("_ '(_') ;")
+
+ "_Ex" :: "[decl,idts,'a pred] => 'a pred" ("'((3exists _ _./ _)')")
+ "_All" :: "[decl,idts,'a pred] => 'a pred" ("'((3forall _ _./ _)')")
- "_Ex" :: [decl,idts,'a pred] => 'a pred ("'((3exists _ _./ _)')")
- "_All" :: [decl,idts,'a pred] => 'a pred ("'((3forall _ _./ _)')")
+ "Mu " :: "[idts, 'a pred] => 'a pred" ("(3mu _./ _)" 1000)
+ "Nu " :: "[idts, 'a pred] => 'a pred" ("(3nu _./ _)" 1000)
+
+ "_case_syntax":: "['a, cases_syn] => 'b" ("(case*_* / _ / esac*)" 10)
+ "_case1" :: "['a, 'b] => case_syn" ("(2*= _ :/ _;)" 10)
+ "" :: "case_syn => cases_syn" ("_")
+ "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ _")
- "Mu " :: [idts, 'a pred] => 'a pred ("(3mu _./ _)" 1000)
- "Nu " :: [idts, 'a pred] => 'a pred ("(3nu _./ _)" 1000)
-
- "_case_syntax":: ['a, cases_syn] => 'b ("(case*_* / _ / esac*)" 10)
- "_case1" :: ['a, 'b] => case_syn ("(2*= _ :/ _;)" 10)
- "" :: case_syn => cases_syn ("_")
- "_case2" :: [case_syn, cases_syn] => cases_syn ("_/ _")
-(* Terms containing a case statement must be post-processed with the function *)
-(* transform_case, defined in MuCalculus.ML. There, all asterikses before the *)
-(* "=" will be replaced by the expression between the two asterikses following *)
-(* "case" and the asteriks after esac will be deleted *)
+(*Terms containing a case statement must be post-processed with the
+ ML function transform_case. There, all asterikses before the "="
+ will be replaced by the expression between the two asterisks
+ following "case" and the asterisk after esac will be deleted *)
-oracle
- Mucke = mk_mucke_mc_oracle
+oracle mc_mucke_oracle ("term") =
+ mk_mc_mucke_oracle
end
-
-
-
--- a/src/HOL/Modelcheck/ROOT.ML Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML Tue Sep 06 16:24:53 2005 +0200
@@ -5,6 +5,14 @@
Basic Modelchecker examples.
*)
+time_use_thy "CTL";
+
+
+(* Einhoven model checker *)
+
+time_use_thy "EindhovenSyn";
+if_eindhoven_enabled time_use_thy "EindhovenExample";
+
(* Mucke -- mu-calculus model checker from Karlsruhe *)
@@ -15,9 +23,3 @@
if_mucke_enabled time_use_thy "MuckeExample2";
-(* Einhoven model checker *)
-
-time_use_thy "CTL";
-time_use_thy "EindhovenSyn";
-
-if_eindhoven_enabled time_use_thy "EindhovenExample";
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Sep 06 16:24:53 2005 +0200
@@ -1,8 +1,6 @@
(* $Id$ *)
-exception MuckeOracleExn of term;
-
val trace_mc = ref false;
@@ -1017,9 +1015,8 @@
end;
(**********************************************************)
-(* mk_mc_oracle: new argument of MuckeOracleExn: source_thy *)
-fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) =
+fun mk_mc_mucke_oracle sign subgoal =
let val Freesubgoal = freeze_thaw subgoal;
val prems = Logic.strip_imp_prems Freesubgoal;