src/Provers/trancl.ML
 changeset 15570 8d8c70b41bab parent 15531 08c8dad8e399 child 15574 b1d1b5bfc464
equal 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`