provide cla_dist_concl;
authorwenzelm
Fri Dec 30 16:56:56 2005 +0100 (2005-12-30)
changeset 185229bdfb6eaf8ab
parent 18521 ee14a65fe764
child 18523 9446cb8e1f65
provide cla_dist_concl;
src/FOL/FOL.thy
src/FOL/cladata.ML
src/HOL/HOL.thy
src/HOL/cladata.ML
     1.1 --- a/src/FOL/FOL.thy	Fri Dec 30 16:56:54 2005 +0100
     1.2 +++ b/src/FOL/FOL.thy	Fri Dec 30 16:56:56 2005 +0100
     1.3 @@ -24,6 +24,15 @@
     1.4  use "FOL_lemmas1.ML"
     1.5  theorems case_split = case_split_thm [case_names True False, cases type: o]
     1.6  
     1.7 +lemma cla_dist_concl:
     1.8 +  assumes x: "~Z_Z ==> PROP X_X"
     1.9 +    and z: "PROP Y_Y ==> Z_Z"
    1.10 +    and y: "PROP X_X ==> PROP Y_Y"
    1.11 +  shows Z_Z
    1.12 +  apply (rule classical)
    1.13 +  apply (erule x [THEN y, THEN z])
    1.14 +  done
    1.15 +
    1.16  use "cladata.ML"
    1.17  setup Cla.setup
    1.18  setup cla_setup
     2.1 --- a/src/FOL/cladata.ML	Fri Dec 30 16:56:54 2005 +0100
     2.2 +++ b/src/FOL/cladata.ML	Fri Dec 30 16:56:56 2005 +0100
     2.3 @@ -9,7 +9,7 @@
     2.4  section "Classical Reasoner";
     2.5  
     2.6  (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     2.7 -structure Make_Elim = Make_Elim_Fun(val classical = classical);
     2.8 +structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
     2.9  
    2.10  (*we don't redeclare the original make_elim (Tactic.make_elim) for 
    2.11    compatibility with strange things done in many existing proofs *)
     3.1 --- a/src/HOL/HOL.thy	Fri Dec 30 16:56:54 2005 +0100
     3.2 +++ b/src/HOL/HOL.thy	Fri Dec 30 16:56:56 2005 +0100
     3.3 @@ -909,6 +909,15 @@
     3.4  
     3.5  subsubsection {* Classical Reasoner setup *}
     3.6  
     3.7 +lemma cla_dist_concl:
     3.8 +  assumes x: "~Z_Z ==> PROP X_X"
     3.9 +    and z: "PROP Y_Y ==> Z_Z"
    3.10 +    and y: "PROP X_X ==> PROP Y_Y"
    3.11 +  shows Z_Z
    3.12 +  apply (rule classical)
    3.13 +  apply (erule x [THEN y, THEN z])
    3.14 +  done
    3.15 +
    3.16  use "cladata.ML"
    3.17  setup hypsubst_setup
    3.18  
     4.1 --- a/src/HOL/cladata.ML	Fri Dec 30 16:56:54 2005 +0100
     4.2 +++ b/src/HOL/cladata.ML	Fri Dec 30 16:56:56 2005 +0100
     4.3 @@ -38,7 +38,7 @@
     4.4  
     4.5  
     4.6  (*** Applying Make_Elim_Fun to create a classical "make_elim" rule ***)
     4.7 -structure Make_Elim = Make_Elim_Fun (val classical = classical);
     4.8 +structure Make_Elim = Make_Elim_Fun (val cla_dist_concl = thm "cla_dist_concl");
     4.9  
    4.10  (*we don't redeclare the original make_elim (Tactic.make_elim) for 
    4.11    compatibliity with strange things done in many existing proofs *)