898 done |
898 done |
899 |
899 |
900 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
900 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P" |
901 by (simp add: QUOT_TRUE_def) |
901 by (simp add: QUOT_TRUE_def) |
902 |
902 |
903 lemma QUOT_TRUE_imp: "QUOT_TRUE a" |
903 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b" |
904 by (simp add: QUOT_TRUE_def) |
904 by (simp add: QUOT_TRUE_def) |
905 |
905 |
906 ML {* |
906 ML {* |
907 fun quot_true_tac ctxt fnctn = |
907 fun quot_true_conv1 ctxt fnctn ctrm = |
908 CSUBGOAL (fn (cgl, i) => |
908 case (term_of ctrm) of |
909 let |
909 (Const (@{const_name QUOT_TRUE}, _) $ x) => |
910 val gl = term_of cgl; |
910 let |
911 val thy = ProofContext.theory_of ctxt; |
911 val fx = fnctn x; |
912 fun find_fun trm = |
912 val thy = ProofContext.theory_of ctxt; |
913 case trm of |
913 val cx = cterm_of thy x; |
914 (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true |
914 val cfx = cterm_of thy fx; |
915 | _ => false |
915 val cxt = ctyp_of thy (fastype_of x); |
916 in |
916 val cfxt = ctyp_of thy (fastype_of fx); |
917 case find_first find_fun (Logic.strip_assums_hyp gl) of |
917 val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp} |
918 SOME (_ $ (_ $ x)) => |
918 in |
919 let |
919 Conv.rewr_conv thm ctrm |
920 val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp} |
920 end |
921 val ps = Logic.strip_params (Thm.concl_of thm'); |
921 *} |
922 val fx = fnctn x; |
922 |
923 val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm'); |
923 ML {* |
924 val insts = [(fx', fx)] |
924 fun quot_true_conv ctxt fnctn ctrm = |
925 |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u)))); |
925 case (term_of ctrm) of |
926 val thm_i = Drule.cterm_instantiate insts thm' |
926 (Const (@{const_name QUOT_TRUE}, _) $ _) => |
927 val thm_j = Thm.forall_elim_vars 1 thm_i |
927 quot_true_conv1 ctxt fnctn ctrm |
928 in |
928 | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm |
929 dtac thm_j i |
929 | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm |
930 end |
930 | _ => Conv.all_conv ctrm |
931 | NONE => error "quot_true_tac!" |
931 *} |
932 | _ => error "quot_true_tac!!" |
932 |
933 end) |
933 ML {* |
934 *} |
934 fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) => |
935 |
935 CONVERSION |
|
936 (Conv.params_conv ~1 (fn ctxt => |
|
937 (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i) |
|
938 *} |
936 |
939 |
937 ML {* fun dest_comb (f $ a) = (f, a) *} |
940 ML {* fun dest_comb (f $ a) = (f, a) *} |
938 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
941 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *} |
939 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
942 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *} |
940 |
943 |