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