src/Provers/trancl.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15574 b1d1b5bfc464
equal deleted inserted replaced
15569:1b3115d1a8df 15570:8d8c70b41bab
    86   | Thm of proof list * thm; 
    86   | Thm of proof list * thm; 
    87 
    87 
    88  exception Cannot; (* internal exception: raised if no proof can be found *)
    88  exception Cannot; (* internal exception: raised if no proof can be found *)
    89 
    89 
    90  fun prove asms = 
    90  fun prove asms = 
    91   let fun pr (Asm i) = nth_elem (i, asms)
    91   let fun pr (Asm i) = List.nth (asms, i)
    92   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    92   |       pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
    93   in pr end;
    93   in pr end;
    94 
    94 
    95   
    95   
    96 (* Internal datatype for inequalities *)
    96 (* Internal datatype for inequalities *)
   325        end
   325        end
   326      | assemble nil _ = nil
   326      | assemble nil _ = nil
   327 
   327 
   328    (* Compute, for each adjacency list, the list with reversed edges,
   328    (* Compute, for each adjacency list, the list with reversed edges,
   329       and concatenate these lists. *)
   329       and concatenate these lists. *)
   330    val flipped = foldr (op @) ((map flip g),nil)
   330    val flipped = Library.foldr (op @) ((map flip g),nil)
   331  
   331  
   332  in assemble g flipped end    
   332  in assemble g flipped end    
   333  
   333  
   334 (* *********************************************************************** *)
   334 (* *********************************************************************** *)
   335 (*                                                                         *)
   335 (*                                                                         *)
   349 
   349 
   350   fun dfs_visit g u  =
   350   fun dfs_visit g u  =
   351       let
   351       let
   352    val _ = visited := u :: !visited
   352    val _ = visited := u :: !visited
   353    val descendents =
   353    val descendents =
   354        foldr (fn ((v,l),ds) => if been_visited v then ds
   354        Library.foldr (fn ((v,l),ds) => if been_visited v then ds
   355             else v :: dfs_visit g v @ ds)
   355             else v :: dfs_visit g v @ ds)
   356         ( ((adjacent eq_comp g u)) ,nil)
   356         ( ((adjacent eq_comp g u)) ,nil)
   357    in  descendents end
   357    in  descendents end
   358  
   358  
   359  in u :: dfs_visit g u end;
   359  in u :: dfs_visit g u end;
   528 val trancl_tac =   SUBGOAL (fn (A, n) =>
   528 val trancl_tac =   SUBGOAL (fn (A, n) =>
   529  let
   529  let
   530   val Hs = Logic.strip_assums_hyp A;
   530   val Hs = Logic.strip_assums_hyp A;
   531   val C = Logic.strip_assums_concl A;
   531   val C = Logic.strip_assums_concl A;
   532   val (rel,subgoals, prf) = mkconcl_trancl C;
   532   val (rel,subgoals, prf) = mkconcl_trancl C;
   533   val prems = flat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   533   val prems = List.concat (ListPair.map (mkasm_trancl rel) (Hs, 0 upto (length Hs - 1)))
   534   val prfs = solveTrancl (prems, C);
   534   val prfs = solveTrancl (prems, C);
   535 
   535 
   536  in
   536  in
   537   METAHYPS (fn asms =>
   537   METAHYPS (fn asms =>
   538     let val thms = map (prove asms) prfs
   538     let val thms = map (prove asms) prfs
   546  let
   546  let
   547   val Hs = Logic.strip_assums_hyp A;
   547   val Hs = Logic.strip_assums_hyp A;
   548   val C = Logic.strip_assums_concl A;
   548   val C = Logic.strip_assums_concl A;
   549   val (rel,subgoals, prf) = mkconcl_rtrancl C;
   549   val (rel,subgoals, prf) = mkconcl_rtrancl C;
   550 
   550 
   551   val prems = flat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   551   val prems = List.concat (ListPair.map (mkasm_rtrancl rel) (Hs, 0 upto (length Hs - 1)))
   552   val prfs = solveRtrancl (prems, C);
   552   val prfs = solveRtrancl (prems, C);
   553  in
   553  in
   554   METAHYPS (fn asms =>
   554   METAHYPS (fn asms =>
   555     let val thms = map (prove asms) prfs
   555     let val thms = map (prove asms) prfs
   556     in rtac (prove thms prf) 1 end) n
   556     in rtac (prove thms prf) 1 end) n