src/Provers/typedsimp.ML
 changeset 32960 69916a850301 parent 32957 675c0c7e6a37 child 33339 d41f77196338
equal inserted replaced
32959:23a8c5ac35f8 32960:69916a850301
`     1 (*  Title: 	typedsimp`
`     1 (*  Title:      Provers/typedsimp.ML`
`     2     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory`
`     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory`
`     3     Copyright   1993  University of Cambridge`
`     3     Copyright   1993  University of Cambridge`
`     4 `
`     4 `
`     5 Functor for constructing simplifiers.  Suitable for Constructive Type`
`     5 Functor for constructing simplifiers.  Suitable for Constructive Type`
`     6 Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try`
`     6 Theory with its typed reflexivity axiom a:A ==> a=a:A.  For most logics try`
`     7 simp.ML.`
`     7 simp.ML.`
`     8 *)`
`     8 *)`
`     9 `
`     9 `
`    10 signature TSIMP_DATA =`
`    10 signature TSIMP_DATA =`
`    11   sig`
`    11   sig`
`    12   val refl: thm		(*Reflexive law*)`
`    12   val refl: thm         (*Reflexive law*)`
`    13   val sym: thm		(*Symmetric law*)`
`    13   val sym: thm          (*Symmetric law*)`
`    14   val trans: thm	(*Transitive law*)`
`    14   val trans: thm        (*Transitive law*)`
`    15   val refl_red: thm	(* reduce(a,a) *)`
`    15   val refl_red: thm     (* reduce(a,a) *)`
`    16   val trans_red: thm	(* [|a=b; reduce(b,c) |] ==> a=c *)`
`    16   val trans_red: thm    (* [|a=b; reduce(b,c) |] ==> a=c *)`
`    17   val red_if_equal: thm (* a=b ==> reduce(a,b) *)`
`    17   val red_if_equal: thm (* a=b ==> reduce(a,b) *)`
`    18   (*Built-in rewrite rules*)`
`    18   (*Built-in rewrite rules*)`
`    19   val default_rls: thm list`
`    19   val default_rls: thm list`
`    20   (*Type checking or similar -- solution of routine conditions*)`
`    20   (*Type checking or similar -- solution of routine conditions*)`
`    21   val routine_tac: thm list -> int -> tactic`
`    21   val routine_tac: thm list -> int -> tactic`
`    74 (*Given list of rewrite rules, return list of both forms, reject others*)`
`    74 (*Given list of rewrite rules, return list of both forms, reject others*)`
`    75 fun process_rewrites rls = `
`    75 fun process_rewrites rls = `
`    76   case process_rules rls of`
`    76   case process_rules rls of`
`    77       (simp_rls,[])  =>  simp_rls`
`    77       (simp_rls,[])  =>  simp_rls`
`    78     | (_,others) => raise THM `
`    78     | (_,others) => raise THM `
`    79 	("process_rewrites: Ill-formed rewrite", 0, others);`
`    79         ("process_rewrites: Ill-formed rewrite", 0, others);`
`    80 `
`    80 `
`    81 (*Process the default rewrite rules*)`
`    81 (*Process the default rewrite rules*)`
`    82 val simp_rls = process_rewrites default_rls;`
`    82 val simp_rls = process_rewrites default_rls;`
`    83 `
`    83 `
`    84 (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac`
`    84 (*If subgoal is too flexible (e.g. ?a=?b or just ?P) then filt_resolve_tac`
`    95   ORELSE'  filt_resolve_tac [refl,refl_red] 1;`
`    95   ORELSE'  filt_resolve_tac [refl,refl_red] 1;`
`    96 `
`    96 `
`    97 (*Resolve with asms, whether rewrites or not*)`
`    97 (*Resolve with asms, whether rewrites or not*)`
`    98 fun asm_res_tac asms =`
`    98 fun asm_res_tac asms =`
`    99     let val (xsimp_rls,xother_rls) = process_rules asms`
`    99     let val (xsimp_rls,xother_rls) = process_rules asms`
`   100     in 	routine_tac xother_rls  ORELSE'  `
`   100     in  routine_tac xother_rls  ORELSE'  `
`   101 	filt_resolve_tac xsimp_rls 2`
`   101         filt_resolve_tac xsimp_rls 2`
`   102     end;`
`   102     end;`
`   103 `
`   103 `
`   104 (*Single step for simple rewriting*)`
`   104 (*Single step for simple rewriting*)`
`   105 fun step_tac (congr_rls,asms) =`
`   105 fun step_tac (congr_rls,asms) =`
`   106     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  `
`   106     asm_res_tac asms   ORELSE'  rewrite_res_tac  ORELSE'  `