src/HOL/Statespace/distinct_tree_prover.ML
author Norbert Schirmer <norbert.schirmer@web.de>
Thu, 18 Dec 2008 11:16:48 +0100
changeset 29247 95d3a82857e5
parent 29064 70a61d58460e
child 29269 5c25a2012975
permissions -rw-r--r--
adapted statespace module to new locales;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     1
(*  Title:      distinct_tree_prover.thy
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     2
    ID:         $Id$
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     3
    Author:     Norbert Schirmer, TU Muenchen
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     4
*)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
     5
25408
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
     6
signature DISTINCT_TREE_PROVER =
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
     7
sig
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
     8
  datatype Direction = Left | Right
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
     9
  val mk_tree : ('a -> Term.term) -> Term.typ -> 'a list -> Term.term
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    10
  val dest_tree : Term.term -> Term.term list
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    11
  val find_tree :
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    12
       Term.term -> Term.term -> Direction list option 
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    13
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    14
  val neq_to_eq_False : Thm.thm
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    15
  val distinctTreeProver : Thm.thm -> Direction list -> Direction list -> Thm.thm
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    16
  val neq_x_y :
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    17
       Proof.context -> Term.term -> Term.term -> string -> Thm.thm option   
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    18
  val distinctFieldSolver : string list -> MetaSimplifier.solver
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    19
  val distinctTree_tac :
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    20
       string list -> Proof.context -> Term.term * int -> Tactical.tactic
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    21
  val distinct_implProver : Thm.thm -> Thm.cterm -> Thm.thm
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    22
  val subtractProver : Term.term -> Thm.cterm -> Thm.thm -> Thm.thm
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    23
  val distinct_simproc : string list -> MetaSimplifier.simproc
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    24
  
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    25
  val discharge : Thm.thm list -> Thm.thm -> Thm.thm
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    26
end;
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    27
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    28
structure DistinctTreeProver : DISTINCT_TREE_PROVER =
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    29
struct
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    30
val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    31
val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    32
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    33
val distinct_left = thm "DistinctTreeProver.distinct_left";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    34
val distinct_right = thm "DistinctTreeProver.distinct_right";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    35
val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    36
val in_set_root = thm "DistinctTreeProver.in_set_root";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    37
val in_set_left = thm "DistinctTreeProver.in_set_left";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    38
val in_set_right = thm "DistinctTreeProver.in_set_right";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    39
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    40
val swap_neq = thm "DistinctTreeProver.swap_neq";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    41
val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    42
25408
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    43
datatype Direction = Left | Right 
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    44
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    45
fun treeT T = Type ("DistinctTreeProver.tree",[T]);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    46
fun mk_tree' e T n []     = Const ("DistinctTreeProver.tree.Tip",treeT T)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    47
  | mk_tree' e T n xs =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    48
     let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    49
       val m = (n - 1) div 2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    50
       val (xsl,x::xsr) = chop m xs;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    51
       val l = mk_tree' e T m xsl;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    52
       val r = mk_tree' e T (n-(m+1)) xsr;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    53
     in Const ("DistinctTreeProver.tree.Node",
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    54
                treeT T --> T --> HOLogic.boolT--> treeT T --> treeT T) $ 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    55
          l$ e x $ HOLogic.false_const $ r 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    56
     end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    57
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    58
fun mk_tree e T xs = mk_tree' e T (length xs) xs;         
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    59
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    60
fun dest_tree (Const ("DistinctTreeProver.tree.Tip",_)) = []
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    61
  | dest_tree (Const ("DistinctTreeProver.tree.Node",_)$l$e$_$r) = dest_tree l @ e :: dest_tree r
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    62
  | dest_tree t = raise TERM ("DistinctTreeProver.dest_tree",[t]);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    63
25408
156f6f7082b8 added signatures;
schirmer
parents: 25171
diff changeset
    64
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    65
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    66
fun lin_find_tree e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    67
  | lin_find_tree e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    68
      if e aconv x 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    69
      then SOME []
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    70
      else (case lin_find_tree e l of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    71
              SOME path => SOME (Left::path)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    72
            | NONE => (case lin_find_tree e r of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    73
                        SOME path => SOME (Right::path)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    74
                       | NONE => NONE))
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    75
  | lin_find_tree e t = raise TERM ("find_tree: input not a tree",[t])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    76
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    77
fun bin_find_tree order e (Const ("DistinctTreeProver.tree.Tip",_)) = NONE
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    78
  | bin_find_tree order e (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    79
      (case order (e,x) of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    80
         EQUAL => SOME []
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    81
       | LESS => Option.map (cons Left) (bin_find_tree order e l)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    82
       | GREATER => Option.map (cons Right) (bin_find_tree order e r))
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    83
  | bin_find_tree order e t = raise TERM ("find_tree: input not a tree",[t])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    84
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    85
fun find_tree e t =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    86
  (case bin_find_tree Term.fast_term_ord e t of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    87
     NONE => lin_find_tree e t
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    88
   | x => x);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    89
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    90
 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    91
fun index_tree (Const ("DistinctTreeProver.tree.Tip",_)) path tab = tab
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    92
  | index_tree (Const ("DistinctTreeProver.tree.Node",_) $ l$ x $ _ $ r) path tab =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    93
      tab 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    94
      |> Termtab.update_new (x,path) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    95
      |> index_tree l (path@[Left])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    96
      |> index_tree r (path@[Right])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    97
  | index_tree t _ _ = raise TERM ("index_tree: input not a tree",[t])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    98
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
    99
fun split_common_prefix xs [] = ([],xs,[])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   100
  | split_common_prefix [] ys = ([],[],ys)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   101
  | split_common_prefix (xs as (x::xs')) (ys as (y::ys')) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   102
     if x=y 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   103
     then let val (ps,xs'',ys'') = split_common_prefix xs' ys' in (x::ps,xs'',ys'') end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   104
     else ([],xs,ys)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   105
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   106
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   107
(* Wrapper around Thm.instantiate. The type instiations of instTs are applied to
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   108
 * the right hand sides of insts
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   109
 *)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   110
fun instantiate instTs insts =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   111
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   112
    val instTs' = map (fn (T,U) => (dest_TVar (typ_of T),typ_of U)) instTs;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   113
    fun substT x = (case AList.lookup (op =) instTs' x of NONE => TVar x | SOME T' => T');
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   114
    fun mapT_and_recertify ct =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   115
      let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   116
        val thy = theory_of_cterm ct;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   117
      in (cterm_of thy (Term.map_types (Term.map_type_tvar substT) (term_of ct))) end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   118
    val insts' = map (apfst mapT_and_recertify) insts;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   119
  in Thm.instantiate (instTs,insts') end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   120
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   121
fun tvar_clash ixn S S' = raise TYPE ("Type variable " ^
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   122
  quote (Term.string_of_vname ixn) ^ " has two distinct sorts",
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   123
  [TVar (ixn, S), TVar (ixn, S')], []);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   124
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   125
fun lookup (tye, (ixn, S)) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   126
  (case AList.lookup (op =) tye ixn of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   127
    NONE => NONE
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   128
  | SOME (S', T) => if S = S' then SOME T else tvar_clash ixn S S');
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   129
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   130
val naive_typ_match =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   131
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   132
    fun match (TVar (v, S), T) subs =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   133
          (case lookup (subs, (v, S)) of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   134
            NONE => ((v, (S, T))::subs)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   135
          | SOME _ => subs)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   136
      | match (Type (a, Ts), Type (b, Us)) subs =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   137
          if a <> b then raise Type.TYPE_MATCH
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   138
          else matches (Ts, Us) subs
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   139
      | match (TFree x, TFree y) subs =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   140
          if x = y then subs else raise Type.TYPE_MATCH
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   141
      | match _ _ = raise Type.TYPE_MATCH
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   142
    and matches (T :: Ts, U :: Us) subs = matches (Ts, Us) (match (T, U) subs)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   143
      | matches _ subs = subs;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   144
  in match end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   145
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   146
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   147
(* expects that relevant type variables are already contained in 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   148
 * term variables. First instantiation of variables is returned without further
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   149
 * checking.
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   150
 *)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   151
fun naive_cterm_first_order_match (t,ct) env =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   152
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   153
    val thy = (theory_of_cterm ct);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   154
    fun mtch (env as (tyinsts,insts)) = fn
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   155
         (Var(ixn,T),ct) =>
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   156
           (case AList.lookup (op =) insts ixn of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   157
             NONE => (naive_typ_match (T,typ_of (ctyp_of_term ct)) tyinsts,
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   158
                      (ixn, ct)::insts)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   159
            | SOME _ => env)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   160
        | (f$t,ct) => let val (cf,ct') = Thm.dest_comb ct;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   161
                      in mtch (mtch env (f,cf)) (t,ct') end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   162
        | _ => env
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   163
  in mtch env (t,ct) end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   164
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   165
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   166
fun mp prem rule = implies_elim rule prem;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   167
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   168
fun discharge prems rule =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   169
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   170
     val thy = theory_of_thm (hd prems);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   171
     val (tyinsts,insts) =  
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   172
           fold naive_cterm_first_order_match (prems_of rule ~~ map cprop_of prems) ([],[]);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   173
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   174
     val tyinsts' = map (fn (v,(S,U)) => (ctyp_of thy (TVar (v,S)),ctyp_of thy U)) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   175
                     tyinsts;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   176
     val insts' = map (fn (idxn,ct) => (cterm_of thy (Var (idxn,typ_of (ctyp_of_term ct))),ct))  
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   177
                     insts;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   178
     val rule' = Thm.instantiate (tyinsts',insts') rule;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   179
   in fold mp prems rule' end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   180
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   181
local
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   182
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   183
val (l_in_set_root,x_in_set_root,r_in_set_root) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   184
  let val (Node_l_x_d,r) = (cprop_of in_set_root) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   185
                         |> Thm.dest_comb |> #2 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   186
                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   187
      val (Node_l,x) = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   188
      val l = Node_l |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   189
  in (l,x,r) end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   190
val (x_in_set_left,r_in_set_left) = 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   191
  let val (Node_l_x_d,r) = (cprop_of in_set_left) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   192
                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   193
                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 |> Thm.dest_comb;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   194
      val x = Node_l_x_d |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   195
  in (x,r) end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   196
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   197
val (x_in_set_right,l_in_set_right) = 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   198
  let val (Node_l,x) = (cprop_of in_set_right) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   199
                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   200
                         |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   201
                         |> Thm.dest_comb |> #1 |> Thm.dest_comb |> #1 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   202
                         |> Thm.dest_comb
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   203
      val l = Node_l |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   204
  in (x,l) end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   205
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   206
in
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   207
(*
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   208
1. First get paths x_path y_path of x and y in the tree.
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   209
2. For the common prefix descend into the tree according to the path
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   210
   and lemmas all_distinct_left/right
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   211
3. If one restpath is empty use distinct_left/right,
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   212
   otherwise all_distinct_left_right
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   213
*)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   214
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   215
fun distinctTreeProver dist_thm x_path y_path =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   216
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   217
    fun dist_subtree [] thm = thm
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   218
      | dist_subtree (p::ps) thm =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   219
         let 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   220
           val rule = (case p of Left => all_distinct_left | Right => all_distinct_right)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   221
         in dist_subtree ps (discharge [thm] rule) end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   222
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   223
    val (ps,x_rest,y_rest) = split_common_prefix x_path y_path;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   224
    val dist_subtree_thm = dist_subtree ps dist_thm;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   225
    val subtree = cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   226
    val (_,[l,_,_,r]) = Drule.strip_comb subtree;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   227
    
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   228
    fun in_set ps tree =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   229
      let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   230
        val (_,[l,x,_,r]) = Drule.strip_comb tree;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   231
        val xT = ctyp_of_term x;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   232
      in (case ps of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   233
            [] => instantiate 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   234
                    [(ctyp_of_term x_in_set_root,xT)]
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   235
                    [(l_in_set_root,l),(x_in_set_root,x),(r_in_set_root,r)] in_set_root
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   236
          | (Left::ps') => 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   237
               let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   238
                  val in_set_l = in_set ps' l;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   239
                  val in_set_left' = instantiate [(ctyp_of_term x_in_set_left,xT)]
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   240
                                      [(x_in_set_left,x),(r_in_set_left,r)] in_set_left;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   241
               in discharge [in_set_l] in_set_left' end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   242
          | (Right::ps') => 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   243
               let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   244
                  val in_set_r = in_set ps' r;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   245
                  val in_set_right' = instantiate [(ctyp_of_term x_in_set_right,xT)] 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   246
                                      [(x_in_set_right,x),(l_in_set_right,l)] in_set_right;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   247
               in discharge [in_set_r] in_set_right' end)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   248
      end 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   249
       
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   250
  fun in_set' [] = raise TERM ("distinctTreeProver",[])
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   251
    | in_set' (Left::ps) = in_set ps l
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   252
    | in_set' (Right::ps) = in_set ps r;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   253
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   254
  fun distinct_lr node_in_set Left  = discharge [dist_subtree_thm,node_in_set] distinct_left 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   255
    | distinct_lr node_in_set Right = discharge [dist_subtree_thm,node_in_set] distinct_right 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   256
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   257
  val (swap,neq) = 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   258
       (case x_rest of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   259
         [] => let 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   260
                 val y_in_set = in_set' y_rest;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   261
               in (false,distinct_lr y_in_set (hd y_rest)) end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   262
       | (xr::xrs) => 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   263
           (case y_rest of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   264
             [] => let 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   265
                     val x_in_set = in_set' x_rest;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   266
               in (true,distinct_lr x_in_set (hd x_rest)) end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   267
           | (yr::yrs) =>
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   268
               let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   269
                 val x_in_set = in_set' x_rest;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   270
                 val y_in_set = in_set' y_rest;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   271
               in (case xr of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   272
                    Left => (false,
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   273
                             discharge [dist_subtree_thm,x_in_set,y_in_set] distinct_left_right)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   274
                   |Right => (true,
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   275
                             discharge [dist_subtree_thm,y_in_set,x_in_set] distinct_left_right))
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   276
               end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   277
        ))
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   278
  in if swap then discharge [neq] swap_neq else neq
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   279
  end  
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   280
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   281
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   282
val delete_root = thm "DistinctTreeProver.delete_root";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   283
val delete_left = thm "DistinctTreeProver.delete_left";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   284
val delete_right = thm "DistinctTreeProver.delete_right";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   285
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   286
fun deleteProver dist_thm [] = delete_root OF [dist_thm]
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   287
  | deleteProver dist_thm (p::ps) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   288
     let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   289
       val dist_rule = (case p of Left => all_distinct_left | Right => all_distinct_right);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   290
       val dist_thm' = discharge [dist_thm] dist_rule 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   291
       val del_rule = (case p of Left => delete_left | Right => delete_right)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   292
       val del = deleteProver dist_thm' ps;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   293
     in discharge [dist_thm, del] del_rule end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   294
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   295
val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   296
val subtract_Node = thm "DistinctTreeProver.subtract_Node";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   297
val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   298
val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   299
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   300
local
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   301
  val (alpha,v) = 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   302
    let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   303
      val ct = subtract_Tip |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   304
               |> Thm.dest_comb |> #2
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   305
      val [alpha] = ct |> Thm.ctyp_of_term |> Thm.dest_ctyp;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   306
    in (alpha, #1 (dest_Var (term_of ct))) end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   307
in
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   308
fun subtractProver (Const ("DistinctTreeProver.tree.Tip",T)) ct dist_thm =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   309
    let 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   310
      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   311
      val thy = theory_of_cterm ct;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   312
      val [alphaI] = #2 (dest_Type T);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   313
    in Thm.instantiate ([(alpha,ctyp_of thy alphaI)],
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   314
                        [(cterm_of thy (Var (v,treeT alphaI)),ct')]) subtract_Tip
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   315
    end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   316
  | subtractProver (Const ("DistinctTreeProver.tree.Node",nT)$l$x$d$r) ct dist_thm =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   317
    let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   318
      val ct' = dist_thm |> Thm.cprop_of |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   319
      val (_,[cl,_,_,cr]) = Drule.strip_comb ct;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   320
      val ps = the (find_tree x (term_of ct'));
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   321
      val del_tree = deleteProver dist_thm ps;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   322
      val dist_thm' = discharge [del_tree, dist_thm] delete_Some_all_distinct; 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   323
      val sub_l = subtractProver (term_of cl) cl (dist_thm');
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   324
      val sub_r = subtractProver (term_of cr) cr 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   325
                    (discharge [sub_l, dist_thm'] subtract_Some_all_distinct_res);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   326
    in discharge [del_tree, sub_l, sub_r] subtract_Node end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   327
end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   328
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   329
val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   330
fun distinct_implProver dist_thm ct =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   331
  let
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   332
    val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   333
    val sub = subtractProver (term_of ctree) ctree dist_thm;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   334
  in subtract_Some_all_distinct OF [sub, dist_thm] end;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   335
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   336
fun get_fst_success f [] = NONE
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   337
  | get_fst_success f (x::xs) = (case f x of NONE => get_fst_success f xs 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   338
                                 | SOME v => SOME v);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   339
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   340
fun neq_x_y ctxt x y name =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   341
  (let
26343
0dd2eab7b296 simplified get_thm(s): back to plain name argument;
wenzelm
parents: 26336
diff changeset
   342
    val dist_thm = the (try (ProofContext.get_thm ctxt) name);
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   343
    val ctree = cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   344
    val tree = term_of ctree;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   345
    val x_path = the (find_tree x tree);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   346
    val y_path = the (find_tree y tree);
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   347
    val thm = distinctTreeProver dist_thm x_path y_path;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   348
  in SOME thm  
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   349
  end handle Option => NONE)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   350
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   351
fun distinctTree_tac names ctxt 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   352
      (Const ("Trueprop",_) $ (Const ("Not", _) $ (Const ("op =", _) $ x $ y)), i) =
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   353
  (case get_fst_success (neq_x_y ctxt x y) names of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   354
     SOME neq => rtac neq i
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   355
   | NONE => no_tac)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   356
  | distinctTree_tac _ _ _ = no_tac;
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   357
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   358
fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   359
     (fn ss => case #context (#1 (rep_ss ss)) of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   360
                 SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   361
                | NONE => fn i => no_tac)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   362
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   363
fun distinct_simproc names =
29064
70a61d58460e more antiquotations;
wenzelm
parents: 26343
diff changeset
   364
  Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
25171
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   365
    (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   366
        case #context (#1 (rep_ss ss)) of
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   367
        SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   368
                      (get_fst_success (neq_x_y ctxt x y) names)
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   369
       | NONE => NONE
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   370
    )
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   371
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   372
end
4a9c25bffc9b added Statespace library
schirmer
parents:
diff changeset
   373
end;