src/FOLP/FOLP.thy
 changeset 48891 c0eafbd55de3 parent 42799 4e33894aec6d child 58889 5b7a9633cfa8
equal inserted replaced
48890:d72ca5742f80 48891:c0eafbd55de3
`     5 `
`     5 `
`     6 header {* Classical First-Order Logic with Proofs *}`
`     6 header {* Classical First-Order Logic with Proofs *}`
`     7 `
`     7 `
`     8 theory FOLP`
`     8 theory FOLP`
`     9 imports IFOLP`
`     9 imports IFOLP`
`    12 begin`
`    10 begin`
`    13 `
`    11 `
`    14 axiomatization cla :: "[p=>p]=>p"`
`    12 axiomatization cla :: "[p=>p]=>p"`
`    15   where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"`
`    13   where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"`
`    16 `
`    14 `
`    97   apply (rule major [THEN notE])`
`    95   apply (rule major [THEN notE])`
`    98   apply (rule r)`
`    96   apply (rule r)`
`    99   apply assumption`
`    97   apply assumption`
`   100   done`
`    98   done`
`   101 `
`    99 `
`   102 use "classical.ML"      (* Patched 'cos matching won't instantiate proof *)`
`   100 ML_file "classical.ML"      (* Patched because matching won't instantiate proof *)`
`   103 use "simp.ML"           (* Patched 'cos matching won't instantiate proof *)`
`   101 ML_file "simp.ML"           (* Patched because matching won't instantiate proof *)`
`   104 `
`   102 `
`   105 ML {*`
`   103 ML {*`
`   106 structure Cla = Classical`
`   104 structure Cla = Classical`
`   107 (`
`   105 (`
`   108   val sizef = size_of_thm`
`   106   val sizef = size_of_thm`
`   137   "?p3 : ~ ~ P <-> P"`
`   135   "?p3 : ~ ~ P <-> P"`
`   138   "?p4 : (~P --> P) <-> P"`
`   136   "?p4 : (~P --> P) <-> P"`
`   139   apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})`
`   137   apply (tactic {* ALLGOALS (Cla.fast_tac FOLP_cs) *})`
`   140   done`
`   138   done`
`   141 `
`   139 `
`   142 use "simpdata.ML"`
`   140 ML_file "simpdata.ML"`
`   143 `
`   141 `
`   144 end`
`   142 end`