src/HOL/Modelcheck/MuckeSyn.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 22819 a7b425bb668c
child 26342 0f65fa163304
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
mueller@6466
     1
(*  Title:      HOL/Modelcheck/MuckeSyn.thy
mueller@6466
     2
    ID:         $Id$
mueller@6466
     3
    Author:     Tobias Hamberger
mueller@6466
     4
    Copyright   1999  TU Muenchen
mueller@6466
     5
*)
mueller@6466
     6
wenzelm@17272
     7
theory MuckeSyn
wenzelm@17272
     8
imports MuCalculus
wenzelm@17272
     9
uses "mucke_oracle.ML"
wenzelm@17272
    10
begin
mueller@6466
    11
wenzelm@17272
    12
(* extended with some operators and case treatment (which requires postprocessing with
mueller@6466
    13
transform_case (from MuCalculus) (TH) *)
mueller@6466
    14
wenzelm@17272
    15
nonterminals
wenzelm@17272
    16
  mutype
mueller@6466
    17
  decl decls
wenzelm@17272
    18
  cases_syn case_syn
wenzelm@10125
    19
mueller@6466
    20
syntax (Mucke output)
wenzelm@17272
    21
  True          :: bool                                 ("true")
wenzelm@17272
    22
  False         :: bool                                 ("false")
wenzelm@17272
    23
  Not           :: "bool => bool"                       ("! _" [40] 40)
wenzelm@17272
    24
  If            :: "[bool, 'a, 'a] => 'a"       ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
mueller@6466
    25
wenzelm@17272
    26
  "op &"        :: "[bool, bool] => bool"               (infixr "&" 35)
wenzelm@17272
    27
  "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
wenzelm@17272
    28
  "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
wenzelm@17272
    29
  "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
wenzelm@17272
    30
  "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
mueller@6466
    31
wenzelm@21524
    32
  All_binder    :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
wenzelm@21524
    33
  Ex_binder     :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
mueller@6466
    34
wenzelm@17272
    35
  "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
wenzelm@17272
    36
  "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
wenzelm@17272
    37
  "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
wenzelm@17272
    38
wenzelm@17272
    39
  "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
mueller@6466
    40
wenzelm@9368
    41
  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
wenzelm@17272
    42
(* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
wenzelm@17272
    43
  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
mueller@6466
    44
wenzelm@17272
    45
  "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
wenzelm@17272
    46
  "_decls"      :: "[decl,decls] => decls"              ("_,/ _")
wenzelm@17272
    47
  ""            :: "decl => decls"                      ("_")
wenzelm@17272
    48
  "_mu"         :: "[decl,decls,'a pred] => 'a pred"    ("mu _ '(_') _ ;")
wenzelm@17272
    49
  "_mudec"      :: "[decl,decls] => 'a pred"            ("mu _ '(_') ;")
wenzelm@17272
    50
  "_nu"         :: "[decl,decls,'a pred] => 'a pred"    ("nu _ '(_') _ ;")
wenzelm@17272
    51
  "_nudec"      :: "[decl,decls] => 'a pred"            ("nu _ '(_') ;")
wenzelm@17272
    52
  "_fun"        :: "[decl,decls,'a pred] => 'a pred"    ("_ '(_') _ ;")
wenzelm@17272
    53
  "_dec"        :: "[decl,decls] => 'a pred"            ("_ '(_') ;")
wenzelm@17272
    54
wenzelm@17272
    55
  "_Ex"         :: "[decl,idts,'a pred] => 'a pred"     ("'((3exists _ _./ _)')")
wenzelm@17272
    56
  "_All"        :: "[decl,idts,'a pred] => 'a pred"     ("'((3forall _ _./ _)')")
mueller@6466
    57
wenzelm@17272
    58
  "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3mu _./ _)" 1000)
wenzelm@17272
    59
  "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3nu _./ _)" 1000)
wenzelm@17272
    60
wenzelm@17272
    61
  "_case_syntax":: "['a, cases_syn] => 'b"              ("(case*_* / _ / esac*)" 10)
wenzelm@17272
    62
  "_case1"      :: "['a, 'b] => case_syn"               ("(2*= _ :/ _;)" 10)
wenzelm@17272
    63
  ""            :: "case_syn => cases_syn"              ("_")
wenzelm@17272
    64
  "_case2"      :: "[case_syn, cases_syn] => cases_syn" ("_/ _")
mueller@6466
    65
wenzelm@17272
    66
(*Terms containing a case statement must be post-processed with the
wenzelm@17272
    67
  ML function transform_case. There, all asterikses before the "="
wenzelm@17272
    68
  will be replaced by the expression between the two asterisks
wenzelm@17272
    69
  following "case" and the asterisk after esac will be deleted *)
mueller@6466
    70
wenzelm@17272
    71
oracle mc_mucke_oracle ("term") =
wenzelm@17272
    72
  mk_mc_mucke_oracle
mueller@6466
    73
wenzelm@22819
    74
ML {*
wenzelm@22819
    75
(* search_mu t searches for Mu terms in term t. In the case of nested Mu's,
wenzelm@22819
    76
   it yields innermost one. If no Mu term is present, search_mu yields NONE
wenzelm@22819
    77
*)
wenzelm@22819
    78
wenzelm@22819
    79
(* extended for treatment of nu (TH) *)
wenzelm@22819
    80
fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = 
wenzelm@22819
    81
	(case (search_mu t2) of
wenzelm@22819
    82
	      SOME t => SOME t 
wenzelm@22819
    83
	    | NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2))
wenzelm@22819
    84
  | search_mu ((Const("MuCalculus.nu",tp)) $ t2) =
wenzelm@22819
    85
        (case (search_mu t2) of
wenzelm@22819
    86
              SOME t => SOME t
wenzelm@22819
    87
            | NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2))
wenzelm@22819
    88
  | search_mu (t1 $ t2) = 
wenzelm@22819
    89
	(case (search_mu t1) of
wenzelm@22819
    90
	      SOME t => SOME t 
wenzelm@22819
    91
	    | NONE     => search_mu t2)
wenzelm@22819
    92
  | search_mu (Abs(_,_,t)) = search_mu t
wenzelm@22819
    93
  | search_mu _ = NONE;
wenzelm@22819
    94
wenzelm@22819
    95
wenzelm@22819
    96
wenzelm@22819
    97
wenzelm@22819
    98
(* seraching a variable in a term. Used in move_mus to extract the
wenzelm@22819
    99
   term-rep of var b in hthm *)
wenzelm@22819
   100
wenzelm@22819
   101
fun search_var s t =
wenzelm@22819
   102
case t of
wenzelm@22819
   103
     t1 $ t2 => (case (search_var s t1) of
wenzelm@22819
   104
		             SOME tt => SOME tt |
wenzelm@22819
   105
			     NONE => search_var s t2) |
wenzelm@22819
   106
     Abs(_,_,t) => search_var s t |
wenzelm@22819
   107
     Var((s1,_),_) => if s = s1 then SOME t else NONE |
wenzelm@22819
   108
     _ => NONE;
wenzelm@22819
   109
	
wenzelm@22819
   110
wenzelm@22819
   111
(* function move_mus:
wenzelm@22819
   112
   Mucke can't deal with nested Mu terms. move_mus i searches for 
wenzelm@22819
   113
   Mu terms in the subgoal i and replaces Mu terms in the conclusion
wenzelm@22819
   114
   by constants and definitions in the premises recursively.
wenzelm@22819
   115
wenzelm@22819
   116
   move_thm is the theorem the performs the replacement. To create NEW
wenzelm@22819
   117
   names for the Mu terms, the indizes of move_thm are incremented by
wenzelm@22819
   118
   max_idx of the subgoal.
wenzelm@22819
   119
*)
wenzelm@22819
   120
wenzelm@22819
   121
local
wenzelm@22819
   122
wenzelm@22819
   123
  val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
wenzelm@22819
   124
	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
wenzelm@22819
   125
		     REPEAT (resolve_tac prems 1)]);
wenzelm@22819
   126
wenzelm@22819
   127
  val sig_move_thm = Thm.theory_of_thm move_thm;
wenzelm@22819
   128
  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
wenzelm@22819
   129
  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
wenzelm@22819
   130
wenzelm@22819
   131
in
wenzelm@22819
   132
wenzelm@22819
   133
fun move_mus i state =
wenzelm@22819
   134
let val sign = Thm.theory_of_thm state;
wenzelm@22819
   135
    val (subgoal::_) = Library.drop(i-1,prems_of state);
wenzelm@22819
   136
    val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *)
wenzelm@22819
   137
    val redex = search_mu concl;
wenzelm@22819
   138
    val idx = let val t = #maxidx (rep_thm state) in 
wenzelm@22819
   139
	      if t < 0 then 1 else t+1 end;
wenzelm@22819
   140
in
wenzelm@22819
   141
case redex of
wenzelm@22819
   142
     NONE => all_tac state |
wenzelm@22819
   143
     SOME redexterm => 
wenzelm@22819
   144
	let val Credex = cterm_of sign redexterm;
wenzelm@22819
   145
	    val aiCterm = 
wenzelm@22819
   146
		cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm));
wenzelm@22819
   147
	    val inst_move_thm = cterm_instantiate 
wenzelm@22819
   148
				[(bCterm,Credex),(aCterm,aiCterm)] move_thm;
wenzelm@22819
   149
	in
wenzelm@22819
   150
            ((rtac inst_move_thm i) THEN (dtac eq_reflection i) 
wenzelm@22819
   151
		THEN (move_mus i)) state
wenzelm@22819
   152
	end
wenzelm@22819
   153
end;
wenzelm@22819
   154
end;
mueller@6466
   155
mueller@6466
   156
wenzelm@22819
   157
fun call_mucke_tac i state =
wenzelm@22819
   158
let val thy = Thm.theory_of_thm state;
wenzelm@22819
   159
    val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state))
wenzelm@22819
   160
in 
wenzelm@22819
   161
(cut_facts_tac [OraAss] i) state
wenzelm@22819
   162
end;
wenzelm@22819
   163
wenzelm@22819
   164
wenzelm@22819
   165
(* transforming fun-defs into lambda-defs *)
wenzelm@22819
   166
wenzelm@22819
   167
val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g";
wenzelm@22819
   168
 by (rtac (extensional eq) 1);
wenzelm@22819
   169
qed "ext_rl";
wenzelm@22819
   170
wenzelm@22819
   171
infix cc;
wenzelm@22819
   172
wenzelm@22819
   173
fun NONE cc xl = xl
wenzelm@22819
   174
  | (SOME x) cc xl = x::xl;
wenzelm@22819
   175
wenzelm@22819
   176
fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z
wenzelm@22819
   177
  | getargs (x $ (Var ((y,_),_))) = y;
wenzelm@22819
   178
wenzelm@22819
   179
fun getfun ((x $ y) $ z) = getfun (x $ y)
wenzelm@22819
   180
  | getfun (x $ _) = x;
wenzelm@22819
   181
wenzelm@22819
   182
local
wenzelm@22819
   183
wenzelm@22819
   184
fun delete_bold [] = []
wenzelm@22819
   185
| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
wenzelm@22819
   186
        then (let val (_::_::_::s) = xs in delete_bold s end)
wenzelm@22819
   187
        else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
wenzelm@22819
   188
                then  (let val (_::_::_::s) = xs in delete_bold s end)
wenzelm@22819
   189
                else (x::delete_bold xs));
wenzelm@22819
   190
wenzelm@22819
   191
fun delete_bold_string s = implode(delete_bold (explode s));
wenzelm@22819
   192
wenzelm@22819
   193
in
wenzelm@22819
   194
wenzelm@22819
   195
(* extension with removing bold font (TH) *)
wenzelm@22819
   196
fun mk_lam_def (_::_) _ _ = NONE  
wenzelm@22819
   197
  | mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t
wenzelm@22819
   198
  | mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = 
wenzelm@22819
   199
    let val thy = theory_of_thm t;
wenzelm@22819
   200
	val fnam = Sign.string_of_term thy (getfun LHS);
wenzelm@22819
   201
	val rhs = Sign.string_of_term thy (freeze_thaw RHS)
wenzelm@22819
   202
	val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs);
wenzelm@22819
   203
    in
wenzelm@22819
   204
	SOME (prove_goal thy gl (fn prems =>
wenzelm@22819
   205
  		[(REPEAT (rtac ext_rl 1)), (rtac t 1) ]))
wenzelm@22819
   206
    end
wenzelm@22819
   207
| mk_lam_def [] _ t= NONE; 
wenzelm@22819
   208
wenzelm@22819
   209
fun mk_lam_defs ([]:thm list) = ([]: thm list) 
wenzelm@22819
   210
  | mk_lam_defs (t::l) = 
wenzelm@22819
   211
      (mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l);
wenzelm@22819
   212
wenzelm@22819
   213
end;
wenzelm@22819
   214
wenzelm@22819
   215
wenzelm@22819
   216
(* first simplification, then model checking *)
wenzelm@22819
   217
wenzelm@22819
   218
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta"));
wenzelm@22819
   219
wenzelm@22819
   220
val pair_eta_expand_proc =
wenzelm@22819
   221
  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
wenzelm@22819
   222
  (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE);
wenzelm@22819
   223
wenzelm@22819
   224
val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def];
wenzelm@22819
   225
wenzelm@22819
   226
wenzelm@22819
   227
(* the interface *)
wenzelm@22819
   228
wenzelm@22819
   229
fun mc_mucke_tac defs i state =
wenzelm@22819
   230
  (case Library.drop (i - 1, Thm.prems_of state) of
wenzelm@22819
   231
    [] => no_tac state
wenzelm@22819
   232
  | subgoal :: _ =>
wenzelm@22819
   233
      EVERY [
wenzelm@22819
   234
        REPEAT (etac thin_rl i),
wenzelm@22819
   235
        cut_facts_tac (mk_lam_defs defs) i,
wenzelm@22819
   236
        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
wenzelm@22819
   237
        move_mus i, call_mucke_tac i,atac i,
wenzelm@22819
   238
        REPEAT (rtac refl i)] state);
wenzelm@22819
   239
wenzelm@22819
   240
(*check if user has mucke installed*)
wenzelm@22819
   241
fun mucke_enabled () = getenv "MUCKE_HOME" <> "";
wenzelm@22819
   242
fun if_mucke_enabled f x = if mucke_enabled () then f x else ();
wenzelm@22819
   243
wenzelm@22819
   244
*}
wenzelm@22819
   245
wenzelm@22819
   246
end